How would one prove the pigeonhole principle with a SAT solver?

Question

Suppose I wanted to find a proof of the pigeonhole principle or show that no proof shorter than $L$ exists. I understand that proof-checking is in NP, so I could write a CNF formula that is satisfiable iff. such a proof exists. What I want to know is, how exactly would one do that? I understand I would assume a set of axioms about sets or something and also the axioms of first-order predicate calculus, and probably also modus ponens and stuff... but how exactly does one do something like this? Can anyone give a construction of such a CNF formula? References to papers or general explanations would be appreciated.

Answer 1

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.