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 (P C ). 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 show- ing optimality of their general relationship reffered to in [2] as size-width trade-off. We moreover obtain the optimality of the size- width trade-off for the widely used restrictions of resolution: reg- ular, Davis-Putnam, negative, positive and linear. As for the sec- ond system, we show that the direct translation to polynomials of a C N F formula having short resolution proofs, cannot be refuted in P C with degree less than log n. A consequence of this is that the simulation of resolution by P C of Clegg, Edmonds and Ipagliazzo [11] cannot be improved to better than quasipolynomial in the case we start with small resolution proofs. We conjecture that the simulation of [11] is optimal.