一句话：提出反链与覆盖两种几何方法，为 Stabbing Planes 证明系统给出组合原理的大小与深度下界。
Stabbing Planes（又称 Branch and Cut）是在整数线性不等式上分支、扩展 DPLL 的证明系统；已有大小/深度下界技术多由 Cutting Planes 推广而来，且常限于提升版本。本文提出两种适用于任意公式的几何方法：反链方法基于 Sperner 定理，覆盖方法利用布尔立方体线性多项式本质覆盖结果并依赖 Alon 组合 Nullstellensatz。作者在鸽巢原理、Tseitin 矛盾、线性排序原理上验证方法：反链法给出鸽巢原理近线性大小与最优对数深度下界，以及完全图上 Tseitin 和线性排序原理的类似下界；覆盖法给出网格图上 Tseitin 的超线性大小与对数深度下界。
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. For size lower bounds these are established by monotone circuit arguments, while for depth these are found via communication complexity and protection. As such these bounds apply for lifted versions 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.
@article{paperbot2790,
title = {Depth lower bounds in Stabbing Planes for combinatorial principles},
author = {Stefan Dantchev and Nicola Galesi and Abdul Ghani and Barnaby Martin},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 1},
year = {2024},
doi = {10.46298/lmcs-20(1:1)2024}
}