Narrow Proofs May Be Maximally Long
From MaRDI portal
Publication:5277920
DOI10.1145/2898435zbMath1367.03104arXiv1409.2731OpenAlexW2396393208WikidataQ61732576 ScholiaQ61732576MaRDI QIDQ5277920
Albert Atserias, Jakob Nordström, Massimo Lauria
Publication date: 12 July 2017
Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1409.2731
SARwidthdegreeresolutionpolynomial calculusproof complexityPCRSherali-Adamspolynomial calculus resolution
Related Items
Unnamed Item, Tight size-degree bounds for sums-of-squares proofs, Circular (Yet Sound) Proofs in Propositional Logic, An Upper Bound for Resolution Size: Characterization of Tractable SAT Instances, Proof Complexity Meets Algebra, Preprocessing of propagation redundant clauses, Nullstellensatz size-degree trade-offs from reversible pebbling, Supercritical Space-Width Trade-offs for Resolution, Short Proofs Are Hard to Find, Size-degree trade-offs for sums-of-squares and positivstellensatz proofs, Nullstellensatz size-degree trade-offs from reversible pebbling, Preprocessing of propagation redundant clauses, MaxSAT Resolution and Subcube Sums
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Relativization makes contradictions harder for resolution
- On the complexity of cutting-plane proofs
- New developments in the theory of Gröbner bases and applications to formal verification
- Tight rank lower bounds for the Sherali-Adams proof system
- Polybori: A framework for Gröbner-basis computations with Boolean polynomials
- The intractability of resolution
- Lower bounds for the polynomial calculus
- Optimality of size-width tradeoffs for resolution
- Mutilated chessboard problem is exponentially hard 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
- Edmonds polytopes and a hierarchy of combinatorial problems
- Proofs as Games
- A Framework for Space Complexity in Algebraic Proof Systems
- Convex Relaxations and Integrality Gaps
- Total Space in Resolution
- Parameterized Bounded-Depth Frege Is not Optimal
- Space Complexity in Propositional Calculus
- A Hierarchy of Relaxations between the Continuous and Convex Hull Representations for Zero-One Programming Problems
- Parity, circuits, and the polynomial-time hierarchy
- Many hard examples for resolution
- Lower Bounds for Lovász–Schrijver Systems and Beyond Follow from Multiparty Communication Complexity
- Size-Space Tradeoffs for Resolution
- Hard examples for resolution
- Cones of Matrices and Set-Functions and 0–1 Optimization
- On Resolution with Clauses of Bounded Size
- 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
- A Generalized Method for Proving Polynomial Calculus Degree Lower Bounds
- Communication lower bounds via critical block sensitivity
- Towards an Understanding of Polynomial Calculus: New Separations and Lower Bounds
- Time-space tradeoffs in resolution
- Hypercontractivity, sum-of-squares proofs, and their applications
- Some trade-off results for polynomial calculus
- LOWER BOUNDS FOR DNF-REFUTATIONS OF A RELATIVIZED WEAK PIGEONHOLE PRINCIPLE
- A Comparison of the Sherali-Adams, Lovász-Schrijver, and Lasserre Relaxations for 0–1 Programming
- Parameterized Complexity of DPLL Search Procedures
- Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
- Linear lower bound on degrees of Positivstellensatz calculus proofs for the parity
- Complexity of Null- and Positivstellensatz proofs
