A small C program to create DIMACS CNF files that encode the pigeonhole problem (i.e. placing n+1 pigeons into n holes).

The SAT encoding of this problem is very straightforward. For each pigeon i and each hole j we have a variable x_{n*(i-1)+j} 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 a total of (n+1) * n propositional variables and (n+1) + n * (n * (n+1) / 2) clauses.

The resulting SAT problem is unsatisfiable.

- pigeon-1.cnf
- pigeon-2.cnf
- pigeon-3.cnf
- pigeon-4.cnf
- pigeon-5.cnf
- pigeon-6.cnf
- pigeon-7.cnf
- pigeon-8.cnf
- pigeon-9.cnf
- pigeon-10.cnf
- pigeon-11.cnf
- pigeon-12.cnf
- pigeon-13.cnf
- pigeon-14.cnf
- pigeon-15.cnf
- pigeon-16.cnf
- pigeon-17.cnf
- pigeon-18.cnf
- pigeon-19.cnf
- pigeon-20.cnf

Last modified: 2007-11-22