DPLL
DPLL, named after Davis, Putnam, Logemann, and Loveland, is a complete backtracking algorithm for determining the satisfiability of propositional logic formulas in conjunctive normal form (CNF). It was developed as an improvement of the earlier Davis–Putnam procedure and remains a foundational method in the study of SAT.
The algorithm operates on a CNF formula by performing a depth-first search over truth assignments. Its two
DPLL typically uses a decision rule to choose an unassigned variable and to try a truth value,
DPLL is a complete procedure: it will determine satisfiability for any CNF formula, though its worst-case running