Trade-offs between size and degree in polynomial calculus

Forskningsoutput: Kapitel i bok/rapport/Conference proceedingKonferenspaper i proceeding

Abstract

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.

Detaljer

Författare
Enheter & grupper
Externa organisationer
  • University of Bordeaux
  • University of Copenhagen
  • KTH Royal Institute of Technology
Forskningsområden

Ämnesklassifikation (UKÄ) – OBLIGATORISK

  • Datavetenskap (datalogi)

Nyckelord

Originalspråkengelska
Titel på värdpublikation11th Innovations in Theoretical Computer Science Conference, ITCS 2020
RedaktörerThomas Vidick
FörlagSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (elektroniskt)9783959771344
StatusPublished - 2020 jan
PublikationskategoriForskning
Peer review utfördJa
Evenemang11th Innovations in Theoretical Computer Science Conference, ITCS 2020 - Seattle, USA
Varaktighet: 2020 jan 122020 jan 14

Publikationsserier

NamnLeibniz International Proceedings in Informatics, LIPIcs
Förlag Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Volym151
ISSN (tryckt)1868-8969

Konferens

Konferens11th Innovations in Theoretical Computer Science Conference, ITCS 2020
LandUSA
OrtSeattle
Period2020/01/122020/01/14