Skip to main content

Lund University Publications

LUND UNIVERSITY LIBRARIES

Automating algebraic proof systems is NP-hard

De Rezende, Susanna F. LU orcid ; Göös, Mika ; Nordström, Jakob LU ; Pitassi, Toniann ; Robere, Robert and Sokolov, Dmitry LU (2021) 53rd Annual ACM SIGACT Symposium on Theory of Computing, STOC 2021 In Proceedings of the Annual ACM Symposium on Theory of Computing p.209-222
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.

Please use this url to cite or link to this publication:
author
; ; ; ; and
organization
publishing date
type
Chapter in Book/Report/Conference proceeding
publication status
published
subject
keywords
algebraic proof systems, automatability, lower bounds, pigeonhole principle, proof complexity
host publication
STOC 2021 - Proceedings of the 53rd Annual ACM SIGACT Symposium on Theory of Computing
series title
Proceedings of the Annual ACM Symposium on Theory of Computing
editor
Khuller, Samir and Williams, Virginia Vassilevska
pages
14 pages
publisher
Association for Computing Machinery (ACM)
conference name
53rd Annual ACM SIGACT Symposium on Theory of Computing, STOC 2021
conference location
Virtual, Online, Italy
conference dates
2021-06-21 - 2021-06-25
external identifiers
  • scopus:85108167467
ISSN
0737-8017
ISBN
9781450380539
DOI
10.1145/3406325.3451080
language
English
LU publication?
yes
id
507bd8d5-7425-4048-9c53-4dec51f53d11
date added to LUP
2021-07-15 13:38:44
date last changed
2025-10-14 09:52:20
@inproceedings{507bd8d5-7425-4048-9c53-4dec51f53d11,
  abstract     = {{<p>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. </p>}},
  author       = {{De Rezende, Susanna F. and Göös, Mika and Nordström, Jakob and Pitassi, Toniann and Robere, Robert and Sokolov, Dmitry}},
  booktitle    = {{STOC 2021 - Proceedings of the 53rd Annual ACM SIGACT Symposium on Theory of Computing}},
  editor       = {{Khuller, Samir and Williams, Virginia Vassilevska}},
  isbn         = {{9781450380539}},
  issn         = {{0737-8017}},
  keywords     = {{algebraic proof systems; automatability; lower bounds; pigeonhole principle; proof complexity}},
  language     = {{eng}},
  pages        = {{209--222}},
  publisher    = {{Association for Computing Machinery (ACM)}},
  series       = {{Proceedings of the Annual ACM Symposium on Theory of Computing}},
  title        = {{Automating algebraic proof systems is NP-hard}},
  url          = {{http://dx.doi.org/10.1145/3406325.3451080}},
  doi          = {{10.1145/3406325.3451080}},
  year         = {{2021}},
}