remove cyclic paths (88ecc3df) · Commits · adc2019 / twd-solver

satsolver.ipynb

0 → 100644

+40112 −0

File added.

Preview size limit exceeded, changes collapsed.

solver.py

+120 −13

Changes for solver.py: 120 added lines, 13 removed lines.
Original line number	Diff line number	Diff line
		# パッケージ

		%matplotlib inline
		#%matplotlib inline
		import numpy as np
		import cv2 as cv # opencv
		import matplotlib
		@@ -84,6 +84,22 @@ def readA(filename):
		i += 1
		return A

		def 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):
		x = block_list[i]['x']
		y = block_list[i]['y']
		r.append(f'BLOCK#{i} @({x},{y})\n')
		return ''.join(r)

		def index2color(index, mode='cell'):
		if mode == 'cell':
		if index == -1:
		@@ -169,8 +185,6 @@ def show(index, read=None):

		plt.imshow(img)



		def add(e, _dict):
		if e not in _dict.keys():
		_dict[e] = len(_dict) + 1
		@@ -194,6 +208,7 @@ def read_satA(filename, Q, nodes, TF=None):
		str_line = file.readline()
		if str_line.startswith('UNSAT'):
		print('UNSAT')
		return None
		else:
		print('SAT')
		str_line = file.readline()
		@@ -214,6 +229,8 @@ def read_satA(filename, Q, nodes, TF=None):
		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):
		@@ -233,6 +250,85 @@ def read_satA(filename, Q, nodes, TF=None):
		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():
		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):
		@@ -263,14 +359,20 @@ def debug_satA(filename, Q, nodes, TF=None):
		return A


		def generate_sat(Q):
		def generate_sat(Q, WH=None):
		nodes = {}
		cnfs = []

		num_b = len(Q['BLOCK'])
		num_l = Q['num_l']
		w = Q['w'] = 20
		h = Q['h'] = 20
		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]

		# ラインからブロック番号, 位置を逆引き
		l2b = [[] for _ in range(num_l+1)]
		@@ -547,7 +649,7 @@ def generate_sat(Q):

		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/Q004_10X10_b8_l9.txt')
		@@ -560,17 +662,22 @@ def main():
		#Q = readQ('./adc2019problem/Q013_10X10_b8_l9.txt')
		#Q = readQ('./adc2019problem/Q014_10X10_b9_l9.txt')
		#Q = readQ('./adc2019problem/Q015_10X10_b8_l9.txt')
		#Q = readQ('./adc2019problem/QRAND327_20X20_b20_l15.txt')
		Q = readQ('./adc2019problem/QRAND368_10X10_b10_l15.txt')

		start_time = time.time()
		nodes,cnfs = generate_sat(Q)
		#start_time = time.time()
		nodes,cnfs = generate_sat(Q, WH=None)
		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)
		#end_time= time.time()
		#print(f"経過時間：{end_time - start_time}")
		#img = QA2img(Q,A)
		#plt.imshow(img)

		main()