Revision #2 Authors: Mika Göös, Jakob Nordström, Toniann Pitassi, Robert Robere, Dmitry Sokolov, Susanna de Rezende

Accepted on: 10th June 2022 18:31

Downloads: 245

Keywords:

We 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 or Polynomial Calculus 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.

We retract the non-automatability result for Sherali-Adams (see footnote on page 1).

Revision #1 Authors: Mika Göös, Jakob Nordström, Toniann Pitassi, Robert Robere, Dmitry Sokolov, Susanna de Rezende

Accepted on: 10th November 2020 18:46

Downloads: 705

Keywords:

We 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.

Added an alternative proof via size-width tradeoffs.

TR20-064 Authors: Mika Göös, Jakob Nordström, Toniann Pitassi, Robert Robere, Dmitry Sokolov, Susanna de Rezende

Publication: 2nd May 2020 14:41

Downloads: 1296

Keywords:

We 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.