Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



TR02-035 | 27th May 2002 00:00

A Combinatorial Characterization of Resolution Width


Authors: Albert Atserias, Víctor Dalmau
Publication: 18th June 2002 17:17
Downloads: 3966


We 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.

ISSN 1433-8092 | Imprint