Depth lower bounds in Stabbing Planes for combinatorial principles
From MaRDI portal
Publication:6137876
DOI10.46298/LMCS-20(1:1)2024arXiv2102.07622MaRDI QIDQ6137876FDOQ6137876
Author name not available (Why is that?)
Publication date: 16 January 2024
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Abstract: Stabbing Planes (also known as Branch and Cut) is a proof system introduced very recently which, informally speaking, extends the DPLL method by branching on integer linear inequalities instead of single variables. The techniques known so far to prove size and depth lower bounds for Stabbing Planes are generalizations of those used for the Cutting Planes proof system established via communication complexity arguments. As such they work for the lifted version of combinatorial statements. Rank lower bounds for Cutting Planes are also obtained by geometric arguments called protection lemmas. In this work we introduce two new geometric approaches to prove size/depth lower bounds in Stabbing Planes working for any formula: (1) the antichain method, relying on Sperner's Theorem and (2) the covering method which uses results on essential coverings of the boolean cube by linear polynomials, which in turn relies on Alon's combinatorial Nullenstellensatz. We demonstrate their use on classes of combinatorial principles such as the Pigeonhole principle, the Tseitin contradictions and the Linear Ordering Principle. By the first method we prove almost linear size lower bounds and optimal logarithmic depth lower bounds for the Pigeonhole principle and analogous lower bounds for the Tseitin contradictions over the complete graph and for the Linear Ordering Principle. By the covering method we obtain a superlinear size lower bound and a logarithmic depth lower bound for Stabbing Planes proof of Tseitin contradictions over a grid graph.
Full work available at URL: https://arxiv.org/abs/2102.07622
Cites Work
- A course in combinatorics.
- Hard examples for resolution
- A Machine-Oriented Logic Based on the Resolution Principle
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
- On the complexity of cutting-plane proofs
- Principles and Practice of Constraint Programming – CP 2003
- Covering the cube by affine hyperplanes
- Essential covers of the cube by hyperplanes
- Title not available (Why is that?)
- Improved Lower Bounds for Tree-Like Resolution over Linear Inequalities
- Discretely ordered modules as a first-order extension of the cutting planes proof system
- Maximal probabilities of convolution powers of discrete uniform distributions
- Title not available (Why is that?)
- Title not available (Why is that?)
- Interpolation by a Game
- Resolution with counting: dag-like lower bounds and different moduli
- Title not available (Why is that?)
- On the power and limitations of branch and cut
- Depth lower bounds in stabbing planes for combinatorial principles
This page was built for publication: Depth lower bounds in Stabbing Planes for combinatorial principles
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6137876)
