Suppose a problem:

Given $n$ pigeons and $m$ holes of sizes $b_{i\le m}$ decide if you can put all pigeons in given holes.

It's possible to find a refutation of size $\mathcal O(n^2\log^2 n)$ of this principle when it's encoded as a conjunction of threshold functions, therefore there must exist a polynomial size Frege refutation any time $n>\sum_{i=1}^m b_i$.

However, is Cutting Planes too weak already to have a polynomial size refutation for the $n=1+ \sum_{i=1}^m b_i$ case?


1 Answer 1


Let $x_{ij}$ state that pigeon $i$ goes to hole $j$. One can axiomatize the pigeonhole principle as follows:

  1. Booleanity: $0 \leq x_{ij} \leq 1$.
  2. Pigeon axioms: for all $i$, $\sum_j x_{ij} \ge 1$.
  3. Hole axioms: for all $j$, $\sum_i x_{ij} \le b_j$.

Summing the pigeon axioms, we get $$ \sum_{ij} x_{ij} \ge n. $$ Summing the hole axioms, we get $$ \sum_{ij} x_{ij} \leq m. $$ Therefore $n \leq m$, which is a contradiction if $m < n$.

You might be interested in other encodings of the pigeonhole principlethey can probably be used to derive the axioms above.


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.