To access the full text documents, please follow this link: http://hdl.handle.net/2117/97286
| dc.contributor | Universitat Politècnica de Catalunya. Departament de Ciències de la Computació |
|---|---|
| dc.contributor | Universitat Politècnica de Catalunya. LOGPROG - Lògica i Programació |
| dc.contributor.author | Bonet Carbonell, M. Luisa |
| dc.contributor.author | Galesi, Nicola |
| dc.date | 1999-02 |
| dc.identifier.citation | Bonet, M., Galesi, N. "The Width-size method for general resolution is optimal". 1999. |
| dc.identifier.uri | http://hdl.handle.net/2117/97286 |
| dc.description.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. |
| dc.language.iso | eng |
| dc.relation | LSI-99-1-R |
| dc.rights | info:eu-repo/semantics/openAccess |
| dc.subject | Àrees temàtiques de la UPC::Informàtica::Informàtica teòrica |
| dc.subject | Width-size method |
| dc.subject | BSW |
| dc.subject | Resolution refutations |
| dc.subject | Resolution proofs |
| dc.title | The Width-size method for general resolution is optimal |
| dc.type | info:eu-repo/semantics/publishedVersion |
| dc.type | info:eu-repo/semantics/report |
Related documents
Other documents of the same author
Bonet Carbonell, M. Luisa; Esteban Ángeles, Juan Luis; Galesi, Nicola; Johannsen, Jan
Bonet Carbonell, M. Luisa; Galesi, Nicola
Atserias, Albert; Galesi, Nicola; Gavaldà Mestre, Ricard
Esteban Ángeles, Juan Luis; Galesi, Nicola; Messner, Jochen