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.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 satisfying 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.