diff --git a/solver.py b/solver.py index 288bc4e9a78de9c03179b44fe68cb2cf8d65718f..34b48627a958e80ec8542343be1bd7be8d905d6e 100644 --- a/solver.py +++ b/solver.py @@ -301,7 +301,7 @@ def read_satA(filename, Q, nodes, TF=None): check_flag[c] = 1 # validation_mapが0 => 端点と接続していない => 閉路 A['map'] = A['map'] * validation_map - + ## 最小矩形に更新 map_l = A['map'] h, w = map_l.shape @@ -316,8 +316,8 @@ def read_satA(filename, Q, nodes, TF=None): if i >= h: break if (map_l[i,:] == 0).all() and (map_b[i,:] == 0).all(): - np.delete(map_l, i, axis=0) - np.delete(map_b, i, axis=0) + 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 @@ -329,8 +329,8 @@ def read_satA(filename, Q, nodes, TF=None): if j >= w: break if (map_l[:,j] == 0).all() and (map_b[:,j] == 0).all(): - np.delete(map_l, j, axis=1) - np.delete(map_b, j, axis=1) + 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 @@ -389,7 +389,7 @@ def read_satA2(filename, Q, nodes, TF=None): index = nodes[key] if TF[index]: A['map'][i][j] = l - return A + ## 閉路の削除 validation_map = np.zeros((h, w), dtype=int) check_flag = np.zeros(num_l+1) @@ -445,8 +445,8 @@ def read_satA2(filename, Q, nodes, TF=None): if i >= h: break if (map_l[i,:] == 0).all() and (map_b[i,:] == 0).all(): - np.delete(map_l, i, axis=0) - np.delete(map_b, i, axis=0) + 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 @@ -458,8 +458,8 @@ def read_satA2(filename, Q, nodes, TF=None): if j >= w: break if (map_l[:,j] == 0).all() and (map_b[:,j] == 0).all(): - np.delete(map_l, j, axis=1) - np.delete(map_b, j, axis=1) + 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 @@ -479,21 +479,21 @@ def debug_satA(filename, Q, nodes, TF=None): num_b = len(Q['BLOCK']) num_l = Q['num_l'] for b in range(1,num_b+1): - b_board = np.zeros((w,h),dtype=bool) + 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[j,i] = TF[index] + 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((w,h),dtype=bool) + 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[j,i] = TF[index] + l_board[i, j] = TF[index] print(f'l{l}=') print(l_board) return A @@ -663,9 +663,6 @@ def generate_sat(Q, WH=None, seed=0): cnf[f'l{l}_{j+dx2}_{i+dy2}'] = '-1' cnf[f'l{l}_{j+dx3}_{i+dy3}'] = '-1' - - - # blockがはみ出る位置には置けない for i in range(h): for j in range(w): @@ -705,27 +702,27 @@ def generate_sat(Q, WH=None, seed=0): cnf[f'l{l}_{j+dx}_{i+dy}'] = '-1' # block同士の衝突禁止 - for i in range(h): - for j in range(w): - for b in range(1, num_b+1): - cells = Q['BLOCK'][b]['cells'] - for i2 in range(i-4,i+5): - if i2 < 0 or i2 >= h: - continue - for j2 in range(j-4,j+5): - if j2 < 0 or j2 >= w: + 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 in range(h-hb+1): + for j in range(w-wb+1): + for i2 in range(i-hb2+1,i+hb): + if i2 < 0 or i2 >= h: continue - for b2 in range(b+1, num_b+1): - cells2 = Q['BLOCK'][b2]['cells'] + 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 - if j+dx < 0 or j+dx >= w or i+dy < 0 or i+dy >= h: - continue for dx2,dy2 in cells2.keys(): - if j2+dx2 < 0 or j2+dx2 >= w or i2+dy2 < 0 or i2+dy2 >= h: - continue if i+dy == i2+dy2 and j+dx == j2+dx2: if not flag: flag = True @@ -733,6 +730,7 @@ def generate_sat(Q, WH=None, seed=0): cnfs.append(cnf) cnf[f'b{b}_{j}_{i}'] = '-1' cnf[f'b{b2}_{j2}_{i2}'] = '-1' + break # block上にないlineは周囲2マスに接続 for i in range(h): @@ -843,6 +841,18 @@ def generate_sat(Q, WH=None, seed=0): 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 = [] @@ -869,24 +879,20 @@ def generate_sat2(Q, WH=None, seed=0): else: bdxdylist.append((b,-dx,-dy)) - for b in range(1,num_b+1): - for i in range(h): - for j in range(w): - nodes[f'b{b}_{j}_{i}'] = len(nodes) + 1 - for l in range(1, num_l+1): - for i in range(h): - for j in range(w): - nodes[f'l{l}_{j}_{i}'] = len(nodes) + 1 - for i in range(h-1): - for j in range(w): - nodes[f'lv_{j}_{i}'] = len(nodes) + 1 - for i in range(h): - for j in range(w-1): - nodes[f'lh_{j}_{i}'] = len(nodes) + 1 + # 変数の作成 + 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が決定的に動く?ので変数の番号をランダムに割り当て - keys = list(nodes.keys()) - values = list(nodes.values()) + values = list(range(1, len(keys)+1)) random.seed(seed) np.random.seed(seed) random.shuffle(values) @@ -896,283 +902,489 @@ def generate_sat2(Q, WH=None, seed=0): for b in range(1,num_b+1): cnf = [] cnfs.append(cnf) - for i in range(h): - for j in range(w): - cnf.append(nodes[f'b{b}_{j}_{i}']) - for i in range(h): - for j in range(w): - for i2 in range(i, h): - for j2 in range(w): - if i < i2 or j < j2: - 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 in range(h): - for j in range(w): - for l in range(1, num_l): - for l2 in range(l+1, num_l+1): + 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'l{l}_{j}_{i}']) - cnf.append(-nodes[f'l{l2}_{j}_{i}']) + 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 i in range(h): - for j in range(w): - for b in range(1, num_b+1): - cells = Q['BLOCK'][b]['cells'] - flag = False - for dx,dy in cells: - if j+dx < 0 or j+dx >= w or i+dy < 0 or i+dy >= h: - break - 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': + 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{int(l_str)}_{j+dx}_{i+dy}']) + 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 i in range(h): - for j in range(w): - for b in range(1, num_b+1): - cells = Q['BLOCK'][b]['cells'] - for dx,dy in cells: - if j+dx < 0 or j+dx >= w or i+dy < 0 or i+dy >= h: - cnf = [] - cnfs.append(cnf) - cnf.append(-nodes[f'b{b}_{j}_{i}']) - break + # 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 i in range(h): - for j in range(w): - for b in range(1, num_b): - cells = Q['BLOCK'][b]['cells'] - for i2 in range(i-3,i+4): + 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-3,j+4): + for j2 in range(j-wb2+1,j+wb): if j2 < 0 or j2 >= w: continue - for b2 in range(b+1, num_b+1): - cells2 = Q['BLOCK'][b2]['cells'] - flag = False - for dx,dy in cells.keys(): - if flag: - break - if j+dx < 0 or j+dx >= w or i+dy < 0 or i+dy >= h: - flag = False - break - for dx2,dy2 in cells2.keys(): - if j2+dx2 < 0 or j2+dx2 >= w or i2+dy2 < 0 or i2+dy2 >= h: - break - if i+dy == i2+dy2 and j+dx == j2+dx2: - if not flag: - flag = True - break + flag = False + for dx,dy in cells.keys(): if flag: - cnf = [] - cnfs.append(cnf) - cnf.append(-nodes[f'b{b}_{j}_{i}']) - cnf.append(-nodes[f'b{b2}_{j2}_{i2}']) - - - + 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 in range(h-1): - for j in 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 in range(h): - for j in 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}']) + 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 in range(h): - for j in range(w): - for l in range(1, num_l+1): - cnf = [] - cnfs.append(cnf) - cnf.append(-nodes[f'l{l}_{j}_{i}']) - if j+1 <= w-1: - cnf.append(nodes[f'lh_{j}_{i}']) - if j-1 >= 0: - cnf.append(nodes[f'lh_{j-1}_{i}']) - if i+1 <= h-1: - cnf.append(nodes[f'lv_{j}_{i}']) - if i-1 >= 0: - cnf.append(nodes[f'lv_{j}_{i-1}']) + 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 in range(h): - for j in range(w): - 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}']) - if len(around) == 2: - continue - if len(around) == 3: + 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(-around[0]) - cnf.append(-around[1]) - cnf.append(-around[2]) - if 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]) + cnf.append(-ar[0]) + cnf.append(-ar[1]) + cnf.append(-ar[2]) # 非端点は周囲2マス以上に接続 - for i in range(h): - for j in range(w): - 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}']) + 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: - for ar in around: - 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(ar) + around_itr = itertools.combinations(around, 1) elif len(around) == 3: - for ar in itertools.combinations(around, 2): - 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(ar[0]) - cnf.append(ar[1]) + around_itr = itertools.combinations(around, 2) elif len(around) == 4: - for ar in itertools.combinations(around, 3): - 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(ar[0]) - cnf.append(ar[1]) - cnf.append(ar[2]) + 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 in range(h): - for j in range(w): - 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}']) + 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(-around[0]) - cnf.append(-around[1]) - elif len(around) == 3: - for ar in itertools.combinations(around, 2): - 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]) - elif len(around) == 4: - for ar in itertools.combinations(around, 2): - 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]) - return nodes,cnfs - ## 不要な制約 + cnf.append(-ar[0]) + cnf.append(-ar[1]) + # 配線していないセルには線を接続しない - for i in range(h): - for j in range(w): - 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}']) - for index in around: + 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) - for l in range(1, num_l+1): - cnf.append(nodes[f'l{l}_{j}_{i}']) - cnf.append(-index) - + 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') + 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/Q003_10X10_b5_l5.txt') #Q = readQ('./adc2019problem/Q004_10X10_b8_l9.txt') #Q = readQ('./adc2019problem/Q005_10X10_b7_l6.txt') #Q = readQ('./adc2019problem/Q006_10X10_b8_l9.txt') @@ -1187,19 +1399,41 @@ def main(): #Q = readQ('./adc2019problem/QRAND368_10X10_b10_l15.txt') #Q = readQ('./adc2019problem/random_problem/QRAND136_30X30_b30_l30.txt') - #start_time = time.time() - nodes,cnfs = generate_sat2(Q, WH=(8,5), seed=0) - print_cnf2(len(nodes), cnfs) - os.system('minisat p.txt a.txt') - A = read_satA2('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) + mode = 3 + + 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()