We'll design a simple program that solves sudoku puzzle using Z3.
# Imports
import z3
We need to encode the rules of the puzzle in propositional logic. To achieve that, we define certain variables that help us get around in the puzzle.
We start by defining a puzzle board,a 9x9 matrix of integer variables to mark the puzzle board.
# Runs a nested loop to create the two dimensional matrix required.
# c_i_j is the cell at ith row and jth column.
board = []
for i in range(9):
column = []
for j in range(9):
column.append(z3.Int("c_{0}_{1}".format(i+1, j+1)))
board.append(column)
board
We define a sudoku instance. 0 denotes empty cells.
sudoku = ( (0,0,0,0,9,4,0,3,0),
(0,0,0,5,1,0,0,0,7),
(0,8,9,0,0,0,0,4,0),
(0,0,0,0,0,0,2,0,8),
(0,6,0,2,0,1,0,5,0),
(1,0,2,0,0,0,0,0,0),
(0,7,0,0,0,0,5,2,0),
(9,0,0,0,6,5,0,0,0),
(0,4,0,9,7,0,0,0,0) )
We create a constraint so that the solver only focuses on empty cells, that is, the cells with 0 in them.
# 'If' is the if-then-else expression.
# Keeps the empty cells for the consideration of solver, while fills the non empty cells into the board from the instance.
instance_constraint = []
# Iterate over all cells in the board to check for empty cells.
for i in range(9):
for j in range(9):
instance_constraint.append(z3.If(sudoku[i][j] == 0, True, board[i][j] == sudoku[i][j]))
instance_constraint
We then encode the cell constraint. A cell must contain a number between 1 and 9.
# 'And' represents the logical and function, denoted as '&'.
cell_constraint = []
# Iterate over all cells in the board to check that all numerals are between 1 and 9.
for i in range(9):
for j in range(9):
cell_constraint.append(z3.And(1 <= board[i][j], board[i][j] <= 9))
cell_constraint
We then encode the row constraint. Every row must have a digit appear only once.
# 'Distinct' makes sure that the ith row shall be full of distinct numbers, that is, no number occuring twice.
# Where, i loops through all the rows of the board.
row_constraint = []
for i in range(9):
# Get a row of the board.
row = board[i]
# Add the distinct constraint for this particular row.
row_constraint.append(z3.Distinct(row))
row_constraint
We then encode the column constraint. Each column must have a digit appear only once.
# 'Distinct' makes sure that the jth column of the ith row shall be full of distinct numbers, that is, no number occuring twice.
# Where, i loops through all the rows of the board and j loops through all the columns of the board.
col_constraint = []
for j in range(9):
# Get the column.
column = []
for i in range(9):
# Append all rows for this particular column.
column.append(board[i][j])
# Add the distinct constraint for this particular column.
col_constraint.append(z3.Distinct(column))
col_constraint
We then encode the sub-square constraint. Every sub-square must have a digit appear only once.
# The first loop goes through all rows and columns in a subsquare, and then all subsquares are looped through.
ssq_constraint = []
# Iterate over all subsquares.
for i0 in range(3):
for j0 in range(3):
# Inside a subsquare, get all the cells.
sub_square = []
for i in range(3):
for j in range(3):
sub_square.append(board[3*i0 + i][3*j0 + j])
# Add the distinct constraint for this particular subsquare.
ssq_constraint.append(z3.Distinct(sub_square))
ssq_constraint
Using Z3's solving abilities.
# Initialize a solver instance
s = z3.Solver()
s
Add all the constraints to the solver.
# 'add' method adds the constraints to the solver.
s.add(instance_constraint)
s.add(cell_constraint)
s.add(row_constraint)
s.add(col_constraint)
s.add(ssq_constraint)
# or just pass a cumulative of constraints to the solver.
#s.add(instance_constraint + cell_constraint + row_constraint + col_constraint + ssq_constraint)
s
Check if the scenario is satisfiable (problem with the given constraints and instance).
# 'check' method verifies the SAT nature of the scenario.
s.check()
If it is satisfiable, then we move on to creating a model for it. Model is the solution of a satisfiability problem (aka system of constraints).
# 'model' method instantiates a model for the given scenario.
if s.check() == z3.sat:
m = s.model()
print(m)
else:
m = None
print("Unsatisfiable")
# 'evaluate' method computes and gives the output of the model.
if m != None:
solution = []
for i in range(9):
column = []
for j in range(9):
column.append(m.evaluate(board[i][j]))
solution.append(column)
z3.print_matrix(solution)