Exponential lower bounds for the pigeonhole principle
T Pitassi, P Beame, R Impagliazzo - Computational complexity, 1993 - Springer
T Pitassi, P Beame, R Impagliazzo
Computational complexity, 1993•SpringerIn this paper we prove an exponential lower bound on the size of bounded-depth Frege
proofs for the pigeonhole principle (PHP). We also obtain an Ω (loglog n)-depth lower bound
for any polynomial-sized Frege proof of the pigeonhole principle. Our theorem nearly
completes the search for the exact complexity of the PHP, as S. Buss has constructed
polynomial-size, log n-depth Frege proofs for the PHP. The main lemma in our proof can be
viewed as a general Håstad-style Switching Lemma for restrictions that are partial …
proofs for the pigeonhole principle (PHP). We also obtain an Ω (loglog n)-depth lower bound
for any polynomial-sized Frege proof of the pigeonhole principle. Our theorem nearly
completes the search for the exact complexity of the PHP, as S. Buss has constructed
polynomial-size, log n-depth Frege proofs for the PHP. The main lemma in our proof can be
viewed as a general Håstad-style Switching Lemma for restrictions that are partial …
Abstract
In this paper we prove an exponential lower bound on the size of bounded-depth Frege proofs for the pigeonhole principle (PHP). We also obtain an Ω(loglogn)-depth lower bound for any polynomial-sized Frege proof of the pigeonhole principle. Our theorem nearly completes the search for the exact complexity of the PHP, as S. Buss has constructed polynomial-size, logn-depth Frege proofs for the PHP. The main lemma in our proof can be viewed as a general Håstad-style Switching Lemma for restrictions that are partial matchings. Our lower bounds for the pigeonhole principle improve on previous superpolynomial lower bounds.
Springer