2 Search Results for "Alekseev, Yaroslav"

Document

DOI: 10.4230/LIPIcs.CCC.2021.21

A Lower Bound for Polynomial Calculus with Extension Rule

Authors: Yaroslav Alekseev

Published in: LIPIcs, Volume 200, 36th Computational Complexity Conference (CCC 2021)

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.

Cite as

Yaroslav Alekseev. A Lower Bound for Polynomial Calculus with Extension Rule. In 36th Computational Complexity Conference (CCC 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 200, pp. 21:1-21:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2021.21},
  URN =		{urn:nbn:de:0030-drops-142959},
  doi =		{10.4230/LIPIcs.CCC.2021.21},
  annote =	{Keywords: proof complexity, algebraic proofs, polynomial calculus}
}

Document

Invited Talk

DOI: 10.4230/LIPIcs.ICALP.2021.5

Algebraic Proof Systems (Invited Talk)

Authors: Toniann Pitassi

Published in: LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)

Abstract

Given a set of polynomial equations over a field F, how hard is it to prove that they are simultaneously unsolvable? In the last twenty years, algebraic proof systems for refuting such systems of equations have been extensively studied, revealing close connections to both upper bounds (connections between short refutations and efficient approximation algorithms) and lower bounds (connections to fundamental questions in circuit complexity.) The Ideal Proof System (IPS) is a simple yet powerful algebraic proof system, with very close connections to circuit lower bounds: [Joshua A. Grochow and Toniann Pitassi, 2018] proved that lower bounds for IPS imply VNP ≠ VP, and very recently connections in the other direction have been made, showing that circuit lower bounds imply IPS lower bounds [Rahul Santhanam and Iddo Tzameret, 2021; Yaroslav Alekseev et al., 2020]. In this talk I will survey the landscape of algebraic proof systems, focusing on their connections to complexity theory, derandomization, and standard proposional proof complexity. I will discuss the state-of-the-art lower bounds, as well as the relationship between algebraic systems and textbook style propositional proof systems. Finally we end with open problems, and some recent progress towards proving superpolynomial lower bounds for bounded-depth Frege systems with modular gates (a major open problem in propositional proof complexity).

Cite as

Toniann Pitassi. Algebraic Proof Systems (Invited Talk). In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, p. 5:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{pitassi:LIPIcs.ICALP.2021.5,
  author =	{Pitassi, Toniann},
  title =	{{Algebraic Proof Systems}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{5:1--5:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.5},
  URN =		{urn:nbn:de:0030-drops-140747},
  doi =		{10.4230/LIPIcs.ICALP.2021.5},
  annote =	{Keywords: complexity theory, proof complexity, algebraic circuits}
}

Refine by Author
1 Alekseev, Yaroslav
1 Pitassi, Toniann

Refine by Classification
2 Theory of computation → Proof complexity
1 Theory of computation → Algebraic complexity theory
1 Theory of computation → Circuit complexity

Refine by Keyword
2 proof complexity
1 algebraic circuits
1 algebraic proofs
1 complexity theory
1 polynomial calculus

Refine by Type
2 document

Refine by Publication Year
2 2021

2 Search Results for "Alekseev, Yaroslav"

A Lower Bound for Polynomial Calculus with Extension Rule

Abstract

Cite as

Algebraic Proof Systems (Invited Talk)

Abstract

Cite as

Thanks for your feedback!

Could not send message