License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CCC.2021.21
URN: urn:nbn:de:0030-drops-142959
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/14295/
Go to the corresponding LIPIcs Volume Portal

Alekseev, Yaroslav

A Lower Bound for Polynomial Calculus with Extension Rule

pdf-format:
LIPIcs-CCC-2021-21.pdf (0.8 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{alekseev:LIPIcs.CCC.2021.21,
  author =	{Alekseev, Yaroslav},
  title =	{{A Lower Bound for Polynomial Calculus with Extension Rule}},
  booktitle =	{36th Computational Complexity Conference (CCC 2021)},
  pages =	{21:1--21:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-193-1},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{200},
  editor =	{Kabanets, Valentine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/14295},
  URN =		{urn:nbn:de:0030-drops-142959},
  doi =		{10.4230/LIPIcs.CCC.2021.21},
  annote =	{Keywords: proof complexity, algebraic proofs, polynomial calculus}
}

Keywords: proof complexity, algebraic proofs, polynomial calculus
Collection: 36th Computational Complexity Conference (CCC 2021)
Issue Date: 2021
Date of publication: 08.07.2021

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI