|
Título:
|
The Width-size method for general resolution is optimal
|
|
Autor/a:
|
Bonet Carbonell, M. Luisa; Galesi, Nicola
|
|
Otros autores:
|
Universitat Politècnica de Catalunya. Departament de Ciències de la Computació; Universitat Politècnica de Catalunya. LOGPROG - Lògica i Programació |
|
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. |
|
Materia(s):
|
-Àrees temàtiques de la UPC::Informàtica::Informàtica teòrica
-Width-size method
-BSW
-Resolution refutations
-Resolution proofs |
|
Derechos:
|
|
|
Tipo de documento:
|
Artículo - Versión publicada
Informe |
|
Compartir:
|
|
