example sudoku solver

pyz3.py

from z3 import *
# https://www.youtube.com/watch?v=9ATC_uBF8ow
# Normal sudoku rules apply.
#  - ALL horizontally and vertically neighbouring digits with the sum 10 are marked with X;
#  - ALL horizontally and vertically neighbouring digits with the sum 5 are marked with V.

# these pairs sum to 10:
#   (0,2) + (1,2),  (0,4) + (1,4), (0,6) + (1,6)
#   (1,1) + (2,1), (1,3) + (2,3), (1,5) + (2,5), (1,7) + (2,7)
#   (2,2) + (3,2), (2,4) + (3,4), (2,6) + (3,6)


# the basis for this solver is from https://stackoverflow.com/questions/23451388/z3-sudoku-solver

# 9x9 matrix of integer variables
X = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(9) ] 
      for i in range(9) ]

# each cell contains a value in {1, ..., 9}
cells_c  = [ And(1 <= X[i][j], X[i][j] <= 9) 
             for i in range(9) for j in range(9) ]

# each row contains a digit at most once
rows_c   = [ Distinct(X[i]) for i in range(9) ]

# each column contains a digit at most once
cols_c   = [ Distinct([ X[i][j] for i in range(9) ]) 
             for j in range(9) ]

# each 3x3 square contains a digit at most once
sq_c     = [ Distinct([ X[3*i0 + i][3*j0 + j] 
                        for i in range(3) for j in range(3) ]) 
             for i0 in range(3) for j0 in range(3) ]

marked_x = [ (0,2), (0,4), (0,6), (1,1), (1,3), (1,5), (1,7), (2,2), (2,4), (2,6) ]
sum10    = [ X[i][j]+X[i+1][j] == 10 for i,j in marked_x ]

# none of the other pairs (x,y)+(x+1,y)   and (x,y)+(x,y+1)  sum to either 5 or 10
not5_v    = [ X[i][j]+X[i+1][j] != 5 for i in range(8) for j in range(9) ]
not5_h    = [ X[i][j]+X[i][j+1] != 5 for i in range(9) for j in range(8) ]
not10_v    = [ X[i][j]+X[i+1][j] != 10 for i in range(8) for j in range(9) if (i,j) not in marked_x ]
not10_h    = [ X[i][j]+X[i][j+1] != 10 for i in range(9) for j in range(8) ]

sudoku_c = cells_c + rows_c + cols_c + sq_c + sum10 + not5_v + not5_h + not10_v + not10_h

# sudoku instance, we use '0' for empty cells
instance = ((0,0,0,0,0,0,0,0,0),
            (0,0,0,0,0,0,0,0,0),
            (0,0,0,0,0,0,0,0,0),
            (0,0,0,0,0,0,0,0,0),
            (0,0,0,0,0,0,0,0,0),
            (0,5,0,3,0,8,0,2,0),
            (2,0,5,0,3,0,6,0,9),
            (0,9,0,4,0,6,0,1,0),
            (0,0,0,0,0,0,0,0,0))

instance_c = [ If(instance[i][j] == 0, 
                  True, 
                  X[i][j] == instance[i][j]) 
               for i in range(9) for j in range(9) ]

s = Solver()
s.add(sudoku_c + instance_c)
if s.check() == sat:
    m = s.model()
    r = [ [ m.evaluate(X[i][j]) for j in range(9) ] 
          for i in range(9) ]
    print_matrix(r)
else:
    print("failed to solve")