Details:
Title | Width Optimality Results for Resolution and Degree Lower Bounds for Polynomial
Calculus | Author(s) | Maria Luisa Bonet, Nicola Galesi | Type | Technical Report, Misc | Abstract | This paper is concerned with the complexity of proofs and of searching for proofs in two propositional proof systems: Resolution and Polynomial Calculus (PC). First we show that the recently proposed algorithm of BenSasson and Wigderson [2] for searching for proofs in resolution cannot give better than weakly exponential performance. This is a consequence of showing optimality of their general relationship called sizewidth trade-off in [2]. 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 Polynomial Calculus, we show that the direct translation to polynomials of a CNF formula having short resolution proofs, cannot be refuted in PC with degree less than Omega(log n). A consequence of this is that the simulation of resolution by PC of Clegg, Edmonds and Impagliazzo [12] cannot be improved to better than quasipolynomial in the case we start with small resolution proofs. We conjecture that the simulation of [12] is optimal. |
Language | English | Year | 2000 | Edition | 0 | Translation |
No | Refereed |
No |
|