Trade-offs between size and degree in polynomial calculus

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Documents

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.

Original languageEnglish
Title of host publication11th Innovations in Theoretical Computer Science Conference, ITCS 2020
EditorsThomas Vidick
PublisherSchloss Dagstuhl - Leibniz-Zentrum für Informatik
Publication dateJan 2020
Pages1-16
Article number72
ISBN (Electronic)9783959771344
DOIs
Publication statusPublished - Jan 2020
Event11th Innovations in Theoretical Computer Science Conference, ITCS 2020 - Seattle, United States
Duration: 12 Jan 202014 Jan 2020

Conference

Conference11th Innovations in Theoretical Computer Science Conference, ITCS 2020
LandUnited States
BySeattle
Periode12/01/202014/01/2020
SeriesLeibniz International Proceedings in Informatics, LIPIcs
Volume151
ISSN1868-8969

    Research areas

  • Colored polynomial local search, PCR, Polynomial calculus, Polynomial calculus resolution, Proof complexity, Resolution, Size-degree trade-off

ID: 251867228