Davis–Putnam–Logemann–Loveland algorithm

DPLL

Class	Boolean satisfiability problem
Worst-case performance	${\displaystyle O(2^{n})}$
Worst-case space complexity	${\displaystyle O(n)}$ (basic algorithm)

In 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 1962 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 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.

After more than 50 years the DPLL procedure still forms the basis for most efficient complete SAT solvers. It has recently been extended for automated theorem proving for fragments of first-order logic.

The SAT problem is important both from theoretical and practical points of view. In complexity theory it was the first problem proved to be NP-complete, and can appear in a broad variety of applications such as model checking, automated planning and scheduling, and diagnosis in artificial intelligence.

...
Wikipedia