Skip to content

Instantly share code, notes, and snippets.

@nlitsme
Created October 14, 2020 13:27
Show Gist options
  • Save nlitsme/0575029291d5f599c32780c22fed24da to your computer and use it in GitHub Desktop.
Save nlitsme/0575029291d5f599c32780c22fed24da to your computer and use it in GitHub Desktop.
example sudoku solver
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")
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment