Ссылки

DOI

  • Ярослав Алексеев

A major proof complexity problem is to prove a superpolynomial lower bound on the length of Frege proofs of arbitrary depth. A more general question is to prove an Extended Frege lower bound. Surprisingly, proving such bounds turns out to be much easier in the algebraic setting. In this paper, we study a proof system that can simulate Extended Frege: an extension of the Polynomial Calculus proof system where we can take a square root and introduce new variables that are equivalent to arbitrary depth algebraic circuits. We prove that an instance of the subset-sum principle, the binary value principle 1 + x1 + 2x2 +... + 2 n1xn = 0 (BVPn), requires refutations of exponential bit size over Q in this system. Part and Tzameret [18] proved an exponential lower bound on the size of Res-Lin (Resolution over linear equations [22]) refutations of BVPn. We show that our system p-simulates Res-Lin and thus we get an alternative exponential lower bound for the size of Res-Lin refutations of BVPn.

Язык оригиналаанглийский
Название основной публикации36th Computational Complexity Conference (CCC 2021)
РедакторыValentine Kabanets
Место публикацииDagstuhl, Germany
ИздательSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Страницы21:1-21:18
Число страниц18
Том200
ISBN (электронное издание)9783959771931
ISBN (печатное издание)978-3-95977-193-1
DOI
СостояниеОпубликовано - 1 июл 2021
Событие36th Computational Complexity Conference, CCC 2021 - Virtual, Toronto, Канада
Продолжительность: 20 июл 202123 июл 2021

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

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

конференция

конференция36th Computational Complexity Conference, CCC 2021
Страна/TерриторияКанада
ГородVirtual, Toronto
Период20/07/2123/07/21

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

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

ID: 84894589