Skip to content

T
twd-solver
Commit 602a3e66 authored by Kento HASEGAWA's avatar Kento HASEGAWA
Browse files
Options

Merge branch 'master' into adc2019-system

parents efe5a32e a3d6f273
Show whitespace changes
Inline Side-by-side
Showing with 762 additions and 13 deletions
solver.py
View file @ 602a3e66
...@@ -9,6 +9,7 @@ import re ...@@ -9,6 +9,7 @@ import re
import glob import glob
import time import time
import random import random
import itertools
if __name__ == '__main__': if __name__ == '__main__':
import cv2 as cv # opencv import cv2 as cv # opencv
...@@ -204,6 +205,15 @@ def print_cnf(nodes, cnfs, filename='p.txt'): ...@@ -204,6 +205,15 @@ def print_cnf(nodes, cnfs, filename='p.txt'):
#s.append(s_sub) #s.append(s_sub)
#print(''.join(s)) #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): def read_satA(filename, Q, nodes, TF=None):
with open(filename, 'r') as file: with open(filename, 'r') as file:
str_line = file.readline() str_line = file.readline()
...@@ -332,6 +342,135 @@ def read_satA(filename, Q, nodes, TF=None): ...@@ -332,6 +342,135 @@ def read_satA(filename, Q, nodes, TF=None):
A['w'] = w A['w'] = w
return A 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): def debug_satA(filename, Q, nodes, TF=None):
TF = [False] * (len(nodes)+1) TF = [False] * (len(nodes)+1)
A = read_satA(filename, Q, nodes, TF) A = read_satA(filename, Q, nodes, TF)
...@@ -359,6 +498,53 @@ def debug_satA(filename, Q, nodes, TF=None): ...@@ -359,6 +498,53 @@ def debug_satA(filename, Q, nodes, TF=None):
print(l_board) print(l_board)
return A 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): def generate_sat(Q, WH=None, seed=0):
nodes = {} nodes = {}
cnfs = [] cnfs = []
...@@ -654,6 +840,546 @@ def generate_sat(Q, WH=None, seed=0): ...@@ -654,6 +840,546 @@ 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'
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):
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(): def main():
Q = readQ('./adc2019problem/Q001_10X10_b8_l11.txt') Q = readQ('./adc2019problem/Q001_10X10_b8_l11.txt')
...@@ -671,20 +1397,43 @@ def main(): ...@@ -671,20 +1397,43 @@ def main():
#Q = readQ('./adc2019problem/Q015_10X10_b8_l9.txt') #Q = readQ('./adc2019problem/Q015_10X10_b8_l9.txt')
#Q = readQ('./adc2019problem/QRAND327_20X20_b20_l15.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')
#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_sat(Q, WH=None, seed=0) nodes,cnfs = generate_sat(Q, WH=None, seed=0)
#print(nodes)
print_cnf(nodes, cnfs) print_cnf(nodes, cnfs)
os.system('minisat p.txt a.txt') os.system('minisat p.txt a.txt')
A = read_satA('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))
#A = debug_satA('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