期刊名称：Electronic Colloquium on Computational Complexity
印刷版ISSN：1433-8092
出版年度：2002
卷号：2002
出版社：Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
摘要：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.
