Journal article:
Samuel R. Buss and Toniann Pitassi.
"Resolution and the Weak Pigeonhole Principle."
Proceedings, Computer Science Logic (CSL'97),
Lecture Notes in Computer Science #1414,
Springer-Verlag, Berlin, 1998, pp. 149-156.
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$.