Z3 Solver

class sudoku_smt_solvers.solvers.z3_solver.Z3Solver(sudoku)

Z3-based SMT solver for Sudoku puzzles.

Uses integer variables and distinct constraints to encode Sudoku rules. Tracks constraint propagation for performance analysis.

Attributes:

sudoku (List[List[int]]): Input puzzle as 25x25 grid size (int): Grid size (25) solver (z3.Solver): Z3 solver instance variables (List[List[z3.Int]]): SMT variables for grid propagated_clauses (int): Counter for constraint additions

Example:

>>> puzzle = [[0 for _ in range(25)] for _ in range(25)]
>>> solver = Z3Solver(puzzle)
>>> solution = solver.solve()

solve()

Solve Sudoku using Z3 SMT solver.

Returns:

Solved 25x25 grid if satisfiable, None if unsatisfiable

Note:

Validates solution before returning to ensure correctness