Time-Space Trade-offs in Resolution: Superpolynomial Lower Bounds for Superlinear Space

DOI10.1137/130914085zbMath1401.68094OpenAlexW2507570475MaRDI QIDQ2817796

Russell Impagliazzo, Chris Beck, P. W. Beame

Publication date: 2 September 2016

Published in: SIAM Journal on Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1137/130914085

zbMATH Keywords

lower boundsresolutiontime-space trade-offsproof complexity

Mathematics Subject Classification ID

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

Related Items

Cumulative Space in Black-White Pebbling and Resolution, Space characterizations of complexity measures and size-space trade-offs in propositional proof systems, Near-optimal lower bounds on regular resolution refutations of Tseitin formulas for all constant-degree graphs, Supercritical Space-Width Trade-offs for Resolution, Bounded-Depth Frege Complexity of Tseitin Formulas for All Graphs, Bounded-depth Frege complexity of Tseitin formulas for all graphs

Uses Software

• Chaff

Cites Work

• Satisfiability, branch-width and Tseitin tautologies
• Near optimal seperation of tree-like and general resolution
• A simplified way of proving trade-off results for resolution
• The intractability of resolution
• Time-space tradeoffs for computing functions, using connectivity properties of their circuits
• Time-space trade-offs in a pebble game
• Space bounds for resolution
• A combinatorial characterization of resolution width
• Polynomial-size Frege and resolution proofs of \(st\)-connectivity and Hex tautologies
• Proofs as Games
• Pebble Games, Proof Complexity, and Time-Space Trade-offs
• Space Complexity in Propositional Calculus
• Hard examples for resolution
• Short proofs are narrow—resolution made simple
• Space complexity of random formulae in resolution
• GRASP: a search algorithm for propositional satisfiability
• Regular resolution lower bounds for the weak pigeonhole principle
• Narrow Proofs May Be Spacious:Separating Space and Width in Resolution
• Some trade-off results for polynomial calculus
• A machine program for theorem-proving
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item