|Type of publication:||Inproceedings|
|Title||Exponential Lower Bounds for DPLL Algorithms on Satisfiable Random 3-CNF Formulas|
|Bibtex cite ID||RACTI-RU1-2012-19|
|Series ||Theory and Applications of Satisfiability Testing – SAT 2012|
|Year published ||2012|
|Organization ||15th International Conference, Trento, Italy, June 17-20, 2012.|
We consider the performance of a number of DPLL algorithms on random 3-CNF formulas with n variables and m = rn clauses. A long series of papers analyzing so-called “myopic” DPLL algorithms has provided a sequence of lower bounds for their satisfiability threshold. Indeed, for each myopic algorithm A it is known that there exists an algorithm-specific clause-density, rA , such that if r 2.78 and the same is true for generalized unit clause for all r > 3.1. Our results imply exponential lower bounds for many other myopic algorithms for densities similarly close to the corresponding rA .