Automating algebraic proof systems is NP-hard

Susanna F. De Rezende; Mika Göös; Jakob Nordström; Toniann Pitassi; Robert Robere; Dmitry Sokolov

doi:10.1145/3406325.3451080

Automating algebraic proof systems is NP-hard

Susanna F. De Rezende, Mika Göös, Jakob Nordström, Toniann Pitassi, Robert Robere, Dmitry Sokolov

Algorithms and Complexity

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › peer review

10 Citationer (Scopus)

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üller (JACM 2020) that established an analogous result for Resolution.

Originalsprog	Engelsk
Titel	STOC 2021 - Proceedings of the 53rd Annual ACM SIGACT Symposium on Theory of Computing
Redaktører	Samir Khuller, Virginia Vassilevska Williams
Forlag	Association for Computing Machinery, Inc.
Publikationsdato	2021
Sider	209-222
ISBN (Elektronisk)	9781450380539
DOI	https://doi.org/10.1145/3406325.3451080
Status	Udgivet - 2021
Begivenhed	53rd Annual ACM SIGACT Symposium on Theory of Computing, STOC 2021 - Virtual, Online, Italien Varighed: 21 jun. 2021 → 25 jun. 2021

Konference

Konference	53rd Annual ACM SIGACT Symposium on Theory of Computing, STOC 2021
Land/Område	Italien
By	Virtual, Online
Periode	21/06/2021 → 25/06/2021
Sponsor	ACM Special Interest Group on Algorithms and Computation Theory (SIGACT)

Bibliografisk note

Funding Information:
Susanna F. de Rezende was supported by Knut and Alice Wal-lenberg grant KAW 2018.0371. Jakob Nordström received funding from the Swedish Research Council grant 2016-00782 and the Independent Research Fund Denmark grant 9040-00389B. Toniann Pitassi did this work supported by NSERC and NSF Grant CCF-1900460. Robert Robere was supported by NSERC, the Charles Simonyi Endowment, and indirectly supported by the National Science Foundation Grant No. CCF-1900460. This material is based on work supported by NSERC and NSF Grant CCF-1900460. Any opinions, findings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.

Publisher Copyright:
© 2021 ACM.

Adgang til dokumentet

10.1145/3406325.3451080

Citationsformater

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. red. / Samir Khuller; Virginia Vassilevska Williams. Association for Computing Machinery, Inc., 2021. s. 209-222.

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › peer review

De Rezende, SF, Göös, M, Nordström, J, Pitassi, T, Robere, R & Sokolov, D 2021, Automating algebraic proof systems is NP-hard. i S Khuller & VV Williams (red), STOC 2021 - Proceedings of the 53rd Annual ACM SIGACT Symposium on Theory of Computing. Association for Computing Machinery, Inc., s. 209-222, 53rd Annual ACM SIGACT Symposium on Theory of Computing, STOC 2021, Virtual, Online, Italien, 21/06/2021. https://doi.org/10.1145/3406325.3451080

@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.",

}

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

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 -