论 Branch and Cut 的能力与局限
计算复杂性
2021-05-24 v2
摘要
Stabbing Planes 证明系统被引入以建模实际混合整数规划求解器中的推理。作为一个证明系统，它足以模拟 Cutting Planes 并反驳 Tseitin 公式——某些模 2 线性方程组的不可满足系统——这些是许多代数证明系统的典型困难例子。在最近一项（令人惊讶的）结果中，Dadush 与 Tiwari 表明，这些 Tseitin 公式的简短反驳可转化为拟多项式规模与深度的 Cutting Planes 证明，反驳了一个长期存在的猜想。这一转化提出了若干有趣问题。首先，是否所有 Stabbing Planes 证明都能被 Cutting Planes 高效模拟。这将使得在 Cutting Planes 系统上所做的大量分析得以提升到实际混合整数规划求解器。其次，这些证明的拟多项式深度是否为 Cutting Planes 所固有。本文在回答这两个问题上取得进展。首先，我们证明任何具有有界系数的 Stabbing Planes 证明 SP* 可转化为 Cutting Planes。作为已知 Cutting Planes 下界的推论，这确立了关于 SP* 的首个指数下界。利用该转化，我们将 Dadush 与 Tiwari 的结果推广，表明 Cutting Planes 对有限域上任何不可满足线性方程组都有简短反驳。如同 Dadush 与 Tiwari 的 Cutting Planes 证明，我们的反驳在深度上也产生拟多项式膨胀，我们猜想这是固有的。作为朝向该猜想的一步，我们发展了一种用于证明 Cutting Planes 证明深度下界的新几何技术。这使我们确立了关于 Tseitin 公式的 Semantic Cutting Planes 证明深度的首个下界。
引用
@article{arxiv.2102.05019,
title = {On the Power and Limitations of Branch and Cut},
author = {Noah Fleming and Mika Göös and Russell Impagliazzo and Toniann Pitassi and Robert Robere and Li-Yang Tan and Avi Wigderson},
journal= {arXiv preprint arXiv:2102.05019},
year = {2021}
}