| z (2007) | |||||||||||||||||
Abstract | |||||||||||||||||
| Abstract. We consider several problems related to the use of resolution-based methods for determining whether a given boolean formula in conjunctive normal form is satisable. First, building on work of Clegg, Edmonds and Impagliazzo, we give an algorithm for unsatisability that when given an unsatisable formula of F nds 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 unsatisability, commonly known as Davis-Putnam procedures and provide the rst 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 had shown that random 3-CNF formulas with a linear number of clauses require exponential size resolution proofs and Fu 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 | |||||||||||||||||
Publication details | |||||||||||||||||
| |||||||||||||||||