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.


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

  • 2
    $\begingroup$ Looks like the extract is from "Extremal Combinatorics: With Applications in Computer Science" by S. Jukna $\endgroup$ Commented Dec 24, 2016 at 20:53

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.