Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Research › peer-review
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.
| Original language | English |
|---|---|
| Title of host publication | 36th Computational Complexity Conference (CCC 2021) |
| Editors | Valentine Kabanets |
| Place of Publication | Dagstuhl, Germany |
| Publisher | Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing |
| Pages | 21:1-21:18 |
| Number of pages | 18 |
| Volume | 200 |
| ISBN (Electronic) | 9783959771931 |
| ISBN (Print) | 978-3-95977-193-1 |
| DOIs | |
| State | Published - 1 Jul 2021 |
| Event | 36th Computational Complexity Conference, CCC 2021 - Virtual, Toronto, Canada Duration: 20 Jul 2021 → 23 Jul 2021 |
| Name | Leibniz International Proceedings in Informatics, LIPIcs |
|---|---|
| Volume | 200 |
| ISSN (Print) | 1868-8969 |
| Conference | 36th Computational Complexity Conference, CCC 2021 |
|---|---|
| Country/Territory | Canada |
| City | Virtual, Toronto |
| Period | 20/07/21 → 23/07/21 |
ID: 84894589