The Width-size method for general resolution is optimal
View/Open
Cita com:
hdl:2117/97286
Document typeResearch report
Defense date1999-02
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
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.
CitationBonet, M., Galesi, N. "The Width-size method for general resolution is optimal". 1999.
Is part ofLSI-99-1-R
Files | Description | Size | Format | View |
---|---|---|---|---|
1400336972.pdf | 728,9Kb | View/Open |