Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Paper:

TR20-064 | 2nd May 2020 02:21

Automating Algebraic Proof Systems is NP-Hard

RSS-Feed




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: 159
Keywords: 


Abstract:

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.



ISSN 1433-8092 | Imprint