Automating algebraic proof systems is NP-hard
Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
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 | |
| 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 |
|---|---|
| Land | Italy |
| By | Virtual, Online |
| Periode | 21/06/2021 → 25/06/2021 |
| Sponsor | ACM Special Interest Group on Algorithms and Computation Theory (SIGACT) |
Bibliographical note
Publisher Copyright:
© 2021 ACM.
- algebraic proof systems, automatability, lower bounds, pigeonhole principle, proof complexity
Research areas
ID: 306691377