TY - JOUR

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

AU - Alekhnovich, Michael

AU - Hirsch, Edward A.

AU - Itsykson, Dmitry

PY - 2005/10/1

Y1 - 2005/10/1

N2 - DPLL (for Davis, Putnam, Logemann, and Loveland) algorithms form the largest family of contemporary algorithms for SAT (the propositional satisfiability problem) and are widely used in applications. The recursion trees of DPLL algorithm executions on unsatisfiable formulas are equivalent to treelike resolution proofs. Therefore, lower bounds for treelike resolution (known since the 1960s) apply to them. However, these lower bounds say nothing about the behavior of such algorithms on satisfiable formulas. Proving exponential lower bounds for them in the most general setting is impossible without proving P ≠ NP; therefore, to prove lower bounds, one has to restrict the power of branching heuristics. In this paper, we give exponential lower bounds for two families of DPLL algorithms: generalized myopic algorithms, which read up to n 1-ε of clauses at each step and see the remaining part of the formula without negations, and drunk algorithms, which choose a variable using any complicated rule and then pick its value at random.

AB - DPLL (for Davis, Putnam, Logemann, and Loveland) algorithms form the largest family of contemporary algorithms for SAT (the propositional satisfiability problem) and are widely used in applications. The recursion trees of DPLL algorithm executions on unsatisfiable formulas are equivalent to treelike resolution proofs. Therefore, lower bounds for treelike resolution (known since the 1960s) apply to them. However, these lower bounds say nothing about the behavior of such algorithms on satisfiable formulas. Proving exponential lower bounds for them in the most general setting is impossible without proving P ≠ NP; therefore, to prove lower bounds, one has to restrict the power of branching heuristics. In this paper, we give exponential lower bounds for two families of DPLL algorithms: generalized myopic algorithms, which read up to n 1-ε of clauses at each step and see the remaining part of the formula without negations, and drunk algorithms, which choose a variable using any complicated rule and then pick its value at random.

KW - DPLL algorithms

KW - Satisfiability

UR - http://www.scopus.com/inward/record.url?scp=33750301291&partnerID=8YFLogxK

U2 - 10.1007/s10817-005-9006-x

DO - 10.1007/s10817-005-9006-x

M3 - Article

AN - SCOPUS:33750301291

VL - 35

SP - 51

EP - 72

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

SN - 0168-7433

IS - 1-3

ER -