Solving Classic Sudoku Problems with Z3 Theorem Prover

Sep 17, 2023

Sudoku is simple yet attractive game. It is played on a 9x9 grid (variants available), divided into nine 3x3 subgrids. The goal is to fill in the empty cells with digits from 1 to 9, in such a way that each digit appears once in every row, every column, and every subgrid.

Z3 is an open-source high-performance theorem prover (satisfiability modulo theories - SAT solver) developed by Microsoft Research. It provides a powerful and efficient tool for solving complex logical formulas and equations.

Procedure is simple:

Create a Z3 Solver:
```
solver = Solver()
```

Generate variables for each cell:

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

Generate digit constraints:

for i in range(9):
    for j in range(9):
        solver.add(And(1 <= X[i][j], X[i][j] <= 9))

Generate row constraints:

for i in range(9):
    solver.add(Distinct(X[i]))

Generate column constrains:

for i in range(9):
    solver.add(Distinct([X[j][i] for j in range(9)]))

Generate subsquare constraints:
```
for i in range(3):
    for j in range(3):
        solver.add(Distinct([X[i*3+k][j*3+l] for k in range(3) for l in range(3)]))
```
I create a couple helper functions for reading a 81-length string as a sudoku problem and display them pretty in console. You can see them in full code.

Now we can solve some classic sudoku problems with Z3:

Problem:
. . . | . . 6 | . . .
. 5 9 | . . . | . . 8
2 . . | . . 8 | . . .
- - - + - - - + - - -
. 4 5 | . . . | . . .
. . 3 | . . . | . . .
. . 6 | . . 3 | . 5 4
- - - + - - - + - - -
. . . | 3 2 5 | . . 6
. . . | . . . | . . .
. . . | . . . | . . .

Solution:
4 3 8 | 2 5 6 | 9 7 1
6 5 9 | 7 1 4 | 2 3 8
2 1 7 | 9 3 8 | 4 6 5
- - - + - - - + - - -
1 4 5 | 6 9 2 | 7 8 3
8 7 3 | 5 4 1 | 6 2 9
9 2 6 | 8 7 3 | 1 5 4
- - - + - - - + - - -
7 9 4 | 3 2 5 | 8 1 6
3 8 2 | 1 6 9 | 5 4 7
5 6 1 | 4 8 7 | 3 9 2

Full code is available at: https://github.com/mrtkp9993/notebooks-blog-posts/blob/main/00_z3_sudoku.ipynb