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.

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.

As such, writing efficient SAT solvers has been a research topic for many years.

[4] Another application that often involves DPLL is automated theorem proving or satisfiability modulo theories (SMT), which is a SAT problem in which propositional variables are replaced with formulas of another mathematical theory.

The DPLL algorithm enhances over the backtracking algorithm by the eager use of the following rules at each step: Unsatisfiability of a given partial assignment is detected if one clause becomes empty, i.e. if all its variables have been assigned in a way that makes the corresponding literals false.

The pseudocode DPLL function only returns whether the final assignment satisfies the formula or not.

[citation needed] In 1989-1990, Stålmarck's method for formula verification was presented and patented.

[7] Runs of DPLL-based algorithms on unsatisfiable instances correspond to tree resolution refutation proofs.