Exponential lower bounds for the pigeonhole principle
Proceedings of the Twenty-Fourth Annual ACM Symposium on Theory of Computing, 1992•dl.acm.org
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 …
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 …
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~(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.