论文标题
二元价值原理的力量
The power of the Binary Value Principle
论文作者
论文摘要
（扩展的）二进制值原理（EBVP：$ \ sum_ {i = 1}^n x_i2^{i -1} = -k $ for $ k> 0 $和$ x^2_i = x_i $）最近受到了很多关注，几个较低的界限已证明了它（Alekseev等人2020年，Alekseev等2020，Alekseev 202222222221），一部分＆temert and temert＆t n s and t zamans，temant＆t n s amer。同样（Alekseev等，2020年）也表明，概率可验证的理想证明系统（IPS）（Grochow and Pitassi 2018）以及EBVP多项式模拟了类似的半隔板证明系统。在本文中，我们考虑使用Tseitin的扩展规则（EXT-PC）的代数版本的多项式演算。与IPS相反，这是一个库克 - 怪异的防护系统。我们表明，在这种情况下，EBVP仍然允许模拟类似的半ge骨系统。我们还证明，它允许模拟平方根规则（Grigoriev and Hirsch 2003），这与（Alekseev 2021）的结果形成鲜明对比，该结果显示了从其正方形的二进制值原理的Ext-PC派生大小的指数下限。另一方面，我们证明了EBVP可能无助于证明布尔公式的指数下限：我们表明，EBVP中CNF中任何不满意的布尔公式的Ext-PC（即使具有平方根规则）的推导，必须是指数级的大小。
The (extended) Binary Value Principle (eBVP: $\sum_{i=1}^n x_i2^{i-1} = -k$ for $k>0$ and $x^2_i=x_i$) has received a lot of attention recently, several lower bounds have been proved for it (Alekseev et al 2020, Alekseev 2021, Part and Tzameret 2021). Also it has been shown (Alekseev et al 2020) that the probabilistically verifiable Ideal Proof System (IPS) (Grochow and Pitassi 2018) 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 2003), which is in sharp contrast with the result of (Alekseev 2021) 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.
