c pigeon-7: placing 8 pigeons into 7 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 56 204 1 2 3 4 5 6 7 0 8 9 10 11 12 13 14 0 15 16 17 18 19 20 21 0 22 23 24 25 26 27 28 0 29 30 31 32 33 34 35 0 36 37 38 39 40 41 42 0 43 44 45 46 47 48 49 0 50 51 52 53 54 55 56 0 -1 -8 0 -1 -15 0 -1 -22 0 -1 -29 0 -1 -36 0 -1 -43 0 -1 -50 0 -8 -15 0 -8 -22 0 -8 -29 0 -8 -36 0 -8 -43 0 -8 -50 0 -15 -22 0 -15 -29 0 -15 -36 0 -15 -43 0 -15 -50 0 -22 -29 0 -22 -36 0 -22 -43 0 -22 -50 0 -29 -36 0 -29 -43 0 -29 -50 0 -36 -43 0 -36 -50 0 -43 -50 0 -2 -9 0 -2 -16 0 -2 -23 0 -2 -30 0 -2 -37 0 -2 -44 0 -2 -51 0 -9 -16 0 -9 -23 0 -9 -30 0 -9 -37 0 -9 -44 0 -9 -51 0 -16 -23 0 -16 -30 0 -16 -37 0 -16 -44 0 -16 -51 0 -23 -30 0 -23 -37 0 -23 -44 0 -23 -51 0 -30 -37 0 -30 -44 0 -30 -51 0 -37 -44 0 -37 -51 0 -44 -51 0 -3 -10 0 -3 -17 0 -3 -24 0 -3 -31 0 -3 -38 0 -3 -45 0 -3 -52 0 -10 -17 0 -10 -24 0 -10 -31 0 -10 -38 0 -10 -45 0 -10 -52 0 -17 -24 0 -17 -31 0 -17 -38 0 -17 -45 0 -17 -52 0 -24 -31 0 -24 -38 0 -24 -45 0 -24 -52 0 -31 -38 0 -31 -45 0 -31 -52 0 -38 -45 0 -38 -52 0 -45 -52 0 -4 -11 0 -4 -18 0 -4 -25 0 -4 -32 0 -4 -39 0 -4 -46 0 -4 -53 0 -11 -18 0 -11 -25 0 -11 -32 0 -11 -39 0 -11 -46 0 -11 -53 0 -18 -25 0 -18 -32 0 -18 -39 0 -18 -46 0 -18 -53 0 -25 -32 0 -25 -39 0 -25 -46 0 -25 -53 0 -32 -39 0 -32 -46 0 -32 -53 0 -39 -46 0 -39 -53 0 -46 -53 0 -5 -12 0 -5 -19 0 -5 -26 0 -5 -33 0 -5 -40 0 -5 -47 0 -5 -54 0 -12 -19 0 -12 -26 0 -12 -33 0 -12 -40 0 -12 -47 0 -12 -54 0 -19 -26 0 -19 -33 0 -19 -40 0 -19 -47 0 -19 -54 0 -26 -33 0 -26 -40 0 -26 -47 0 -26 -54 0 -33 -40 0 -33 -47 0 -33 -54 0 -40 -47 0 -40 -54 0 -47 -54 0 -6 -13 0 -6 -20 0 -6 -27 0 -6 -34 0 -6 -41 0 -6 -48 0 -6 -55 0 -13 -20 0 -13 -27 0 -13 -34 0 -13 -41 0 -13 -48 0 -13 -55 0 -20 -27 0 -20 -34 0 -20 -41 0 -20 -48 0 -20 -55 0 -27 -34 0 -27 -41 0 -27 -48 0 -27 -55 0 -34 -41 0 -34 -48 0 -34 -55 0 -41 -48 0 -41 -55 0 -48 -55 0 -7 -14 0 -7 -21 0 -7 -28 0 -7 -35 0 -7 -42 0 -7 -49 0 -7 -56 0 -14 -21 0 -14 -28 0 -14 -35 0 -14 -42 0 -14 -49 0 -14 -56 0 -21 -28 0 -21 -35 0 -21 -42 0 -21 -49 0 -21 -56 0 -28 -35 0 -28 -42 0 -28 -49 0 -28 -56 0 -35 -42 0 -35 -49 0 -35 -56 0 -42 -49 0 -42 -56 0 -49 -56 0