| Abstract: | 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. Bibliography: 11 titles.Translated from Zapiski Nauchnykh Seminarov POMI, Vol. 293, 2002, pp. 139–148.This revised version was published online in April 2005 with a corrected cover date and article title. |
