Title
Automating algebraic proof systems is NP-hard
Abstract
ABSTRACTWe 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 Müller (JACM 2020) that established an analogous result for Resolution.
Year
DOI
Venue
2021
10.1145/3406325.3451080
ACM Symposium on Theory of Computing
DocType
Citations 
PageRank 
Conference
0
0.34
References 
Authors
0
6
Name
Order
Citations
PageRank
Susanna F. de Rezende1134.35
Mika Göös200.34
Jakob Nordström317721.76
Toniann Pitassi400.34
Robert Robere502.03
Dmitry Sokolov677.85