diff --git a/solver.py b/solver.py index a36f0524af2ad5ec4143c6270d60a9c900393606..34b48627a958e80ec8542343be1bd7be8d905d6e 100644 --- a/solver.py +++ b/solver.py @@ -9,6 +9,7 @@ import re import glob import time import random +import itertools if __name__ == '__main__': import cv2 as cv # opencv @@ -204,6 +205,15 @@ def print_cnf(nodes, cnfs, filename='p.txt'): #s.append(s_sub) #print(''.join(s)) +def print_cnf2(num, cnfs, filename='p.txt'): + s = [] + s.append(f'p cnf {num} {len(cnfs)}\n') + for cnf in cnfs: + cnf = [str(i) for i in cnf] + s.append((' '.join(cnf))+' 0\n') + with open(filename, 'w') as file: + file.write(''.join(s)) + def read_satA(filename, Q, nodes, TF=None): with open(filename, 'r') as file: str_line = file.readline() @@ -331,6 +341,135 @@ def read_satA(filename, Q, nodes, TF=None): A['h'] = h A['w'] = w return A + +def read_satA2(filename, Q, nodes, TF=None): + with open(filename, 'r') as file: + str_line = file.readline() + if str_line.startswith('UNSAT'): + print('UNSAT') + return None + else: + print('SAT') + str_line = file.readline() + ss = str_line.split() + if TF is None: + TF = [False] * (len(nodes)+1) + for num_s in ss: + num = int(num_s) + if num>0: + TF[num] = True + else: + TF[-num] = False + w = Q['w'] + h = Q['h'] + A = {'BLOCK':{}} + A['w'] = w + A['h'] = h + A['map'] = np.zeros((h,w), dtype=int) + num_b = len(Q['BLOCK']) + num_l = Q['num_l'] + A['num_b'] = num_b + A['num_l'] = num_l + for i in range(1, num_b+1): + A['BLOCK'][i] = {'index':i,'x':0,'y':0} + for i in range(h): + for j in range(w): + for b in range(1,num_b+1): + key = f'b{b}_{j}_{i}' + if key not in nodes.keys(): + break + index = nodes[key] + if TF[index]: + A['BLOCK'][b]['x'] = j + A['BLOCK'][b]['y'] = i + for l in range(1,num_l+1): + key = f'l{l}_{j}_{i}' + if key not in nodes.keys(): + break + index = nodes[key] + if TF[index]: + A['map'][i][j] = l + + ## 閉路の削除 + validation_map = np.zeros((h, w), dtype=int) + check_flag = np.zeros(num_l+1) + map = A['map'] + + # 端点から探索し + for b in range(1, num_b): + for dx,dy in Q['BLOCK'][b]['cells'].keys(): + c = Q['BLOCK'][b]['cells'][(dx,dy)] + + # 配線でないならcontinue + if c == '+' or c == '0': + continue + c = int(c) + + # 探索済みならcontinue + if check_flag[c] == 1: + continue + + x, y = A['BLOCK'][b]['x']+dx, A['BLOCK'][b]['y']+dy + while True: + validation_map[y, x] = 1 + x -= 1 + if x >= 0 and map[y, x] == c and validation_map[y, x] == 0: + continue + x += 2 + if x <= w-1 and map[y, x] == c and validation_map[y, x] == 0: + continue + x -= 1 + y -= 1 + if y >= 0 and map[y, x] == c and validation_map[y, x] == 0: + continue + y += 2 + if y <= h-1 and map[y, x] == c and validation_map[y, x] == 0: + continue + y -= 1 + break + check_flag[c] = 1 + # validation_mapが0 => 端点と接続していない => 閉路 + A['map'] = A['map'] * validation_map + + ## 最小矩形に更新 + map_l = A['map'] + h, w = map_l.shape + map_b = np.zeros((h, w), dtype=int) + for b in range(1, num_b+1): + x = A['BLOCK'][b]['x'] + y = A['BLOCK'][b]['y'] + for dx,dy in Q['BLOCK'][b]['cells'].keys(): + map_b[y+dy,x+dx] = b + i = 0 + while True: + if i >= h: + break + if (map_l[i,:] == 0).all() and (map_b[i,:] == 0).all(): + map_l = np.delete(map_l, i, axis=0) + map_b = np.delete(map_b, i, axis=0) + for b in range(1, num_b+1): + if A['BLOCK'][b]['y'] > i: + A['BLOCK'][b]['y'] -= 1 + h -= 1 + i -= 1 + i += 1 + j = 0 + while True: + if j >= w: + break + if (map_l[:,j] == 0).all() and (map_b[:,j] == 0).all(): + map_l = np.delete(map_l, j, axis=1) + map_b = np.delete(map_b, j, axis=1) + for b in range(1, num_b+1): + if A['BLOCK'][b]['x'] > j: + A['BLOCK'][b]['x'] -= 1 + w -= 1 + j -= 1 + j += 1 + A['map'] = map_l + A['h'] = h + A['w'] = w + return A def debug_satA(filename, Q, nodes, TF=None): TF = [False] * (len(nodes)+1) @@ -358,6 +497,53 @@ def debug_satA(filename, Q, nodes, TF=None): print(f'l{l}=') print(l_board) return A + +def debug_satA2(filename, Q, nodes, TF=None): + TF = [False] * (len(nodes)+1) + A = read_satA(filename, Q, nodes, TF) + w = Q['w'] + h = Q['h'] + num_b = len(Q['BLOCK']) + num_l = Q['num_l'] + v_board = np.zeros((h-1, w),dtype=bool) + for i in range(h-1): + for j in range(w): + key = f'lv_{j}_{i}' + index = nodes[key] + v_board[i, j] = TF[index] + print(f'lv=') + print(v_board) + h_board = np.zeros((h, w-1),dtype=bool) + for i in range(h): + for j in range(w-1): + key = f'lh_{j}_{i}' + index = nodes[key] + h_board[i, j] = TF[index] + print(f'lh=') + print(h_board) + + +# for b in range(1,num_b+1): +# b_board = np.zeros((h,w),dtype=bool) +# for i in range(h): +# for j in range(w): +# key = f'b{b}_{j}_{i}' +# index = nodes[key] +# b_board[i, j] = TF[index] +# print(f'b{b}=') +# print(b_board) + for l in range(1,num_l+1): + l_board = np.zeros((h, w),dtype=bool) + for i in range(h): + for j in range(w): + key = f'l{l}_{j}_{i}' + index = nodes[key] + l_board[i, j] = TF[index] + print(f'l{l}=') + print(l_board) + + + return A def generate_sat(Q, WH=None, seed=0): nodes = {} @@ -654,6 +840,546 @@ def generate_sat(Q, WH=None, seed=0): cnf[f'l{l}_{j+dx2}_{i+dy2}'] = '-1' return nodes,cnfs + +def _get_around(j, i, w, h, nodes): + around = [] + if j+1 <= w-1: + around.append(nodes[f'lh_{j}_{i}']) + if j-1 >= 0: + around.append(nodes[f'lh_{j-1}_{i}']) + if i+1 <= h-1: + around.append(nodes[f'lv_{j}_{i}']) + if i-1 >= 0: + around.append(nodes[f'lv_{j}_{i-1}']) + return around + +def generate_sat2(Q, WH=None, seed=0): + nodes = {} + cnfs = [] + + num_b = len(Q['BLOCK']) + num_l = Q['num_l'] + w = Q['w'] + h = Q['h'] + + if not WH is None: + w = WH[0] + h = WH[1] + Q['w'] = WH[0] + Q['h'] = WH[1] + + # 端点制約に使用 + bdxdylist = [] + for b in range(1, num_b+1): + cells = Q['BLOCK'][b]['cells'] + for dx,dy in cells.keys(): + v = cells[(dx,dy)] + if v == '+' or v == '0': + continue + else: + bdxdylist.append((b,-dx,-dy)) + + # 変数の作成 + keys = [] + for i, j in itertools.product(range(h),range(w)): + for b in range(1,num_b+1): + keys.append(f'b{b}_{j}_{i}') + for l in range(1,num_l+1): + keys.append(f'l{l}_{j}_{i}') + if i != h-1: + keys.append(f'lv_{j}_{i}') + if j != w-1: + keys.append(f'lh_{j}_{i}') + + # minisatが決定的に動く?ので変数の番号をランダムに割り当て + values = list(range(1, len(keys)+1)) + 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 = [] + cnfs.append(cnf) + for i, j in itertools.product(range(h),range(w)): + cnf.append(nodes[f'b{b}_{j}_{i}']) + for i, j in itertools.product(range(h),range(w)): + for i2 in range(i, h): + for j2 in range(w): + if i == i2 and j >= j2: + continue + cnf = [] + cnfs.append(cnf) + cnf.append(-nodes[f'b{b}_{j}_{i}']) + cnf.append(-nodes[f'b{b}_{j2}_{i2}']) + + # line 0 or 1 + for i, j in itertools.product(range(h),range(w)): + for l in range(1, num_l): + for l2 in range(l+1, num_l+1): + cnf = [] + cnfs.append(cnf) + cnf.append(-nodes[f'l{l}_{j}_{i}']) + cnf.append(-nodes[f'l{l2}_{j}_{i}']) + + # block位置に対してライン位置が決定 + for b in range(1, num_b+1): + cells = Q['BLOCK'][b]['cells'] + wb = Q['BLOCK'][b]['w'] + hb = Q['BLOCK'][b]['h'] + for i, j in itertools.product(range(h-hb+1),range(w-wb+1)): + for dx,dy in cells: + l_str = cells[(dx,dy)] + if l_str == '+': + for l in range(1,num_l+1): + cnf = [] + cnfs.append(cnf) + cnf.append(-nodes[f'b{b}_{j}_{i}']) + cnf.append(-nodes[f'l{l}_{j+dx}_{i+dy}']) + elif l_str != '0': + cnf = [] + cnfs.append(cnf) + cnf.append(-nodes[f'b{b}_{j}_{i}']) + cnf.append(nodes[f'l{int(l_str)}_{j+dx}_{i+dy}']) + + # blockがはみ出る位置には置けない + for b in range(1, num_b+1): + cells = Q['BLOCK'][b]['cells'] + wb = Q['BLOCK'][b]['w'] + hb = Q['BLOCK'][b]['h'] + for i, j in itertools.product(range(h),range(w)): + if i <= h - hb and j <= w - wb: + continue + cnf = [] + cnfs.append(cnf) + cnf.append(-nodes[f'b{b}_{j}_{i}']) + + # block同士の衝突禁止 + for b in range(1, num_b+1): + cells = Q['BLOCK'][b]['cells'] + wb = Q['BLOCK'][b]['w'] + hb = Q['BLOCK'][b]['h'] + for b2 in range(b+1, num_b+1): + cells2 = Q['BLOCK'][b2]['cells'] + wb2 = Q['BLOCK'][b2]['w'] + hb2 = Q['BLOCK'][b2]['h'] + for i, j in itertools.product(range(h-hb+1),range(w-wb+1)): + for i2 in range(i-hb2+1,i+hb): + if i2 < 0 or i2 >= h: + continue + for j2 in range(j-wb2+1,j+wb): + if j2 < 0 or j2 >= w: + continue + flag = False + for dx,dy in cells.keys(): + if flag: + break + for dx2,dy2 in cells2.keys(): + if i+dy == i2+dy2 and j+dx == j2+dx2: + if not flag: + flag = True + cnf = [] + cnfs.append(cnf) + cnf.append(-nodes[f'b{b}_{j}_{i}']) + cnf.append(-nodes[f'b{b2}_{j2}_{i2}']) + break + + # 接続セルの配線は等しい + for i, j in itertools.product(range(h-1),range(w)): + for l in range(1, num_l+1): + cnf = [] + cnfs.append(cnf) + cnf.append(-nodes[f'lv_{j}_{i}']) + cnf.append(-nodes[f'l{l}_{j}_{i}']) + cnf.append(nodes[f'l{l}_{j}_{i+1}']) + cnf = [] + cnfs.append(cnf) + cnf.append(-nodes[f'lv_{j}_{i}']) + cnf.append(nodes[f'l{l}_{j}_{i}']) + cnf.append(-nodes[f'l{l}_{j}_{i+1}']) + for i, j in itertools.product(range(h),range(w-1)): + for l in range(1, num_l+1): + cnf = [] + cnfs.append(cnf) + cnf.append(-nodes[f'lh_{j}_{i}']) + cnf.append(-nodes[f'l{l}_{j}_{i}']) + cnf.append(nodes[f'l{l}_{j+1}_{i}']) + cnf = [] + cnfs.append(cnf) + cnf.append(-nodes[f'lh_{j}_{i}']) + cnf.append(nodes[f'l{l}_{j}_{i}']) + cnf.append(-nodes[f'l{l}_{j+1}_{i}']) + + # 接続していない配線は異なる + for i, j in itertools.product(range(h-1),range(w)): + for l in range(1, num_l+1): + cnf = [] + cnfs.append(cnf) + cnf.append(nodes[f'lv_{j}_{i}']) + cnf.append(-nodes[f'l{l}_{j}_{i}']) + cnf.append(-nodes[f'l{l}_{j}_{i+1}']) + for i, j in itertools.product(range(h),range(w-1)): + for l in range(1, num_l+1): + cnf = [] + cnfs.append(cnf) + cnf.append(nodes[f'lh_{j}_{i}']) + cnf.append(-nodes[f'l{l}_{j}_{i}']) + cnf.append(-nodes[f'l{l}_{j+1}_{i}']) + + # line孤立禁止 + for i, j in itertools.product(range(h),range(w)): + for l in range(1, num_l+1): + cnf = [] + cnfs.append(cnf) + cnf.append(-nodes[f'l{l}_{j}_{i}']) + around = _get_around(j, i, w, h, nodes) + cnf.extend(around) + + # line三叉禁止 + for i, j in itertools.product(range(h),range(w)): + around = _get_around(j, i, w, h, nodes) + if len(around) == 2: + continue + elif len(around) == 3: + cnf = [] + cnfs.append(cnf) + cnf.append(-around[0]) + cnf.append(-around[1]) + cnf.append(-around[2]) + elif len(around) == 4: + for ar in itertools.combinations(around, 3): + cnf = [] + cnfs.append(cnf) + cnf.append(-ar[0]) + cnf.append(-ar[1]) + cnf.append(-ar[2]) + + # 非端点は周囲2マス以上に接続 + for i, j in itertools.product(range(h),range(w)): + for l in range(1, num_l+1): + around = _get_around(j, i, w, h, nodes) + if len(around) == 2: + around_itr = itertools.combinations(around, 1) + elif len(around) == 3: + around_itr = itertools.combinations(around, 2) + elif len(around) == 4: + around_itr = itertools.combinations(around, 3) + else: + # assert error + around_itr = [] + for ar in around_itr: + cnf = [] + cnfs.append(cnf) + for b,mdx,mdy in bdxdylist: + if i+mdy < 0 or i+mdy >= h or j+mdx < 0 or j+mdx >= w: + continue + cnf.append(nodes[f'b{b}_{j+mdx}_{i+mdy}']) + cnf.append(-nodes[f'l{l}_{j}_{i}']) + cnf.extend(list(ar)) + + # 端点は周囲2マス以上に接続禁止 + for i, j in itertools.product(range(h),range(w)): + around = _get_around(j, i, w, h, nodes) + if len(around) == 2: + around_itr = [around] + elif len(around) == 3: + around_itr = itertools.combinations(around, 2) + elif len(around) == 4: + around_itr = itertools.combinations(around, 2) + else: + # assert error + around_itr = [] + for ar in around_itr: + for b,mdx,mdy in bdxdylist: + if i+mdy < 0 or i+mdy >= h or j+mdx < 0 or j+mdx >= w: + continue + cnf = [] + cnfs.append(cnf) + cnf.append(-nodes[f'b{b}_{j+mdx}_{i+mdy}']) + cnf.append(-ar[0]) + cnf.append(-ar[1]) + + # 配線していないセルには線を接続しない + for i, j in itertools.product(range(h),range(w)): + around = _get_around(j, i, w, h, nodes) + for index in around: + cnf = [] + cnfs.append(cnf) + for l in range(1, num_l+1): + cnf.append(nodes[f'l{l}_{j}_{i}']) + cnf.append(-index) + + # コの字禁止 + for i, j in itertools.product(range(h-1),range(w-1)): + cnf = [] + cnfs.append(cnf) + cnf.append(-nodes[f'lv_{j}_{i}']) + cnf.append(-nodes[f'lv_{j+1}_{i}']) + cnf.append(-nodes[f'lh_{j}_{i}']) + cnf = [] + cnfs.append(cnf) + cnf.append(-nodes[f'lv_{j}_{i}']) + cnf.append(-nodes[f'lv_{j+1}_{i}']) + cnf.append(-nodes[f'lh_{j}_{i+1}']) + cnf = [] + cnfs.append(cnf) + cnf.append(-nodes[f'lv_{j}_{i}']) + cnf.append(-nodes[f'lh_{j}_{i}']) + cnf.append(-nodes[f'lh_{j}_{i+1}']) + cnf = [] + cnfs.append(cnf) + cnf.append(-nodes[f'lv_{j+1}_{i}']) + cnf.append(-nodes[f'lh_{j}_{i}']) + cnf.append(-nodes[f'lh_{j}_{i+1}']) + + return nodes,cnfs + +############# +## 協調動作用 +def ensemble_readQ(filename): + Q = {'BLOCK':{}} + max_l = 0 + with open(filename, 'r') as file: + while True: + str_line = file.readline() + if not str_line: + break + result = split(str_line) + if result == []: + continue + if result[0] == 'SIZE': + Q['w'] = int(result[1]) + Q['h'] = int(result[2]) + elif result[0] == 'BLOCK_NUM': + Q['num_b'] = int(result[1]) + Q['n'] = Q['num_b'] + elif result[0] == 'BLOCK': + index = int(result[1]) + w = int(result[2]) + h = int(result[3]) + if index not in Q['BLOCK']: + Q['BLOCK'][index] = [] + cells = {} + b = {'index':index,'w':w,'h':h,'cells':cells} + Q['BLOCK'][index].append(b) + for i in range(h): + subline = file.readline() + subr = split(subline) + for j in range(w): + if subr[j] != '0': + cells[(j,i)] = subr[j] + if subr[j] != '+': + num = int(subr[j]) + if num > max_l: + max_l = num + Q['num_l'] = max_l + return Q + +def ensemble_generate_sat(Q, WH=None, seed=0): + nodes = {} + cnfs = [] + + num_b = len(Q['BLOCK']) + num_l = Q['num_l'] + w = Q['w'] + h = Q['h'] + + if not WH is None: + w = WH[0] + h = WH[1] + Q['w'] = WH[0] + Q['h'] = WH[1] + + # 変数の作成 + keys = [] + for b in range(1,num_b+1): + b_list = Q['BLOCK'][b] + num_bb = len(b_list) + for bb in range(num_bb): + # 0-origin + for i, j in itertools.product(range(h),range(w)): + keys.append(f'b{b}-{bb}_{j}_{i}') + + # minisatが決定的に動く?ので変数の番号をランダムに割り当て + values = list(range(1, len(keys)+1)) + random.seed(seed) + np.random.seed(seed) + random.shuffle(values) + nodes = dict(zip(keys, values)) + + # b and bb one-hot + for b in range(1,num_b+1): + b_list = Q['BLOCK'][b] + num_bb = len(b_list) + b_all = [] + for bb in range(num_bb): + for i, j in itertools.product(range(h),range(w)): + b_all.append(nodes[f'b{b}-{bb}_{j}_{i}']) + cnf = [] + cnfs.append(cnf) + cnf.extend(b_all) + for index,index2 in itertools.combinations(b_all, 2): + cnf = [] + cnfs.append(cnf) + cnf.append(-index) + cnf.append(-index2) + + # blockがはみ出る位置には置けない + for b in range(1,num_b+1): + b_list = Q['BLOCK'][b] + num_bb = len(b_list) + for bb in range(num_bb): + cells = Q['BLOCK'][b][bb]['cells'] + wb = Q['BLOCK'][b][bb]['w'] + hb = Q['BLOCK'][b][bb]['h'] + for i, j in itertools.product(range(h),range(w)): + if i <= h - hb and j <= w - wb: + continue + cnf = [] + cnfs.append(cnf) + cnf.append(-nodes[f'b{b}-{bb}_{j}_{i}']) + + # block同士の衝突禁止 + for b,b2 in itertools.combinations(range(1,num_b+1),2): + b_list = Q['BLOCK'][b] + num_bb = len(b_list) + b_list2 = Q['BLOCK'][b2] + num_bb2 = len(b_list2) + for bb,bb2 in itertools.product(range(num_bb),range(num_bb2)): + cells = Q['BLOCK'][b][bb]['cells'] + wb = Q['BLOCK'][b][bb]['w'] + hb = Q['BLOCK'][b][bb]['h'] + cells2 = Q['BLOCK'][b2][bb2]['cells'] + wb2 = Q['BLOCK'][b2][bb2]['w'] + hb2 = Q['BLOCK'][b2][bb2]['h'] + for i, j in itertools.product(range(h-hb+1),range(w-wb+1)): + for i2,j2 in itertools.product(range(i-hb2+1,i+hb),range(j-wb2+1,j+wb)): + if i2 < 0 or i2 >= h or j2 < 0 or j2 >= w: + continue + flag = False + for dx,dy in cells.keys(): + if flag: + break + for dx2,dy2 in cells2.keys(): + if i+dy == i2+dy2 and j+dx == j2+dx2: + if not flag: + flag = True + cnf = [] + cnfs.append(cnf) + cnf.append(-nodes[f'b{b}-{bb}_{j}_{i}']) + cnf.append(-nodes[f'b{b2}-{bb2}_{j2}_{i2}']) + break + + return nodes,cnfs + +def ensemble_print_cnf(nodes, cnfs, filename='p.txt'): + print_cnf2(len(nodes), cnfs, filename=filename) + +def ensemble_read_satA(filename, Q, nodes, TF=None): + with open(filename, 'r') as file: + str_line = file.readline() + if str_line.startswith('UNSAT'): + print('UNSAT') + return None + else: + print('SAT') + str_line = file.readline() + ss = str_line.split() + if TF is None: + TF = [False] * (len(nodes)+1) + for num_s in ss: + num = int(num_s) + if num>0: + TF[num] = True + else: + TF[-num] = False + w = Q['w'] + h = Q['h'] + A = {'BLOCK':{}} + A['w'] = w + A['h'] = h + A['map'] = np.zeros((h,w), dtype=int) + num_b = len(Q['BLOCK']) + num_l = Q['num_l'] + A['num_b'] = num_b + A['num_l'] = num_l + A['n'] = num_b + for i in range(1, num_b+1): + A['BLOCK'][i] = {'index':i,'offset':0,'x':0,'y':0} + for b in range(1,num_b+1): + b_list = Q['BLOCK'][b] + num_bb = len(b_list) + for bb in range(num_bb): + for i, j in itertools.product(range(h), range(w)): + key = f'b{b}-{bb}_{j}_{i}' + if key not in nodes.keys(): + continue + index = nodes[key] + if TF[index]: + A['BLOCK'][b]['offset'] = bb + A['BLOCK'][b]['x'] = j + A['BLOCK'][b]['y'] = i + + ## 最小矩形に更新 + map_b = np.zeros((h, w), dtype=int) + for b in range(1, num_b+1): + bb = A['BLOCK'][b]['offset'] + x = A['BLOCK'][b]['x'] + y = A['BLOCK'][b]['y'] + for dx,dy in Q['BLOCK'][b][bb]['cells'].keys(): + map_b[y+dy,x+dx] = b + i = 0 + while True: + if i >= h: + break + if (map_b[i,:] == 0).all(): + map_b = np.delete(map_b, i, axis=0) + for b in range(1, num_b+1): + if A['BLOCK'][b]['y'] > i: + A['BLOCK'][b]['y'] -= 1 + h -= 1 + i -= 1 + i += 1 + j = 0 + while True: + if j >= w: + break + if (map_b[:,j] == 0).all(): + map_b = np.delete(map_b, j, axis=1) + for b in range(1, num_b+1): + if A['BLOCK'][b]['x'] > j: + A['BLOCK'][b]['x'] -= 1 + w -= 1 + j -= 1 + j += 1 + A['map'] = np.zeros((h,w), dtype=int) + A['h'] = h + A['w'] = w + return A + +def ensemble_strA(A): + r = [] + w = A['w'] + h = A['h'] + num_b = A['num_b'] + r.append(f'SIZE {w}X{h}\n') + for i in range(h): + r.append(','.join(map(str,A['map'][i]))) + r.append('\n') + block_list = A['BLOCK'] + for i in range(1, num_b+1): + bb = block_list[i]['offset'] + x = block_list[i]['x'] + y = block_list[i]['y'] + r.append(f'BLOCK#{i}-{bb} @({x},{y})\n') + return ''.join(r) + + +## 協調動作用 +############# + + def main(): Q = readQ('./adc2019problem/Q001_10X10_b8_l11.txt') @@ -671,20 +1397,43 @@ def main(): #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/random_problem/QRAND136_30X30_b30_l30.txt') + + mode = 3 - #start_time = time.time() - 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) - if A is None: - return - print(strA(A)) - #A = debug_satA('a.txt', Q, nodes) - #end_time= time.time() - #print(f"経過時間：{end_time - start_time}") - #img = QA2img(Q,A) - #plt.imshow(img) + if mode == 1: + # cell-line variables + #start_time = time.time() + nodes,cnfs = generate_sat(Q, WH=None, seed=0) + #print(nodes) + print_cnf(nodes, cnfs) + os.system('minisat p.txt a.txt') + A = read_satA('a.txt', Q, nodes) + if A is None: + return + print(strA(A)) + #debug_satA2('a.txt', Q, nodes) + #end_time= time.time() + #print(f"経過時間：{end_time - start_time}") + #img = QA2img(Q,A) + #plt.imshow(img) + elif mode == 2: + # line variables + nodes,cnfs = generate_sat2(Q, WH=None, seed=0) + print_cnf2(nodes, cnfs) + os.system('minisat p.txt a.txt') + A = read_satA2('a.txt', Q, nodes) + if A is None: + return + print(strA(A)) + elif mode == 3: + # ensemble + Q = ensemble_readQ('./qq.txt') + nodes,cnfs = ensemble_generate_sat(Q, WH=None, seed=0) + ensemble_print_cnf(nodes, cnfs) + os.system('minisat p.txt a.txt') + A = ensemble_read_satA('a.txt', Q, nodes) + print(ensemble_strA(A)) if __name__ == '__main__': main()