Abstract:
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.