Automating Algebraic Proof Systems is NP-Hard
Publikation: Working paper › Forskning
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.
Originalsprog | Engelsk |
---|---|
Udgiver | Electronic Colloquium on Computational Complexity |
Antal sider | 34 |
Status | Udgivet - 1 maj 2020 |
Links
- https://eccc.weizmann.ac.il/report/2020/064/
Forlagets udgivne version
ID: 251872387