In [1]:
from boolexpr import *
In [2]:
ctx = Context()
In [3]:
DIGITS = "123456789"
In [4]:
X = ctx.get_vars("x", 9, 9, 9)
In [5]:
V = and_s(*[
and_s(*[
onehot(*[ X[r,c,v] for v in range(9) ])
for c in range(9)
])
for r in range(9)
])
In [6]:
R = and_s(*[
and_s(*[
onehot(*[ X[r,c,v] for c in range(9) ])
for v in range(9)
])
for r in range(9)
])
In [7]:
C = and_s(*[
and_s(*[
onehot(*[ X[r,c,v] for r in range(9) ])
for v in range(9)
])
for c in range(9)
])
In [8]:
B = and_s(*[
and_s(*[
onehot(*[ X[3*br+r,3*bc+c,v]
for r in range(3) for c in range(3) ])
for v in range(9)
])
for br in range(3) for bc in range(3)
])
In [9]:
S = and_s(V, R, C, B)
In [10]:
>>> def parse_grid(grid):
chars = [c for c in grid if c in DIGITS or c in "0."]
assert len(chars) == 9 ** 2
return and_s(*[ X[i//9,i%9,int(c)-1]
for i, c in enumerate(chars) if c in DIGITS ])
In [11]:
grid = ( ".73|...|8.."
"..4|13.|.5."
".85|..6|31."
"---+---+---"
"5..|.9.|.3."
"..8|.1.|5.."
".1.|.6.|..7"
"---+---+---"
".51|6..|28."
".4.|.52|9.."
"..2|...|64." )
In [12]:
def get_val(point, r, c):
for v in range(9):
if point[X[r,c,v]]:
return DIGITS[v]
return "X"
In [13]:
def display(point):
chars = list()
for r in range(9):
for c in range(9):
if c in (3, 6):
chars.append("|")
chars.append(get_val(point, r, c))
if r != 8:
chars.append("\n")
if r in (2, 5):
chars.append("---+---+---\n")
print("".join(chars))
In [14]:
f = and_s(S, parse_grid(grid))
solns = list(f.iter_sat())
# Verify there is exactly one solution
assert len(solns) == 1
display(solns[0])
In [ ]: