The power of the Binary Value Principle

The (extended) Binary Value Principle (eBVP, the equation ∑_i=1ⁿx_i2ⁱ⁻¹=−k for k>0 and Boolean variables x_i) has received a lot of attention recently, several lower bounds have been proved for it [1,2,11]. Also it has been shown [1] that the probabilistically verifiable Ideal Proof System (IPS) [8] together with eBVP polynomially simulates a similar semialgebraic proof system. In this paper we consider Polynomial Calculus with an algebraic version of Tseitin's extension rule (Ext-PC) that introduces a new variable for any polynomial. 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 [6], which is in sharp contrast with the result of [2] 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.