文章基本信息

标题：Trade-Offs Between Size and Degree in Polynomial Calculus
本地全文：下载
作者：Guillaume Lagarde ; Jakob Nordstr{"o}m ; Dmitry Sokolov 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2020
卷号：151
页码：1-16
DOI：10.4230/LIPIcs.ITCS.2020.72
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：Building on [Clegg et al. '96], [Impagliazzo et al. '99] established that if an unsatisfiable k-CNF formula over n variables has a refutation of size S in the polynomial calculus resolution proof system, then this formula also has a refutation of degree k + O(â^S(n log S)). The proof of this works by converting a small-size refutation into a small-degree one, but at the expense of increasing the proof size exponentially. This raises the question of whether it is possible to achieve both small size and small degree in the same refutation, or whether the exponential blow-up is inherent. Using and extending ideas from [Thapen '16], who studied the analogous question for the resolution proof system, we prove that a strong size-degree trade-off is necessary.
关键词：proof complexity; polynomial calculus; polynomial calculus resolution; PCR; size-degree trade-off; resolution; colored polynomial local search