The Width-size method for general resolution is optimal

Abstract

The Width-Size Method for resolution was recently introduced by Ben-Sasson and Wigderson (BSW): Short Proofs are Narrow - Resolution Made Simple STOC 99). They found a trade-off between two complexity measures for Resolution refutations: the size (i.e. the number of clauses) and the width (i.e. the size of the largest clause). Using this trade-off they reduced

the problem of giving lower bounds on the size to that of giving lower bounds on the width and gave a unified method to obtain all previously known lower bounds on the size of Resolution refutations. Moreover, the use of the width as a complexity measure for Resolution proofs suggested a new very simple algorithm for searching for Resolution proof. Here we face with the following question (also stated as an open problem in BSW): can the size-width trade-off be improved in the case of unrestricted resolution ? We give a negative answer to this question showing that the result of BSW is optimal. Our result, also holds for the most commonly used restrictions of Resolution like Regular, Davis-Putnam, Positive, Negative and Linear.

A consequence of our result is that the width-based algorithm proposed by BSW for searching for Resolution proofs cannot be used to show the automatizability of Resolution and its restrictions.