The Surprising Power of Constant Depth Algebraic Proofs
PROCEEDINGS OF THE 35TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2020)(2020)
Abstract
A major open problem in proof complexity is to prove superpolynomial lower bounds for AC(empty set) [p] -Frege proofs. This system is the analog of AC(empty set) [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 AC(empty set) [p]-Frege. Significant and extensive degree lower bounds have been obtained for a variety of subsystems of AC(empty set) [p]-Frege, including Nullstellensatz ([3]), Polynomial Calculus ([9]), and SOS ([14]). However to date there has been no progress on AC(empty set) [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 AC(empty set) [q] -Frege for any prime q independent of the characteristic of the underlying field. They can also effectively simulate TCempty set-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 AC(empty set )[p]-Frege, but also for systems as strong as TCempty set-Frege.
MoreTranslated text
Key words
Proof Complexity,Polynomial Calculus,Algebraic proofs,AC(empty set)[p]-Frege,bounded depth
AI Read Science
Must-Reading Tree
Example
![](https://originalfileserver.aminer.cn/sys/aminer/pubs/mrt_preview.jpeg)
Generate MRT to find the research sequence of this paper
Chat Paper
Summary is being generated by the instructions you defined