Forget Manual Solving, Let Z3 Crack The Code

A Formal Approach for Solving Logic Puzzles with an SMT Solver

You know the feeling. That moment when a Sudoku grid snaps into place, the hidden shapes of a Nonogram finally emerge from the pixels, or a perfectly balanced Kakuro sum falls into line. It’s the thrill of logic, the satisfaction of a challenge overcome by sheer brainpower.

But have you ever noticed just how similar these seemingly different puzzles are? At their core, they all boil down to the exact same thing: a set of constrains that must be satisfied. What if I told you there’s a powerful, elegant way to encode those rules, not just for one puzzle, but for all of them, and instantly reveal the answer? Welcome to the formal approach to puzzle-solving.

For the rest of this post, I’ll be assuming you’re familiar with the standard rules of*Sudoku* , Kakuro , and Nonograms. If you need a quick refresher on any of them, please take a moment now to look them up before we proceed.

Introducing the SMT Solver

You are right to see the similarity. The elegant solution to these diverse problems lies in Constraint Satisfaction. This is where we introduce the star of the show: an SMT Solver , specifically Z3 from Microsoft Research. SMT stands for Satisfiability Modulo Theories. Don’t let the name scare you. Think of it as a highly specialized logic engine that takes all your puzzle’s rules, your “constraints”, and determines if a configuration exists that makes every single rule true simultaneously. If it does, Z3 finds that configuration for you: the solution.

If no configuration exists that satisfies all the rules, Z3 returns a result of “unsatisfiable.” This happens when your puzzle is logically flawed, perhaps because it was designed poorly or because the starting clues are contradictory. For instance, if you provide a Sudoku with two of the same number in a single row as a starting point, Z3 will quickly determine that the puzzle is impossible, which is often a useful insight in itself.

Another example for Unsatisfiable Sudoku, can you see why?

Not Sat Solver

Now, you may have heard of a simpler SAT Solver , which only deals with pure Boolean logic, meaning statements that are strictly true or false. It’s worth a quick aside: in theoretical computer science, SAT is an NP-complete problem , meaning it’s generally considered one of the hardest problems to solve efficiently. However, in the real world, modern SAT solvers use clever heuristics and techniques that make them incredibly fast and capable of solving most practical instances.

An SMT Solver , however, is much more powerful. It extends SAT by adding support for common mathematical concepts, or “Theories ,” like integers, real numbers, and arithmetic. This is critical for puzzles like Kakuro , which rely heavily on summing numbers, or even Sudoku , which uses integer constraints. Z3 allows us to easily model all those numeric, non-Boolean puzzle requirements, giving us a universal key to cracking these challenges.

The concept of using computers to solve logic puzzles is certainly not new, specialized Sudoku and Nonogram solvers have been around for years. However, the true elegance of the formal approach lies in its generality. Instead of building a new, dedicated solver for every puzzle type, we can use one strong and general tool like Z3 to tackle a huge range of problems with surprisingly little, highly adaptable code. That versatility is the real game-changer, and we’ll see exactly how it works soon.

Introducing Z3

Before we dive into the code, let’s formally introduce the tool. Z3 is one of the world’s most powerful and widely used SMT solvers , developed by Microsoft Research and open-sourced under the MIT License. Initially built for complex problems in software verification , Z3 handles logical formulas and mathematical constraints with exceptional speed. While its core engine is C++, it provides robust bindings for languages like C, C++, Java, .NET, and Python. For this post, however, we will exclusively use the user-friendly Python binding , as it allows us to quickly and elegantly model our puzzles without unnecessary overhead.

Z3 101: The Essentials

First, you’ll need the Python bindings:

pip install z3-solver

Now, let’s look at the four core components you need to translate any problem into Z3 code.

1. Variables: Defining the Unknowns

In Z3, everything starts with variables that represent the unknown values you’re trying to find. Because Z3 supports various logical Theories , these variables aren’t just true/false statements, they can represent numbers, arrays, and more.

• Int(’name’): Creates an Integer variable (e.g., for numbers 1-9).

• Bool(’name’): Creates a Boolean variable (True/False).

• Ints(’a b c’): A shorthand for creating multiple integer variables.

Example:

from z3 import *
x = Int(’x’) 
is_true = Bool(’flag’)

2. Constraints: Writing the Rules

Constraints are the logical formulas that must be true for the system to have a solution. You build these using familiar comparison operators (<, ==, >) and Z3’s specialized logic functions.

• And(c1, c2, ...): Requires all contained constraints to be true.

• Or(c1, c2, ...): Requires at least one contained constraint to be true.

• Distinct(a, b, c): Forces all listed variables to have different values.

• x + y == 10: Represents standard arithmetic constraints.

Example:

We can use the simple solve() function to find values for variables that meet a system of constraints:

