1. |
- De Rezende, Susanna F., et al.
(author)
-
Automating algebraic proof systems is NP-hard
- 2021
-
In: STOC 2021 - Proceedings of the 53rd Annual ACM SIGACT Symposium on Theory of Computing. - New York, NY, USA : ACM. - 0737-8017. - 9781450380539 ; , s. 209-222
-
Conference paper (peer-reviewed)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.
|
|
2. |
- Garg, Ankit, et al.
(author)
-
Monotone Circuit Lower Bounds from Resolution
- 2020
-
In: Theory of Computing. - : Theory of Computing Exchange. - 1557-2862. ; 16
-
Journal article (peer-reviewed)abstract
- For any unsatisfiable CNF formula F that is hard to refute in the Resolution proof system, we show that a gadget-composed version of F is hard to refute in any proof system whose lines are computed by efficient communication protocols-or, equivalently, that a monotone function associated with F has large monotone circuit complexity. Our result extends to monotone real circuits, which yields new lower bounds for the Cutting Planes proof system.
|
|