文章基本信息

标题：Automating Algebraic Proof Systems is NP-Hard
本地全文：下载
作者：Mika Göös ; Jakob Nordström ; Toniann Pitassi 等
期刊名称：Electronic Colloquium on Computational Complexity
印刷版ISSN：1433-8092
出版年度：2020
卷号：2020
页码：1-30
出版社：Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
摘要：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¨uller (FOCS 2019) that established an analogous result for Resolution.