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$.

Back to Sam Buss's publications page.