[neel_k]

This note represents a rare misstep by Dijkstra: the pigeonhole principle actually is a special and important principle worthy of a special name of its own. For example:

1. When you formulate the pigeonhole principle in propositional logic, its resolution proofs are exponentially large. Since modern SAT solvers are basically very fancy propositional resolution provers, this gives you a nice way to find hard instances for them. It also makes the question of when propositional proof systems can be more succinct than one another is also a fundamental question in complexity theory.

2. It also arises in geometry: a compactness for metric spaces is essentially the statement that the pigeonhole principle applies to the space.

I don't have a unified perspective of these two facts, but either one of them is really striking. As a result I'm okay with giving the pigeonhole principle its own natural language name.

[coldtea]

>This note represents a rare misstep by Dijkstra

Rare? He was often biased by his preferences, teaching styles, and opinions, in his notes, as opposed to pure science/logic.

[andrepd]

SAT solvers overwhelmingly don't use resolution. Modern state of the art solvers use DPLL/CDCL.

[53x15]

I think neel_k was referring to the fact that when a DPLL or CDCL solver concludes UNSAT you can take the trace its backtracking activity and rewrite it from the bottom up as a resolution refutation. So in this sense the solvers are finding resolution proofs.

[CJefferson]

While they indeed don't use resolution directly, DPLL/CDCL is in many ways equivalent.

Most modern SAT solvers will still have trouble with the pigeon-hole style problems (although some have inbuilt explicit detection, or symmetry breaking, which will let them solve it efficiently).

[ogogmad]

Do you have a reference for 2? Thanks.

[neel_k]

Willie Wong wrote a nice blog post about this a while ago:

https://williewong.wordpress.com/2010/03/18/compactness-part...

[tprice7]

The fact that every infinite sequence of points in a compact metric space has a cluster point is sort of like the pigeonhole principle. The grandparent comment in my opinion makes much more sense if the phrase "a compactness for metric spaces" is replaced by "sequential compactness for metric spaces".