@inproceedings{507bd8d5742540489c534dec51f53d11,
title = "Automating algebraic proof systems is NP-hard",
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 M{\"u}ller (JACM 2020) that established an analogous result for Resolution. ",
keywords = "algebraic proof systems, automatability, lower bounds, pigeonhole principle, proof complexity",
author = "{De Rezende}, {Susanna F.} and Mika G{\"o}{\"o}s and Jakob Nordstr{\"o}m and Toniann Pitassi and Robert Robere and Dmitry Sokolov",
year = "2021",
doi = "10.1145/3406325.3451080",
language = "English",
series = "Proceedings of the Annual ACM Symposium on Theory of Computing",
publisher = "Association for Computing Machinery (ACM)",
pages = "209--222",
editor = "Samir Khuller and Williams, {Virginia Vassilevska}",
booktitle = "STOC 2021 - Proceedings of the 53rd Annual ACM SIGACT Symposium on Theory of Computing",
address = "United States",
note = "53rd Annual ACM SIGACT Symposium on Theory of Computing, STOC 2021 ; Conference date: 21-06-2021 Through 25-06-2021",
}