Hard satisfiable formulas for DPLL-type algorithms
Sergey Nikolenko · arXiv (Cornell University) · 2003
We address lower bounds on the time complexity of algorithms solving the propositional satisfiability problem. Namely, we consider two DPLL-type algorithms, enhanced with the unit clause and pure literal heuristics. Exponential lower bounds for solving satisfiability on provably satisfiable formulas are proven.