c Boolean vector synthesis problem c n=4 m=2 k=6 A=16 c Specification: c 0 0 0 0 --> 0 0 c 0 0 0 1 --> 0 1 c 0 0 1 0 --> 1 0 c 0 0 1 1 --> 1 1 c 0 1 0 0 --> 0 1 c 0 1 0 1 --> 0 1 c 0 1 1 0 --> 1 0 c 0 1 1 1 --> 1 1 c 1 0 0 0 --> 1 0 c 1 0 0 1 --> 1 0 c 1 0 1 0 --> 1 0 c 1 0 1 1 --> 1 1 c 1 1 0 0 --> 1 1 c 1 1 0 1 --> 1 1 c 1 1 1 0 --> 1 1 c 1 1 1 1 --> 1 1 c Decision variables: c s[1][1] is 1 c s[1][2] is 2 c s[1][3] is 3 c s[1][4] is 4 c s[2][1] is 5 c s[2][2] is 6 c s[2][3] is 7 c s[2][4] is 8 c s[3][1] is 9 c s[3][2] is 10 c s[3][3] is 11 c s[3][4] is 12 c s[4][1] is 13 c s[4][2] is 14 c s[4][3] is 15 c s[4][4] is 16 c s[5][1] is 17 c s[5][2] is 18 c s[5][3] is 19 c s[5][4] is 20 c s[6][1] is 21 c s[6][2] is 22 c s[6][3] is 23 c s[6][4] is 24 c sp[1][1] is 25 c sp[1][2] is 26 c sp[1][3] is 27 c sp[1][4] is 28 c sp[2][1] is 29 c sp[2][2] is 30 c sp[2][3] is 31 c sp[2][4] is 32 c sp[3][1] is 33 c sp[3][2] is 34 c sp[3][3] is 35 c sp[3][4] is 36 c sp[4][1] is 37 c sp[4][2] is 38 c sp[4][3] is 39 c sp[4][4] is 40 c sp[5][1] is 41 c sp[5][2] is 42 c sp[5][3] is 43 c sp[5][4] is 44 c sp[6][1] is 45 c sp[6][2] is 46 c sp[6][3] is 47 c sp[6][4] is 48 c w[1][1] is 49 c w[1][2] is 50 c w[2][1] is 51 c w[2][2] is 52 c w[3][1] is 53 c w[3][2] is 54 c w[4][1] is 55 c w[4][2] is 56 c w[5][1] is 57 c w[5][2] is 58 c w[6][1] is 59 c w[6][2] is 60 c Auxiliary variables: c z[1][1][1] is 61 c z[1][1][2] is 62 c z[1][2][1] is 63 c z[1][2][2] is 64 c z[1][3][1] is 65 c z[1][3][2] is 66 c z[1][4][1] is 67 c z[1][4][2] is 68 c z[1][5][1] is 69 c z[1][5][2] is 70 c z[1][6][1] is 71 c z[1][6][2] is 72 c z[2][1][1] is 73 c z[2][1][2] is 74 c z[2][2][1] is 75 c z[2][2][2] is 76 c z[2][3][1] is 77 c z[2][3][2] is 78 c z[2][4][1] is 79 c z[2][4][2] is 80 c z[2][5][1] is 81 c z[2][5][2] is 82 c z[2][6][1] is 83 c z[2][6][2] is 84 c z[3][1][1] is 85 c z[3][1][2] is 86 c z[3][2][1] is 87 c z[3][2][2] is 88 c z[3][3][1] is 89 c z[3][3][2] is 90 c z[3][4][1] is 91 c z[3][4][2] is 92 c z[3][5][1] is 93 c z[3][5][2] is 94 c z[3][6][1] is 95 c z[3][6][2] is 96 c z[4][1][1] is 97 c z[4][1][2] is 98 c z[4][2][1] is 99 c z[4][2][2] is 100 c z[4][3][1] is 101 c z[4][3][2] is 102 c z[4][4][1] is 103 c z[4][4][2] is 104 c z[4][5][1] is 105 c z[4][5][2] is 106 c z[4][6][1] is 107 c z[4][6][2] is 108 c z[5][1][1] is 109 c z[5][1][2] is 110 c z[5][2][1] is 111 c z[5][2][2] is 112 c z[5][3][1] is 113 c z[5][3][2] is 114 c z[5][4][1] is 115 c z[5][4][2] is 116 c z[5][5][1] is 117 c z[5][5][2] is 118 c z[5][6][1] is 119 c z[5][6][2] is 120 c z[6][1][1] is 121 c z[6][1][2] is 122 c z[6][2][1] is 123 c z[6][2][2] is 124 c z[6][3][1] is 125 c z[6][3][2] is 126 c z[6][4][1] is 127 c z[6][4][2] is 128 c z[6][5][1] is 129 c z[6][5][2] is 130 c z[6][6][1] is 131 c z[6][6][2] is 132 c z[7][1][1] is 133 c z[7][1][2] is 134 c z[7][2][1] is 135 c z[7][2][2] is 136 c z[7][3][1] is 137 c z[7][3][2] is 138 c z[7][4][1] is 139 c z[7][4][2] is 140 c z[7][5][1] is 141 c z[7][5][2] is 142 c z[7][6][1] is 143 c z[7][6][2] is 144 c z[8][1][1] is 145 c z[8][1][2] is 146 c z[8][2][1] is 147 c z[8][2][2] is 148 c z[8][3][1] is 149 c z[8][3][2] is 150 c z[8][4][1] is 151 c z[8][4][2] is 152 c z[8][5][1] is 153 c z[8][5][2] is 154 c z[8][6][1] is 155 c z[8][6][2] is 156 c z[9][1][1] is 157 c z[9][1][2] is 158 c z[9][2][1] is 159 c z[9][2][2] is 160 c z[9][3][1] is 161 c z[9][3][2] is 162 c z[9][4][1] is 163 c z[9][4][2] is 164 c z[9][5][1] is 165 c z[9][5][2] is 166 c z[9][6][1] is 167 c z[9][6][2] is 168 c z[10][1][1] is 169 c z[10][1][2] is 170 c z[10][2][1] is 171 c z[10][2][2] is 172 c z[10][3][1] is 173 c z[10][3][2] is 174 c z[10][4][1] is 175 c z[10][4][2] is 176 c z[10][5][1] is 177 c z[10][5][2] is 178 c z[10][6][1] is 179 c z[10][6][2] is 180 c z[11][1][1] is 181 c z[11][1][2] is 182 c z[11][2][1] is 183 c z[11][2][2] is 184 c z[11][3][1] is 185 c z[11][3][2] is 186 c z[11][4][1] is 187 c z[11][4][2] is 188 c z[11][5][1] is 189 c z[11][5][2] is 190 c z[11][6][1] is 191 c z[11][6][2] is 192 c z[12][1][1] is 193 c z[12][1][2] is 194 c z[12][2][1] is 195 c z[12][2][2] is 196 c z[12][3][1] is 197 c z[12][3][2] is 198 c z[12][4][1] is 199 c z[12][4][2] is 200 c z[12][5][1] is 201 c z[12][5][2] is 202 c z[12][6][1] is 203 c z[12][6][2] is 204 c z[13][1][1] is 205 c z[13][1][2] is 206 c z[13][2][1] is 207 c z[13][2][2] is 208 c z[13][3][1] is 209 c z[13][3][2] is 210 c z[13][4][1] is 211 c z[13][4][2] is 212 c z[13][5][1] is 213 c z[13][5][2] is 214 c z[13][6][1] is 215 c z[13][6][2] is 216 c z[14][1][1] is 217 c z[14][1][2] is 218 c z[14][2][1] is 219 c z[14][2][2] is 220 c z[14][3][1] is 221 c z[14][3][2] is 222 c z[14][4][1] is 223 c z[14][4][2] is 224 c z[14][5][1] is 225 c z[14][5][2] is 226 c z[14][6][1] is 227 c z[14][6][2] is 228 c z[15][1][1] is 229 c z[15][1][2] is 230 c z[15][2][1] is 231 c z[15][2][2] is 232 c z[15][3][1] is 233 c z[15][3][2] is 234 c z[15][4][1] is 235 c z[15][4][2] is 236 c z[15][5][1] is 237 c z[15][5][2] is 238 c z[15][6][1] is 239 c z[15][6][2] is 240 c z[16][1][1] is 241 c z[16][1][2] is 242 c z[16][2][1] is 243 c z[16][2][2] is 244 c z[16][3][1] is 245 c z[16][3][2] is 246 c z[16][4][1] is 247 c z[16][4][2] is 248 c z[16][5][1] is 249 c z[16][5][2] is 250 c z[16][6][1] is 251 c z[16][6][2] is 252 p cnf 252 766 1 25 0 5 29 0 9 33 0 13 37 0 17 41 0 21 45 0 2 26 0 6 30 0 10 34 0 14 38 0 18 42 0 22 46 0 3 27 0 7 31 0 11 35 0 15 39 0 19 43 0 23 47 0 4 28 0 8 32 0 12 36 0 16 40 0 20 44 0 24 48 0 -49 -1 -2 -3 -4 0 -51 -5 -6 -7 -8 0 -53 -9 -10 -11 -12 0 -55 -13 -14 -15 -16 0 -57 -17 -18 -19 -20 0 -59 -21 -22 -23 -24 0 -49 -1 -2 -3 -28 0 -51 -5 -6 -7 -32 0 -53 -9 -10 -11 -36 0 -55 -13 -14 -15 -40 0 -57 -17 -18 -19 -44 0 -59 -21 -22 -23 -48 0 -49 -1 -26 -3 -4 0 -51 -5 -30 -7 -8 0 -53 -9 -34 -11 -12 0 -55 -13 -38 -15 -16 0 -57 -17 -42 -19 -20 0 -59 -21 -46 -23 -24 0 -49 -1 -26 -3 -28 0 -51 -5 -30 -7 -32 0 -53 -9 -34 -11 -36 0 -55 -13 -38 -15 -40 0 -57 -17 -42 -19 -44 0 -59 -21 -46 -23 -48 0 -50 -1 -2 -3 -4 0 -52 -5 -6 -7 -8 0 -54 -9 -10 -11 -12 0 -56 -13 -14 -15 -16 0 -58 -17 -18 -19 -20 0 -60 -21 -22 -23 -24 0 -50 -1 -2 -27 -4 0 -52 -5 -6 -31 -8 0 -54 -9 -10 -35 -12 0 -56 -13 -14 -39 -16 0 -58 -17 -18 -43 -20 0 -60 -21 -22 -47 -24 0 -50 -1 -26 -27 -4 0 -52 -5 -30 -31 -8 0 -54 -9 -34 -35 -12 0 -56 -13 -38 -39 -16 0 -58 -17 -42 -43 -20 0 -60 -21 -46 -47 -24 0 -50 -25 -2 -3 -4 0 -52 -29 -6 -7 -8 0 -54 -33 -10 -11 -12 0 -56 -37 -14 -15 -16 0 -58 -41 -18 -19 -20 0 -60 -45 -22 -23 -24 0 -50 -25 -2 -3 -28 0 -52 -29 -6 -7 -32 0 -54 -33 -10 -11 -36 0 -56 -37 -14 -15 -40 0 -58 -41 -18 -19 -44 0 -60 -45 -22 -23 -48 0 -50 -25 -2 -27 -4 0 -52 -29 -6 -31 -8 0 -54 -33 -10 -35 -12 0 -56 -37 -14 -39 -16 0 -58 -41 -18 -43 -20 0 -60 -45 -22 -47 -24 0 85 87 89 91 93 95 0 97 99 101 103 105 107 0 133 135 137 139 141 143 0 145 147 149 151 153 155 0 157 159 161 163 165 167 0 169 171 173 175 177 179 0 181 183 185 187 189 191 0 193 195 197 199 201 203 0 205 207 209 211 213 215 0 217 219 221 223 225 227 0 229 231 233 235 237 239 0 241 243 245 247 249 251 0 74 76 78 80 82 84 0 98 100 102 104 106 108 0 110 112 114 116 118 120 0 122 124 126 128 130 132 0 146 148 150 152 154 156 0 194 196 198 200 202 204 0 206 208 210 212 214 216 0 218 220 222 224 226 228 0 230 232 234 236 238 240 0 242 244 246 248 250 252 0 -85 49 0 -87 51 0 -89 53 0 -91 55 0 -93 57 0 -95 59 0 -97 49 0 -99 51 0 -101 53 0 -103 55 0 -105 57 0 -107 59 0 -133 49 0 -135 51 0 -137 53 0 -139 55 0 -141 57 0 -143 59 0 -145 49 0 -147 51 0 -149 53 0 -151 55 0 -153 57 0 -155 59 0 -157 49 0 -159 51 0 -161 53 0 -163 55 0 -165 57 0 -167 59 0 -169 49 0 -171 51 0 -173 53 0 -175 55 0 -177 57 0 -179 59 0 -181 49 0 -183 51 0 -185 53 0 -187 55 0 -189 57 0 -191 59 0 -193 49 0 -195 51 0 -197 53 0 -199 55 0 -201 57 0 -203 59 0 -205 49 0 -207 51 0 -209 53 0 -211 55 0 -213 57 0 -215 59 0 -217 49 0 -219 51 0 -221 53 0 -223 55 0 -225 57 0 -227 59 0 -229 49 0 -231 51 0 -233 53 0 -235 55 0 -237 57 0 -239 59 0 -241 49 0 -243 51 0 -245 53 0 -247 55 0 -249 57 0 -251 59 0 -74 50 0 -76 52 0 -78 54 0 -80 56 0 -82 58 0 -84 60 0 -98 50 0 -100 52 0 -102 54 0 -104 56 0 -106 58 0 -108 60 0 -110 50 0 -112 52 0 -114 54 0 -116 56 0 -118 58 0 -120 60 0 -122 50 0 -124 52 0 -126 54 0 -128 56 0 -130 58 0 -132 60 0 -146 50 0 -148 52 0 -150 54 0 -152 56 0 -154 58 0 -156 60 0 -194 50 0 -196 52 0 -198 54 0 -200 56 0 -202 58 0 -204 60 0 -206 50 0 -208 52 0 -210 54 0 -212 56 0 -214 58 0 -216 60 0 -218 50 0 -220 52 0 -222 54 0 -224 56 0 -226 58 0 -228 60 0 -230 50 0 -232 52 0 -234 54 0 -236 56 0 -238 58 0 -240 60 0 -242 50 0 -244 52 0 -246 54 0 -248 56 0 -250 58 0 -252 60 0 -85 1 0 -87 5 0 -89 9 0 -91 13 0 -93 17 0 -95 21 0 -85 2 0 -87 6 0 -89 10 0 -91 14 0 -93 18 0 -95 22 0 -85 27 0 -87 31 0 -89 35 0 -91 39 0 -93 43 0 -95 47 0 -85 4 0 -87 8 0 -89 12 0 -91 16 0 -93 20 0 -95 24 0 -97 1 0 -99 5 0 -101 9 0 -103 13 0 -105 17 0 -107 21 0 -97 2 0 -99 6 0 -101 10 0 -103 14 0 -105 18 0 -107 22 0 -97 27 0 -99 31 0 -101 35 0 -103 39 0 -105 43 0 -107 47 0 -97 28 0 -99 32 0 -101 36 0 -103 40 0 -105 44 0 -107 48 0 -133 1 0 -135 5 0 -137 9 0 -139 13 0 -141 17 0 -143 21 0 -133 26 0 -135 30 0 -137 34 0 -139 38 0 -141 42 0 -143 46 0 -133 27 0 -135 31 0 -137 35 0 -139 39 0 -141 43 0 -143 47 0 -133 4 0 -135 8 0 -137 12 0 -139 16 0 -141 20 0 -143 24 0 -145 1 0 -147 5 0 -149 9 0 -151 13 0 -153 17 0 -155 21 0 -145 26 0 -147 30 0 -149 34 0 -151 38 0 -153 42 0 -155 46 0 -145 27 0 -147 31 0 -149 35 0 -151 39 0 -153 43 0 -155 47 0 -145 28 0 -147 32 0 -149 36 0 -151 40 0 -153 44 0 -155 48 0 -157 25 0 -159 29 0 -161 33 0 -163 37 0 -165 41 0 -167 45 0 -157 2 0 -159 6 0 -161 10 0 -163 14 0 -165 18 0 -167 22 0 -157 3 0 -159 7 0 -161 11 0 -163 15 0 -165 19 0 -167 23 0 -157 4 0 -159 8 0 -161 12 0 -163 16 0 -165 20 0 -167 24 0 -169 25 0 -171 29 0 -173 33 0 -175 37 0 -177 41 0 -179 45 0 -169 2 0 -171 6 0 -173 10 0 -175 14 0 -177 18 0 -179 22 0 -169 3 0 -171 7 0 -173 11 0 -175 15 0 -177 19 0 -179 23 0 -169 28 0 -171 32 0 -173 36 0 -175 40 0 -177 44 0 -179 48 0 -181 25 0 -183 29 0 -185 33 0 -187 37 0 -189 41 0 -191 45 0 -181 2 0 -183 6 0 -185 10 0 -187 14 0 -189 18 0 -191 22 0 -181 27 0 -183 31 0 -185 35 0 -187 39 0 -189 43 0 -191 47 0 -181 4 0 -183 8 0 -185 12 0 -187 16 0 -189 20 0 -191 24 0 -193 25 0 -195 29 0 -197 33 0 -199 37 0 -201 41 0 -203 45 0 -193 2 0 -195 6 0 -197 10 0 -199 14 0 -201 18 0 -203 22 0 -193 27 0 -195 31 0 -197 35 0 -199 39 0 -201 43 0 -203 47 0 -193 28 0 -195 32 0 -197 36 0 -199 40 0 -201 44 0 -203 48 0 -205 25 0 -207 29 0 -209 33 0 -211 37 0 -213 41 0 -215 45 0 -205 26 0 -207 30 0 -209 34 0 -211 38 0 -213 42 0 -215 46 0 -205 3 0 -207 7 0 -209 11 0 -211 15 0 -213 19 0 -215 23 0 -205 4 0 -207 8 0 -209 12 0 -211 16 0 -213 20 0 -215 24 0 -217 25 0 -219 29 0 -221 33 0 -223 37 0 -225 41 0 -227 45 0 -217 26 0 -219 30 0 -221 34 0 -223 38 0 -225 42 0 -227 46 0 -217 3 0 -219 7 0 -221 11 0 -223 15 0 -225 19 0 -227 23 0 -217 28 0 -219 32 0 -221 36 0 -223 40 0 -225 44 0 -227 48 0 -229 25 0 -231 29 0 -233 33 0 -235 37 0 -237 41 0 -239 45 0 -229 26 0 -231 30 0 -233 34 0 -235 38 0 -237 42 0 -239 46 0 -229 27 0 -231 31 0 -233 35 0 -235 39 0 -237 43 0 -239 47 0 -229 4 0 -231 8 0 -233 12 0 -235 16 0 -237 20 0 -239 24 0 -241 25 0 -243 29 0 -245 33 0 -247 37 0 -249 41 0 -251 45 0 -241 26 0 -243 30 0 -245 34 0 -247 38 0 -249 42 0 -251 46 0 -241 27 0 -243 31 0 -245 35 0 -247 39 0 -249 43 0 -251 47 0 -241 28 0 -243 32 0 -245 36 0 -247 40 0 -249 44 0 -251 48 0 -74 1 0 -76 5 0 -78 9 0 -80 13 0 -82 17 0 -84 21 0 -74 2 0 -76 6 0 -78 10 0 -80 14 0 -82 18 0 -84 22 0 -74 3 0 -76 7 0 -78 11 0 -80 15 0 -82 19 0 -84 23 0 -74 28 0 -76 32 0 -78 36 0 -80 40 0 -82 44 0 -84 48 0 -98 1 0 -100 5 0 -102 9 0 -104 13 0 -106 17 0 -108 21 0 -98 2 0 -100 6 0 -102 10 0 -104 14 0 -106 18 0 -108 22 0 -98 27 0 -100 31 0 -102 35 0 -104 39 0 -106 43 0 -108 47 0 -98 28 0 -100 32 0 -102 36 0 -104 40 0 -106 44 0 -108 48 0 -110 1 0 -112 5 0 -114 9 0 -116 13 0 -118 17 0 -120 21 0 -110 26 0 -112 30 0 -114 34 0 -116 38 0 -118 42 0 -120 46 0 -110 3 0 -112 7 0 -114 11 0 -116 15 0 -118 19 0 -120 23 0 -110 4 0 -112 8 0 -114 12 0 -116 16 0 -118 20 0 -120 24 0 -122 1 0 -124 5 0 -126 9 0 -128 13 0 -130 17 0 -132 21 0 -122 26 0 -124 30 0 -126 34 0 -128 38 0 -130 42 0 -132 46 0 -122 3 0 -124 7 0 -126 11 0 -128 15 0 -130 19 0 -132 23 0 -122 28 0 -124 32 0 -126 36 0 -128 40 0 -130 44 0 -132 48 0 -146 1 0 -148 5 0 -150 9 0 -152 13 0 -154 17 0 -156 21 0 -146 26 0 -148 30 0 -150 34 0 -152 38 0 -154 42 0 -156 46 0 -146 27 0 -148 31 0 -150 35 0 -152 39 0 -154 43 0 -156 47 0 -146 28 0 -148 32 0 -150 36 0 -152 40 0 -154 44 0 -156 48 0 -194 25 0 -196 29 0 -198 33 0 -200 37 0 -202 41 0 -204 45 0 -194 2 0 -196 6 0 -198 10 0 -200 14 0 -202 18 0 -204 22 0 -194 27 0 -196 31 0 -198 35 0 -200 39 0 -202 43 0 -204 47 0 -194 28 0 -196 32 0 -198 36 0 -200 40 0 -202 44 0 -204 48 0 -206 25 0 -208 29 0 -210 33 0 -212 37 0 -214 41 0 -216 45 0 -206 26 0 -208 30 0 -210 34 0 -212 38 0 -214 42 0 -216 46 0 -206 3 0 -208 7 0 -210 11 0 -212 15 0 -214 19 0 -216 23 0 -206 4 0 -208 8 0 -210 12 0 -212 16 0 -214 20 0 -216 24 0 -218 25 0 -220 29 0 -222 33 0 -224 37 0 -226 41 0 -228 45 0 -218 26 0 -220 30 0 -222 34 0 -224 38 0 -226 42 0 -228 46 0 -218 3 0 -220 7 0 -222 11 0 -224 15 0 -226 19 0 -228 23 0 -218 28 0 -220 32 0 -222 36 0 -224 40 0 -226 44 0 -228 48 0 -230 25 0 -232 29 0 -234 33 0 -236 37 0 -238 41 0 -240 45 0 -230 26 0 -232 30 0 -234 34 0 -236 38 0 -238 42 0 -240 46 0 -230 27 0 -232 31 0 -234 35 0 -236 39 0 -238 43 0 -240 47 0 -230 4 0 -232 8 0 -234 12 0 -236 16 0 -238 20 0 -240 24 0 -242 25 0 -244 29 0 -246 33 0 -248 37 0 -250 41 0 -252 45 0 -242 26 0 -244 30 0 -246 34 0 -248 38 0 -250 42 0 -252 46 0 -242 27 0 -244 31 0 -246 35 0 -248 39 0 -250 43 0 -252 47 0 -242 28 0 -244 32 0 -246 36 0 -248 40 0 -250 44 0 -252 48 0