Coding Interview – Solve Sudokus Using Python and Z3
Tags: python, career, algorithms, tutorial
Published: 2022-03-01 13:52:54


## What is a Sudoku?

A [Sudoku](https://en.wikipedia.org/wiki/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:


![Image description](https://dev-to-uploads.s3.amazonaws.com/uploads/articles/869kx9tl0kysvuauvhw8.png)

## What is a SAT-Solver?

A [SAT-solver](https://en.wikipedia.org/wiki/Boolean_satisfiability_problem) 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.

```python
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.
```python
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)
```python
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
```python
rows_c   = [ Distinct(X[i]) for i in range(9) ]
```

> Every digit has to be placed exactly once in each column
```python
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
```python
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:

```python
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:

```python
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`:


```python
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:

```python
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](https://bas.surf/codinginterview) or subscribe to my newsletter! You can also [follow me on Twitter](https://twitter.com/bascodes).