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. ред. / Samir Khuller; Virginia Vassilevska Williams. Association for Computing Machinery, 2021. стр. 209-222 (Proceedings of the Annual ACM Symposium on Theory of Computing).

Результаты исследований: Публикации в книгах, отчётах, сборниках, трудах конференций › статья в сборнике материалов конференции › Рецензирование

Harvard

De Rezende, SF, Göös, M, Nordström, J, Pitassi, T, Robere, R & Sokolov, D 2021, Automating algebraic proof systems is NP-hard. в S Khuller & VV Williams (ред.), 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, стр. 209-222, 53rd Annual ACM SIGACT Symposium on Theory of Computing, STOC 2021, Virtual, Online, Италия, 21/06/21. https://doi.org/10.1145/3406325.3451080

APA

De Rezende, S. F., Göös, M., Nordström, J., Pitassi, T., Robere, R., & Sokolov, D. (2021). Automating algebraic proof systems is NP-hard. в S. Khuller, & V. V. Williams (Ред.), STOC 2021 - Proceedings of the 53rd Annual ACM SIGACT Symposium on Theory of Computing (стр. 209-222). (Proceedings of the Annual ACM Symposium on Theory of Computing). Association for Computing Machinery. https://doi.org/10.1145/3406325.3451080

Vancouver

De Rezende SF, Göös M, Nordström J, Pitassi T, Robere R, Sokolov D. Automating algebraic proof systems is NP-hard. в Khuller S, Williams VV, Редакторы, STOC 2021 - Proceedings of the 53rd Annual ACM SIGACT Symposium on Theory of Computing. Association for Computing Machinery. 2021. стр. 209-222. (Proceedings of the Annual ACM Symposium on Theory of Computing). https://doi.org/10.1145/3406325.3451080

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. Редактор / Samir Khuller ; Virginia Vassilevska Williams. Association for Computing Machinery, 2021. стр. 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 -

ID: 84277175