Sciweavers

Share
JCSS
2008

A combinatorial characterization of resolution width

10 years 4 months ago
A combinatorial characterization of resolution width
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 wellknown 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.
Albert Atserias, Víctor Dalmau
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2008
Where JCSS
Authors Albert Atserias, Víctor Dalmau
Comments (0)
books