Automating Algebraic Proof Systems is NP-Hard
Research output: Working paper › Research
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.
Original language | English |
---|---|
Publisher | Electronic Colloquium on Computational Complexity |
Number of pages | 34 |
Publication status | Published - 1 May 2020 |
Links
- https://eccc.weizmann.ac.il/report/2020/064/
Final published version
ID: 251872387