DPLL algorithm

DPLL

After 5 fruitless attempts (red), choosing the variable assignment a=1, b=1 leads, after unit propagation (bottom), to success (green): the top left CNF formula is satisfiable.
Class	Boolean satisfiability problem
Data structure	Binary tree
Worst-case performance	${\displaystyle O(2^{n})}$
Best-case performance	${\displaystyle O(1)}$ (constant)
Worst-case space complexity	${\displaystyle O(n)}$ (basic algorithm)

In logic and computer science, 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, i.e. for solving the CNF-SAT problem.

It was introduced in 1961 by Martin Davis, George Logemann and Donald W. Loveland and is a refinement of the earlier Davis–Putnam algorithm, which is a resolution-based procedure developed by Davis and Hilary Putnam in 1960. Especially in older publications, the Davis–Logemann–Loveland algorithm is often referred to as the "Davis–Putnam method" or the "DP algorithm". Other common names that maintain the distinction are DLL and DPLL.