c pigeon-12: placing 13 pigeons into 12 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 156 949 1 2 3 4 5 6 7 8 9 10 11 12 0 13 14 15 16 17 18 19 20 21 22 23 24 0 25 26 27 28 29 30 31 32 33 34 35 36 0 37 38 39 40 41 42 43 44 45 46 47 48 0 49 50 51 52 53 54 55 56 57 58 59 60 0 61 62 63 64 65 66 67 68 69 70 71 72 0 73 74 75 76 77 78 79 80 81 82 83 84 0 85 86 87 88 89 90 91 92 93 94 95 96 0 97 98 99 100 101 102 103 104 105 106 107 108 0 109 110 111 112 113 114 115 116 117 118 119 120 0 121 122 123 124 125 126 127 128 129 130 131 132 0 133 134 135 136 137 138 139 140 141 142 143 144 0 145 146 147 148 149 150 151 152 153 154 155 156 0 -1 -13 0 -1 -25 0 -1 -37 0 -1 -49 0 -1 -61 0 -1 -73 0 -1 -85 0 -1 -97 0 -1 -109 0 -1 -121 0 -1 -133 0 -1 -145 0 -13 -25 0 -13 -37 0 -13 -49 0 -13 -61 0 -13 -73 0 -13 -85 0 -13 -97 0 -13 -109 0 -13 -121 0 -13 -133 0 -13 -145 0 -25 -37 0 -25 -49 0 -25 -61 0 -25 -73 0 -25 -85 0 -25 -97 0 -25 -109 0 -25 -121 0 -25 -133 0 -25 -145 0 -37 -49 0 -37 -61 0 -37 -73 0 -37 -85 0 -37 -97 0 -37 -109 0 -37 -121 0 -37 -133 0 -37 -145 0 -49 -61 0 -49 -73 0 -49 -85 0 -49 -97 0 -49 -109 0 -49 -121 0 -49 -133 0 -49 -145 0 -61 -73 0 -61 -85 0 -61 -97 0 -61 -109 0 -61 -121 0 -61 -133 0 -61 -145 0 -73 -85 0 -73 -97 0 -73 -109 0 -73 -121 0 -73 -133 0 -73 -145 0 -85 -97 0 -85 -109 0 -85 -121 0 -85 -133 0 -85 -145 0 -97 -109 0 -97 -121 0 -97 -133 0 -97 -145 0 -109 -121 0 -109 -133 0 -109 -145 0 -121 -133 0 -121 -145 0 -133 -145 0 -2 -14 0 -2 -26 0 -2 -38 0 -2 -50 0 -2 -62 0 -2 -74 0 -2 -86 0 -2 -98 0 -2 -110 0 -2 -122 0 -2 -134 0 -2 -146 0 -14 -26 0 -14 -38 0 -14 -50 0 -14 -62 0 -14 -74 0 -14 -86 0 -14 -98 0 -14 -110 0 -14 -122 0 -14 -134 0 -14 -146 0 -26 -38 0 -26 -50 0 -26 -62 0 -26 -74 0 -26 -86 0 -26 -98 0 -26 -110 0 -26 -122 0 -26 -134 0 -26 -146 0 -38 -50 0 -38 -62 0 -38 -74 0 -38 -86 0 -38 -98 0 -38 -110 0 -38 -122 0 -38 -134 0 -38 -146 0 -50 -62 0 -50 -74 0 -50 -86 0 -50 -98 0 -50 -110 0 -50 -122 0 -50 -134 0 -50 -146 0 -62 -74 0 -62 -86 0 -62 -98 0 -62 -110 0 -62 -122 0 -62 -134 0 -62 -146 0 -74 -86 0 -74 -98 0 -74 -110 0 -74 -122 0 -74 -134 0 -74 -146 0 -86 -98 0 -86 -110 0 -86 -122 0 -86 -134 0 -86 -146 0 -98 -110 0 -98 -122 0 -98 -134 0 -98 -146 0 -110 -122 0 -110 -134 0 -110 -146 0 -122 -134 0 -122 -146 0 -134 -146 0 -3 -15 0 -3 -27 0 -3 -39 0 -3 -51 0 -3 -63 0 -3 -75 0 -3 -87 0 -3 -99 0 -3 -111 0 -3 -123 0 -3 -135 0 -3 -147 0 -15 -27 0 -15 -39 0 -15 -51 0 -15 -63 0 -15 -75 0 -15 -87 0 -15 -99 0 -15 -111 0 -15 -123 0 -15 -135 0 -15 -147 0 -27 -39 0 -27 -51 0 -27 -63 0 -27 -75 0 -27 -87 0 -27 -99 0 -27 -111 0 -27 -123 0 -27 -135 0 -27 -147 0 -39 -51 0 -39 -63 0 -39 -75 0 -39 -87 0 -39 -99 0 -39 -111 0 -39 -123 0 -39 -135 0 -39 -147 0 -51 -63 0 -51 -75 0 -51 -87 0 -51 -99 0 -51 -111 0 -51 -123 0 -51 -135 0 -51 -147 0 -63 -75 0 -63 -87 0 -63 -99 0 -63 -111 0 -63 -123 0 -63 -135 0 -63 -147 0 -75 -87 0 -75 -99 0 -75 -111 0 -75 -123 0 -75 -135 0 -75 -147 0 -87 -99 0 -87 -111 0 -87 -123 0 -87 -135 0 -87 -147 0 -99 -111 0 -99 -123 0 -99 -135 0 -99 -147 0 -111 -123 0 -111 -135 0 -111 -147 0 -123 -135 0 -123 -147 0 -135 -147 0 -4 -16 0 -4 -28 0 -4 -40 0 -4 -52 0 -4 -64 0 -4 -76 0 -4 -88 0 -4 -100 0 -4 -112 0 -4 -124 0 -4 -136 0 -4 -148 0 -16 -28 0 -16 -40 0 -16 -52 0 -16 -64 0 -16 -76 0 -16 -88 0 -16 -100 0 -16 -112 0 -16 -124 0 -16 -136 0 -16 -148 0 -28 -40 0 -28 -52 0 -28 -64 0 -28 -76 0 -28 -88 0 -28 -100 0 -28 -112 0 -28 -124 0 -28 -136 0 -28 -148 0 -40 -52 0 -40 -64 0 -40 -76 0 -40 -88 0 -40 -100 0 -40 -112 0 -40 -124 0 -40 -136 0 -40 -148 0 -52 -64 0 -52 -76 0 -52 -88 0 -52 -100 0 -52 -112 0 -52 -124 0 -52 -136 0 -52 -148 0 -64 -76 0 -64 -88 0 -64 -100 0 -64 -112 0 -64 -124 0 -64 -136 0 -64 -148 0 -76 -88 0 -76 -100 0 -76 -112 0 -76 -124 0 -76 -136 0 -76 -148 0 -88 -100 0 -88 -112 0 -88 -124 0 -88 -136 0 -88 -148 0 -100 -112 0 -100 -124 0 -100 -136 0 -100 -148 0 -112 -124 0 -112 -136 0 -112 -148 0 -124 -136 0 -124 -148 0 -136 -148 0 -5 -17 0 -5 -29 0 -5 -41 0 -5 -53 0 -5 -65 0 -5 -77 0 -5 -89 0 -5 -101 0 -5 -113 0 -5 -125 0 -5 -137 0 -5 -149 0 -17 -29 0 -17 -41 0 -17 -53 0 -17 -65 0 -17 -77 0 -17 -89 0 -17 -101 0 -17 -113 0 -17 -125 0 -17 -137 0 -17 -149 0 -29 -41 0 -29 -53 0 -29 -65 0 -29 -77 0 -29 -89 0 -29 -101 0 -29 -113 0 -29 -125 0 -29 -137 0 -29 -149 0 -41 -53 0 -41 -65 0 -41 -77 0 -41 -89 0 -41 -101 0 -41 -113 0 -41 -125 0 -41 -137 0 -41 -149 0 -53 -65 0 -53 -77 0 -53 -89 0 -53 -101 0 -53 -113 0 -53 -125 0 -53 -137 0 -53 -149 0 -65 -77 0 -65 -89 0 -65 -101 0 -65 -113 0 -65 -125 0 -65 -137 0 -65 -149 0 -77 -89 0 -77 -101 0 -77 -113 0 -77 -125 0 -77 -137 0 -77 -149 0 -89 -101 0 -89 -113 0 -89 -125 0 -89 -137 0 -89 -149 0 -101 -113 0 -101 -125 0 -101 -137 0 -101 -149 0 -113 -125 0 -113 -137 0 -113 -149 0 -125 -137 0 -125 -149 0 -137 -149 0 -6 -18 0 -6 -30 0 -6 -42 0 -6 -54 0 -6 -66 0 -6 -78 0 -6 -90 0 -6 -102 0 -6 -114 0 -6 -126 0 -6 -138 0 -6 -150 0 -18 -30 0 -18 -42 0 -18 -54 0 -18 -66 0 -18 -78 0 -18 -90 0 -18 -102 0 -18 -114 0 -18 -126 0 -18 -138 0 -18 -150 0 -30 -42 0 -30 -54 0 -30 -66 0 -30 -78 0 -30 -90 0 -30 -102 0 -30 -114 0 -30 -126 0 -30 -138 0 -30 -150 0 -42 -54 0 -42 -66 0 -42 -78 0 -42 -90 0 -42 -102 0 -42 -114 0 -42 -126 0 -42 -138 0 -42 -150 0 -54 -66 0 -54 -78 0 -54 -90 0 -54 -102 0 -54 -114 0 -54 -126 0 -54 -138 0 -54 -150 0 -66 -78 0 -66 -90 0 -66 -102 0 -66 -114 0 -66 -126 0 -66 -138 0 -66 -150 0 -78 -90 0 -78 -102 0 -78 -114 0 -78 -126 0 -78 -138 0 -78 -150 0 -90 -102 0 -90 -114 0 -90 -126 0 -90 -138 0 -90 -150 0 -102 -114 0 -102 -126 0 -102 -138 0 -102 -150 0 -114 -126 0 -114 -138 0 -114 -150 0 -126 -138 0 -126 -150 0 -138 -150 0 -7 -19 0 -7 -31 0 -7 -43 0 -7 -55 0 -7 -67 0 -7 -79 0 -7 -91 0 -7 -103 0 -7 -115 0 -7 -127 0 -7 -139 0 -7 -151 0 -19 -31 0 -19 -43 0 -19 -55 0 -19 -67 0 -19 -79 0 -19 -91 0 -19 -103 0 -19 -115 0 -19 -127 0 -19 -139 0 -19 -151 0 -31 -43 0 -31 -55 0 -31 -67 0 -31 -79 0 -31 -91 0 -31 -103 0 -31 -115 0 -31 -127 0 -31 -139 0 -31 -151 0 -43 -55 0 -43 -67 0 -43 -79 0 -43 -91 0 -43 -103 0 -43 -115 0 -43 -127 0 -43 -139 0 -43 -151 0 -55 -67 0 -55 -79 0 -55 -91 0 -55 -103 0 -55 -115 0 -55 -127 0 -55 -139 0 -55 -151 0 -67 -79 0 -67 -91 0 -67 -103 0 -67 -115 0 -67 -127 0 -67 -139 0 -67 -151 0 -79 -91 0 -79 -103 0 -79 -115 0 -79 -127 0 -79 -139 0 -79 -151 0 -91 -103 0 -91 -115 0 -91 -127 0 -91 -139 0 -91 -151 0 -103 -115 0 -103 -127 0 -103 -139 0 -103 -151 0 -115 -127 0 -115 -139 0 -115 -151 0 -127 -139 0 -127 -151 0 -139 -151 0 -8 -20 0 -8 -32 0 -8 -44 0 -8 -56 0 -8 -68 0 -8 -80 0 -8 -92 0 -8 -104 0 -8 -116 0 -8 -128 0 -8 -140 0 -8 -152 0 -20 -32 0 -20 -44 0 -20 -56 0 -20 -68 0 -20 -80 0 -20 -92 0 -20 -104 0 -20 -116 0 -20 -128 0 -20 -140 0 -20 -152 0 -32 -44 0 -32 -56 0 -32 -68 0 -32 -80 0 -32 -92 0 -32 -104 0 -32 -116 0 -32 -128 0 -32 -140 0 -32 -152 0 -44 -56 0 -44 -68 0 -44 -80 0 -44 -92 0 -44 -104 0 -44 -116 0 -44 -128 0 -44 -140 0 -44 -152 0 -56 -68 0 -56 -80 0 -56 -92 0 -56 -104 0 -56 -116 0 -56 -128 0 -56 -140 0 -56 -152 0 -68 -80 0 -68 -92 0 -68 -104 0 -68 -116 0 -68 -128 0 -68 -140 0 -68 -152 0 -80 -92 0 -80 -104 0 -80 -116 0 -80 -128 0 -80 -140 0 -80 -152 0 -92 -104 0 -92 -116 0 -92 -128 0 -92 -140 0 -92 -152 0 -104 -116 0 -104 -128 0 -104 -140 0 -104 -152 0 -116 -128 0 -116 -140 0 -116 -152 0 -128 -140 0 -128 -152 0 -140 -152 0 -9 -21 0 -9 -33 0 -9 -45 0 -9 -57 0 -9 -69 0 -9 -81 0 -9 -93 0 -9 -105 0 -9 -117 0 -9 -129 0 -9 -141 0 -9 -153 0 -21 -33 0 -21 -45 0 -21 -57 0 -21 -69 0 -21 -81 0 -21 -93 0 -21 -105 0 -21 -117 0 -21 -129 0 -21 -141 0 -21 -153 0 -33 -45 0 -33 -57 0 -33 -69 0 -33 -81 0 -33 -93 0 -33 -105 0 -33 -117 0 -33 -129 0 -33 -141 0 -33 -153 0 -45 -57 0 -45 -69 0 -45 -81 0 -45 -93 0 -45 -105 0 -45 -117 0 -45 -129 0 -45 -141 0 -45 -153 0 -57 -69 0 -57 -81 0 -57 -93 0 -57 -105 0 -57 -117 0 -57 -129 0 -57 -141 0 -57 -153 0 -69 -81 0 -69 -93 0 -69 -105 0 -69 -117 0 -69 -129 0 -69 -141 0 -69 -153 0 -81 -93 0 -81 -105 0 -81 -117 0 -81 -129 0 -81 -141 0 -81 -153 0 -93 -105 0 -93 -117 0 -93 -129 0 -93 -141 0 -93 -153 0 -105 -117 0 -105 -129 0 -105 -141 0 -105 -153 0 -117 -129 0 -117 -141 0 -117 -153 0 -129 -141 0 -129 -153 0 -141 -153 0 -10 -22 0 -10 -34 0 -10 -46 0 -10 -58 0 -10 -70 0 -10 -82 0 -10 -94 0 -10 -106 0 -10 -118 0 -10 -130 0 -10 -142 0 -10 -154 0 -22 -34 0 -22 -46 0 -22 -58 0 -22 -70 0 -22 -82 0 -22 -94 0 -22 -106 0 -22 -118 0 -22 -130 0 -22 -142 0 -22 -154 0 -34 -46 0 -34 -58 0 -34 -70 0 -34 -82 0 -34 -94 0 -34 -106 0 -34 -118 0 -34 -130 0 -34 -142 0 -34 -154 0 -46 -58 0 -46 -70 0 -46 -82 0 -46 -94 0 -46 -106 0 -46 -118 0 -46 -130 0 -46 -142 0 -46 -154 0 -58 -70 0 -58 -82 0 -58 -94 0 -58 -106 0 -58 -118 0 -58 -130 0 -58 -142 0 -58 -154 0 -70 -82 0 -70 -94 0 -70 -106 0 -70 -118 0 -70 -130 0 -70 -142 0 -70 -154 0 -82 -94 0 -82 -106 0 -82 -118 0 -82 -130 0 -82 -142 0 -82 -154 0 -94 -106 0 -94 -118 0 -94 -130 0 -94 -142 0 -94 -154 0 -106 -118 0 -106 -130 0 -106 -142 0 -106 -154 0 -118 -130 0 -118 -142 0 -118 -154 0 -130 -142 0 -130 -154 0 -142 -154 0 -11 -23 0 -11 -35 0 -11 -47 0 -11 -59 0 -11 -71 0 -11 -83 0 -11 -95 0 -11 -107 0 -11 -119 0 -11 -131 0 -11 -143 0 -11 -155 0 -23 -35 0 -23 -47 0 -23 -59 0 -23 -71 0 -23 -83 0 -23 -95 0 -23 -107 0 -23 -119 0 -23 -131 0 -23 -143 0 -23 -155 0 -35 -47 0 -35 -59 0 -35 -71 0 -35 -83 0 -35 -95 0 -35 -107 0 -35 -119 0 -35 -131 0 -35 -143 0 -35 -155 0 -47 -59 0 -47 -71 0 -47 -83 0 -47 -95 0 -47 -107 0 -47 -119 0 -47 -131 0 -47 -143 0 -47 -155 0 -59 -71 0 -59 -83 0 -59 -95 0 -59 -107 0 -59 -119 0 -59 -131 0 -59 -143 0 -59 -155 0 -71 -83 0 -71 -95 0 -71 -107 0 -71 -119 0 -71 -131 0 -71 -143 0 -71 -155 0 -83 -95 0 -83 -107 0 -83 -119 0 -83 -131 0 -83 -143 0 -83 -155 0 -95 -107 0 -95 -119 0 -95 -131 0 -95 -143 0 -95 -155 0 -107 -119 0 -107 -131 0 -107 -143 0 -107 -155 0 -119 -131 0 -119 -143 0 -119 -155 0 -131 -143 0 -131 -155 0 -143 -155 0 -12 -24 0 -12 -36 0 -12 -48 0 -12 -60 0 -12 -72 0 -12 -84 0 -12 -96 0 -12 -108 0 -12 -120 0 -12 -132 0 -12 -144 0 -12 -156 0 -24 -36 0 -24 -48 0 -24 -60 0 -24 -72 0 -24 -84 0 -24 -96 0 -24 -108 0 -24 -120 0 -24 -132 0 -24 -144 0 -24 -156 0 -36 -48 0 -36 -60 0 -36 -72 0 -36 -84 0 -36 -96 0 -36 -108 0 -36 -120 0 -36 -132 0 -36 -144 0 -36 -156 0 -48 -60 0 -48 -72 0 -48 -84 0 -48 -96 0 -48 -108 0 -48 -120 0 -48 -132 0 -48 -144 0 -48 -156 0 -60 -72 0 -60 -84 0 -60 -96 0 -60 -108 0 -60 -120 0 -60 -132 0 -60 -144 0 -60 -156 0 -72 -84 0 -72 -96 0 -72 -108 0 -72 -120 0 -72 -132 0 -72 -144 0 -72 -156 0 -84 -96 0 -84 -108 0 -84 -120 0 -84 -132 0 -84 -144 0 -84 -156 0 -96 -108 0 -96 -120 0 -96 -132 0 -96 -144 0 -96 -156 0 -108 -120 0 -108 -132 0 -108 -144 0 -108 -156 0 -120 -132 0 -120 -144 0 -120 -156 0 -132 -144 0 -132 -156 0 -144 -156 0