# Coding Interview – Solve Sudokus Using Python and Z3

## What is a Sudoku?

A Sudoku is a Japanese number placing puzzle. It’s a grid of 9x9 fields, and the objective is to fill each cell of this field with a number between 1 and 9.

To fill the missing fields, there are a few rules to follow:

• Each cell must contain a digit (1 to 9)
• Every digit has to be placed exactly once in each row
• Every digit has to be placed exactly once in each column
• Every digit has to be placed exactly once in each 3x3 subgrid

Here is an example of a Sudoku - the red digits denote the solution:

## What is a SAT-Solver?

A SAT-solver is a software that takes in a definition of mathematical rules along with some variables. Its goal is to find a solution that satisfies all of these rules.

A simple way to think about the class of problems a SAT-solver can solve is a System of Linear Equations.

Let’s say that `x` denotes the price of some item. We know that a pack of four items costs \$20. Our first equation is then given by:

`4 * x == 20`

Now, let’s say that we have \$40 in our pockets. How many items (`y`) can we buy at a price of \$`x`? Our second equation is therefore given by:

`x * y == 40`

Obviously the solution to these equations is given by `x = 5` and `y = 8`.

There are several ways to solve such a system in a computer programme. However, we focus on using the `z3-solver` package to find a solution.

``````from z3 import *

x = Int("price")
y = Int("qty")

s = Solver()
s.check()
print(s.model())``````

## Using `z3` to solve a Sudoku

The only thing we have to do now is to express the Sudoku rules as conditions for `z3`.

First we create an Integer Variable for each cell of the Sudoku grid.

``````X = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(9) ]
for i in range(9) ]``````

Each cell must contain a digit (1 to 9)

``````cells_c  = [ And(1 <= X[i][j], X[i][j] <= 9)
for i in range(9) for j in range(9) ]``````

Every digit has to be placed exactly once in each row

``rows_c   = [ Distinct(X[i]) for i in range(9) ]``

Every digit has to be placed exactly once in each column

``````cols_c   = [ Distinct([ X[i][j] for i in range(9) ])
for j in range(9) ]``````

Every digit has to be placed exactly once in each 3x3 subgrid

``````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) ]``````

Now that we have each condition as code, we can chain these conditions:

``sudoku_c = cells_c + rows_c + cols_c + sq_c``

By now, we have described the Sudoku with Z3. Now, we have to put the actual values into the system.

The example Sudoku from the image above could be written as:

``````instance = ((5,3,0,0,7,0,0,0,0),
(6,0,0,1,9,5,0,0,0),
(0,9,8,0,0,0,0,6,0),
(8,0,0,0,6,0,0,0,3),
(4,0,0,8,0,3,0,0,1),
(7,0,0,0,2,0,0,0,6),
(0,6,0,0,0,0,2,8,0),
(0,0,0,4,1,9,0,0,5),
(0,0,0,0,8,0,0,7,9))``````

Note that we use the number `0` to indicate blank fields. We need to convert this input to the variables managed by `z3`:

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

The last step is just creating a `Solver` object and let `z3` do the magic to find a solution which satisfies all our rules:

``````s = Solver()                                            # (1)
if s.check() == sat:                                    # (3)
m = s.model()                                       # (4)
r = [ [ m.evaluate(X[i][j]) for j in range(9) ]     # (5)
for i in range(9) ]
print_matrix(r)                                     # (6)
else:
print("failed to solve")                            # (7)``````
• `(1)`: Create the `Solver` object
• `(2)`: Adding our ruleset and our pre-filled grid to the solver
• `(3)`: let `z3` check if there is at least one solution `sat`isfying all the rules
• `(4)`: the `model()` method now assigns a value to each variable we defined
• `(5)`: with the `evaluate()` method, we now just extract each variable’s value to build a 9x9 matrix
• `(6)`: print the matrix
• `(7)`: If we had provided an unsolvable Sudoku, we would get an error message here

And that’s it. Our final result looks like that:

``````[[5, 3, 4, 6, 7, 8, 9, 1, 2],
[6, 7, 2, 1, 9, 5, 3, 4, 8],
[1, 9, 8, 3, 4, 2, 5, 6, 7],
[8, 5, 9, 7, 6, 1, 4, 2, 3],
[4, 2, 6, 8, 5, 3, 7, 9, 1],
[7, 1, 3, 9, 2, 4, 8, 5, 6],
[9, 6, 1, 5, 3, 7, 2, 8, 4],
[2, 8, 7, 4, 1, 9, 6, 3, 5],
[3, 4, 5, 2, 8, 6, 1, 7, 9]]``````