DPLL Satisfiability Search
Follow unit implications and backtracking decisions to find a satisfying assignment or prove that none exists.
Free theory articleFollow unit implications and backtracking decisions to find a satisfying assignment or prove that none exists.
Concept & interpretation
The Davis-Putnam-Logemann-Loveland (DPLL) algorithm is a complete, backtracking-based search algorithm for deciding the satisfiability of propositional logic formulae in Conjunctive Normal Form (CNF).
Experiment with the native controls
Open the interactive DPLL Satisfiability Search module.
- Examine the default Formula which contains clauses separated by semicolons.
- Click Step to reveal one recursive call after source-order unit propagation. Observe how DPLL selects the first unassigned variable and branches on it (trying
truefirst). - Notice when a branch leads to a conflict (a clause evaluates to false), the algorithm backtracks to try the alternative assignment (
false). - If a unit clause is formed, observe how unit propagation immediately forces the assignment of the remaining literal without branching.
- Click Finish to immediately find the terminal SAT/UNSAT state and the witness assignment.