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.