In [3]:
import Numberjack
G = Numberjack.Matrix(9, 9, -9, 9)
model = Numberjack.Model()
a = model.add
visited = {}
def t(start, end, total):
results = []
r1, c1 = start
r2, c2 = end
if r1 == r2:
results = [G[r1][c] for c in range(c1, c2 + 1)]
elif c1 == c2:
results = [G[r][c1] for r in range(r1, r2 + 1)]
else:
raise Exception(start, end)
for exp in results:
visited[exp.name()] = True
model.add(Numberjack.Sum(results) == total)
model.add(Numberjack.AllDiff([Numberjack.Abs(x) for x in results]))
for x in results:
model.add(x != 0)
def r(row, start, end, total):
t((row, start), (row, end), total)
def c(col, start, end, total):
t((start, col), (end, col), total)
r(0, 0, 4, 31) ; r(0, 6, 8, 7)
r(1, 0, 4, 1) ; r(1, 6, 8, 7)
r(2, 0, 2, 7) ; r(2, 4, 8, 29)
r(3, 2, 5, 12) ; r(3, 7, 8, 4)
r(4, 0, 3, 29) ; r(4, 5, 8, 11)
r(5, 0, 1, 6) ; r(5, 3, 6, 19)
r(6, 0, 4, 3) ; r(6, 6, 8, 10)
r(7, 0, 2, 13) ; r(7, 4, 8, 15)
r(8, 0, 2, 15) ; r(8, 4, 8, 15)
c(0, 0, 2, 12) ; c(0, 4, 8, 34)
c(1, 0, 2, 5) ; c(1, 4, 8, 17)
c(2, 0, 4, 29) ; c(2, 6, 8, 7)
c(3, 0, 1, 4) ; c(3, 3, 6, 12)
c(4, 0, 3, -1) ; c(4, 5, 8, 17)
c(5, 2, 5, 12) ; c(5, 7, 8, 5)
c(6, 0, 2, -3) ; c(6, 4, 8, 22)
c(7, 0, 4, 19) ; c(7, 6, 8, 11)
c(8, 0, 4, 21) ; c(8, 6, 8, 11)
for r in range(9):
group = []
for c in range(9):
if G[r][c].name() in visited:
group.append(G[r][c])
a(Numberjack.Sum([x < 0 for x in group]) == 1)
for c in range(9):
group = []
for r in range(9):
if G[r][c].name() in visited:
group.append(G[r][c])
a(Numberjack.Sum([x < 0 for x in group]) == 1)
solver = model.load('Mistral')
solver.solve()
print("is_sat", solver.is_sat())
print("is_unsat", solver.is_unsat())
for r in range(9):
row = []
for c in range(9):
if G[r][c].name() in visited:
row.append('%2d' % G[r][c].get_value())
else:
row.append('##')
print('\t'.join(row))
In [ ]: