## 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.add(4 * x == 20)
s.add(x * y == 40)
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)
s.add(sudoku_c + instance_c) # (2)
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]]
```

## Your Coding Interview

I hope that this little tutorial helped you prepare for your Coding Interview in Python. I will add more algorithm examples like this in the future. Stay tuned and check my blog for updates or subscribe to my newsletter! You can also follow me on Twitter.