TY - GEN

T1 - Automating algebraic proof systems is NP-hard

AU - De Rezende, Susanna F.

AU - Göös, Mika

AU - Nordström, Jakob

AU - Pitassi, Toniann

AU - Robere, Robert

AU - Sokolov, Dmitry

N1 - Publisher Copyright:
© 2021 ACM.

PY - 2021/6/15

Y1 - 2021/6/15

N2 - 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.

AB - 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.

KW - algebraic proof systems

KW - automatability

KW - lower bounds

KW - pigeonhole principle

KW - proof complexity

UR - http://www.scopus.com/inward/record.url?scp=85108167467&partnerID=8YFLogxK

U2 - 10.1145/3406325.3451080

DO - 10.1145/3406325.3451080

M3 - Conference contribution

AN - SCOPUS:85108167467

T3 - Proceedings of the Annual ACM Symposium on Theory of Computing

SP - 209

EP - 222

BT - STOC 2021 - Proceedings of the 53rd Annual ACM SIGACT Symposium on Theory of Computing

A2 - Khuller, Samir

A2 - Williams, Virginia Vassilevska

PB - Association for Computing Machinery

T2 - 53rd Annual ACM SIGACT Symposium on Theory of Computing, STOC 2021

Y2 - 21 June 2021 through 25 June 2021

ER -