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

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

12 Citations (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.

Original language	English
Title of host publication	STOC 2021 - Proceedings of the 53rd Annual ACM SIGACT Symposium on Theory of Computing
Editors	Samir Khuller, Virginia Vassilevska Williams
Publisher	Association for Computing Machinery, Inc.
Publication date	2021
Pages	209-222
ISBN (Electronic)	9781450380539
DOIs	https://doi.org/10.1145/3406325.3451080
Publication status	Published - 2021
Event	53rd Annual ACM SIGACT Symposium on Theory of Computing, STOC 2021 - Virtual, Online, Italy Duration: 21 Jun 2021 → 25 Jun 2021

Conference

Conference	53rd Annual ACM SIGACT Symposium on Theory of Computing, STOC 2021
Country/Territory	Italy
City	Virtual, Online
Period	21/06/2021 → 25/06/2021
Sponsor	ACM Special Interest Group on Algorithms and Computation Theory (SIGACT)

Bibliographical note

Publisher Copyright:
© 2021 ACM.

Keywords

algebraic proof systems
automatability
lower bounds
pigeonhole principle
proof complexity

Access to Document

10.1145/3406325.3451080

Cite this

Automating algebraic proof systems is NP-hard. / De Rezende, Susanna F.; Göös, Mika; Nordström, Jakob et al.
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

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.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 -