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.
Optimality of size-width tradeoffs for resolution / Maria Luisa, Bonet; Galesi, Nicola. - In: COMPUTATIONAL COMPLEXITY. - ISSN 1016-3328. - STAMPA. - 10:4(2001), pp. 261-276. [10.1007/s000370100000]
Optimality of size-width tradeoffs for resolution
GALESI, NICOLA
2001
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.