ECCC-Report TR06-133https://eccc.weizmann.ac.il/report/2006/133Comments and Revisions published for TR06-133en-usTue, 17 Oct 2006 18:23:43 +0200
Paper TR06-133
| The Resolution Width Problem is EXPTIME-Complete |
Alex Hertel,
Alasdair Urquhart
https://eccc.weizmann.ac.il/report/2006/133The importance of {\em width} as a resource in resolution theorem proving
has been emphasized in work of Ben-Sasson and Wigderson. Their results show that lower
bounds on the size of resolution refutations can be proved in a uniform manner by
demonstrating lower bounds on the width of refutations, and that there is a simple
dynamic programming procedure for automated theorem proving, based on the search for
small width proofs. The present article shows that the problem of determining, given
a set of clauses Sigma and an integer k, whether Sigma has a refutation of width k,
is EXPTIME-complete. The proof is by a reduction from the Existential k-pebble game,
proved EXPTIME-complete by Kolaitis and Panttaja.
Tue, 17 Oct 2006 18:23:43 +0200https://eccc.weizmann.ac.il/report/2006/133