DPLL Solver

class sudoku_smt_solvers.solvers.dpll_solver.DPLLSolver(sudoku: List[List[int]])

DPLL-based Sudoku solver using SAT encoding.

Solves 25x25 Sudoku puzzles by converting them to CNF (Conjunctive Normal Form) and using DPLL to find a satisfying assignment.

Attributes:

sudoku (List[List[int]]): Input puzzle as 25x25 grid size (int): Grid size (25) cnf (CNF): PySAT CNF formula object solver (Solver): PySAT Glucose3 solver instance propagated_clauses (int): Counter for clause additions

Example:

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

solve() → List[List[int]] | None

Solve Sudoku puzzle using DPLL SAT solver.

Returns:

Solved 25x25 grid if satisfiable, None if unsatisfiable

Raises:

SudokuError: If solver produces invalid solution Exception: For other solver errors

Note:

Uses Glucose3 SAT solver from PySAT