Automating cutting planes is NP-hard
Mika Göös, Sajin Koroth, Ian Mertz, Toniann Pitassi · 2020
We show that Cutting Planes (CP) proofs are hard to find: Given an unsatisfiable formula F, It is -hard to find a CP refutation of F in time polynomial in the length of the shortest such refutation; and 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.