文章基本信息

标题：Automating Cutting Planes is NP-Hard
本地全文：下载
作者：Mika Göös ; Sajin Koroth ; Ian Mertz 等
期刊名称：Electronic Colloquium on Computational Complexity
印刷版ISSN：1433-8092
出版年度：2020
卷号：2020
页码：1-29
出版社：Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
摘要：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¨uller (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.