DOI

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.

Язык оригиналаанглийский
Название основной публикации11th Innovations in Theoretical Computer Science Conference, ITCS 2020
РедакторыThomas Vidick
ИздательSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (электронное издание)9783959771344
ISBN (печатное издание)9783959771344
DOI
СостояниеОпубликовано - янв 2020
Опубликовано для внешнего пользованияДа
Событие11th Innovations in Theoretical Computer Science Conference, ITCS 2020 - Seattle, Соединенные Штаты Америки
Продолжительность: 12 янв 202014 янв 2020

Серия публикаций

НазваниеLeibniz International Proceedings in Informatics, LIPIcs
Том151
ISSN (печатное издание)1868-8969

конференция

конференция11th Innovations in Theoretical Computer Science Conference, ITCS 2020
Страна/TерриторияСоединенные Штаты Америки
ГородSeattle
Период12/01/2014/01/20

    Предметные области Scopus

  • Программный продукт

ID: 51953946