Exponential lower bounds for the running time of DPLL algorithms on satisfiable formulas

DPLL (for Davis, Putnam, Logemann, and Loveland) algorithms form the largest family of contemporary algorithms for SAT (the propositional satis ability problem) and are widely used in applications. The recursion trees of DPLL algorithm executions on unsatis able formulas are equivalent to tree-like resolution proofs. Therefore, lower bounds for tree-like resolution (which are known since 1960s) apply to them