In [18]:

    

import Numberjack
G = Numberjack.Matrix(9, 9, 1, 9, 'x')
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(results))


def r(row, start, end, total):
  t((row, start), (row, end), total)


def c(col, start, end, total):
  t((start, col), (end, col), total)


A = Numberjack.Variable([4, 8, 15, 16, 23, 42], 'A')
B = Numberjack.Variable([4, 15, 16, 23, 42], 'B')
C = Numberjack.Variable([4, 8, 15, 16, 23, 42], 'C')
D = Numberjack.Variable([4, 8, 15, 16, 23, 42], 'D')
E = Numberjack.Variable([4, 8, 15, 16, 23, 42], 'E')
F = Numberjack.Variable([4, 8, 15, 16, 23, 42], 'F')
LETTERS = [A, B, C, D, E, F]
model.add(Numberjack.AllDiff(LETTERS))

r(0, 0, 1, 9)  ; r(0, 5, 6, B)
r(1, 0, 3, 25) ; r(1, 5, 7, 17)
r(2, 2, 3, 10) ; r(2, 7, 8, 5)
r(3, 1, 4, 13) ; r(3, 6, 8, 6)
r(4, 1, 7, F)
r(5, 0, 2, 22) ; r(5, 4, 7, 21)
r(6, 0, 1, 6)  ; r(6, 5, 6, 5)
r(7, 1, 3, 15) ; r(7, 5, 8, 11)
r(8, 2, 3, D)  ; r(8, 7, 8, 9)

c(0, 0, 1, 10) ; c(0, 5, 6, 13)
c(1, 0, 1, 12) ; c(1, 3, 7, 22)
c(2, 1, 5, C)  ; c(2, 7, 8, 12)
c(3, 1, 4, 28) ; c(3, 7, 8, 3)
c(4, 3, 5, A)
c(5, 0, 1, 6)  ; c(5, 4, 7, 20)
c(6, 0, 1, 12) ; c(6, 3, 7, E)
c(7, 1, 5, 17) ; c(7, 7, 8, 10)
c(8, 2, 3, 3)  ; c(8, 7, 8, 6)


solver = model.load('MiniSat')
solver.solve()

n = 0

unchanged = {}

extractions = []

print("is_sat", solver.is_sat())
print("is_unsat", solver.is_unsat())


def cache(name, value):
  coerced = '%2d' % value
  if name not in unchanged:
    unchanged[name] = coerced
  elif unchanged[name] != coerced:
    unchanged[name] = '?'

while solver.getNextSolution():
  n += 1
  print('#%s' % n)

  for l in LETTERS:
    print(l.name(), l.get_value())
    cache(l.name(), l.get_value())

  for r in range(9):
    row = []
    for c in range(9):
      name = G[r][c].name()
      if name in visited:
        value = G[r][c].get_value()
        cache(name, value)
        row.append('%2d' % value)
      else:
        row.append('##')
    print('\t'.join(row))

print('unchanged', unchanged)

for l in LETTERS:
  print(l.name(), unchanged[l.name()])

for r in range(9):
  row = []
  for c in range(9):
    name = G[r][c].name()
    if name in visited:
      row.append(unchanged[name])
    else:
      row.append('##')
  print('\t'.join(row))
print(unchanged)


    

    




is_sat True
is_unsat False
#1
A 15
B 4
C 16
D 8
E 23
F 42
 4	 5	##	##	##	 1	 3	##	##
 6	 7	 4	 8	##	 5	 9	 3	##
##	##	 1	 9	##	##	##	 4	 1
##	 1	 2	 6	 4	##	 3	 1	 2
##	 4	 3	 5	 8	 9	 6	 7	##
 9	 7	 6	##	 3	 7	 9	 2	##
 4	 2	##	##	##	 1	 4	##	##
