Pigeonhole formula

also: pigeonhole principle, php

The family of CNF instances asserting that n+1 pigeons fit in n holes with no two sharing. They are unsatisfiable, and every resolution proof of that is exponentially long, so they are the standard way to show that a solver's cleverness is heuristic rather than a change in worst-case behaviour.

Assert that $n + 1$ pigeons occupy $n$ holes with no hole shared. With $x_{i, j}$ meaning pigeon $i$ is in hole $j$ :

i = 1 ⋀ n + 1 (j = 1 ⋁ n x_{i, j}) \land j = 1 ⋀ n i < i^{'} ⋀ (\neg x_{i, j} \lor \neg x_{i^{'}, j})

The formula is unsatisfiable, and obviously so to a human, who counts. A resolution proof cannot count: Haken showed in 1985 that every resolution refutation of these formulas has size $2^{Ω (n)}$ . Since CDCL produces resolution proofs, that is an unconditional lower bound on every CDCL solver, whatever its heuristics.

This is why the family is the standard sanity check on a solver's claims. Clause learning and activity heuristics change which instances are tractable; they do not change the worst case, and the pigeonhole formulas are the cleanest way to see the difference. Around $n = 12$ the runtime is already measured in minutes.