Solving Classic Sudoku Problems with Z3 Theorem Prover
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 opensource highperformance 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 81length 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/notebooksblogposts/blob/main/00_z3_sudoku.ipynb