npycomp.solvers.

DPLL

class npycomp.solvers.DPLL(clauses: list[tuple[str]])

Davis-Putnam-Logemann-Loveland (DPLL) solver for SAT.

Implementation of The Davis–Putnam–Logemann–Loveland (DPLL) recursive backtracking procedure for solving the SAT problem. The algorithm runs by choosing a literal, assigning a truth value to it, simplifying the formula and then recursively checking if the simplified formula is satisfiable; if this is the case, the original formula is satisfiable; otherwise, the same recursive check is done assuming the opposite truth value.

The DPLL algorithm improves over naive backtracking by applying unit propagation and pure literal elimination to simplify the formula at each step. These techniques reduce the total search space and improve the efficiency of the algorithm.

Unit propagation. If a clause contains only one unassigned literal, the literal can be assigned to true, and all clauses containing the literal can be removed.

Pure literal elimination. If a literal is pure if it appears with only one polarity in the formula. Pure literals can always be assigned in a way that makes the clauses containing them true.

Parameters:

clauseslist[tuple[str]]

A list of clauses in conjunctive normal form (CNF).

Attributes:

formula

Methods

model_to_string(model)	Convert a model to a human-readible string.
solve()	Solve a SAT problem.