Skip to content

T
twd-solver
Commit a3d6f273 authored by tawada's avatar tawada
Browse files
Options

add ensemble_solver

parents a0713f54 cc3172d3
Show whitespace changes
Inline Side-by-side
Showing with 529 additions and 295 deletions
solver.py
View file @ a3d6f273
...@@ -316,8 +316,8 @@ def read_satA(filename, Q, nodes, TF=None): ...@@ -316,8 +316,8 @@ def read_satA(filename, Q, nodes, TF=None):
if i >= h: if i >= h:
break break
if (map_l[i,:] == 0).all() and (map_b[i,:] == 0).all(): if (map_l[i,:] == 0).all() and (map_b[i,:] == 0).all():
np.delete(map_l, i, axis=0) map_l = np.delete(map_l, i, axis=0)
np.delete(map_b, i, axis=0) map_b = np.delete(map_b, i, axis=0)
for b in range(1, num_b+1): for b in range(1, num_b+1):
if A['BLOCK'][b]['y'] > i: if A['BLOCK'][b]['y'] > i:
A['BLOCK'][b]['y'] -= 1 A['BLOCK'][b]['y'] -= 1
...@@ -329,8 +329,8 @@ def read_satA(filename, Q, nodes, TF=None): ...@@ -329,8 +329,8 @@ def read_satA(filename, Q, nodes, TF=None):
if j >= w: if j >= w:
break break
if (map_l[:,j] == 0).all() and (map_b[:,j] == 0).all(): if (map_l[:,j] == 0).all() and (map_b[:,j] == 0).all():
np.delete(map_l, j, axis=1) map_l = np.delete(map_l, j, axis=1)
np.delete(map_b, j, axis=1) map_b = np.delete(map_b, j, axis=1)
for b in range(1, num_b+1): for b in range(1, num_b+1):
if A['BLOCK'][b]['x'] > j: if A['BLOCK'][b]['x'] > j:
A['BLOCK'][b]['x'] -= 1 A['BLOCK'][b]['x'] -= 1
...@@ -389,7 +389,7 @@ def read_satA2(filename, Q, nodes, TF=None): ...@@ -389,7 +389,7 @@ def read_satA2(filename, Q, nodes, TF=None):
index = nodes[key] index = nodes[key]
if TF[index]: if TF[index]:
A['map'][i][j] = l A['map'][i][j] = l
return A
## 閉路の削除 ## 閉路の削除
validation_map = np.zeros((h, w), dtype=int) validation_map = np.zeros((h, w), dtype=int)
check_flag = np.zeros(num_l+1) check_flag = np.zeros(num_l+1)
...@@ -445,8 +445,8 @@ def read_satA2(filename, Q, nodes, TF=None): ...@@ -445,8 +445,8 @@ def read_satA2(filename, Q, nodes, TF=None):
if i >= h: if i >= h:
break break
if (map_l[i,:] == 0).all() and (map_b[i,:] == 0).all(): if (map_l[i,:] == 0).all() and (map_b[i,:] == 0).all():
np.delete(map_l, i, axis=0) map_l = np.delete(map_l, i, axis=0)
np.delete(map_b, i, axis=0) map_b = np.delete(map_b, i, axis=0)
for b in range(1, num_b+1): for b in range(1, num_b+1):
if A['BLOCK'][b]['y'] > i: if A['BLOCK'][b]['y'] > i:
A['BLOCK'][b]['y'] -= 1 A['BLOCK'][b]['y'] -= 1
...@@ -458,8 +458,8 @@ def read_satA2(filename, Q, nodes, TF=None): ...@@ -458,8 +458,8 @@ def read_satA2(filename, Q, nodes, TF=None):
if j >= w: if j >= w:
break break
if (map_l[:,j] == 0).all() and (map_b[:,j] == 0).all(): if (map_l[:,j] == 0).all() and (map_b[:,j] == 0).all():
np.delete(map_l, j, axis=1) map_l = np.delete(map_l, j, axis=1)
np.delete(map_b, j, axis=1) map_b = np.delete(map_b, j, axis=1)
for b in range(1, num_b+1): for b in range(1, num_b+1):
if A['BLOCK'][b]['x'] > j: if A['BLOCK'][b]['x'] > j:
A['BLOCK'][b]['x'] -= 1 A['BLOCK'][b]['x'] -= 1
...@@ -479,21 +479,21 @@ def debug_satA(filename, Q, nodes, TF=None): ...@@ -479,21 +479,21 @@ def debug_satA(filename, Q, nodes, TF=None):
num_b = len(Q['BLOCK']) num_b = len(Q['BLOCK'])
num_l = Q['num_l'] num_l = Q['num_l']
for b in range(1,num_b+1): 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 i in range(h):
for j in range(w): for j in range(w):
key = f'b{b}_{j}_{i}' key = f'b{b}_{j}_{i}'
index = nodes[key] index = nodes[key]
b_board[j,i] = TF[index] b_board[i, j] = TF[index]
print(f'b{b}=') print(f'b{b}=')
print(b_board) print(b_board)
for l in range(1,num_l+1): 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 i in range(h):
for j in range(w): for j in range(w):
key = f'l{l}_{j}_{i}' key = f'l{l}_{j}_{i}'
index = nodes[key] index = nodes[key]
l_board[j,i] = TF[index] l_board[i, j] = TF[index]
print(f'l{l}=') print(f'l{l}=')
print(l_board) print(l_board)
return A return A
...@@ -663,9 +663,6 @@ def generate_sat(Q, WH=None, seed=0): ...@@ -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+dx2}_{i+dy2}'] = '-1'
cnf[f'l{l}_{j+dx3}_{i+dy3}'] = '-1' cnf[f'l{l}_{j+dx3}_{i+dy3}'] = '-1'
# blockがはみ出る位置には置けない # blockがはみ出る位置には置けない
for i in range(h): for i in range(h):
for j in range(w): for j in range(w):
...@@ -705,27 +702,27 @@ def generate_sat(Q, WH=None, seed=0): ...@@ -705,27 +702,27 @@ def generate_sat(Q, WH=None, seed=0):
cnf[f'l{l}_{j+dx}_{i+dy}'] = '-1' cnf[f'l{l}_{j+dx}_{i+dy}'] = '-1'
# block同士の衝突禁止 # block同士の衝突禁止
for i in range(h):
for j in range(w):
for b in range(1, num_b+1): for b in range(1, num_b+1):
cells = Q['BLOCK'][b]['cells'] cells = Q['BLOCK'][b]['cells']
for i2 in range(i-4,i+5): 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: if i2 < 0 or i2 >= h:
continue continue
for j2 in range(j-4,j+5): for j2 in range(j-wb2+1,j+wb):
if j2 < 0 or j2 >= w: if j2 < 0 or j2 >= w:
continue continue
for b2 in range(b+1, num_b+1):
cells2 = Q['BLOCK'][b2]['cells']
flag = False flag = False
for dx,dy in cells.keys(): for dx,dy in cells.keys():
if flag: if flag:
break break
if j+dx < 0 or j+dx >= w or i+dy < 0 or i+dy >= h:
continue
for dx2,dy2 in cells2.keys(): 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 i+dy == i2+dy2 and j+dx == j2+dx2:
if not flag: if not flag:
flag = True flag = True
...@@ -733,6 +730,7 @@ def generate_sat(Q, WH=None, seed=0): ...@@ -733,6 +730,7 @@ def generate_sat(Q, WH=None, seed=0):
cnfs.append(cnf) cnfs.append(cnf)
cnf[f'b{b}_{j}_{i}'] = '-1' cnf[f'b{b}_{j}_{i}'] = '-1'
cnf[f'b{b2}_{j2}_{i2}'] = '-1' cnf[f'b{b2}_{j2}_{i2}'] = '-1'
break
# block上にないlineは周囲2マスに接続 # block上にないlineは周囲2マスに接続
for i in range(h): for i in range(h):
...@@ -843,6 +841,18 @@ def generate_sat(Q, WH=None, seed=0): ...@@ -843,6 +841,18 @@ def generate_sat(Q, WH=None, seed=0):
return nodes,cnfs 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): def generate_sat2(Q, WH=None, seed=0):
nodes = {} nodes = {}
cnfs = [] cnfs = []
...@@ -869,24 +879,20 @@ def generate_sat2(Q, WH=None, seed=0): ...@@ -869,24 +879,20 @@ def generate_sat2(Q, WH=None, seed=0):
else: else:
bdxdylist.append((b,-dx,-dy)) bdxdylist.append((b,-dx,-dy))
# 変数の作成
keys = []
for i, j in itertools.product(range(h),range(w)):
for b in range(1,num_b+1): for b in range(1,num_b+1):
for i in range(h): keys.append(f'b{b}_{j}_{i}')
for j in range(w): for l in range(1,num_l+1):
nodes[f'b{b}_{j}_{i}'] = len(nodes) + 1 keys.append(f'l{l}_{j}_{i}')
for l in range(1, num_l+1): if i != h-1:
for i in range(h): keys.append(f'lv_{j}_{i}')
for j in range(w): if j != w-1:
nodes[f'l{l}_{j}_{i}'] = len(nodes) + 1 keys.append(f'lh_{j}_{i}')
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
# minisatが決定的に動く?ので変数の番号をランダムに割り当て # minisatが決定的に動く?ので変数の番号をランダムに割り当て
keys = list(nodes.keys()) values = list(range(1, len(keys)+1))
values = list(nodes.values())
random.seed(seed) random.seed(seed)
np.random.seed(seed) np.random.seed(seed)
random.shuffle(values) random.shuffle(values)
...@@ -896,22 +902,20 @@ def generate_sat2(Q, WH=None, seed=0): ...@@ -896,22 +902,20 @@ def generate_sat2(Q, WH=None, seed=0):
for b in range(1,num_b+1): for b in range(1,num_b+1):
cnf = [] cnf = []
cnfs.append(cnf) cnfs.append(cnf)
for i in range(h): for i, j in itertools.product(range(h),range(w)):
for j in range(w):
cnf.append(nodes[f'b{b}_{j}_{i}']) cnf.append(nodes[f'b{b}_{j}_{i}'])
for i in range(h): for i, j in itertools.product(range(h),range(w)):
for j in range(w):
for i2 in range(i, h): for i2 in range(i, h):
for j2 in range(w): for j2 in range(w):
if i < i2 or j < j2: if i == i2 and j >= j2:
continue
cnf = [] cnf = []
cnfs.append(cnf) cnfs.append(cnf)
cnf.append(-nodes[f'b{b}_{j}_{i}']) cnf.append(-nodes[f'b{b}_{j}_{i}'])
cnf.append(-nodes[f'b{b}_{j2}_{i2}']) cnf.append(-nodes[f'b{b}_{j2}_{i2}'])
# line 0 or 1 # line 0 or 1
for i in range(h): for i, j in itertools.product(range(h),range(w)):
for j in range(w):
for l in range(1, num_l): for l in range(1, num_l):
for l2 in range(l+1, num_l+1): for l2 in range(l+1, num_l+1):
cnf = [] cnf = []
...@@ -920,14 +924,12 @@ def generate_sat2(Q, WH=None, seed=0): ...@@ -920,14 +924,12 @@ def generate_sat2(Q, WH=None, seed=0):
cnf.append(-nodes[f'l{l2}_{j}_{i}']) cnf.append(-nodes[f'l{l2}_{j}_{i}'])
# block位置に対してライン位置が決定 # block位置に対してライン位置が決定
for i in range(h):
for j in range(w):
for b in range(1, num_b+1): for b in range(1, num_b+1):
cells = Q['BLOCK'][b]['cells'] cells = Q['BLOCK'][b]['cells']
flag = False 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: 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)] l_str = cells[(dx,dy)]
if l_str == '+': if l_str == '+':
for l in range(1,num_l+1): for l in range(1,num_l+1):
...@@ -942,56 +944,49 @@ def generate_sat2(Q, WH=None, seed=0): ...@@ -942,56 +944,49 @@ def generate_sat2(Q, WH=None, seed=0):
cnf.append(nodes[f'l{int(l_str)}_{j+dx}_{i+dy}']) cnf.append(nodes[f'l{int(l_str)}_{j+dx}_{i+dy}'])
# blockがはみ出る位置には置けない # blockがはみ出る位置には置けない
for i in range(h):
for j in range(w):
for b in range(1, num_b+1): for b in range(1, num_b+1):
cells = Q['BLOCK'][b]['cells'] cells = Q['BLOCK'][b]['cells']
for dx,dy in cells: wb = Q['BLOCK'][b]['w']
if j+dx < 0 or j+dx >= w or i+dy < 0 or i+dy >= h: 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 = [] cnf = []
cnfs.append(cnf) cnfs.append(cnf)
cnf.append(-nodes[f'b{b}_{j}_{i}']) cnf.append(-nodes[f'b{b}_{j}_{i}'])
break
# block同士の衝突禁止 # block同士の衝突禁止
for i in range(h): for b in range(1, num_b+1):
for j in range(w):
for b in range(1, num_b):
cells = Q['BLOCK'][b]['cells'] cells = Q['BLOCK'][b]['cells']
for i2 in range(i-3,i+4): 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: if i2 < 0 or i2 >= h:
continue continue
for j2 in range(j-3,j+4): for j2 in range(j-wb2+1,j+wb):
if j2 < 0 or j2 >= w: if j2 < 0 or j2 >= w:
continue continue
for b2 in range(b+1, num_b+1):
cells2 = Q['BLOCK'][b2]['cells']
flag = False flag = False
for dx,dy in cells.keys(): for dx,dy in cells.keys():
if flag: if flag:
break 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(): 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 i+dy == i2+dy2 and j+dx == j2+dx2:
if not flag: if not flag:
flag = True flag = True
break
if flag:
cnf = [] cnf = []
cnfs.append(cnf) cnfs.append(cnf)
cnf.append(-nodes[f'b{b}_{j}_{i}']) cnf.append(-nodes[f'b{b}_{j}_{i}'])
cnf.append(-nodes[f'b{b2}_{j2}_{i2}']) cnf.append(-nodes[f'b{b2}_{j2}_{i2}'])
break
# 接続セルの配線は等しい # 接続セルの配線は等しい
for i in range(h-1): for i, j in itertools.product(range(h-1),range(w)):
for j in range(w):
for l in range(1, num_l+1): for l in range(1, num_l+1):
cnf = [] cnf = []
cnfs.append(cnf) cnfs.append(cnf)
...@@ -1003,8 +998,7 @@ def generate_sat2(Q, WH=None, seed=0): ...@@ -1003,8 +998,7 @@ def generate_sat2(Q, WH=None, seed=0):
cnf.append(-nodes[f'lv_{j}_{i}']) cnf.append(-nodes[f'lv_{j}_{i}'])
cnf.append(nodes[f'l{l}_{j}_{i}']) cnf.append(nodes[f'l{l}_{j}_{i}'])
cnf.append(-nodes[f'l{l}_{j}_{i+1}']) cnf.append(-nodes[f'l{l}_{j}_{i+1}'])
for i in range(h): for i, j in itertools.product(range(h),range(w-1)):
for j in range(w-1):
for l in range(1, num_l+1): for l in range(1, num_l+1):
cnf = [] cnf = []
cnfs.append(cnf) cnfs.append(cnf)
...@@ -1017,43 +1011,43 @@ def generate_sat2(Q, WH=None, seed=0): ...@@ -1017,43 +1011,43 @@ def generate_sat2(Q, WH=None, seed=0):
cnf.append(nodes[f'l{l}_{j}_{i}']) cnf.append(nodes[f'l{l}_{j}_{i}'])
cnf.append(-nodes[f'l{l}_{j+1}_{i}']) cnf.append(-nodes[f'l{l}_{j+1}_{i}'])
# line孤立禁止 # 接続していない配線は異なる
for i in range(h): for i, j in itertools.product(range(h-1),range(w)):
for j in range(w):
for l in range(1, num_l+1): for l in range(1, num_l+1):
cnf = [] cnf = []
cnfs.append(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}'])
if j+1 <= w-1: 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'lh_{j}_{i}'])
if j-1 >= 0: cnf.append(-nodes[f'l{l}_{j}_{i}'])
cnf.append(nodes[f'lh_{j-1}_{i}']) cnf.append(-nodes[f'l{l}_{j+1}_{i}'])
if i+1 <= h-1:
cnf.append(nodes[f'lv_{j}_{i}']) # line孤立禁止
if i-1 >= 0: for i, j in itertools.product(range(h),range(w)):
cnf.append(nodes[f'lv_{j}_{i-1}']) 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三叉禁止 # line三叉禁止
for i in range(h): for i, j in itertools.product(range(h),range(w)):
for j in range(w): around = _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}'])
if len(around) == 2: if len(around) == 2:
continue continue
if len(around) == 3: elif len(around) == 3:
cnf = [] cnf = []
cnfs.append(cnf) cnfs.append(cnf)
cnf.append(-around[0]) cnf.append(-around[0])
cnf.append(-around[1]) cnf.append(-around[1])
cnf.append(-around[2]) cnf.append(-around[2])
if len(around) == 4: elif len(around) == 4:
for ar in itertools.combinations(around, 3): for ar in itertools.combinations(around, 3):
cnf = [] cnf = []
cnfs.append(cnf) cnfs.append(cnf)
...@@ -1062,80 +1056,41 @@ def generate_sat2(Q, WH=None, seed=0): ...@@ -1062,80 +1056,41 @@ def generate_sat2(Q, WH=None, seed=0):
cnf.append(-ar[2]) cnf.append(-ar[2])
# 非端点は周囲2マス以上に接続 # 非端点は周囲2マス以上に接続
for i in range(h): for i, j in itertools.product(range(h),range(w)):
for j in range(w): for l in range(1, num_l+1):
around = [] around = _get_around(j, i, w, h, nodes)
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: if len(around) == 2:
for ar in around: around_itr = itertools.combinations(around, 1)
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)
elif len(around) == 3: elif len(around) == 3:
for ar in itertools.combinations(around, 2): around_itr = 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])
elif len(around) == 4: elif len(around) == 4:
for ar in itertools.combinations(around, 3): around_itr = itertools.combinations(around, 3)
else:
# assert error
around_itr = []
for ar in around_itr:
cnf = [] cnf = []
cnfs.append(cnf) cnfs.append(cnf)
for b,mdx,mdy in bdxdylist: for b,mdx,mdy in bdxdylist:
if i+mdy < 0 or i+mdy >= h or j+mdx < 0 or j+mdx >= w: if i+mdy < 0 or i+mdy >= h or j+mdx < 0 or j+mdx >= w:
continue continue
cnf.append(nodes[f'b{b}_{j+mdx}_{i+mdy}']) cnf.append(nodes[f'b{b}_{j+mdx}_{i+mdy}'])
cnf.append(ar[0]) cnf.append(-nodes[f'l{l}_{j}_{i}'])
cnf.append(ar[1]) cnf.extend(list(ar))
cnf.append(ar[2])
# 端点は周囲2マス以上に接続禁止 # 端点は周囲2マス以上に接続禁止
for i in range(h): for i, j in itertools.product(range(h),range(w)):
for j in range(w): around = _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}'])
if len(around) == 2: if len(around) == 2:
for b,mdx,mdy in bdxdylist: around_itr = [around]
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: elif len(around) == 3:
for ar in itertools.combinations(around, 2): around_itr = 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: elif len(around) == 4:
for ar in itertools.combinations(around, 2): around_itr = itertools.combinations(around, 2)
else:
# assert error
around_itr = []
for ar in around_itr:
for b,mdx,mdy in bdxdylist: for b,mdx,mdy in bdxdylist:
if i+mdy < 0 or i+mdy >= h or j+mdx < 0 or j+mdx >= w: if i+mdy < 0 or i+mdy >= h or j+mdx < 0 or j+mdx >= w:
continue continue
...@@ -1144,20 +1099,10 @@ def generate_sat2(Q, WH=None, seed=0): ...@@ -1144,20 +1099,10 @@ def generate_sat2(Q, WH=None, seed=0):
cnf.append(-nodes[f'b{b}_{j+mdx}_{i+mdy}']) cnf.append(-nodes[f'b{b}_{j+mdx}_{i+mdy}'])
cnf.append(-ar[0]) cnf.append(-ar[0])
cnf.append(-ar[1]) cnf.append(-ar[1])
return nodes,cnfs
## 不要な制約
# 配線していないセルには線を接続しない # 配線していないセルには線を接続しない
for i in range(h): for i, j in itertools.product(range(h),range(w)):
for j in range(w): around = _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}'])
for index in around: for index in around:
cnf = [] cnf = []
cnfs.append(cnf) cnfs.append(cnf)
...@@ -1165,14 +1110,281 @@ def generate_sat2(Q, WH=None, seed=0): ...@@ -1165,14 +1110,281 @@ def generate_sat2(Q, WH=None, seed=0):
cnf.append(nodes[f'l{l}_{j}_{i}']) cnf.append(nodes[f'l{l}_{j}_{i}'])
cnf.append(-index) 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 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(): 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/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/Q004_10X10_b8_l9.txt')
#Q = readQ('./adc2019problem/Q005_10X10_b7_l6.txt') #Q = readQ('./adc2019problem/Q005_10X10_b7_l6.txt')
#Q = readQ('./adc2019problem/Q006_10X10_b8_l9.txt') #Q = readQ('./adc2019problem/Q006_10X10_b8_l9.txt')
...@@ -1187,19 +1399,41 @@ def main(): ...@@ -1187,19 +1399,41 @@ def main():
#Q = readQ('./adc2019problem/QRAND368_10X10_b10_l15.txt') #Q = readQ('./adc2019problem/QRAND368_10X10_b10_l15.txt')
#Q = readQ('./adc2019problem/random_problem/QRAND136_30X30_b30_l30.txt') #Q = readQ('./adc2019problem/random_problem/QRAND136_30X30_b30_l30.txt')
mode = 3
if mode == 1:
# cell-line variables
#start_time = time.time() #start_time = time.time()
nodes,cnfs = generate_sat2(Q, WH=(8,5), seed=0) nodes,cnfs = generate_sat(Q, WH=None, seed=0)
print_cnf2(len(nodes), cnfs) #print(nodes)
print_cnf(nodes, cnfs)
os.system('minisat p.txt a.txt') os.system('minisat p.txt a.txt')
A = read_satA2('a.txt', Q, nodes) A = read_satA('a.txt', Q, nodes)
if A is None: if A is None:
return return
print(strA(A)) print(strA(A))
debug_satA2('a.txt', Q, nodes) #debug_satA2('a.txt', Q, nodes)
#end_time= time.time() #end_time= time.time()
#print(f"経過時間：{end_time - start_time}") #print(f"経過時間：{end_time - start_time}")
#img = QA2img(Q,A) #img = QA2img(Q,A)
#plt.imshow(img) #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__': if __name__ == '__main__':
main() main()
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment