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