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 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 relationship between size and width cannot be made subpolynomial.Supported in part by CICYT TIN2004-04343 and by the European Commission through the RTN COMBSTRU HPRN-CT2002-00278. Research partially supported by the MEC under the program “Ramon y Cajal,” grants TIC 2002-04470-C03 and TIC 2002-04019-C03, the EU PASCAL Network of Excellence, IST-2002-506778, and the MODNET Marie Curie Research Training Network, MRTN-CT-2004-512234