Результаты исследований: Публикации в книгах, отчётах, сборниках, трудах конференций › статья в сборнике материалов конференции › Рецензирование
A Lower Bound for Polynomial Calculus with Extension Rule. / Алексеев, Ярослав.
36th Computational Complexity Conference (CCC 2021). ред. / Valentine Kabanets. Том 200 Dagstuhl, Germany : Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2021. стр. 21:1-21:18 21 (Leibniz International Proceedings in Informatics, LIPIcs; Том 200).Результаты исследований: Публикации в книгах, отчётах, сборниках, трудах конференций › статья в сборнике материалов конференции › Рецензирование
}
TY - GEN
T1 - A Lower Bound for Polynomial Calculus with Extension Rule
AU - Алексеев, Ярослав
N1 - Publisher Copyright: © Yaroslav Alekseev; licensed under Creative Commons License CC-BY 4.0
PY - 2021/7/1
Y1 - 2021/7/1
N2 - 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 n− 1xn = 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.
AB - 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 n− 1xn = 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.
KW - proof complexity
KW - algebraic proofs
KW - polynomial calculus
KW - Algebraic proofs
KW - Proof complexity
KW - Polynomial calculus
UR - http://www.scopus.com/inward/record.url?scp=85115327553&partnerID=8YFLogxK
UR - https://www.mendeley.com/catalogue/227aac05-81ef-3896-888e-08350304fe4e/
U2 - 10.4230/LIPIcs.CCC.2021.21
DO - 10.4230/LIPIcs.CCC.2021.21
M3 - Conference contribution
SN - 978-3-95977-193-1
VL - 200
T3 - Leibniz International Proceedings in Informatics, LIPIcs
SP - 21:1-21:18
BT - 36th Computational Complexity Conference (CCC 2021)
A2 - Kabanets, Valentine
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
CY - Dagstuhl, Germany
T2 - 36th Computational Complexity Conference, CCC 2021
Y2 - 20 July 2021 through 23 July 2021
ER -
ID: 84894589