22/06/2020

Automating cutting planes is NP-hard

Mika Göös, Sajin Koroth, Ian Mertz, Toniann Pitassi

Keywords: Lifting theorems, Cutting Planes, Proof Complexity, Automatability

Abstract: 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. 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(r).

 0
 0
 0
 0
This is an embedded video. Talk and the respective paper are published at STOC 2020 virtual conference. If you are one of the authors of the paper and want to manage your upload, see the question "My papertalk has been externally embedded..." in the FAQ section.

Comments

Post Comment
no comments yet
code of conduct: tbd

Similar Papers