Automating Cutting Planes is NP-Hard}
STOC '20: 52nd Annual ACM SIGACT Symposium on Theory of Computing Chicago IL USA June, 2020, pp. 68-77, 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 ...More
PPT (Upload PPT)