ECCC-Report TR20-064https://eccc.weizmann.ac.il/report/2020/064Comments and Revisions published for TR20-064en-usTue, 10 Nov 2020 18:46:40 +0200
Revision 1
| 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/064#revision1We 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 (JACM 2020) that established an analogous result for Resolution.Tue, 10 Nov 2020 18:46:40 +0200https://eccc.weizmann.ac.il/report/2020/064#revision1
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