|Title||A Study of Proof Search Algorithms for Resolution and Polynomial Calculus|
|Author(s)|| Maria Luisa Bonet, Nicola Galesi|
|Type||Article in Conference Proceedings|
|Abstract||This paper is concerned with the complexity of proofs and of searching for proofs in two propositional proof system: Resolution and Polynomial Calculus (PC). For the former system we show that the recently proposed algorithm of [BW99] 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 [BW99] as size-width trade-off. We moreover obtain the optimality of the size-width 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 translation to polynomials of a CNF formula having short resolution proofs, cannot be refuted in PC with degree less than OmegaGammaan/ n). A consequence of this is that the simulation of resolution by PC of|
[CEI97] cannot be improved to better than quasipolynomial in the case we start with small resolution proofs. We conjecture that the simulation of [CE197] is optimal.
|Address||New York, NY, USA|