Abstract.
This paper is concerned with the complexity of proofs and of searching for proofs in resolution. We show that the recently proposed algorithm of Ben-Sasson & Wigderson for searching for proofs in resolution cannot give better than weakly exponential performance. This is a consequence of our main result: we show the optimality of the general relationship called size-width tradeoffs in Ben-Sasson & Wigderson. Moreover we obtain the optimality of the size-width tradeoffs for the widely used restrictions of resolution: regular, Davis-Putnam, negative, positive.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
Author information
Authors and Affiliations
Additional information
Received: January 31, 2000.
Rights and permissions
About this article
Cite this article
Bonet, M., Galesi, N. Optimality of size-width tradeoffs for resolution. Comput. complex. 10, 261–276 (2001). https://doi.org/10.1007/s000370100000
Issue Date:
DOI: https://doi.org/10.1007/s000370100000