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.