Depth lower bounds in Stabbing Planes for combinatorial principles

DOI10.46298/LMCS-20(1:1)2024MaRDI QIDQ6137876zbMATH OpenFDO

Authors

Publication date 16 January 2024

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2102.07622

zbMATH Keywords

computational complexitylower boundscutting planesproof complexityStabbing Planes

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

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.

Cites work

• scientific article; zbMATH DE number 6829289 (Why is no real title available?)
• scientific article; zbMATH DE number 7561762 (Why is no real title available?)
• A Computing Procedure for Quantification Theory
• A Machine-Oriented Logic Based on the Resolution Principle
• A course in combinatorics.
• A machine program for theorem-proving
• Covering the cube by affine hyperplanes
• Depth lower bounds in stabbing planes for combinatorial principles
• Discretely ordered modules as a first-order extension of the cutting planes proof system
• Essential covers of the cube by hyperplanes
• Hard examples for resolution
• Improved Lower Bounds for Tree-Like Resolution over Linear Inequalities
• Interpolation by a Game
• Maximal probabilities of convolution powers of discrete uniform distributions
• On the complexity of cutting-plane proofs
• On the power and limitations of branch and cut
• Rank bounds and integrality gaps for cutting planes procedures
• Resolution with counting: dag-like lower bounds and different moduli
• Stabbing planes
• Ten challenges \textit{redux}: recent progress in propositional reasoning and search

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)