ECCC-Report TR20-064https://eccc.weizmann.ac.il/report/2020/064Comments and Revisions published for TR20-064en-usSat, 02 May 2020 14:41:48 +0300
Paper TR20-064
| Automating Algebraic Proof Systems is NP-Hard |
Mika Göös,
Susanna de Rezende,
Jakob Nordström,
Toniann Pitassi,
Robert Robere,
Dmitry Sokolov
https://eccc.weizmann.ac.il/report/2020/064We show that algebraic proofs are hard to find: Given an unsatisfiable CNF formula $F$, it is NP-hard to find a refutation of $F$ in the Nullstellensatz, Polynomial Calculus, or Sherali--Adams proof systems in time polynomial in the size of the shortest such refutation. Our work extends, and gives a simplified proof of, the recent breakthrough of Atserias and Muller (FOCS 2019) that established an analogous result for Resolution.Sat, 02 May 2020 14:41:48 +0300https://eccc.weizmann.ac.il/report/2020/064