On the power and limitations of branch and cut
On the power and limitations of branch and cut
复制标题
论分支与剪切的威力和局限性
DOI：
10.4230/lipics.ccc.2021.6
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
A. Wigderson
中科院分区：
文献类型：
--
作者：
Noah Fleming;Mika Göös;R. Impagliazzo;T. Pitassi;Robert Robere;Li;A. Wigderson
引入捅刀平面证明系统[8]，对实际混合整数规划求解中所进行的推理进行建模。作为一个证明系统，它足够强大，可以模拟切割平面，并反驳tseittin公式-某些不可满足的线性方程组mod2 -这是许多代数证明系统的典型硬例子。在最近的（令人惊讶的）结果中，Dadush和Tiwari[25]表明，这些对tseittin公式的简短反驳可以转化为准多项式的尺寸和深度切割面证明，反驳了一个长期存在的猜想。这个翻译提出了几个有趣的问题。首先，是否所有的刺切面证明都能有效地通过切面来模拟。这将允许在切割平面系统上所做的大量分析被提升到实际的混合整数规划求解器。第二，这些证明的拟多项式深度是否是切割平面所固有的。在本文中，我们在回答这两个问题方面取得了进展。首先，我们证明了任何具有有界系数（SP*）的刺穿平面证明都可以转化为切割平面。作为切割平面已知下界的结果，这建立了SP*上的第一个指数下界。利用这一翻译，我们推广了Dadush和Tiwari的结果，证明了切割平面对有限域上任何不可满足的线性方程组都有简短的反驳。就像Dadush和Tiwari的切面证明一样，我们的反驳也引起了一个深入的拟多项式爆炸，我们推测这是固有的。作为实现这一猜想的一步，我们开发了一种新的几何技术来证明切割平面深度的下界。这允许我们建立语义切割平面深度的第一个下界来证明tseittin公式。
The Stabbing Planes proof system [8] was introduced to model the reasoning carried out in practical mixed integer programming solvers. As a proof system, it is powerful enough to simulate Cutting Planes and to refute the Tseitin formulas - certain unsatisfiable systems of linear equations mod2 - which are canonical hard examples for many algebraic proof systems. In a recent (and surprising) result, Dadush and Tiwari [25] showed that these short refutations of the Tseitin formulas could be translated into quasi-polynomial size and depth Cutting Planes proofs, refuting a long-standing conjecture. This translation raises several interesting questions. First, whether all Stabbing Planes proofs can be efficiently simulated by Cutting Planes. This would allow for the substantial analysis done on the Cutting Planes system to be lifted to practical mixed integer programming solvers. Second, whether the quasi-polynomial depth of these proofs is inherent to Cutting Planes. In this paper we make progress towards answering both of these questions. First, we show that any Stabbing Planes proof with bounded coefficients (SP*) can be translated into Cutting Planes. As a consequence of the known lower bounds for Cutting Planes, this establishes the first exponential lower bounds on SP*. Using this translation, we extend the result of Dadush and Tiwari to show that Cutting Planes has short refutations of any unsatisfiable system of linear equations over a finite field. Like the Cutting Planes proofs of Dadush and Tiwari, our refutations also incur a quasi-polynomial blow-up in depth, and we conjecture that this is inherent. As a step towards this conjecture, we develop a new geometric technique for proving lower bounds on the depth of Cutting Planes proofs. This allows us to establish the first lower bounds on the depth of Semantic Cutting Planes proofs of the Tseitin formulas.
自动化切割平面是 NP 困难的
DOI：
10.1145/3357713.3384248
发表时间：
2020
期刊：
STOC 2020: Proceedings of the 52nd Annual ACM SIGACT Symposium on Theory of Computing
影响因子：
--
作者：
Göös, M;Koroth, S;Mertz, I;Pitassi, T.
通讯作者：
Pitassi, T.
刺击飞机
DOI：
10.48550/arxiv.1710.03219
发表时间：
2022
期刊：
ArXivorg
影响因子：
--
作者：
Beame, Paul;Fleming, Noah;Impagliazzo, Russell;Pankratov, Denis;Pitassi, Toniann;Robere, Robert
通讯作者：
Robere, Robert
极其深刻的证明
影响因子：
--
作者：
Fleming, Noah and
通讯作者：
Fleming, Noah and