Home | Quick Search | Advanced Search | Bibliography submission | Bibliography submission using bibtex | Bibliography submission using bibtex file | Links | Help | Internal


TitleA Study of Proof Search Algorithms for Resolution and Polynomial Calculus
Author(s) Maria Luisa Bonet, Nicola Galesi
TypeArticle in Conference Proceedings
AbstractThis 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.
PublisherIEEE Press
AddressNew York, NY, USA
Translation No
Refereed No