Revision #2 Authors: Russell Impagliazzo, Sasank Mouli, Toniann Pitassi

Accepted on: 11th January 2020 08:01

Downloads: 206

Keywords:

A major open problem in proof complexity is to prove super-polynomial lower bounds for AC^0[p]-Frege proofs. This system is the analog of AC^0[p], the class of bounded depth circuits with prime modular counting gates. Despite strong lower bounds for this class dating back thirty years (Razborov, '86 and Smolensky, '87), there are no significant lower bounds for AC^0[p]-Frege. Significant and extensive *degree* lower bounds have been obtained for a variety of subsystems of AC^0[p]-Frege, including Nullstellensatz (Beame et. al. '94), Polynomial Calculus (Clegg et. al. '96), and SOS (Griegoriev and Vorobjov, '01). However to date there has been no progress on AC^0[p]-Frege lower bounds.

In this paper we study constant-depth extensions of the Polynomial Calculus introduced by Griegoriev and Hirsch, '03. We show that these extensions are much more powerful than was previously known. Our main result is that small depth Polynomial Calculus (over a sufficiently large field) can polynomially simulate all of the well-studied semialgebraic proof systems: Cutting Planes, Sherali-Adams and Sum-of-Squares, and they can also quasi-polynomially simulate AC^0[p]-Frege as well as TC^0-Frege. Thus, proving strong lower bounds for AC^0[p]-Frege would seem to require proving lower bounds for systems as strong as TC^0-Frege.

Revision #1 Authors: Russell Impagliazzo, Sasank Mouli, Toniann Pitassi

Accepted on: 11th January 2020 08:00

Downloads: 89

Keywords:

A major open problem in proof complexity is to prove super-polynomial lower bounds for AC^0[p]-Frege proofs. This system is the analog of AC^0[p], the class of bounded depth circuits with prime modular counting gates. Despite strong lower bounds for this class dating back thirty years (Razborov, '86 and Smolensky, '87), there are no significant lower bounds for AC^0[p]-Frege. Significant and extensive *degree* lower bounds have been obtained for a variety of subsystems of AC^0[p]-Frege, including Nullstellensatz (Beame et. al. '94), Polynomial Calculus (Clegg et. al. '96), and SOS (Griegoriev and Vorobjov, '01). However to date there has been no progress on AC^0[p]-Frege lower bounds.

In this paper we study constant-depth extensions of the Polynomial Calculus introduced by Griegoriev and Hirsch, '03. We show that these extensions are much more powerful than was previously known. Our main result is that small depth Polynomial Calculus (over a sufficiently large field) can polynomially simulate all of the well-studied semialgebraic proof systems: Cutting Planes, Sherali-Adams and Sum-of-Squares, and they can also quasi-polynomially simulate AC^0[p]-Frege as well as TC^0-Frege. Thus, proving strong lower bounds for AC^0[p]-Frege would seem to require proving lower bounds for systems as strong as TC^0-Frege.

Restructured the proofs and added details where necessary

TR19-024 Authors: Russell Impagliazzo, Sasank Mouli, Toniann Pitassi

Publication: 27th February 2019 23:48

Downloads: 543

Keywords:

A major open problem in proof complexity is to prove super-polynomial lower bounds for AC^0[p]-Frege proofs. This system is the analog of AC^0[p], the class of bounded depth circuits with prime modular counting gates. Despite strong lower bounds for this class dating back thirty years (Razborov, '86 and Smolensky, '87), there are no significant lower bounds for AC^0[p]-Frege. Significant and extensive *degree* lower bounds have been obtained for a variety of subsystems of AC^0[p]-Frege, including Nullstellensatz (Beame et. al. '94), Polynomial Calculus (Clegg et. al. '96), and SOS (Griegoriev and Vorobjov, '01). However to date there has been no progress on AC^0[p]-Frege lower bounds.

In this paper we study constant-depth extensions of the Polynomial Calculus introduced by Griegoriev and Hirsch, '03. We show that these extensions are much more powerful than was previously known. Our main result is that small depth Polynomial Calculus (over a sufficiently large field) can polynomially simulate all of the well-studied semialgebraic proof systems: Cutting Planes, Sherali-Adams and Sum-of-Squares, and they can also quasi-polynomially simulate AC^0[p]-Frege as well as TC^0-Frege. Thus, proving strong lower bounds for AC^0[p]-Frege would seem to require proving lower bounds for systems as strong as TC^0-Frege.