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, 2021. p. 209-222 (Proceedings of the Annual ACM Symposium on Theory of Computing).
Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › 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. Proceedings of the Annual ACM Symposium on Theory of Computing, Association for Computing Machinery, pp. 209-222, 53rd Annual ACM SIGACT Symposium on Theory of Computing, STOC 2021, Virtual, Online, Italy,
21/06/21.
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). (Proceedings of the Annual ACM Symposium on Theory of Computing). Association for Computing Machinery.
https://doi.org/10.1145/3406325.3451080Vancouver
Author
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, 2021. pp. 209-222 (Proceedings of the Annual ACM Symposium on Theory of Computing).
BibTeX
@inproceedings{8003246146c74da7adc6d8735b872778,
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",
month = jun,
day = "15",
doi = "10.1145/3406325.3451080",
language = "English",
series = "Proceedings of the Annual ACM Symposium on Theory of Computing",
publisher = "Association for Computing Machinery",
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",
}
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/6/15
Y1 - 2021/6/15
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
UR - http://www.scopus.com/inward/record.url?scp=85108167467&partnerID=8YFLogxK
UR - https://www.mendeley.com/catalogue/99429387-26ea-39e1-bef3-56631e16341d/
U2 - 10.1145/3406325.3451080
DO - 10.1145/3406325.3451080
M3 - Conference contribution
AN - SCOPUS:85108167467
T3 - Proceedings of the Annual ACM Symposium on Theory of Computing
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
T2 - 53rd Annual ACM SIGACT Symposium on Theory of Computing, STOC 2021
Y2 - 21 June 2021 through 25 June 2021
ER -
