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


TitleWidth Optimality Results for Resolution and Degree Lower Bounds for Polynomial Calculus
Author(s) Maria Luisa Bonet, Nicola Galesi
TypeTechnical Report, Misc
AbstractThis 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.
Translation No
Refereed No