ECCC-Report TR20-049https://eccc.weizmann.ac.il/report/2020/049Comments and Revisions published for TR20-049en-usFri, 17 Apr 2020 01:12:13 +0300
Paper TR20-049
| Automating Cutting Planes is NP-Hard |
Mika Göös,
Sajin Koroth,
Ian Mertz,
Toniann Pitassi
https://eccc.weizmann.ac.il/report/2020/049We 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 Muller (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.Fri, 17 Apr 2020 01:12:13 +0300https://eccc.weizmann.ac.il/report/2020/049