Space bounds for resolution

DOI10.1006/inco.2001.2921zbMath1005.03009MaRDI QIDQ1854472

Juan Luis Esteban, Jacobo Toran

Publication date: 14 January 2003

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1006/inco.2001.2921

Mathematics Subject Classification ID

68Q25: Analysis of algorithms and problem complexity

03B35: Mechanization of proofs and logical operations

03F20: Complexity of proofs

Related Items

Unnamed Item, Supercritical Space-Width Trade-offs for Resolution, The Complexity of Propositional Proofs, The depth of resolution proofs, A simplified way of proving trade-off results for resolution, A combinatorial characterization of treelike resolution space, On space and depth in resolution, A note about \(k\)-DNF resolution, Cliques enumeration and tree-like resolution proofs, On semantic cutting planes with very small coefficients, On the complexity of resolution with bounded conjunctions, The treewidth of proofs, Space proof complexity for random 3-CNFs, A characterization of tree-like resolution size, A combinatorial characterization of resolution width, A Framework for Space Complexity in Algebraic Proof Systems, Time-Space Trade-offs in Resolution: Superpolynomial Lower Bounds for Superlinear Space, Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers, A Tutorial on Time and Space Bounds in Tree-Like Resolution, Total Space in Resolution, Space Complexity in Polynomial Calculus, Autonomous Resolution Based on DNA Strand Displacement

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The intractability of resolution
• Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas
• Short proofs are narrow—resolution made simple
• Space complexity in propositional calculus
• Many hard examples for resolution
• Hard examples for resolution
• Lower bounds for resolution and cutting plane proofs and monotone computations