from z3 import *
x, y = Ints(’x y’)
solve(x > 2, y < 10, x + 2*y == 7)
# Output: [y = 0, x = 7]

3. The Solver: The Engine

The Solver object is the central component where you accumulate your constraints and ask Z3 to find a solution.

• s = Solver(): Initializes the solver.

• s.add(constraint): Asserts constraints into the solver’s stack.

• s.check(): Executes the search. Returns sat (solvable), unsat (unsolvable), or unknown.

TheunsatResult: If s.check() returns unsat, it means your problem is logically flawed—no set of assignments can satisfy all the rules simultaneously.

4. The Model: The Answer

If s.check() returns sat (satisfiable), the solver has successfully found a solution. This assignment of values is called the Model.

• m = s.model(): Retrieves the solution object.

• m[variable]: Extracts the solved value for a specific variable from the model.

  from z3 import *
  x = Int(’x’)
  s = Solver()
  s.add(x * 2 == 14)

  if s.check() == sat:
  m = s.model()
  # The output will be ‘7’
  print(m[x])

For deeper guidance and advanced topics, I suggest reading the Official Tutorial — it’s a great resource for getting a deeper understanding of Z3’s more advanced features.

By understanding these four building blocks, you have everything required to translate the rules of our logic puzzles into Z3’s logical language. Our goal is to create a single, general function for each puzzle that captures its fundamental rules. Once those core constraints are in the solver, plugging in a specific puzzle instance is trivial. We’ll start with the most familiar puzzle.

Sudoku: The Constraint Classic

A standard 9x9 Sudoku has four universal constraints: every cell must contain a value from 1 to 9, and every row, column, and 3x3 block must contain distinct values. We can translate these rules directly into Z3.

The General Solver Function

We’ll define a function, solve_sudoku, that takes a sudoku object (which holds the puzzle’s structure and clues) as its input.

from z3 import *

def solve_sudoku(sudoku: SudokoPuzzle) -> dict[str, str]:
  “”“Solves the given Sudoku puzzle using Z3’s SMT capabilities.”“”

  solver = Solver()

  # 9x9 grid of Z3 Integer variables
  # Assuming ‘sudoku.positions’ is a list of all 81 cell names (’A1’, ‘A2’, ... ‘I9’)
  symbols = {pos: Int(pos) for pos in sudoku.positions}

1. General Constraints (The Rules)

Next, we add the three core uniqueness constraints using Z3’s powerful Distinct function.

# Constraint 1: Cell Range [1, 9]
  for symbol in symbols.values():
    solver.add(And(symbol >= 1, symbol <= 9))

# Constraint 2: Rows must have distinct values
for row in “ABCDEFGHI”:
  row_symbols = [symbols[row + col] for col in “123456789”]
  solver.add(Distinct(row_symbols))

# Constraint 3: Columns must have distinct values
for col in “123456789”:
  col_symbols = [symbols[row + col] for row in “ABCDEFGHI”]
  solver.add(Distinct(col_symbols))

# Constraint 4: 3x3 Blocks must have distinct values
for i in range(3):
  for j in range(3):
    # List comprehension to select cells in the 3x3 block
    block_symbols = [symbols[”ABCDEFGHI”[m + i * 3] + “123456789”[n + j * 3]] 
                     for m in range(3) for n in range(3)]
    solver.add(Distinct(block_symbols))

2. Instance Constraints (The Clues)

With the general rules loaded, we now add the specific clues from the puzzle instance passed in the sudoku parameter.

# Assuming ‘sudoku.grid’ is a dictionary like {’A1’: ‘5’, ‘A2’: ‘0’, ...}
for pos, value in sudoku.grid.items():
  if value != “0”: 
    solver.add(symbols[pos] == int(value)) 

3. Solving and Interpreting the Model

The final step is to ask the solver to find a solution and extract the model.

if solver.check() != sat:
  raise Exception(”Unsolvable Sudoku provided!”)

  # Retrieve the model (the solution)
  model = solver.model()

  # Extract the final integer value for every cell
  values = {pos: model.evaluate(symbol).as_string() for pos, symbol in symbols.items()}

  # The function returns the solved values
  return values

The resulting code is essentially a direct translation of the Sudoku rules into Z3 constraints. The puzzle-agnostic power of the SMT solver is clear: we didn’t write an algorithm to search for the solution, we simply wrote the code to describe the solution.

Now, let’s look at Kakuro , where we’ll leverage Z3’s powerful Arithmetic Theory.

An Example for Sudoku Puzzle

Kakuro: The Arithmetic Challenge

Unlike Sudoku, Kakuro (or Cross Sums) requires both uniqueness (no repeated digits in a run) and arithmetic (the cells in a run must sum to a target). This is where the power of the Arithmetic Theory within the SMT solver becomes essential.

The General Solver Function

