Lifting with Simple Gadgets and Applications to Circuit and Proof Complexity
Lifting with Simple Gadgets and Applications to Circuit and Proof Complexity
复制标题
DOI：
10.1109/focs46700.2020.00011
复制
发表时间：
2020-01
期刊：
影响因子：
--
通讯作者：
Or Meir;Jakob Nordström;T. Pitassi;Robert Robere;Susanna F. de Rezende
中科院分区：
文献类型：
--
作者：
Or Meir;Jakob Nordström;T. Pitassi;Robert Robere;Susanna F. de Rezende
我们显著地加强和推广了Pitassi和Robere（2018）的将Nullstellenerance度提升到单调跨度程序大小的定理，以便它适用于任何具有足够高秩的小工具，特别是对于有用的小工具，如相等和大于。我们应用我们的广义定理来解决三个开放的问题：·我们提出的第一个结果，证明了一个分离的证明力切割平面与无界与多项式有界系数。具体来说，我们展示CNF公式，可以反驳在二次长度和常数线空间中的切割平面与无界系数，但对于其中有没有反驳在次指数长度和次多项式线空间，如果系数被限制为多项式的大小。·给出了单调布尔公式与单调真实的公式的第一个显式分离。具体来说，我们给出了一个明确的家庭的功能，可以计算的单调真实的公式的近线性大小，但需要单调布尔公式的指数大小。以前只知道非显式分离。·我们给出了迄今为止单调布尔公式和单调布尔电路之间最强的分离。也就是说，我们证明了经典的GEN问题，它具有多项式大小的单调布尔电路，需要大小为2 ^{\Omega（n/\text{polylog}（n））}$的单调布尔公式。一个重要的技术成分，这可能是独立的利益，是我们表明，反驳卵石公式的Nullstellenbranch度的DAG $G$在任何领域正好与可逆卵石价格的$G$。特别地，这意味着相应的伪造子句搜索问题的标准决策树复杂度和奇偶性决策树复杂度是相等的。这是一个扩展的抽象。该文件的完整版本可在https://arxiv.org/abs/2001.02144上查阅。
We significantly strengthen and generalize the theorem lifting Nullstellensatz degree to monotone span program size by Pitassi and Robere (2018) so that it works for any gadget with high enough rank, in particular, for useful gadgets such as equality and greater-than. We apply our generalized theorem to solve three open problems: •We present the first result that demonstrates a separation in proof power for cutting planes with unbounded versus polynomially bounded coefficients. Specifically, we exhibit CNF formulas that can be refuted in quadratic length and constant line space in cutting planes with unbounded coefficients, but for which there are no refutations in subexponential length and subpolynomial line space if coefficients are restricted to be of polynomial magnitude. •We give the first explicit separation between monotone Boolean formulas and monotone real formulas. Specifically, we give an explicit family of functions that can be computed with monotone real formulas of nearly linear size but require monotone Boolean formulas of exponential size. Previously only a non-explicit separation was known. •We give the strongest separation to-date between monotone Boolean formulas and monotone Boolean circuits. Namely, we show that the classical GEN problem, which has polynomial-size monotone Boolean circuits, requires monotone Boolean formulas of size $2^{\Omega(n/\text{polylog}(n))}$. An important technical ingredient, which may be of independent interest, is that we show that the Nullstellensatz degree of refuting the pebbling formula over a DAG $G$ over any field coincides exactly with the reversible pebbling price of $G$. In particular, this implies that the standard decision tree complexity and the parity decision tree complexity of the corresponding falsified clause search problem are equal. This is an extended abstract. The full version of the paper is available at https://arxiv.org/abs/2001.02144.