# SAT instances of the Pigeon Hole Problem

The Pigeon Hole problem asks whether it is possible to place
*n+1* pigeons in *n* holes without two pigeons being in the
same hole (obviously, it's not possible).

#### SAT encoding

The SAT encoding of this problem is very straightforward. For each
pigeon *i* we have a variable *x_{ij}* which means that
pigeon *i* is placed in hole *j*. Then we have *n+1*
clauses which say that a pigeon has to be placed in some hole. Then
for each hole we have a set of clauses ensuring that only one single
pigeon is placed into that hole. This encoding leads to in total
*n * (n+1)* propositional variables and to *(n+1) +
n * (n * (n+1) / 2)* clauses.
#### Benchmark instances

There are five instances available at the DIMACS benchmark set which
encode the pigeon hole problem for six to ten holes; details on the
instances are given in Table 1.

**instance ** |
**holes ** |
**vars ** |
**clauses ** |
**satisfiable? ** |

hole6.cnf |
6 |
42 |
133 |
no |

hole7.cnf |
7 |
56 |
204 |
no |

hole8.cnf |
8 |
72 |
297 |
no |

hole9.cnf |
9 |
90 |
415 |
no |

hole10.cnf |
10 |
110 |
561 |
no |

**Table 1:** SAT-encodings of the pigeon hole problem

#### Acknowledgements

The instances have originally
been contributed by John Hooker
and are also contained in a collection of SAT instances at the
Forschungsinstitut fü anwendungsorientierte Wissensverarbeitung in
Ulm, Germany.