We define the solve_kakuro function to accept the KakuroPuzzle object. This solver leverages Z3’s Sum and Distinct functions together to enforce the puzzle rules.

To manage the runs, we utilize a simple helper function, get_sum_run, which identifies the sequence of cells for any given clue.

from z3 import Solver, Int, Sum, Distinct, sat, And, Not, Ints

# Helper function to identify the sequence of cells for a clue
def get_sum_run(
    puzzle: KakuroPuzzle, first_x: int, first_y: int, direction: str
) -> list[Cell]:
    “”“Get cells involved in a sum run starting from a clue cell”“”
    rows, cols = puzzle.size
    cells = []

    if direction == “right”:
        for x in range(first_x + 1, cols):
            if puzzle.is_wall(x, first_y): break
            cells.append((x, first_y))
    else:
        for y in range(first_y + 1, rows):
            if puzzle.is_wall(first_x, y): break
            cells.append((first_x, y))
    return cells

def solve_kakuro(puzzle: KakuroPuzzle) -> Solution | None:
    rows, cols = puzzle.size
    solver = Solver()

    # Create grid of Z3 Integer variables
    grid = [[Int(f”cell_{col}_{row}”) for row in range(rows)] for col in range(cols)]

1. General Constraints (The Rules and Clues)

These constraints establish the size and valid range for every cell in the grid, including 0 for the clue/wall cells.

# Constraint 1: Cell Range [1, 9] for fillable cells
for row in range(rows):
    for col in range(cols):
        if puzzle.get_clue(col, row):
            # Clue cells (walls) are assigned a constant 0
            solver.add(grid[col][row] == 0)
        else:
            # Fillable cells must be between 1 and 9
            solver.add(And(grid[col][row] >= 1, grid[col][row] <= 9))

2. Instance Constraints (Sums and Uniqueness)

For every sum clue provided, we apply two simultaneous constraints to the run of cells that follows: the numbers must sum correctly, and all numbers must be unique.

# Add sum and uniqueness constraints for every clue
for clue in puzzle.clues:
    x, y, row_sum, col_sum = clue.x, clue.y, clue.row_sum, clue.col_sum

    # Horizontal Run
    if row_sum is not None:
        if right_cells := get_sum_run(puzzle, x, y, “right”):
            cell_vars = [grid[col][row] for col, row in right_cells]

            # Sum Constraint & Uniqueness Constraint
            solver.add(Sum(cell_vars) == row_sum)
            solver.add(Distinct(cell_vars))

    # Vertical Run
    if col_sum is not None:
        if down_cells := get_sum_run(puzzle, x, y, “down”):
            cell_vars = [grid[col][row] for col, row in down_cells]

            # Sum Constraint & Uniqueness Constraint
            solver.add(Sum(cell_vars) == col_sum)
            solver.add(Distinct(cell_vars))

3. Solving and Interpreting the Model

The final step is to retrieve the solution, filtering out the zeros corresponding to the clue/wall cells.

if solver.check() == sat:
        model = solver.model()
        solution_cells = []

        # Iterate over the grid to extract the non-zero (fillable) values
        for col in range(cols):
            for row in range(rows):
                if value := model.evaluate(grid[col][row]).as_long():
                    if value > 0:
                        solution_cells.append(SolutionCell(col, row, value))

        return solution_cells
    return None

The difference between the Sudoku and Kakuro solutions is minimal in terms of code complexity — the SMT solver handles the massive increase in logical complexity (arithmetic) seamlessly.

If you want to see the complete solutions, with visualizer and scrapper too, check out my github repository for the problem.

An Example For Kakuro Puzzle

Nonogram: Modeling Challenge

The journey from Sudoku (simple uniqueness) to Kakuro (uniqueness plus arithmetic) shows how Z3’s SMT capabilities handle increasing logical complexity with minimal code changes. However, Nonograms (or Picross) present a slightly different, more abstract modeling challenge.

Nonograms swap the Integer Theory for a complex sequence problem. The constraints aren’t simple sums or distinct values; they are rules governing the arrangement of blocks (True/False cells) in a line, separated by at least one space, to match the clue numbers.

This problem is solvable using the exact same Z3 tools you’ve already learned — Boolean variables, logic operators, and creative constraint formulation — but correctly defining the sequence logic is considerably harder.

Your Challenge: I spent several hours finding an elegant way to model the sequence constraints for Nonograms using the Z3 API. Now that you have the knowledge of Variables , Constraints , Solvers , and Models , I’m leaving the Nonogram solver as a challenge to you. If you solve it, I would love to see and discuss your solution in the comments! 💡

Thank you for joining me on this formal journey into puzzle-solving. I hope this post inspires you to look at your daily newspaper puzzles not just as a pastime, but as a fascinating challenge in Constraint Satisfaction.

---

Originally published on AI Superhero