Pigeonhole formula

The pigeonhole formulas encode, as a set of clauses, the false statement that $n + 1$ pigeons fit into $n$ holes without two pigeons sharing a hole. The pigeonhole principle says this is impossible, and any person convinces themselves of it by counting. Resolution, the proof system that SAT solvers work in, cannot count: Armin Haken proved in 1985 that every resolution refutation of the pigeonhole formulas has size exponential in $n$ ^[1]. As a result, DPLL and CDCL solvers take exponential time on formulas with only a few hundred clauses. Stronger proof systems, such as extended resolution, cutting planes and Frege systems, have polynomial-size proofs^[3]^[4]^[5], so the family marks the boundary between resolution and reasoning that can count. It was proposed as a hard example by Cook and Reckhow in 1979^[2].

§ 01

The formulas

For pigeons $i = 1, \dots, n + 1$ and holes $j = 1, \dots, n$ , the variable $x_{i, j}$ means that pigeon $i$ is in hole $j$ . The formula $PHP_{n}^{n + 1}$ says that each pigeon is in some hole and no hole holds two pigeons:

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})

It has $n (n + 1)$ variables, $n + 1$ pigeon clauses of length $n$ , and $n (2 n + 1)$ hole clauses of length 2. Nothing in it prevents a pigeon from occupying two holes; adding those constraints gives the functional pigeonhole formula, and requiring every hole to be used gives the onto version. Both are also hard for resolution.

The formula for four pigeons and three holes. Each dashed line is a variable. Any attempt to place the pigeons, like the one shown, leaves some pigeon without a hole or puts two in one hole.

§ 02

Resolution lower bound

Haken showed that every resolution refutation of $PHP_{n}^{n + 1}$ contains at least $2^{Ω (n)}$ clauses^[1]. His proof considers the assignments that place $n$ of the pigeons in distinct holes, which falsify only the clause of the remaining pigeon, and shows that a short refutation would have to contain a clause that is falsified by many of these assignments at once and yet is wide, of which there cannot be few. Beame and Pitassi gave a simpler proof in 1996^[6], and Ben-Sasson and Wigderson derived such bounds from the width of refutations^[10]. For many more pigeons than holes, the weak pigeonhole principle, Raz showed in 2004 that resolution still needs exponential size, however many pigeons there are^[7]^[9].

Since every CDCL run on an unsatisfiable formula is a resolution refutation, the bound applies to every such solver, whatever its heuristics.

Solving the formulas with increasing numbers of holes, using a CDCL solver.

Running it.

holes  variables  clauses  CDCL conflicts
    3         12       22               7
    4         20       45              28
    5         30       81             154
    6         42      133             758
    7         56      204            4164
    8         72      297           34671

Conflicts grow by a factor of five to eight with each additional hole, a straight line on a logarithmic scale.

Each extra hole multiplies the number of conflicts by five to eight; the formula for eight holes, with 72 variables and 297 clauses, already takes tens of thousands of conflicts, and production solvers, although far faster, are stopped by formulas with a dozen or so holes.

§ 03

Short proofs

The principle has a two-line counting proof: summing the pigeon constraints gives at least $n + 1$ occupied places, and summing the hole constraints gives at most $n$ . Proof systems that can express this argument prove the formulas efficiently.

In cutting planes, clauses become linear inequalities over 0–1 variables, and the rules add inequalities and round coefficients. The hole constraints $\sum_{i} x_{i, j} \leq 1$ can be derived from the pairwise clauses in a polynomial number of steps, and adding them to the pigeon constraints $\sum_{j} x_{i, j} \geq 1$ cancels every variable and leaves $0 \geq 1$ ^[4].

The final step of the cutting-planes proof: adding all pigeon and hole inequalities.

(* The counting argument as a derivation over linear inequalities. For
   each pigeon, sum over holes of p(i,j) >= 1; for each hole, sum over
   pigeons of p(i,j) <= 1. Adding all of them cancels every variable. *)
let refute n =
  (* represent sum_{i,j} c(i,j) p(i,j) + k >= 0 by its coefficients *)
  let coef = Array.make_matrix (n + 1) n 0 and const = ref 0 and steps = ref 0 in
  for i = 0 to n do                          (* p(i,0) + ... + p(i,n-1) - 1 >= 0 *)
    for j = 0 to n - 1 do coef.(i).(j) <- coef.(i).(j) + 1 done;
    const := !const - 1; incr steps
  done;
  for j = 0 to n - 1 do                      (* 1 - p(0,j) - ... - p(n,j) >= 0 *)
    for i = 0 to n do coef.(i).(j) <- coef.(i).(j) - 1 done;
    const := !const + 1; incr steps
  done;
  let cancelled = Array.for_all (Array.for_all (( = ) 0)) coef in
  (cancelled, !const, !steps)

Running it.

n =    3: 7 inequalities added, variables cancelled: true, result: -1 >= 0
n =   10: 21 inequalities added, variables cancelled: true, result: -1 >= 0
n = 1000: 2001 inequalities added, variables cancelled: true, result: -1 >= 0

Cook showed in 1976 that extended resolution, which may introduce new variables as abbreviations, has polynomial-size proofs, by reducing the principle for $n$ holes to that for $n - 1$ ^[3]. Buss gave polynomial-size proofs in Frege systems, the textbook proof systems of propositional logic, in 1987^[5].

§ 04

In practice

Because the formula is symmetric under permuting pigeons and permuting holes, a solver that breaks the symmetry, for instance by adding clauses that force pigeons into holes in a canonical order, can finish much faster^[8]. Pseudo-Boolean solvers, which reason with cardinality constraints directly, refute it at once once the constraints have been recognized. Plain CDCL solvers do neither, and the formulas are part of the standard suite for testing claims about solver performance.

§ 05

History

The pigeonhole principle is attributed to Dirichlet, who used it in 1834 under the name Schubfachprinzip, the drawer principle. Cook and Reckhow, founding propositional proof complexity in 1979, proposed its propositional form as a candidate for a tautology without short proofs in some proof systems^[2]. Cook had already shown that extended resolution proves it efficiently^[3]. Haken's lower bound for resolution in 1985 was the first exponential lower bound for resolution without restrictions^[1], and cutting-planes and Frege proofs of polynomial size followed in 1987^[4]^[5]. The weak pigeonhole principle remained open for resolution until 2004^[7].