add solver2 (a0713f54) · Commits · adc2019 / twd-solver

solver.py

+518 −6

Changes for solver.py: 518 added lines, 6 removed lines.
Original line number	Diff line number	Diff line
		@@ -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()
		@@ -332,6 +342,135 @@ def read_satA(filename, Q, nodes, TF=None):
		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
		return A
		## 閉路の削除
		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():
		np.delete(map_l, i, axis=0)
		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():
		np.delete(map_l, j, axis=1)
		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)
		A = read_satA(filename, Q, nodes, TF)
		@@ -359,6 +498,52 @@ def debug_satA(filename, Q, nodes, TF=None):
		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 = {}
		@@ -657,11 +842,337 @@ def generate_sat(Q, WH=None, seed=0):
		cnf[f'l{l}_{j+dx2}_{i+dy2}'] = '-1'
		return nodes,cnfs


		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))

		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

		# 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 = []
		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):
		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':
		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 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):
		if i2 < 0 or i2 >= h:
		continue
		for j2 in range(j-3,j+4):
		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
		if flag:
		cnf = []
		cnfs.append(cnf)
		cnf.append(-nodes[f'b{b}_{j}_{i}'])
		cnf.append(-nodes[f'b{b2}_{j2}_{i2}'])




		# 接続セルの配線は等しい
		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}'])

		# 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}'])

		# 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:
		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])

		# 非端点は周囲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}'])
		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)
		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])
		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])
		# 端点は周囲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}'])
		if len(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(-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
		## 不要な制約
		# 配線していないセルには線を接続しない
		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:
		cnf = []
		cnfs.append(cnf)
		for l in range(1, num_l+1):
		cnf.append(nodes[f'l{l}_{j}_{i}'])
		cnf.append(-index)

		return nodes,cnfs


		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')
		@@ -674,16 +1185,17 @@ 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')

		#start_time = time.time()
		nodes,cnfs = generate_sat(Q, WH=None, seed=0)
		print_cnf(nodes, cnfs)
		nodes,cnfs = generate_sat2(Q, WH=(8,5), seed=0)
		print_cnf2(len(nodes), cnfs)
		os.system('minisat p.txt a.txt')
		A = read_satA('a.txt', Q, nodes)
		A = read_satA2('a.txt', Q, nodes)
		if A is None:
		return
		print(strA(A))
		#A = debug_satA('a.txt', Q, nodes)
		debug_satA2('a.txt', Q, nodes)
		#end_time= time.time()
		#print(f"経過時間：{end_time - start_time}")
		#img = QA2img(Q,A)