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