TY - GEN
T1 - Exponential lower bounds for DPLL algorithms on satisfiable random 3-CNF formulas
AU - Achlioptas, Dimitris
AU - Menchaca-Mendez, Ricardo
PY - 2012
Y1 - 2012
N2 - 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, r A, such that if r < rA, the algorithm finds a satisfying assignment in linear time. For example, rA equals 8/3 = 2.66.. for orderred-dll and 3.003... for generalized unit clause. We prove that for densities well within the provably satisfiable regime, every backtracking extension of either of these algorithms takes exponential time. Specifically, all extensions of orderred-dll take exponential time for 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.
AB - 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, r A, such that if r < rA, the algorithm finds a satisfying assignment in linear time. For example, rA equals 8/3 = 2.66.. for orderred-dll and 3.003... for generalized unit clause. We prove that for densities well within the provably satisfiable regime, every backtracking extension of either of these algorithms takes exponential time. Specifically, all extensions of orderred-dll take exponential time for 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.
UR - http://www.scopus.com/inward/record.url?scp=84864219705&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-31612-8_25
DO - 10.1007/978-3-642-31612-8_25
M3 - Contribución a la conferencia
SN - 9783642316111
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 327
EP - 340
BT - Theory and Applications of Satisfiability Testing, SAT 2012 - 15th International Conference, Proceedings
T2 - 15th International Conference on Theory and Applications of Satisfiability Testing, SAT 2012
Y2 - 17 June 2012 through 20 June 2012
ER -