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 the work of Clegg, Edmonds, and Impagliazzo in [Proceedings of the Twenty-Eighth Annual ACM Symposium on Theory of Computing, Philadelphia, PA, 1996, ACM, New York, 1996, pp. 174--183], we give an algorithm for unsatisfiability that when given an unsatisfiable formula of F finds a resolution proof of F. The runtime of our algorithm is subexponential in the size of the shortest resolution proof of F. Next, we investigate a class of backtrack search algorithms for producing resolution refutations of unsatisfiability, commonly known as Davis--Putnam procedures, and provide the first asymptotically tight 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 formulas representing the pigeonhole principle and for randomly generated formulas. For random formulas, Chvatal and Szemeredi [J. ACM, 35 (1988), pp. 759--768] had shown that random 3-CNF formulas with a linear number of clauses require exponential size resolution proofs, and Fu [On the Complexity of Proof Systems, Ph.D. thesis, University of Toronto, Toronto, ON, Canada, 1995] extended their results to k-CNF formulas. These proofs apply only when the number of clauses is Ω(n log n). We show that a lower bound of the form 2^nγ holds with high probability even when the number of clauses is n(k+2)/4-ε.