The basic idea of the Davis-Putnam-Logemann-Loveland (DPLL) procedure (Davis et al., 1962, Davis and Putnam, 1960) for testing satisfiability of CNF formulas is to branch on variables, setting them to TRUE or FALSE, until either an initial clause is violated (i.e. has all literals set to FALSE) or no more clauses remain in the simplified residual formula. In the former case, we backtrack to the last branching decision whose other branch has not been tried yet, reverse the decision, and proceed recursively. In the latter, we terminate with a satisfying assignment. If all possible branches have been unsuccessfully tried, the formula is declared unsatisfiable. To increase efficiency, unit clauses (those with only one unset literal) are immediately set to true. Pure literals (those whose negation does not appear) are also set to TRUE as a preprocessing step and, in some implementations, in the simplification process after every branch.
In this paper, we will use the term DPLL to denote the basic branching and backtracking procedure described above. It will not include learning conflict clauses when backtracking, but will allow intelligent branching heuristics as well as common extensions such as fast backtracking and restarts. Note that this is in contrast with the occasional use of the term DPLL to encompass practically all branching and backtracking approaches to SAT, including those involving learning.