A Study of Proof Search Algorithms for Resolution and Polynomial Calculus

This paper is concerned with the complexity of proofs and of searching for proofs in two propositional proof systems: Resolution and Polynomial Calculus (PC). For the former system we show that the recently proposed algorithm of BenSasson and Wigderson [2] for searching for proofs cannot give better than weakly exponential performance. This is a consequence of showing optimality of their general relationship reffered to in [2] as size-width trade-off. We moreoverobtain the optimality of the sizewidth trade-off for the widely used restrictions of resolution: regular, Davis-Putnam, negative, positive and linear. As for the second system, we show that the direct translation to polynomials of a CNF formula having short resolution proofs, cannotbe refuted in PC with degree less than logn. A consequence of this is that the simulation of resolution by PC of Clegg, Edmonds and Impagliazzo [11] cannot be improved to better than quasipolynomial in the case we start with small resolution proofs....

• Type: Conference
• Year: 1999
• Where: FOCS
• Authors: Maria Luisa Bonet, Nicola Galesi
• Keywords: FOCS 1999, Propositional Proof Systems, Resolution Proofs, Short Resolution Proofs, Theoretical Computer Science