2026-10-04T05:22:28Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:14295 2024-03-06T09:53:54Z ddc:004 open_access

A Lower Bound for Polynomial Calculus with Extension Rule Alekseev, Yaroslav proof complexity algebraic proofs polynomial calculus 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 + x₁ + 2 x₂ + … + 2^{n-1} x_n = 0 (BVP_n), requires refutations of exponential bit size over ℚ in this system. Part and Tzameret [Fedor Part and Iddo Tzameret, 2020] proved an exponential lower bound on the size of Res-Lin (Resolution over linear equations [Ran Raz and Iddo Tzameret, 2008]) refutations of BVP_n. 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 BVP_n. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Yaroslav Alekseev 2021 Is Part Of LIPIcs, Volume 200, 36th Computational Complexity Conference (CCC 2021) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CCC.2021.21 urn:nbn:de:0030-drops-142959 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2021.21 eng https://creativecommons.org/licenses/by/4.0/legalcode