2026-07-24T08:01:25Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:11757 2024-03-06T10:48:38Z ddc:004 open_access

Trade-Offs Between Size and Degree in Polynomial Calculus Lagarde, Guillaume Nordström, Jakob Sokolov, Dmitry Swernofsky, Joseph proof complexity polynomial calculus polynomial calculus resolution PCR size-degree trade-off resolution colored polynomial local search 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(√(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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Guillaume Lagarde and Jakob Nordström and Dmitry Sokolov and Joseph Swernofsky 2020 Is Part Of LIPIcs, Volume 151, 11th Innovations in Theoretical Computer Science Conference (ITCS 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITCS.2020.72 urn:nbn:de:0030-drops-117573 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2020.72 eng https://creativecommons.org/licenses/by/3.0/legalcode