c pigeon-3: placing 4 pigeons into 3 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 12 22
1 2 3 0
4 5 6 0
7 8 9 0
10 11 12 0
-1 -4 0
-1 -7 0
-1 -10 0
-4 -7 0
-4 -10 0
-7 -10 0
-2 -5 0
-2 -8 0
-2 -11 0
-5 -8 0
-5 -11 0
-8 -11 0
-3 -6 0
-3 -9 0
-3 -12 0
-6 -9 0
-6 -12 0
-9 -12 0