The Efficiency of Resolution and Davis--Putnam Procedures

We consider several problems related to the use of resolution-based methods for determining whether a given boolean formula in conjunctive normal form is satisfiable. First, building on work of Clegg, Edmonds and Impagliazzo, we give an algorithm for satisfiability that when given an unsatisfiable formula of F finds a resolution proof of F, and the runtime of our algorithm is nontrivial as a function of the size of the shortest resolution proof of F. Next we investigate a class of backtrack search algorithms, commonly known as Davis-Putnam procedures and provide the first average-case complexity analysis for their behavior on random formulas. In particular, for a simple algorithm in this class, called ordered DLL we prove that the running time of the algorithm on a randomly generated k-CNF formula with n variables and m clauses is 2(n(n/m)1/(k-2)) with probability 1 - o(1). Finally, we give new lower bounds on res(F), the size of the smallest resolution refutation of F, for a class of...

• Type: Journal
• Year: 2002
• Where: SIAMCOMP
• Authors: Paul Beame, Richard M. Karp, Toniann Pitassi, Michael E. Saks
• Keywords: Algorithm, NSF Grant, Resolution Proof, SIAMCOMP 2002