DPLL(T) Solver

class sudoku_smt_solvers.solvers.dpllt_solver.DPLLTSolver(sudoku: List[List[int]])

DPLL(T) solver combining SAT solving with theory propagation.

Extends basic DPLL SAT solving with theory propagation for Sudoku rules, enabling more efficient pruning of the search space.

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 theory_state (dict): Dynamic tracking of theory constraints decision_level (int): Current depth in decision tree propagated_clauses (int): Counter for clause additions

Example:

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

extract_solution(model: List[int]) → List[List[int]]

Convert SAT model to Sudoku grid.

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

Solve Sudoku using DPLL(T) algorithm.

Returns:

Solved 25x25 grid if satisfiable, None if unsatisfiable

Raises:

SudokuError: If solver produces invalid solution

Note:

Combines SAT solving with theory propagation in DPLL(T) style