Exponential lower bounds for the pigeonhole principle
Paul W. Beame, Russell Impagliazzo, Jan Krajı́ček, Toniann Pitassi, Pavel Pudlák, Alan R. Woods · 1992
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 ~(log log rz)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 Sam Buss has constructed polynomial-size, log ndepth 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.