Para acceder a los documentos con el texto completo, por favor, siga el siguiente enlace: http://hdl.handle.net/2117/97286

The Width-size method for general resolution is optimal
Bonet Carbonell, M. Luisa; Galesi, Nicola
Universitat Politècnica de Catalunya. Departament de Ciències de la Computació; Universitat Politècnica de Catalunya. LOGPROG - Lògica i Programació
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.
Àrees temàtiques de la UPC::Informàtica::Informàtica teòrica
Width-size method
BSW
Resolution refutations
Resolution proofs
info:eu-repo/semantics/publishedVersion
Informe
         

Mostrar el registro completo del ítem

Documentos relacionados

Otros documentos del mismo autor/a

Atserias, Albert; Galesi, Nicola; Gavaldà Mestre, Ricard
Ansótegui, Carlos; Bonet Carbonell, M. Luisa; Levy Díaz, Jordi
Ansótegui Gil, Carlos; Bonet Carbonell, M. Luisa; Levy Díaz, Jordi
Ansótegui Gil, Carlos; Bonet Carbonell, M. Luisa; Gabàs, Joel; Levy Díaz, Jordi
Bonet Carbonell, M. Luisa; John, Katherine St.