diff --git a/solver.py b/solver.py index c11f9a4d910d78dafc949fca1adcbf138ef7a7b6..65c83e49b766574f9e21bffd63d2c1dfb8b77d4f 100644 --- a/solver.py +++ b/solver.py @@ -206,15 +206,222 @@ def print_cnf(nodes, cnfs, filename='p.txt'): #print(''.join(s)) def print_cnf2(nodes, cnfs, filename='p.txt'): - num = len(nodes) s = [] - s.append(f'p cnf {num} {len(cnfs)}\n') + s.append(f'p cnf {len(nodes)} {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 _get_map_b(Q,A): + map_b = np.zeros((A['h'], A['w']), dtype=int) + for b in range(1, Q['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 + return map_b + +def optimize(Q, A): + Q, A = del_blank(Q, A) + num_b = Q['num_b'] + num_l = Q['num_l'] + map_l = A['map'] + h, w = map_l.shape + map_b = _get_map_b(Q,A) + + # 左に動かす + while True: + updated = False + for b in range(1,num_b+1): + cells = Q['BLOCK'][b]['cells'] + x, y = A['BLOCK'][b]['x'], A['BLOCK'][b]['y'] + canMove = True + for dx,dy in cells.keys(): + if cells[(dx,dy)] != '+': + # とりあえず配線のあるブロックは動かさない + canMove = False + break + if x+dx-1 < 0: + canMove = False + break + if map_b[y+dy,x+dx-1] != 0 and map_b[y+dy,x+dx-1] != b: + canMove = False + break + if map_l[y+dy,x+dx-1] != 0: + canMove = False + break + if not canMove: + continue + # 左に動かせる! + A['BLOCK'][b]['x'] = x-1 + for dx,dy in cells.keys(): + map_b[y+dy,x+dx] = 0 + for dx,dy in cells.keys(): + map_b[y+dy,x+dx-1] = b + updated = True + if not updated: + break + else: + Q, A = del_blank(Q, A) + map_b = _get_map_b(Q,A) + h, w = map_b.shape + # 上に動かす + while True: + updated = False + for b in range(1,num_b+1): + cells = Q['BLOCK'][b]['cells'] + x, y = A['BLOCK'][b]['x'], A['BLOCK'][b]['y'] + canMove = True + for dx,dy in cells.keys(): + if cells[(dx,dy)] != '+': + # とりあえず配線のあるブロックは動かさない + canMove = False + break + if y+dy-1 < 0: + canMove = False + break + if map_b[y+dy-1,x+dx] != 0 and map_b[y+dy-1,x+dx] != b: + canMove = False + break + if map_l[y+dy-1,x+dx] != 0: + canMove = False + break + if not canMove: + continue + # 上に動かせる! + A['BLOCK'][b]['y'] = y-1 + for dx,dy in cells.keys(): + map_b[y+dy,x+dx] = 0 + for dx,dy in cells.keys(): + map_b[y+dy-1,x+dx] = b + updated = True + if not updated: + break + else: + Q, A = del_blank(Q, A) + map_b = _get_map_b(Q,A) + h, w = map_b.shape + # 右に動かす + while True: + updated = False + for b in range(1,num_b+1): + cells = Q['BLOCK'][b]['cells'] + x, y = A['BLOCK'][b]['x'], A['BLOCK'][b]['y'] + canMove = True + for dx,dy in cells.keys(): + if cells[(dx,dy)] != '+': + # とりあえず配線のあるブロックは動かさない + canMove = False + break + if x+dx+1 >= w: + canMove = False + break + if map_b[y+dy,x+dx+1] != 0 and map_b[y+dy,x+dx+1] != b: + canMove = False + break + if map_l[y+dy,x+dx+1] != 0: + canMove = False + break + if not canMove: + continue + # 右に動かせる! + A['BLOCK'][b]['x'] = x+1 + for dx,dy in cells.keys(): + map_b[y+dy,x+dx] = 0 + for dx,dy in cells.keys(): + map_b[y+dy,x+dx+1] = b + updated = True + if not updated: + break + else: + Q, A = del_blank(Q, A) + map_b = _get_map_b(Q,A) + h, w = map_b.shape + # 下に動かす + while True: + updated = False + for b in range(1,num_b+1): + cells = Q['BLOCK'][b]['cells'] + x, y = A['BLOCK'][b]['x'], A['BLOCK'][b]['y'] + canMove = True + for dx,dy in cells.keys(): + if cells[(dx,dy)] != '+': + # とりあえず配線のあるブロックは動かさない + canMove = False + break + if y+dy+1 >= h: + canMove = False + break + if map_b[y+dy+1,x+dx] != 0 and map_b[y+dy+1,x+dx] != b: + canMove = False + break + if map_l[y+dy+1,x+dx] != 0: + canMove = False + break + if not canMove: + continue + # 上に動かせる! + A['BLOCK'][b]['y'] = y+1 + for dx,dy in cells.keys(): + map_b[y+dy,x+dx] = 0 + for dx,dy in cells.keys(): + map_b[y+dy+1,x+dx] = b + updated = True + if not updated: + break + else: + Q, A = del_blank(Q, A) + map_b = _get_map_b(Q,A) + h, w = map_b.shape + + return A + +def del_blank(Q, A): + num_b = Q['num_b'] + num_l = Q['num_l'] + ## 最小矩形に更新 + 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 Q, A + def read_satA(filename, Q, nodes, TF=None): with open(filename, 'r') as file: str_line = file.readline() @@ -302,45 +509,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 - 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 + A = optimize(Q, A) return A def read_satA2(filename, Q, nodes, TF=None): @@ -1390,15 +1559,16 @@ def main(): #Q = readQ('./adc2019problem/Q005_10X10_b7_l6.txt') #Q = readQ('./adc2019problem/Q006_10X10_b8_l9.txt') #Q = readQ('./adc2019problem/Q007_10X10_b7_l8.txt') - #Q = readQ('./adc2019problem/Q008_10X10_b10_l0.txt') + Q = readQ('./adc2019problem/Q008_10X10_b10_l0.txt') #Q = readQ('./adc2019problem/Q009_10X10_b7_l9.txt') #Q = readQ('./adc2019problem/Q010_10X10_b20_l24.txt') #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/QRAND327_20X20_b20_l15.txt') #Q = readQ('./adc2019problem/QRAND368_10X10_b10_l15.txt') #Q = readQ('./adc2019problem/random_problem/QRAND136_30X30_b30_l30.txt') + #Q = readQ('./Q1.txt') mode = 1