The Surprising Power of Constant Depth Algebraic Proofs
The Surprising Power of Constant Depth Algebraic Proofs
复制标题
恒定深度代数证明的惊人力量
DOI：
10.1145/3373718.3394754
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Pitassi, T.
中科院分区：
文献类型：
--
作者：
Impagliazzo, R;Mouli, S;Pitassi, T.
证明复杂性的一个主要公开问题是证明AC0[p]-Frege证明的超多项式下界。该系统是AC0[p]的模拟，AC0[p]是一类具有素数模计数门的有界深度电路。尽管这一类的强大下界可以追溯到30年前([28，30])，但AC0[p]-Frege没有显著的下界。AC0[p]-Frege的各种子系统，包括Nullstellensatz([3])、多项式演算([9])和SOS([14])，都得到了重要的广义度下界。然而，到目前为止，关于AC0[p]-Frege下界的研究还没有进展。本文研究了多项式演算的常深度延拓[13]。我们表明，这些扩展比以前所知的要强大得多。我们的主要结果是，小深度(≤43)多项式演算(在足够大的视场上)可以多项式有效地模拟所有研究得很好的半代数证明系统：割平面、Sherali-Adams、平方和(SoS)和正态Stellensatz演算(Dynamic Sos)。此外，它们还能以准多项式有效地模拟任意素数q的AC0[q]-Frege，而与基本场的特性无关。如果允许深度成比例增长，它们还可以有效地模拟TC0-Frege。因此，证明多项式演算的常深度延拓的强下界不仅可以给出AC0[p]-Frege的下界，也可以给出像TC0-Frege这样强的系统的下界。
A major open problem in proof complexity is to prove superpolynomial lower bounds for AC0[p]-Frege proofs. This system is the analog of AC0 [p], the class of bounded depth circuits with prime modular counting gates. Despite strong lower bounds for this class dating back thirty years ([28, 30]), there are no significant lower bounds for AC0 [p]-Frege. Significant and extensive degree lower bounds have been obtained for a variety of subsystems of AC0[p]-Frege, including Nullstellensatz ([3]), Polynomial Calculus ([9]), and SOS ([14]). However to date there has been no progress on AC0 [p]-Frege lower bounds.In this paper we study constant-depth extensions of the Polynomial Calculus [13]. We show that these extensions are much more powerful than was previously known. Our main result is that small depth (≤ 43) Polynomial Calculus (over a sufficiently large field) can polynomially effectively simulate all of the well-studied semialgebraic proof systems: Cutting Planes, Sherali-Adams, Sum-of-Squares (SOS), and Positivstellensatz Calculus (Dynamic SOS). Additionally, they can also quasi-polynomially effectively simulate AC0[q]-Frege for any prime q independent of the characteristic of the underlying field. They can also effectively simulate TC0-Frege if the depth is allowed to grow proportionally. Thus, proving strong lower bounds for constant-depth extensions of Polynomial Calculus would not only give lower bounds for AC0 [p]-Frege, but also for systems as strong as TC0-Frege.
登录
查看更多内容
有效的多项式模拟
DOI：
--
发表时间：
2010
期刊：
--
影响因子：
--
作者：
T. Pitassi;R. Santhanam
通讯作者：
R. Santhanam
小多数深度的阈值电路
DOI：
10.1006/inco.1998.2732
发表时间：
1998
期刊：
Inf. Comput.
影响因子：
--
作者：
Alexis Maciel;D. Thérien
通讯作者：
D. Thérien
关于阈值电路功率的说明
DOI：
10.1109/sfcs.1989.63538
发表时间：
1989
期刊：
30th Annual Symposium on Foundations of Computer Science
影响因子：
--
作者：
Eric Allender
通讯作者：
Eric Allender
有界算术和恒定深度命题证明中的折叠模块化计数
DOI：
--
发表时间：
2015
期刊：
影响因子：
--
作者：
S. Buss;L. Kolodziejczyk;K. Zdanowski
通讯作者：
K. Zdanowski
使用模块化连接词走向有界深度弗雷格证明的下界
DOI：
--
发表时间：
1996
期刊：
Proof Complexity and Feasible Arithmetics
影响因子：
--
作者：
Alexis Maciel;T. Pitassi
通讯作者：
T. Pitassi