From small space to small width in resolution
From MaRDI portal
Abstract: In 2003, Atserias and Dalmau resolved a major open question about the resolution proof system by establishing that the space complexity of CNF formulas is always an upper bound on the width needed to refute them. Their proof is beautiful but somewhat mysterious in that it relies heavily on tools from finite model theory. We give an alternative, completely elementary proof that works by simple syntactic manipulations of resolution refutations. As a by-product, we develop a "black-box" technique for proving space lower bounds via a "static" complexity measure that works against any resolution refutation---previous techniques have been inherently adaptive. We conclude by showing that the related question for polynomial calculus (i.e., whether space is an upper bound on degree) seems unlikely to be resolvable by similar methods.
Recommendations
- From small space to small width in resolution
- Size-space tradeoffs for resolution
- A tradeoff between length and width in resolution
- Total space in resolution is at least width squared
- scientific article; zbMATH DE number 1304340
- Space bounds for resolution
- Optimality of size-width tradeoffs for resolution
- Supercritical space-width trade-offs for resolution
- Supercritical space-width trade-offs for resolution
- Towards an optimal separation of space and length in resolution
Cited in
(7)- A note about k-DNF resolution
- Cliques enumeration and tree-like resolution proofs
- On semantic cutting planes with very small coefficients
- Space complexity in propositional calculus
- Small Spans in Scaled Dimension
- Narrow proofs may be spacious: separating space and width in resolution
- From small space to small width in resolution
This page was built for publication: From small space to small width in resolution
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2965493)
