3 ms·
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
by neel_k 6y ago
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.
- ogogmad 6y agoDo you have a reference for 2? Thanks.
- neel_k 6y agoWillie Wong wrote a nice blog post about this a while ago: https://williewong.wordpress.com/2010/03/18/compactness-part-1-degrees-of-freedom/ https://williewong.wordpress.com/2010/03/18/compactness-part...
- tprice7 6y agoThe 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".
- andrepd 6y agoSAT solvers overwhelmingly don't use resolution. Modern state of the art solvers use DPLL/CDCL.
- 53x15 6y agoI 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 6y agoWhile 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).
- coldtea 6y ago>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.
- deleted 6y ago[deleted]