Optimality of size-width trade-offs for resolution

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 tradeoff in Ben-Sasson & Wigderson. Moreover we obtain the optimality of the size-width tradeoff for the widely used restrictions of resolution: regular, Davis-Putnam, negative, positive