TR22-176 Authors: Yaroslav Alekseev, Edward Hirsch

Publication: 4th December 2022 06:21

Downloads: 218

Keywords:

The (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.