Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Paper:

TR04-041 | 18th May 2004 00:00

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

RSS-Feed




TR04-041
Authors: Michael Alekhnovich, Edward Hirsch, Dmitry Itsykson
Publication: 19th May 2004 08:34
Downloads: 3563
Keywords: 


Abstract:

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 tree-like resolution proofs. Therefore, lower bounds for tree-like resolution (which are known since 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 would be equivalent to proving P\neq NP. In this paper, we give exponential lower bounds for two families of DPLL algorithms: generalized myopic algorithms (that read upto n^{1-\epsilon} of clauses at each step and see the remaining part of the formula without negations) and drunk algorithms (that choose a variable using any complicated rule and then pick its value at random).



ISSN 1433-8092 | Imprint