 The Davis-Putnam-Logemann-Loveland (DPLL) algorithm was one of the first SAT search algorithms (Davis &amp; Putnam 1960; Davis, Logemman &amp; Loveland 1962) and is still considered one of the best complete SAT solvers; many of the complete SAT procedures in existence today can be considered optimizations and generalizations of DPLL. In essence, DPLL search procedures proceed by considering ways in which assignments can be chosen to make the original formula true. For example, consider the formula in CNF