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  42  133  no 
hole7.cnf  56  204  no 
hole8.cnf  72  297  no 
hole9.cnf  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.