c pigeon-4: placing 5 pigeons into 4 holes
c 
c File generated by 'pigeonhole', (c) Tjark Weber
c 
c The SAT encoding of this problem is very straightforward.  For each pigeon i
c and each hole j we have a variable x_{n*(i-1)+j} which means that pigeon i
c is placed in hole j.  Then we have n+1 clauses which say that a pigeon has
c to be placed in some hole.  Then for each hole we have a set of clauses
c ensuring that only one single pigeon is placed into that hole.
c 
c This encoding leads to a total of (n+1) * n propositional variables and
c (n+1) + n * (n * (n+1) / 2) clauses.
c 
c The resulting SAT problem is unsatisfiable.
c 
p cnf 20 45
1 2 3 4 0
5 6 7 8 0
9 10 11 12 0
13 14 15 16 0
17 18 19 20 0
-1 -5 0
-1 -9 0
-1 -13 0
-1 -17 0
-5 -9 0
-5 -13 0
-5 -17 0
-9 -13 0
-9 -17 0
-13 -17 0
-2 -6 0
-2 -10 0
-2 -14 0
-2 -18 0
-6 -10 0
-6 -14 0
-6 -18 0
-10 -14 0
-10 -18 0
-14 -18 0
-3 -7 0
-3 -11 0
-3 -15 0
-3 -19 0
-7 -11 0
-7 -15 0
-7 -19 0
-11 -15 0
-11 -19 0
-15 -19 0
-4 -8 0
-4 -12 0
-4 -16 0
-4 -20 0
-8 -12 0
-8 -16 0
-8 -20 0
-12 -16 0
-12 -20 0
-16 -20 0