##	 8	 5	 2	##	 3	 1	 2	 5
##	##	 7	 1	##	##	##	 8	 1
unchanged {'A': '15', 'B': ' 4', 'C': '16', 'D': ' 8', 'E': '23', 'F': '42', 'x0.0': ' 4', 'x0.1': ' 5', 'x0.5': ' 1', 'x0.6': ' 3', 'x1.0': ' 6', 'x1.1': ' 7', 'x1.2': ' 4', 'x1.3': ' 8', 'x1.5': ' 5', 'x1.6': ' 9', 'x1.7': ' 3', 'x2.2': ' 1', 'x2.3': ' 9', 'x2.7': ' 4', 'x2.8': ' 1', 'x3.1': ' 1', 'x3.2': ' 2', 'x3.3': ' 6', 'x3.4': ' 4', 'x3.6': ' 3', 'x3.7': ' 1', 'x3.8': ' 2', 'x4.1': ' 4', 'x4.2': ' 3', 'x4.3': ' 5', 'x4.4': ' 8', 'x4.5': ' 9', 'x4.6': ' 6', 'x4.7': ' 7', 'x5.0': ' 9', 'x5.1': ' 7', 'x5.2': ' 6', 'x5.4': ' 3', 'x5.5': ' 7', 'x5.6': ' 9', 'x5.7': ' 2', 'x6.0': ' 4', 'x6.1': ' 2', 'x6.5': ' 1', 'x6.6': ' 4', 'x7.1': ' 8', 'x7.2': ' 5', 'x7.3': ' 2', 'x7.5': ' 3', 'x7.6': ' 1', 'x7.7': ' 2', 'x7.8': ' 5', 'x8.2': ' 7', 'x8.3': ' 1', 'x8.7': ' 8', 'x8.8': ' 1'}
A 15
B  4
C 16
D  8
E 23
F 42
 4	 5	##	##	##	 1	 3	##	##
 6	 7	 4	 8	##	 5	 9	 3	##
##	##	 1	 9	##	##	##	 4	 1
##	 1	 2	 6	 4	##	 3	 1	 2
##	 4	 3	 5	 8	 9	 6	 7	##
 9	 7	 6	##	 3	 7	 9	 2	##
 4	 2	##	##	##	 1	 4	##	##
##	 8	 5	 2	##	 3	 1	 2	 5
##	##	 7	 1	##	##	##	 8	 1
{'A': '15', 'B': ' 4', 'C': '16', 'D': ' 8', 'E': '23', 'F': '42', 'x0.0': ' 4', 'x0.1': ' 5', 'x0.5': ' 1', 'x0.6': ' 3', 'x1.0': ' 6', 'x1.1': ' 7', 'x1.2': ' 4', 'x1.3': ' 8', 'x1.5': ' 5', 'x1.6': ' 9', 'x1.7': ' 3', 'x2.2': ' 1', 'x2.3': ' 9', 'x2.7': ' 4', 'x2.8': ' 1', 'x3.1': ' 1', 'x3.2': ' 2', 'x3.3': ' 6', 'x3.4': ' 4', 'x3.6': ' 3', 'x3.7': ' 1', 'x3.8': ' 2', 'x4.1': ' 4', 'x4.2': ' 3', 'x4.3': ' 5', 'x4.4': ' 8', 'x4.5': ' 9', 'x4.6': ' 6', 'x4.7': ' 7', 'x5.0': ' 9', 'x5.1': ' 7', 'x5.2': ' 6', 'x5.4': ' 3', 'x5.5': ' 7', 'x5.6': ' 9', 'x5.7': ' 2', 'x6.0': ' 4', 'x6.1': ' 2', 'x6.5': ' 1', 'x6.6': ' 4', 'x7.1': ' 8', 'x7.2': ' 5', 'x7.3': ' 2', 'x7.5': ' 3', 'x7.6': ' 1', 'x7.7': ' 2', 'x7.8': ' 5', 'x8.2': ' 7', 'x8.3': ' 1', 'x8.7': ' 8', 'x8.8': ' 1'}

In [ ]: