CVC5 Solver

class sudoku_smt_solvers.solvers.cvc5_solver.CVC5Solver(sudoku)

CVC5-based Sudoku solver using SMT encoding.

Solves 25x25 Sudoku puzzles by encoding the problem as an SMT formula and using CVC5 to find a satisfying assignment.

Attributes:

sudoku (List[List[int]]): Input puzzle as 25x25 grid size (int): Grid size (always 25) solver (Solver): CVC5 solver instance variables (List[List[Term]]): SMT variables for each cell propagated_clauses (int): Counter for clause assertions

Example:

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

solve()

Solve the Sudoku puzzle using CVC5.

Returns:

Solved 25x25 grid if satisfiable, None if unsatisfiable

Raises:

Exception: If solver encounters an error

Note:

Always cleans up solver resources, even on failure