A tradeoff between length and width in resolution

DOI10.4086/TOC.2016.V012A005MaRDI QIDQ2816413zbMATH OpenOpenAlexFDO

Authors Neil Thapen

Publication date 22 August 2016

Published in Theory of Computing (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4086/toc.2016.v012a005

zbMATH Keywords

lower boundproof complexityreflectionresolutiontrade-offtradeoff between length and widthwidth

Mathematics Subject Classification ID

Complexity of proofs (03F20) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Review text

In this paper, the author investigates the connection between the length of the resolution refutation and its width. Since any short refutation can be transformed into a ``narrow one, the author shows that the ``narrow refutation must be essential longer than the initial short refutation.NEWLINENEWLINE The author describes a family of CNF-formulas with small width which have a refutation of polynomial length and shows that the corresponding ``narrow refutation must be of an exponential length. The CNF-formulas described in the paper are a propositional version of the colored polynomial local search principle.

Recommendations

• Narrow proofs may be maximally long
• Width versus size in resolution proofs
• Narrow proofs may be spacious: separating space and width in resolution
• Theory and Applications of Models of Computation
• Short proofs are narrow—resolution made simple

Cites work

• A simplified way of proving trade-off results for resolution
• On the weak pigeonhole principle
• Proofs as Games
• Short proofs are narrow—resolution made simple
• Size-space tradeoffs for resolution

Cited in

(18)

• Unrestricted resolution versus N-resolution
• Resolution-limited measure and dimension
• Optimality of size-width tradeoffs for resolution
• A note about k-DNF resolution
• Nullstellensatz size-degree trade-offs from reversible pebbling
• Random resolution refutations
• Width and size of regular resolution proofs
• From small space to small width in resolution
• A new kind of tradeoffs in propositional proof complexity
• Randomized feasible interpolation and monotone circuits with a local oracle
• Nullstellensatz size-degree trade-offs from reversible pebbling
• Resolution lower bounds for refutation statements
• Supercritical space-width trade-offs for resolution
• Narrow proofs may be maximally long
• Theory and Applications of Models of Computation
• A simple supercritical tradeoff between size and height in resolution
• Supercritical size-width tree-like resolution trade-offs for graph isomorphism
• A simplified way of proving trade-off results for resolution

This page was built for publication: A tradeoff between length and width in resolution

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2816413)