Standard
Automating Algebraic Proof Systems is NP-Hard. / de Rezende, Susanna F.; Göös, Mika; Nordström, Jakob; Pitassi, Toniann; Robere, Robert; Sokolov, Dmitry.
Electronic Colloquium on Computational Complexity, 2020.
Research output: Working paper › Research
Harvard
de Rezende, SF, Göös, M
, Nordström, J, Pitassi, T, Robere, R & Sokolov, D 2020 '
Automating Algebraic Proof Systems is NP-Hard' Electronic Colloquium on Computational Complexity. <
https://eccc.weizmann.ac.il/report/2020/064/>
APA
de Rezende, S. F., Göös, M.
, Nordström, J., Pitassi, T., Robere, R., & Sokolov, D. (2020).
Automating Algebraic Proof Systems is NP-Hard. Electronic Colloquium on Computational Complexity.
https://eccc.weizmann.ac.il/report/2020/064/Vancouver
de Rezende SF, Göös M, Nordström J, Pitassi T, Robere R, Sokolov D. Automating Algebraic Proof Systems is NP-Hard. Electronic Colloquium on Computational Complexity. 2020 May 1.
Author
de Rezende, Susanna F. ; Göös, Mika ; Nordström, Jakob ; Pitassi, Toniann ; Robere, Robert ; Sokolov, Dmitry. / Automating Algebraic Proof Systems is NP-Hard. Electronic Colloquium on Computational Complexity, 2020.
Bibtex
@techreport{706a9771b323491a9204b914bb4e775c,
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 Muller (JACM 2020) that established an analogous result for Resolution.",
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",
year = "2020",
month = may,
day = "1",
language = "English",
publisher = "Electronic Colloquium on Computational Complexity",
type = "WorkingPaper",
institution = "Electronic Colloquium on Computational Complexity",
}
RIS
TY - UNPB
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 - 2020/5/1
Y1 - 2020/5/1
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 Muller (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 Muller (JACM 2020) that established an analogous result for Resolution.
M3 - Working paper
BT - Automating Algebraic Proof Systems is NP-Hard
PB - Electronic Colloquium on Computational Complexity
ER -
