Details:
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. |
Language | English | Pages | 422-432 | Publisher | IEEE Press | Address | New York, NY, USA | Year | 1999 | Edition | 0 | Translation |
No | Refereed |
No |
|