Supercritical Space-Width Trade-offs for Resolution
DOI10.1137/16M1109072zbMath1485.03235OpenAlexW3005509650MaRDI QIDQ5215515
Christoph Berkholz, Jakob Nordström
Publication date: 12 February 2020
Published in: SIAM Journal on Computing (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1137/16m1109072
Logic in computer science (03B70) Complexity of computation (including implicit computational complexity) (03D15) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15) Complexity of proofs (03F20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The intractability of resolution
- Space bounds for resolution
- Space proof complexity for random 3-CNFs
- A combinatorial characterization of resolution width
- The Efficiency of Resolution and Davis--Putnam Procedures
- Time-Space Trade-offs in Resolution: Superpolynomial Lower Bounds for Superlinear Space
- Total Space in Resolution
- Pebble Games, Proof Complexity, and Time-Space Trade-offs
- Space Complexity in Propositional Calculus
- A New Kind of Tradeoffs in Propositional Proof Complexity
- Many hard examples for resolution
- Size-Space Tradeoffs for Resolution
- Hard examples for resolution
- The relative efficiency of propositional proof systems
- Short proofs are narrow—resolution made simple
- Space complexity of random formulae in resolution
- GRASP: a search algorithm for propositional satisfiability
- Total Space in Resolution Is at Least Width Squared
- Near-Optimal Lower Bounds on Quantifier Depth and Weisfeiler--Leman Refinement Steps
- Narrow Proofs May Be Spacious:Separating Space and Width in Resolution
- Narrow Proofs May Be Maximally Long
- Some trade-off results for polynomial calculus
- A Machine-Oriented Logic Based on the Resolution Principle
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
This page was built for publication: Supercritical Space-Width Trade-offs for Resolution
