Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



TR06-133 | 14th October 2006 00:00

The Resolution Width Problem is EXPTIME-Complete


Authors: Alex Hertel, Alasdair Urquhart
Publication: 17th October 2006 18:23
Downloads: 1569


The 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.

ISSN 1433-8092 | Imprint