Automating algebraic proof systems is NP-hard

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

Research output: Chapter in Book/Report/Conference proceedingConference contributionResearchpeer-review

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 languageEnglish
Title of host publicationSTOC 2021 - Proceedings of the 53rd Annual ACM SIGACT Symposium on Theory of Computing
EditorsSamir Khuller, Virginia Vassilevska Williams
PublisherAssociation for Computing Machinery
Pages209-222
Number of pages14
ISBN (Electronic)9781450380539
DOIs
StatePublished - 15 Jun 2021
Event53rd Annual ACM SIGACT Symposium on Theory of Computing, STOC 2021 - Virtual, Online, Italy
Duration: 21 Jun 202125 Jun 2021

Publication series

NameProceedings of the Annual ACM Symposium on Theory of Computing
ISSN (Print)0737-8017

Conference

Conference53rd Annual ACM SIGACT Symposium on Theory of Computing, STOC 2021
Country/TerritoryItaly
CityVirtual, Online
Period21/06/2125/06/21

Scopus subject areas

  • Software

Keywords

  • algebraic proof systems
  • automatability
  • lower bounds
  • pigeonhole principle
  • proof complexity

Fingerprint

Dive into the research topics of 'Automating algebraic proof systems is NP-hard'. Together they form a unique fingerprint.

Cite this