__Journal article:__

** Samuel R. Buss and Toniann Pitassi.
"Resolution and the Weak Pigeonhole Principle."
**

** Download article: postscript or PDF. **

** Abstract: **We give new upper bounds for resolution
proofs of the weak pigeonhole principle. We also give lower bounds for tree-like
resolution proofs. We present a normal form for resolution proofs of pigeonhole principles
based on a new monotone resolution rule.

The results of this paper are as follows. In section~3 we present a normal form for resolution proofs of pigeonhole principle tautologies. Normal form resolution proofs contain only positive occurrences of variables; the usual resolution rule is replaced by a new monotone resolution rule. The sizes of monotone resolution proofs are polynomially related to the sizes of resolution proofs. As a corollary, we prove that resolution proofs of the onto version of the pigeonhole principle are not significantly shorter than resolution proofs of the non-onto pigeonhole principle. In section~4, we give a polynomial upper bound on the size of resolution proofs of $\PHP^m_n$ for $m=2^{\sqrt{n\log n}}$. This improves on the upper bound $n^2 2^n$ for proofs of $\PHP^{n+1}_n$; which shows that having additional domain elements can make the pigeonhole principle easier to prove. In section~5, we prove an exponential lower bound on the size of tree-like resolution proofs of $\PHP^m_n$.