from itertools import product, combinations, count, chain
import numpy as np
from time import time
import pycosat
GRIDS = """\
000000068900000002000400500041000000000035000050000000000800010300000700000100400
080000400300600000000700005100200000000000052400000000700000300000080060020050000
080000100300500000000600004100200000000000042700000000600000300000080050020040000
000200400005000800030070000000108030100400000000000050024000100000050000600000000
400750000002030000000000000000500064010000000000000080570000300000002100600400000
050003600200700000000000000830400000000020070000000100000001200700000040040060000
000040230800500000000000000060001000000020700300000400000300068002400000010000000
""".split()
_N = 3 # for 9x9 grid size
N = _N ** 2
gen = count(1)
dom = range(N)
cnf_vars = {v : next(gen) for v in product(dom, repeat=3)} # création des variables booléennes
revert = dict(zip(cnf_vars.values(), cnf_vars.keys())) # mapping inverse variables -> index
# precompute indexes
rows = [[(i, j) for j in dom] for i in dom]
cols = [[(i, j) for i in dom] for j in dom]
blocs = [[(i, j) for i, j in product(range(x, x + _N), range(y, y + _N))]
for x, y in product(range(0, N, _N), repeat=2)]
# on preconstruit la liste des contraintes, qui est valable pour toute grille
cnf = []
# existence : pour chaque case, il existe (au moins) une valeur entre 1 et N
cnf.extend([[cnf_vars[i,j,k] for k in range(N)]
for i, j in product(dom, repeat=2)])
# unicite : pour chaque ligne/colonne/bloc, il y a une seule valeur k entre 1 et N
cnf.extend([[-cnf_vars[i1,j1,k], -cnf_vars[i2,j2,k]]
for row in rows
for (i1,j1), (i2,j2) in combinations(row, 2)
for k in dom])
cnf.extend([[-cnf_vars[i1,j1,k], -cnf_vars[i2,j2,k]]
for col in cols
for (i1,j1), (i2,j2) in combinations(col, 2)
for k in dom])
cnf.extend([[-cnf_vars[i1,j1,k], -cnf_vars[i2,j2,k]]
for bloc in blocs
for (i1,j1), (i2,j2) in combinations(bloc, 2)
for k in dom
if i1 != i2 and j1 != j2]) # avoid redundancy from rows/cols
def make_grid(s):
return np.array(list(map(int, s))).reshape((N,N))
def grid_constraints(grid):
#yield grid-specific clauses to list of constraints
return [[cnf_vars[i, j, grid[i][j] - 1]]
for i, j in product(dom, repeat=2)
if grid[i][j] != 0]
def decode(result):
solution = {revert[v][:2]: revert[v][2] + 1 for v in result if v > 0}
return [[solution[i,j] for j in dom] for i in dom]
def solve(grid):
clauses = grid_constraints(grid)
result = pycosat.solve(chain(cnf, clauses))
return result if isinstance(result, str) else decode(result)
t1 = time()
for grid in map(make_grid, GRIDS):
solution = solve(grid)
if isinstance(solution, str):
print(solution)
t2 = time()
print("%d grids" % len(GRIDS))
print("elapsed time %.4fs (average by grid: %.3fs)" % (t2-t1, (t2-t1) / len(GRIDS)))