ECCC-Report TR22-176https://eccc.weizmann.ac.il/report/2022/176Comments and Revisions published for TR22-176en-usSun, 04 Dec 2022 06:21:35 +0200
Paper TR22-176
| The power of the Binary Value Principle |
Yaroslav Alekseev,
Edward Hirsch
https://eccc.weizmann.ac.il/report/2022/176The (extended) Binary Value Principle (eBVP, the equation $\sum x_i 2^{i-1} = -k$ for $k > 0$
and in the presence of $x_i^2=x_i$) has received a lot of attention recently, several lower
bounds have been proved for it [Alekseev et al 20, Alekseev 21, Part and Tzameret 21].
Also it has been shown [Alekseev et al 20] that the
probabilistically verifiable Ideal Proof System (IPS) [Grochow and Pitassi 18] together with eBVP
polynomially simulates a similar semialgebraic proof system. In this paper we consider
Polynomial Calculus with the algebraic version of Tseitinâ€™s extension rule (Ext-PC). Contrary
to IPS, this is a Cook--Reckhow proof system. We show that in this context eBVP still allows
to simulate similar semialgebraic systems. We also prove that it allows to simulate the
Square Root Rule [Grigoriev and Hirsch 03], which is in sharp contrast with the result of [Alekseev 21] that shows
an exponential lower bound on the size of Ext-PC derivations of the Binary Value Principle
from its square. On the other hand, we demonstrate that eBVP probably does not help in
proving exponential lower bounds for Boolean formulas: we show that an Ext-PC (even with
the Square Root Rule) derivation of any unsatisfiable Boolean formula in CNF from eBVP
must be of exponential size.Sun, 04 Dec 2022 06:21:35 +0200https://eccc.weizmann.ac.il/report/2022/176