Narrow proofs may be maximally long
From MaRDI portal
Abstract: We prove that there are 3-CNF formulas over n variables that can be refuted in resolution in width w but require resolution proofs of size n^Omega(w). This shows that the simple counting argument that any formula refutable in width w must have a proof in size n^O(w) is essentially tight. Moreover, our lower bound generalizes to polynomial calculus resolution (PCR) and Sherali-Adams, implying that the corresponding size upper bounds in terms of degree and rank are tight as well. Our results do not extend all the way to Lasserre, however, where the formulas we study have proofs of constant rank and size polynomial in both n and w.
Recommendations
Cites work
- scientific article; zbMATH DE number 1256733 (Why is no real title available?)
- scientific article; zbMATH DE number 1179974 (Why is no real title available?)
- scientific article; zbMATH DE number 1757962 (Why is no real title available?)
- scientific article; zbMATH DE number 1916823 (Why is no real title available?)
- scientific article; zbMATH DE number 1390276 (Why is no real title available?)
- scientific article; zbMATH DE number 3373541 (Why is no real title available?)
- scientific article; zbMATH DE number 3029852 (Why is no real title available?)
- A Comparison of the Sherali-Adams, Lovász-Schrijver, and Lasserre Relaxations for 0–1 Programming
- A Hierarchy of Relaxations between the Continuous and Convex Hull Representations for Zero-One Programming Problems
- A combinatorial characterization of resolution width
- A framework for space complexity in algebraic proof systems
- A generalized method for proving polynomial calculus degree lower bounds
- A tradeoff between length and width in resolution
- Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
- Communication lower bounds via critical block sensitivity
- Complexity of Null- and Positivstellensatz proofs
- Cones of Matrices and Set-Functions and 0–1 Optimization
- Convex relaxations and integrality gaps
- Edmonds polytopes and a hierarchy of combinatorial problems
- GRASP: a search algorithm for propositional satisfiability
- Hard examples for resolution
- Hypercontractivity, sum-of-squares proofs, and their applications
- Linear lower bound on degrees of Positivstellensatz calculus proofs for the parity
- Lower Bounds for Lovász–Schrijver Systems and Beyond Follow from Multiparty Communication Complexity
- Lower bounds for DNF-refutations of a relativized weak pigeonhole principle
- Lower bounds for the polynomial calculus
- Lower bounds for the polynomial calculus and the Gröbner basis algorithm
- Many hard examples for resolution
- Mutilated chessboard problem is exponentially hard for resolution
- New developments in the theory of Gröbner bases and applications to formal verification
- On Resolution with Clauses of Bounded Size
- On the complexity of cutting-plane proofs
- Optimality of size-width tradeoffs for resolution
- Parameterized Complexity of DPLL Search Procedures
- Parameterized bounded-depth Frege is not optimal
- Parity, circuits, and the polynomial-time hierarchy
- Polybori: A framework for Gröbner-basis computations with Boolean polynomials
- Proofs as Games
- Relativization makes contradictions harder for resolution
- Short proofs are narrow—resolution made simple
- Size-space tradeoffs for resolution
- Some trade-off results for polynomial calculus (extended abstract)
- Space Complexity in Propositional Calculus
- Space complexity of random formulae in resolution
- Space proof complexity for random 3-CNFs
- The intractability of resolution
- The relative efficiency of propositional proof systems
- Tight rank lower bounds for the Sherali-Adams proof system
- Tight size-degree bounds for sums-of-squares proofs
- Time-space tradeoffs in resolution, superpolynomial lower bounds for superlinear space
- Total space in resolution
- Towards an understanding of polynomial calculus: new separations and lower bounds (extended abstract)
Cited in
(20)- Narrow proofs may be spacious, separating space and width in resolution
- Proof Complexity Meets Algebra
- Proof complexity and the binary encoding of combinatorial principles
- Size-degree trade-offs for sums-of-squares and positivstellensatz proofs
- A tradeoff between length and width in resolution
- Separations in proof complexity and TFNP
- MaxSAT Resolution and Subcube Sums
- An upper bound for resolution size: characterization of tractable SAT instances
- Preprocessing of propagation redundant clauses
- Preprocessing of propagation redundant clauses
- Nullstellensatz size-degree trade-offs from reversible pebbling
- Narrow proofs may be spacious: separating space and width in resolution
- The relation between polynomial calculus, Sherali-Adams, and sum-of-squares proofs
- Nullstellensatz size-degree trade-offs from reversible pebbling
- Improving resolution width lower bounds for k-CNFs with applications to the strong exponential time hypothesis
- Tight size-degree bounds for sums-of-squares proofs
- Short Proofs Are Hard to Find
- Supercritical space-width trade-offs for resolution
- TFNP intersections through the Lens of feasible disjunction
- Circular (Yet Sound) Proofs in Propositional Logic
This page was built for publication: Narrow proofs may be maximally long
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5277920)
