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
- A combinatorial characterization of resolution width
- A Comparison of the Sherali-Adams, Lovász-Schrijver, and Lasserre Relaxations for 0–1 Programming
- A framework for space complexity in algebraic proof systems
- A generalized method for proving polynomial calculus degree lower bounds
- A Hierarchy of Relaxations between the Continuous and Convex Hull Representations for Zero-One Programming Problems
- 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
- 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?)
- Hypercontractivity, sum-of-squares proofs, and their applications
- Linear lower bound on degrees of Positivstellensatz calculus proofs for the parity
- Lower bounds for DNF-refutations of a relativized weak pigeonhole principle
- Lower Bounds for Lovász–Schrijver Systems and Beyond Follow from Multiparty Communication Complexity
- 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 bounded-depth Frege is not optimal
- Parameterized Complexity of DPLL Search Procedures
- 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
(22)- Tight size-degree bounds for sums-of-squares proofs
- Nullstellensatz size-degree trade-offs from reversible pebbling
- Preprocessing of propagation redundant clauses
- A tradeoff between length and width in resolution
- Narrow proofs may be spacious, separating space and width in resolution
- An upper bound for resolution size: characterization of tractable SAT instances
- The relation between polynomial calculus, Sherali-Adams, and sum-of-squares proofs
- scientific article; zbMATH DE number 1342212 (Why is no real title available?)
- Proof Complexity Meets Algebra
- Short Proofs Are Hard to Find
- Nullstellensatz size-degree trade-offs from reversible pebbling
- Size-degree trade-offs for sums-of-squares and positivstellensatz proofs
- Narrow proofs may be spacious: separating space and width in resolution
- Supercritical space-width trade-offs for resolution
- MaxSAT Resolution and Subcube Sums
- Preprocessing of propagation redundant clauses
- Circular (Yet Sound) Proofs in Propositional Logic
- Proof complexity and the binary encoding of combinatorial principles
- TFNP intersections through the Lens of feasible disjunction
- Separations in proof complexity and TFNP
- On the power and limitations of branch and cut
- Improving resolution width lower bounds for k-CNFs with applications to the strong exponential time hypothesis
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)
