论文标题
自动切割飞机是NP-HARD}
Automating Cutting Planes is NP-Hard}
论文作者
论文摘要
我们表明，剪平飞机（CP）证明很难找到：给定一个不满意的公式$ f $， 1）在最短的反驳的长度上，找到$ f $ in Time多项式的CP反驳是NP-HARD；和 2）除非Gap-litting-Set允许使用非平凡的算法，否则在最短的反驳的长度上，人们找不到$ f $ $ f $的CP反驳。 第一个结果扩大了Atserias和Müller（Focs 2019）的最新突破，该突破建立了分辨率的类似结果。我们的证明依赖于两个新的提升定理：（1）具有许多输出位的小工具类似于DAG。 （2）类似树的举升，该提升模拟了$ r $ round协议，并具有查询复杂性的小工具$ o（\ log r）$独立于输入长度。
We show that Cutting Planes (CP) proofs are hard to find: Given an unsatisfiable formula $F$, 1) It is NP-hard to find a CP refutation of $F$ in time polynomial in the length of the shortest such refutation; and 2)unless Gap-Hitting-Set admits a nontrivial algorithm, one cannot find a tree-like CP refutation of $F$ in time polynomial in the length of the shortest such refutation. The first result extends the recent breakthrough of Atserias and Müller (FOCS 2019) that established an analogous result for Resolution. Our proofs rely on two new lifting theorems: (1) Dag-like lifting for gadgets with many output bits. (2) Tree-like lifting that simulates an $r$-round protocol with gadgets of query complexity $O(\log r)$ independent of input length.
