另一种 Nonogram Solver
翻出很久以前写的一个 nonogram 求解器，它不显式建模黑白格，而是通过前缀计数间接建模。
例如一行是"3 2 4"，通常建成这一行有3黑格，至少1白格，2黑格，1白格，4黑格。 而这种求解方法把它建模成，每一个格子的数字，表示这一行到目前位置走过了多少个黑格。 又因为行、列都不超过99，通过除余100来将行、列走过的黑格数建到一起（v = 100 * col + row）。 这样"3 2 4"在行上的数字可能就是"1 2 3 3 4 5 5 5 5 5 6 7 8 9 9"， 计数值的停留表示了黑块的结束。 为了保证两个黑块间有一个白格，我们要求边界前缀值出现不止一次，而块内部的前缀值只能出现一次。
相比常规解法，这种解法更间接，更不直观，更慢，但很好玩。
from z3 import * # noqa: F403
from colorama import Fore, Back, Style
COLS = '''
4
1 4
1 5 2
1 4 4
7 6
5 6
5
5
7
8
9
8
8
7
4
'''
ROWS = '''
3
1 1
3 2 4
6 6
6 7
5 7
4 8
1 8
9
9
7
4
3
4
3
'''
def _to_sum(str):
str_to_int_lst = lambda lst: list(map(lambda x: int(x), lst))
rows_str = map(lambda y: y.split(' '),
filter(lambda x: len(x) > 0, str.split('\n')))
rows = map(lambda x: str_to_int_lst(x), rows_str)
return list(rows)
cols = _to_sum(COLS)
rows = _to_sum(ROWS)
SIZE = len(cols)
solver = Solver()
input = [Int(f'a_{x+1}_{y+1}') for x in range(SIZE) for y in range(SIZE)]
elem = lambda row, col: input[row * SIZE + col]
for i in range(SIZE):
for j in range(SIZE):
solver.add(elem(i, j) >= 0)
for i in range(SIZE):
for j in range(SIZE - 1):
solver.add(Or([elem(i, j+1) % 100 == elem(i, j) % 100, elem(i, j+1) % 100 == elem(i, j) % 100 + 1]))
solver.add(Or([elem(j+1, i) / 100 == elem(j, i) / 100, elem(j+1, i) / 100 == elem(j, i) / 100 + 1]))
# cols
for i in range(SIZE):
col = []
for j in range(SIZE):
col.append(input[j * SIZE + i])
solver.add(Or([col[0] / 100 == 0, col[0] / 100 == 1]))
total = 0
totals = []
for s in cols[i]:
total += s
totals.append(total)
totals.pop()
for j in range(1, total):
cnt = Sum([If(j == x / 100, 1, 0) for x in col])
if j in totals:
solver.add(cnt > 1)
else:
solver.add(cnt == 1)
solver.add(elem(SIZE - 1, i) / 100 == total)
# rows
for i in range(SIZE):
row = input[i * SIZE:i * SIZE + SIZE]
solver.add(Or([row[0] % 100 == 0, row[0] % 100 == 1]))
total = 0
totals = []
for s in rows[i]:
total += s
totals.append(total)
totals.pop()
for j in range(1, total):
cnt = Sum([If(j == x % 100, 1, 0) for x in row])
if j in totals:
solver.add(cnt > 1)
else:
solver.add(cnt == 1)
solver.add(elem(i, SIZE - 1) % 100 == total)
# implies
# first block
solver.add(elem(0, 0) % 100 == elem(0, 0) / 100)
for i in range(1, SIZE):
# first col
solver.add(Implies(elem(i, 0) % 100 == 0, elem(i, 0) / 100 == elem(i-1, 0) / 100))
solver.add(Implies(elem(i, 0) % 100 == 1, elem(i, 0) / 100 == elem(i-1, 0) / 100 + 1))
# first row
solver.add(Implies(elem(0, i) / 100 == 0, elem(0, i) % 100 == elem(0, i-1) % 100))
solver.add(Implies(elem(0, i) / 100 == 1, elem(0, i) % 100 == elem(0, i-1) % 100 + 1))
# other blocks
for col in range(1, SIZE):
for row in range(1, SIZE):
solver.add(Implies(elem(row, col) / 100 == elem(row-1, col) / 100 + 1, elem(row, col) % 100 == elem(row, col-1) % 100 + 1))
solver.add(Implies(elem(row, col) / 100 == elem(row-1, col) / 100, elem(row, col) % 100 == elem(row, col-1) % 100))
print(solver.check())
## output
my_j = -2
def my_print(s, end='\n'):
global my_j
my_j += 1
l = len(s)
r = l // 10 + 1
for i in range(r):
if (i % 2 == 0) ^ ((my_j // 5) % 2 == 0):
print(Back.WHITE + Fore.BLACK + s[i*10:10+i*10], end='')
else:
print(Back.BLACK + Fore.WHITE + s[i*10:10+i*10], end='')
print(Style.RESET_ALL, end=end)
m = solver.model()
result = []
for i in range(SIZE):
old_v = 0
line = []
line_block = []
for j in range(SIZE):
v = m.evaluate(m[input[i * SIZE + j]]).as_long()
line.append(v)
line_block.append('■' if (v % 100) > (old_v % 100) else ' ')
old_v = v
# print(x, end='')
# print('')
print(line)
result.append(line_block)
print('#.', end='')
my_print('.'.join(map(lambda x: str(x%10), range(1, SIZE + 1))), end='.\n')
k = 0
for i in result:
k += 1
print(f'{k%10}.', end='')
my_print('.'.join(i), end='.\n')