Automating algebraic proof systems is NP-hard

Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningfagfællebedømt

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

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.

OriginalsprogEngelsk
TitelSTOC 2021 - Proceedings of the 53rd Annual ACM SIGACT Symposium on Theory of Computing
RedaktørerSamir Khuller, Virginia Vassilevska Williams
ForlagAssociation for Computing Machinery, Inc.
Publikationsdato2021
Sider209-222
ISBN (Elektronisk)9781450380539
DOI
StatusUdgivet - 2021
Begivenhed53rd Annual ACM SIGACT Symposium on Theory of Computing, STOC 2021 - Virtual, Online, Italien
Varighed: 21 jun. 202125 jun. 2021

Konference

Konference53rd Annual ACM SIGACT Symposium on Theory of Computing, STOC 2021
LandItalien
ByVirtual, Online
Periode21/06/202125/06/2021
SponsorACM 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.

ID: 306691377