Resolution proofs of generalized pigeonhole principles (Q920967)

The generalized pigeonhole principle is that for positive integers \(m>n\), if m pigeons sit in n holes, then some hole contains more than one pigeon. The ordinary pigeonhole principle has \(m=n+1\). For a fixed m and n the authors exhibit a set \(S_{m,n}\) of propositional clauses which encodes the generalized pigeonhole principle. The number of clauses in this set is \(O(nm^ 2)\). They show that any resolution refutation of \(S_{m,n}\) will contain at least \((3/2)^{n^ 2/50m}\) steps. It follows that the size of the refutation is exponential in n if \(m=cn\) for a constant \(c>1\). This extends work of \textit{A. Haken} [ibid. 39, 297-308 (1985; Zbl 0586.03010)], who gave a similar result for the ordinary pigeonhole principle. In contrast, it is known (references are given in the paper) that for a large number of common propositional logic proof systems, including all Frege systems, polynomial-sized proofs are possible for the pigeonhole principle. Furthermore, it is known that all these systems are polynomially equivalent in the size of proofs they generate. That is, given a proof of length l in one of these systems, there will be a corresponding proof in any other whose length is at most p(l), where p is a polynomial. Therefore, the result of Haken shows that resolution is not polynomially equivalent to any Frege system. The authors of the present paper strengthen this by showing that there is a constant k such that resolution is not polynomially equivalent even to formula-depth k Frege systems.