diff --git a/solver.py b/solver.py index 658c9c32981c5f1d61e7c4ecde30f6f477116b2e..2cbbbdfd51648f5dbf5cb906f52bdc51cb674355 100644 --- a/solver.py +++ b/solver.py @@ -8,6 +8,7 @@ import math import re import glob import time +import random if __name__ == '__main__': import cv2 as cv # opencv @@ -359,7 +360,7 @@ def debug_satA(filename, Q, nodes, TF=None): return A -def generate_sat(Q, WH=None): +def generate_sat(Q, WH=None, seed=0): nodes = {} cnfs = [] @@ -395,6 +396,15 @@ def generate_sat(Q, WH=None): for i in range(h): for j in range(w): nodes[f'l{l}_{j}_{i}'] = len(nodes) + 1 + + # minisatが決定的に動く?ので変数の番号をランダムに割り当て + keys = list(nodes.keys()) + values = list(nodes.values()) + random.seed(seed) + np.random.seed(seed) + random.shuffle(values) + nodes = dict(zip(keys, values)) + # b one-hot for b in range(1,num_b+1): cnf = {} @@ -649,7 +659,7 @@ def generate_sat(Q, WH=None): def main(): - #Q = readQ('./adc2019problem/Q001_10X10_b8_l11.txt') + Q = readQ('./adc2019problem/Q001_10X10_b8_l11.txt') #Q = readQ('./adc2019problem/Q002_10X10_b8_l9.txt') #Q = readQ('./adc2019problem/Q003_10X10_b5_l5.txt') #Q = readQ('./adc2019problem/Q004_10X10_b8_l9.txt') @@ -663,10 +673,10 @@ def main(): #Q = readQ('./adc2019problem/Q014_10X10_b9_l9.txt') #Q = readQ('./adc2019problem/Q015_10X10_b8_l9.txt') #Q = readQ('./adc2019problem/QRAND327_20X20_b20_l15.txt') - Q = readQ('./adc2019problem/QRAND368_10X10_b10_l15.txt') + #Q = readQ('./adc2019problem/QRAND368_10X10_b10_l15.txt') #start_time = time.time() - nodes,cnfs = generate_sat(Q, WH=None) + nodes,cnfs = generate_sat(Q, WH=None, seed=0) print_cnf(nodes, cnfs) os.system('minisat p.txt a.txt') A = read_satA('a.txt', Q, nodes) diff --git a/twd_solver.py b/twd_solver.py index e7e33ea74873d192750b3b97a1121b8f688fcf42..810b7fd05a91768f85c81328220bd2621b2bc24d 100644 --- a/twd_solver.py +++ b/twd_solver.py @@ -1,6 +1,7 @@ import argparse import os import subprocess +import time if __name__ == '__main__': import solver @@ -31,6 +32,7 @@ def solve(params): problem = params['problem'] timeout = params['timeout'] + seed = params.get('seed', int(time.time)) basedir = os.path.abspath(os.path.dirname(__file__))