Skip to main content
This tutorial shows how to build a complete Sudoku solver using Z3’s constraint solving capabilities. We’ll encode the rules of Sudoku as constraints and let Z3 find solutions.

​
Sudoku Rules

Sudoku is played on a 9x9 grid where:
  1. Each cell contains a number from 1 to 9
  2. Each row must contain all digits 1-9 with no repetition
  3. Each column must contain all digits 1-9 with no repetition
  4. Each 3x3 sub-grid must contain all digits 1-9 with no repetition
Let’s encode these rules as Z3 constraints.

​
Building the Solver

1

Set up the grid

Create a 9x9 grid of integer variables to represent the Sudoku board:
from z3 import *

# Create 9x9 matrix of integer variables
cells = [[Int(f"cell_{row}_{col}") for col in range(9)] for row in range(9)]
Each variable represents one cell in the Sudoku grid. The name cell_row_col helps identify each cell’s position.
2

Create solver and add range constraints

Every cell must contain a digit from 1 to 9:
s = Solver()

# Each cell contains a digit 1-9
for row in range(9):
    for col in range(9):
        s.add(cells[row][col] >= 1)
        s.add(cells[row][col] <= 9)
3

Add row constraints

Each row must contain distinct values (all different):
# Each row contains distinct values
for row in range(9):
    s.add(Distinct(cells[row]))
Distinct() is a powerful Z3 constraint that ensures all its arguments have different values.
4

Add column constraints

Each column must contain distinct values:
# Each column contains distinct values
for col in range(9):
    column = [cells[row][col] for row in range(9)]
    s.add(Distinct(column))
5

Add 3x3 sub-grid constraints

Each 3x3 sub-grid must contain distinct values:
# Each 3x3 sub-grid contains distinct values
for box_row in range(3):
    for box_col in range(3):
        box = []
        for row in range(3):
            for col in range(3):
                box.append(cells[box_row * 3 + row][box_col * 3 + col])
        s.add(Distinct(box))
This iterates over the nine 3x3 boxes and ensures each contains distinct digits.
6

Add initial values (puzzle input)

For a specific puzzle, add constraints for the given cells:
# Example puzzle (0 represents empty cells)
puzzle = [
    [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]
]

# Add constraints for given cells
for row in range(9):
    for col in range(9):
        if puzzle[row][col] != 0:
            s.add(cells[row][col] == puzzle[row][col])
7

Solve and display the result

# Solve the puzzle
if s.check() == sat:
    m = s.model()
    print("Solution found:")
    for row in range(9):
        if row % 3 == 0 and row != 0:
            print("-" * 21)
        for col in range(9):
            if col % 3 == 0 and col != 0:
                print("|", end=" ")
            print(m[cells[row][col]], end=" ")
        print()
else:
    print("No solution exists")

​
Complete Working Example

from z3 import *

def solve_sudoku(puzzle):
    """
    Solve a Sudoku puzzle using Z3.
    
    Args:
        puzzle: 9x9 list where 0 represents empty cells
    
    Returns:
        9x9 list with the solution, or None if unsolvable
    """
    # Create 9x9 matrix of integer variables
    cells = [[Int(f"cell_{row}_{col}") for col in range(9)] for row in range(9)]
    
    s = Solver()
    
    # Each cell contains a digit 1-9
    for row in range(9):
        for col in range(9):
            s.add(cells[row][col] >= 1, cells[row][col] <= 9)
    
    # Each row contains distinct values
    for row in range(9):
        s.add(Distinct(cells[row]))
    
    # Each column contains distinct values
    for col in range(9):
        s.add(Distinct([cells[row][col] for row in range(9)]))
    
    # Each 3x3 sub-grid contains distinct values
    for box_row in range(3):
        for box_col in range(3):
            box = []
            for row in range(3):
                for col in range(3):
                    box.append(cells[box_row * 3 + row][box_col * 3 + col])
            s.add(Distinct(box))
    
    # Add constraints for given cells
    for row in range(9):
        for col in range(9):
            if puzzle[row][col] != 0:
                s.add(cells[row][col] == puzzle[row][col])
    
    # Solve
    if s.check() == sat:
        m = s.model()
        solution = [[m[cells[row][col]].as_long() for col in range(9)] for row in range(9)]
        return solution
    else:
        return None

def print_sudoku(grid):
    """Pretty print a Sudoku grid."""
    for row in range(9):
        if row % 3 == 0 and row != 0:
            print("-" * 21)
        for col in range(9):
            if col % 3 == 0 and col != 0:
                print("|", end=" ")
            print(grid[row][col], end=" ")
        print()

# Example puzzle
puzzle = [
    [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]
]

print("Puzzle:")
print_sudoku(puzzle)
print("\nSolution:")
solution = solve_sudoku(puzzle)
if solution:
    print_sudoku(solution)
else:
    print("No solution found")
Expected output: 
Puzzle:
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

Solution:
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

​
Advanced: Miracle Sudoku

Miracle Sudoku adds special constraints on top of regular Sudoku rules:
  • Any two cells separated by a knight’s move (in chess) cannot contain the same digit
  • Any two cells separated by a king’s move cannot contain the same digit
  • Any two orthogonally adjacent cells cannot contain consecutive digits
Here’s how to add these constraints: 
def add_miracle_constraints(solver, cells):
    """Add miracle sudoku constraints."""
    
    # Knight move offsets
    knight_moves = [(1, 2), (2, 1), (2, -1), (1, -2),
                    (-1, -2), (-2, -1), (-2, 1), (-1, 2)]
    
    # King move offsets (diagonal only, adjacent covered by consecutive rule)
    king_moves = [(1, 1), (1, -1), (-1, 1), (-1, -1)]
    
    # Apply knight and king constraints
    for row in range(9):
        for col in range(9):
            for dr, dc in knight_moves + king_moves:
                new_row, new_col = row + dr, col + dc
                if 0 <= new_row < 9 and 0 <= new_col < 9:
                    solver.add(cells[row][col] != cells[new_row][new_col])
    
    # Orthogonally adjacent cells cannot be consecutive
    ortho_moves = [(0, 1), (0, -1), (1, 0), (-1, 0)]
    for row in range(9):
        for col in range(9):
            for dr, dc in ortho_moves:
                new_row, new_col = row + dr, col + dc
                if 0 <= new_row < 9 and 0 <= new_col < 9:
                    diff = cells[row][col] - cells[new_row][new_col]
                    solver.add(diff != 1, diff != -1)
Miracle Sudoku can be solved with as few as 2 given digits due to the strong constraints.

​
Performance Tips

Int() variables are more efficient than Real() for discrete problems like Sudoku.
Add the most restrictive constraints first. This helps Z3 prune the search space faster.
For harder puzzles, you can use specific solver tactics:
s = Then('simplify', 'solve-eqs', 'smt').solver()

​
Next Steps

Basic Solving

Review fundamental constraint solving concepts

Optimization

Learn how to find optimal solutions, not just feasible ones

Build docs developers (and LLMs) love

Get started for freeTalk to us