How would one prove the pigeonhole principle with a SAT solver?
SAT solvers work in the propositional calculus, and usually accept as input a formula in conjunctive normal form. There are several different propositional variants of the pigeonhole principle; they are all contradictions, and the actual pigeonhole principle is their negation. One of them, which states that there is a one-to-one mapping from $\{1,\ldots,n\}$ to $\{1,\ldots,n-1\}$, is described in page 2 of this book extract (apparently Jukna's Extremal Combinatorics), where you can also find an exponential lower bound for refuting the pigeonhole principle in the resolution proof system.

(Reiterating, to prove that there is no one-to-one mapping from $\{1,\ldots,n\}$ to $\{1,\ldots,n-1\}$, we instead refute the formula stating that such a mapping does exist.)

SAT solvers are (almost) all based on the DPLL procedure (with some hacks such as clause learning), and so when they refute a statement, their transcript can be converted to a resolution refutation. Therefore the lower bound mentioned above shows that SAT solvers will have a hard time refuting the pigeonhole principle.