ECCC-Report TR02-035https://eccc.weizmann.ac.il/report/2002/035Comments and Revisions published for TR02-035en-usTue, 18 Jun 2002 17:17:27 +0300
Paper TR02-035
| A Combinatorial Characterization of Resolution Width |
Albert Atserias,
VĂctor Dalmau
https://eccc.weizmann.ac.il/report/2002/035We provide a characterization of the resolution
width introduced in the context of Propositional Proof Complexity
in terms of the existential pebble game introduced
in the context of Finite Model Theory. The characterization
is tight and purely combinatorial. Our
first application of this result is a surprising
proof that the minimum space of refuting a 3-CNF formula
is always bounded from below by the minimum width
of refuting it (minus 3). This solves a well-known open
problem. The second application is the unification of
several width lower bound arguments, and a new width
lower bound for the Dense Linear Order Principle. Since
we also show that this principle has Resolution refutations
of polynomial size, this provides yet another example
showing that the size-width relationship is tight.
Tue, 18 Jun 2002 17:17:27 +0300https://eccc.weizmann.ac.il/report/2002/035