The Width-size method for general resolution is optimal
Document typeResearch report
Rights accessOpen Access
All rights reserved. This work is protected by the corresponding intellectual and industrial property rights. Without prejudice to any existing legal exemptions, reproduction, distribution, public communication or transformation of this work are prohibited without permission of the copyright holder
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.
CitationBonet, M., Galesi, N. "The Width-size method for general resolution is optimal". 1999.
Is part ofLSI-99-1-R