c pigeon-8: placing 9 pigeons into 8 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 72 297 1 2 3 4 5 6 7 8 0 9 10 11 12 13 14 15 16 0 17 18 19 20 21 22 23 24 0 25 26 27 28 29 30 31 32 0 33 34 35 36 37 38 39 40 0 41 42 43 44 45 46 47 48 0 49 50 51 52 53 54 55 56 0 57 58 59 60 61 62 63 64 0 65 66 67 68 69 70 71 72 0 -1 -9 0 -1 -17 0 -1 -25 0 -1 -33 0 -1 -41 0 -1 -49 0 -1 -57 0 -1 -65 0 -9 -17 0 -9 -25 0 -9 -33 0 -9 -41 0 -9 -49 0 -9 -57 0 -9 -65 0 -17 -25 0 -17 -33 0 -17 -41 0 -17 -49 0 -17 -57 0 -17 -65 0 -25 -33 0 -25 -41 0 -25 -49 0 -25 -57 0 -25 -65 0 -33 -41 0 -33 -49 0 -33 -57 0 -33 -65 0 -41 -49 0 -41 -57 0 -41 -65 0 -49 -57 0 -49 -65 0 -57 -65 0 -2 -10 0 -2 -18 0 -2 -26 0 -2 -34 0 -2 -42 0 -2 -50 0 -2 -58 0 -2 -66 0 -10 -18 0 -10 -26 0 -10 -34 0 -10 -42 0 -10 -50 0 -10 -58 0 -10 -66 0 -18 -26 0 -18 -34 0 -18 -42 0 -18 -50 0 -18 -58 0 -18 -66 0 -26 -34 0 -26 -42 0 -26 -50 0 -26 -58 0 -26 -66 0 -34 -42 0 -34 -50 0 -34 -58 0 -34 -66 0 -42 -50 0 -42 -58 0 -42 -66 0 -50 -58 0 -50 -66 0 -58 -66 0 -3 -11 0 -3 -19 0 -3 -27 0 -3 -35 0 -3 -43 0 -3 -51 0 -3 -59 0 -3 -67 0 -11 -19 0 -11 -27 0 -11 -35 0 -11 -43 0 -11 -51 0 -11 -59 0 -11 -67 0 -19 -27 0 -19 -35 0 -19 -43 0 -19 -51 0 -19 -59 0 -19 -67 0 -27 -35 0 -27 -43 0 -27 -51 0 -27 -59 0 -27 -67 0 -35 -43 0 -35 -51 0 -35 -59 0 -35 -67 0 -43 -51 0 -43 -59 0 -43 -67 0 -51 -59 0 -51 -67 0 -59 -67 0 -4 -12 0 -4 -20 0 -4 -28 0 -4 -36 0 -4 -44 0 -4 -52 0 -4 -60 0 -4 -68 0 -12 -20 0 -12 -28 0 -12 -36 0 -12 -44 0 -12 -52 0 -12 -60 0 -12 -68 0 -20 -28 0 -20 -36 0 -20 -44 0 -20 -52 0 -20 -60 0 -20 -68 0 -28 -36 0 -28 -44 0 -28 -52 0 -28 -60 0 -28 -68 0 -36 -44 0 -36 -52 0 -36 -60 0 -36 -68 0 -44 -52 0 -44 -60 0 -44 -68 0 -52 -60 0 -52 -68 0 -60 -68 0 -5 -13 0 -5 -21 0 -5 -29 0 -5 -37 0 -5 -45 0 -5 -53 0 -5 -61 0 -5 -69 0 -13 -21 0 -13 -29 0 -13 -37 0 -13 -45 0 -13 -53 0 -13 -61 0 -13 -69 0 -21 -29 0 -21 -37 0 -21 -45 0 -21 -53 0 -21 -61 0 -21 -69 0 -29 -37 0 -29 -45 0 -29 -53 0 -29 -61 0 -29 -69 0 -37 -45 0 -37 -53 0 -37 -61 0 -37 -69 0 -45 -53 0 -45 -61 0 -45 -69 0 -53 -61 0 -53 -69 0 -61 -69 0 -6 -14 0 -6 -22 0 -6 -30 0 -6 -38 0 -6 -46 0 -6 -54 0 -6 -62 0 -6 -70 0 -14 -22 0 -14 -30 0 -14 -38 0 -14 -46 0 -14 -54 0 -14 -62 0 -14 -70 0 -22 -30 0 -22 -38 0 -22 -46 0 -22 -54 0 -22 -62 0 -22 -70 0 -30 -38 0 -30 -46 0 -30 -54 0 -30 -62 0 -30 -70 0 -38 -46 0 -38 -54 0 -38 -62 0 -38 -70 0 -46 -54 0 -46 -62 0 -46 -70 0 -54 -62 0 -54 -70 0 -62 -70 0 -7 -15 0 -7 -23 0 -7 -31 0 -7 -39 0 -7 -47 0 -7 -55 0 -7 -63 0 -7 -71 0 -15 -23 0 -15 -31 0 -15 -39 0 -15 -47 0 -15 -55 0 -15 -63 0 -15 -71 0 -23 -31 0 -23 -39 0 -23 -47 0 -23 -55 0 -23 -63 0 -23 -71 0 -31 -39 0 -31 -47 0 -31 -55 0 -31 -63 0 -31 -71 0 -39 -47 0 -39 -55 0 -39 -63 0 -39 -71 0 -47 -55 0 -47 -63 0 -47 -71 0 -55 -63 0 -55 -71 0 -63 -71 0 -8 -16 0 -8 -24 0 -8 -32 0 -8 -40 0 -8 -48 0 -8 -56 0 -8 -64 0 -8 -72 0 -16 -24 0 -16 -32 0 -16 -40 0 -16 -48 0 -16 -56 0 -16 -64 0 -16 -72 0 -24 -32 0 -24 -40 0 -24 -48 0 -24 -56 0 -24 -64 0 -24 -72 0 -32 -40 0 -32 -48 0 -32 -56 0 -32 -64 0 -32 -72 0 -40 -48 0 -40 -56 0 -40 -64 0 -40 -72 0 -48 -56 0 -48 -64 0 -48 -72 0 -56 -64 0 -56 -72 0 -64 -72 0