Pigeonhole problems

The pigeonhole problem involves showing that it is impossible to put $n+1$ pigeons into $n$ holes if each pigeon must go into a distinct hole. If we write $p_{ij}$ for the fact that pigeon $i$ is in hole $j$, then a straightforward axiomatization says that every pigeon must be in at least one hole:

$$p_{i1} \vee p_{i2} \vee \cdots \vee p_{in} \mbox{ for $i=1,\dots,n+1$}$$ (9)

and that no two pigeons can be in the same hole:

$$\neg p_{ik} \vee \neg p_{jk} \mbox{ for $1\leq i<j\leq n+1$\ and $k=1,\dots,n$}$$ (10)

Note that there are in all $\Theta(n^3)$ axioms of the form (10).

It is well known that there is no polynomial-sized proof of the unsatisfiability of the axioms (9)-(10) [HakenHaken1985]. The proof is technical, but the essential reason is that the pigeonhole problem is ``all about'' counting. At some point, proving that you can't put $n+1$ pigeons into $n$ holes requires saying that you can't put $n$ pigeons into the last $n-1$ holes, thus $n-1$ pigeons into the last $n-2$ holes, and so on. Saying this in the language of SAT is awkward, and it is possible to show that no proof of the pigeonhole problem can be completed without, at some point, working with extremely long individual clauses. Once again, we see the connection to expressive efficiency; for readers interested in additional details, Pitassi's Pitassi:complexity explanation is reasonably accessible.