Standard
Automating algebraic proof systems is NP-hard. / De Rezende, Susanna F.; Göös, Mika; Nordström, Jakob; Pitassi, Toniann; Robere, Robert; Sokolov, Dmitry.
STOC 2021 - Proceedings of the 53rd Annual ACM SIGACT Symposium on Theory of Computing. ed. / Samir Khuller; Virginia Vassilevska Williams. Association for Computing Machinery, Inc., 2021. p. 209-222.
Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Harvard
De Rezende, SF, Göös, M
, Nordström, J, Pitassi, T, Robere, R & Sokolov, D 2021,
Automating algebraic proof systems is NP-hard. in S Khuller & VV Williams (eds),
STOC 2021 - Proceedings of the 53rd Annual ACM SIGACT Symposium on Theory of Computing. Association for Computing Machinery, Inc., pp. 209-222, 53rd Annual ACM SIGACT Symposium on Theory of Computing, STOC 2021, Virtual, Online, Italy,
21/06/2021.
https://doi.org/10.1145/3406325.3451080APA
De Rezende, S. F., Göös, M.
, Nordström, J., Pitassi, T., Robere, R., & Sokolov, D. (2021).
Automating algebraic proof systems is NP-hard. In S. Khuller, & V. V. Williams (Eds.),
STOC 2021 - Proceedings of the 53rd Annual ACM SIGACT Symposium on Theory of Computing (pp. 209-222). Association for Computing Machinery, Inc..
https://doi.org/10.1145/3406325.3451080Vancouver
De Rezende SF, Göös M
, Nordström J, Pitassi T, Robere R, Sokolov D.
Automating algebraic proof systems is NP-hard. In Khuller S, Williams VV, editors, STOC 2021 - Proceedings of the 53rd Annual ACM SIGACT Symposium on Theory of Computing. Association for Computing Machinery, Inc. 2021. p. 209-222
https://doi.org/10.1145/3406325.3451080Author
De Rezende, Susanna F. ; Göös, Mika ; Nordström, Jakob ; Pitassi, Toniann ; Robere, Robert ; Sokolov, Dmitry. / Automating algebraic proof systems is NP-hard. STOC 2021 - Proceedings of the 53rd Annual ACM SIGACT Symposium on Theory of Computing. editor / Samir Khuller ; Virginia Vassilevska Williams. Association for Computing Machinery, Inc., 2021. pp. 209-222
Bibtex
@inproceedings{4c952b6e0bae438f9bcaa33d5e946ba9,
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",
note = "Publisher Copyright: {\textcopyright} 2021 ACM.; 53rd Annual ACM SIGACT Symposium on Theory of Computing, STOC 2021 ; Conference date: 21-06-2021 Through 25-06-2021",
year = "2021",
doi = "10.1145/3406325.3451080",
language = "English",
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",
publisher = "Association for Computing Machinery, Inc.",
}
RIS
TY - GEN
T1 - Automating algebraic proof systems is NP-hard
AU - De Rezende, Susanna F.
AU - Göös, Mika
AU - Nordström, Jakob
AU - Pitassi, Toniann
AU - Robere, Robert
AU - Sokolov, Dmitry
N1 - Publisher Copyright:
© 2021 ACM.
PY - 2021
Y1 - 2021
N2 - 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üller (JACM 2020) that established an analogous result for Resolution.
AB - 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üller (JACM 2020) that established an analogous result for Resolution.
KW - algebraic proof systems
KW - automatability
KW - lower bounds
KW - pigeonhole principle
KW - proof complexity
U2 - 10.1145/3406325.3451080
DO - 10.1145/3406325.3451080
M3 - Article in proceedings
AN - SCOPUS:85108167467
SP - 209
EP - 222
BT - STOC 2021 - Proceedings of the 53rd Annual ACM SIGACT Symposium on Theory of Computing
A2 - Khuller, Samir
A2 - Williams, Virginia Vassilevska
PB - Association for Computing Machinery, Inc.
T2 - 53rd Annual ACM SIGACT Symposium on Theory of Computing, STOC 2021
Y2 - 21 June 2021 through 25 June 2021
ER -
