loading...
A Combinatorial Characterization of ResolutionWidth
Aarhus, Denmark July 07-July 10
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/CCC.2003.121442418th Annual IEEE Conference on Comput ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
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.