loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
18th Annual IEEE Conference on Computational Complexity (CCC'03)
A Combinatorial Characterization of ResolutionWidth
Aarhus, Denmark
July 07-July 10
ISBN: 0-7695-1879-6
Albert Atserias, Universital Politecnica de Catalunya
V? Dalmau, Universitat Pompeu Fabra
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.
Citation:
Albert Atserias, V? Dalmau, "A Combinatorial Characterization of ResolutionWidth," ccc, pp.239, 18th Annual IEEE Conference on Computational Complexity (CCC'03), 2003
Usage of this product signifies your acceptance of the Terms of Use.