Space Complexity in Polynomial Calculus

DOI10.1137/120895950zbMath1372.03099OpenAlexW1944379106WikidataQ61732581 ScholiaQ61732581MaRDI QIDQ2944568

Massimo Lauria, Yuval Filmus, Jakob Nordström, Noga Ron-Zewi, Neil Thapen

Publication date: 2 September 2015

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

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

zbMATH Keywords

lower boundsresolutionpolynomial calculusproof complexityspacePCRpolynomial calculus resolution

Mathematics Subject Classification ID

Related Items (4)

Cumulative Space in Black-White Pebbling and Resolution ⋮ On semantic cutting planes with very small coefficients ⋮ Resolution and the binary encoding of combinatorial principles ⋮ Total Space in Resolution

Uses Software

• PolyBoRi
• Chaff

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On the power of clause-learning SAT solvers as resolution engines
• On the complexity of cutting-plane proofs
• Random CNF's are hard for the polynomial calculus
• A simplified way of proving trade-off results for resolution
• New developments in the theory of Gröbner bases and applications to formal verification
• Polybori: A framework for Gröbner-basis computations with Boolean polynomials
• The intractability of resolution
• Lower bounds for the polynomial calculus
• Space bounds for resolution
• Lower bounds for the polynomial calculus and the Gröbner basis algorithm
• Space proof complexity for random 3-CNFs
• A combinatorial characterization of resolution width
• The Efficiency of Resolution and Davis--Putnam Procedures
• Total Space in Resolution
• Pebble Games, Proof Complexity, and Time-Space Trade-offs
• Pseudo-partitions, transversality and locality
• Space Complexity in Propositional Calculus
• Many hard examples for resolution
• Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
• Size-Space Tradeoffs for Resolution
• Hard examples for resolution
• The relative efficiency of propositional proof systems
• Lower bounds for resolution and cutting plane proofs and monotone computations
• Short proofs are narrow—resolution made simple
• Space complexity of random formulae in resolution
• GRASP: a search algorithm for propositional satisfiability
• A Generalized Method for Proving Polynomial Calculus Degree Lower Bounds
• Lower Bounds for Width-Restricted Clause Learning on Small Width Formulas
• Narrow Proofs May Be Spacious:Separating Space and Width in Resolution
• Communication lower bounds via critical block sensitivity
• Towards an Understanding of Polynomial Calculus: New Separations and Lower Bounds
• Time-space tradeoffs in resolution
• On the virtue of succinct proofs
• The Complexity of Propositional Proofs
• 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
• Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
• Linear gaps between degrees for the polynomial calculus modulo distinct primes

This page was built for publication: Space Complexity in Polynomial Calculus