1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151
| from z3 import *
# for i in range(1, 32): # print('x' + str(i) + ',', end='') # print(' = Ints(\'', end='') # for i in range(1, 32): # print('x'+str(i),end=' ') # print('\')') x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27, x28, x29, x30 = Ints( 'x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30') solver = Solver() # for i in range(30): # str = input() # print('solver.add('+str+')') solver.add( 334 * x28 + 100 * x27 + 369 * x26 + 124 * x25 + 278 * x24 + 158 * x23 + 162 * x22 + 145 * x19 + 27 * x17 + 91 * x15 + 195 * x14 + 342 * x13 + 391 * x10 + 204 * x9 + 302 * x8 + 153 * x7 + 292 * x6 + 382 * x5 + 221 * x4 + 316 * x3 + 118 * x2 + 295 * x1 + 247 * x0 + 236 * x11 + 27 * x12 + 361 * x16 + 81 * x18 + 105 * x20 + 65 * x21 + 67 * x29 + 41 * x30 == 596119) solver.add( 371 * x29 + 338 * x28 + 269 * x27 + 312 * x26 + 67 * x25 + 299 * x24 + 235 * x23 + 294 * x22 + 303 * x21 + 211 * x20 + 122 * x19 + 333 * x18 + 341 * x15 + 111 * x14 + 253 * x13 + 68 * x12 + 347 * x11 + 44 * x10 + 262 * x9 + 357 * x8 + 323 * x5 + 141 * x4 + 329 * x3 + 378 * x2 + 316 * x1 + 235 * x0 + 59 * x6 + 37 * x7 + 264 * x16 + 73 * x17 + 126 * x30 == 634009) solver.add( 337 * x29 + 338 * x28 + 118 * x27 + 82 * x26 + 239 * x21 + 58 * x20 + 304 * x19 + 330 * x18 + 377 * x17 + 306 * x16 + 221 * x13 + 345 * x12 + 124 * x11 + 272 * x10 + 270 * x9 + 229 * x8 + 377 * x7 + 373 * x6 + 297 * x5 + 112 * x4 + 386 * x3 + 90 * x2 + 361 * x1 + 236 * x0 + 386 * x14 + 73 * x15 + 315 * x22 + 33 * x23 + 141 * x24 + 129 * x25 + 123 * x30 == 685705) solver.add( 367 * x29 + 55 * x28 + 374 * x27 + 150 * x24 + 350 * x23 + 141 * x22 + 124 * x21 + 366 * x20 + 230 * x19 + 307 * x18 + 191 * x17 + 153 * x12 + 383 * x11 + 145 * x10 + 109 * x9 + 209 * x8 + 158 * x7 + 221 * x6 + 188 * x5 + 22 * x4 + 146 * x3 + 306 * x2 + 230 * x1 + 13 * x0 + 287 * x13 + 257 * x14 + 137 * x15 + 7 * x16 + 52 * x25 + 31 * x26 + 355 * x30 == 557696) solver.add( 100 * x29 + 191 * x28 + 362 * x27 + 55 * x26 + 210 * x25 + 359 * x24 + 348 * x21 + 83 * x20 + 395 * x19 + 350 * x16 + 291 * x15 + 220 * x12 + 196 * x11 + 399 * x8 + 68 * x7 + 84 * x6 + 281 * x5 + 334 * x4 + 53 * x3 + 399 * x2 + 338 * x0 + 18 * x1 + 148 * x9 + 21 * x10 + 174 * x13 + 36 * x14 + 2 * x17 + 41 * x18 + 137 * x22 + 24 * x23 + 368 * x30 == 538535) solver.add( 188 * x29 + 128 * x26 + 93 * x25 + 248 * x24 + 83 * x23 + 207 * x22 + 217 * x19 + 309 * x16 + 16 * x15 + 135 * x14 + 251 * x13 + 200 * x12 + 49 * x11 + 119 * x10 + 356 * x9 + 398 * x8 + 303 * x7 + 224 * x6 + 208 * x5 + 244 * x4 + 209 * x3 + 189 * x2 + 302 * x1 + 395 * x0 + 314 * x17 + 13 * x18 + 310 * x20 + 21 * x21 + 67 * x27 + 127 * x28 + 100 * x30 == 580384) solver.add( 293 * x29 + 343 * x28 + 123 * x27 + 387 * x26 + 114 * x25 + 303 * x24 + 248 * x23 + 258 * x21 + 218 * x20 + 180 * x19 + 196 * x18 + 398 * x17 + 398 * x14 + 138 * x9 + 292 * x8 + 38 * x7 + 179 * x6 + 190 * x5 + 57 * x4 + 358 * x3 + 191 * x2 + 215 * x1 + 88 * x0 + 22 * x10 + 72 * x11 + 357 * x12 + 9 * x13 + 389 * x15 + 81 * x16 + 85 * x30 == 529847) solver.add( 311 * x29 + 202 * x28 + 234 * x27 + 272 * x26 + 55 * x25 + 328 * x24 + 246 * x23 + 362 * x22 + 86 * x21 + 75 * x20 + 142 * x17 + 244 * x16 + 216 * x15 + 281 * x14 + 398 * x13 + 322 * x12 + 251 * x11 + 357 * x8 + 76 * x7 + 292 * x6 + 389 * x5 + 275 * x4 + 312 * x3 + 200 * x2 + 110 * x1 + 203 * x0 + 99 * x9 + 21 * x10 + 269 * x18 + 33 * x19 + 356 * x30 == 631652) solver.add( 261 * x29 + 189 * x26 + 55 * x25 + 23 * x24 + 202 * x23 + 185 * x22 + 182 * x21 + 285 * x20 + 217 * x17 + 157 * x16 + 232 * x15 + 132 * x14 + 169 * x13 + 154 * x12 + 121 * x11 + 389 * x10 + 376 * x9 + 292 * x6 + 225 * x5 + 155 * x4 + 234 * x3 + 149 * x2 + 241 * x1 + 312 * x0 + 368 * x7 + 129 * x8 + 226 * x18 + 288 * x19 + 201 * x27 + 288 * x28 + 69 * x30 == 614840) solver.add( 60 * x29 + 118 * x28 + 153 * x27 + 139 * x26 + 23 * x25 + 279 * x24 + 396 * x23 + 287 * x22 + 237 * x19 + 266 * x18 + 149 * x17 + 193 * x16 + 395 * x15 + 97 * x14 + 16 * x13 + 286 * x12 + 105 * x11 + 88 * x10 + 282 * x9 + 55 * x8 + 134 * x7 + 114 * x6 + 101 * x5 + 116 * x4 + 271 * x3 + 186 * x2 + 263 * x1 + 313 * x0 + 149 * x20 + 129 * x21 + 145 * x30 == 510398) solver.add( 385 * x29 + 53 * x28 + 112 * x27 + 8 * x26 + 232 * x25 + 145 * x24 + 313 * x23 + 156 * x22 + 321 * x21 + 358 * x20 + 46 * x19 + 382 * x18 + 144 * x16 + 222 * x14 + 329 * x13 + 161 * x12 + 335 * x11 + 50 * x10 + 373 * x9 + 66 * x8 + 44 * x7 + 59 * x6 + 292 * x5 + 39 * x4 + 53 * x3 + 310 * x0 + 154 * x1 + 24 * x2 + 396 * x15 + 81 * x17 + 355 * x30 == 558740) solver.add( 249 * x29 + 386 * x28 + 313 * x27 + 74 * x26 + 22 * x25 + 168 * x24 + 305 * x21 + 358 * x20 + 191 * x19 + 202 * x18 + 14 * x15 + 114 * x14 + 224 * x13 + 134 * x12 + 274 * x11 + 372 * x10 + 159 * x9 + 233 * x8 + 70 * x7 + 287 * x6 + 297 * x5 + 318 * x4 + 177 * x3 + 173 * x2 + 270 * x1 + 163 * x0 + 77 * x16 + 25 * x17 + 387 * x22 + 18 * x23 + 345 * x30 == 592365) solver.add( 392 * x29 + 385 * x28 + 302 * x27 + 13 * x25 + 27 * x24 + 99 * x22 + 343 * x19 + 324 * x18 + 223 * x17 + 372 * x16 + 261 * x15 + 181 * x14 + 203 * x13 + 232 * x12 + 305 * x11 + 393 * x10 + 325 * x9 + 231 * x8 + 92 * x7 + 142 * x6 + 22 * x5 + 86 * x4 + 264 * x3 + 300 * x2 + 387 * x1 + 360 * x0 + 225 * x20 + 127 * x21 + 2 * x23 + 80 * x26 + 268 * x30 == 619574) solver.add( 270 * x28 + 370 * x27 + 235 * x26 + 96 * x22 + 85 * x20 + 150 * x19 + 140 * x18 + 94 * x17 + 295 * x16 + 19 * x14 + 176 * x12 + 94 * x11 + 258 * x10 + 302 * x9 + 171 * x8 + 66 * x7 + 278 * x6 + 193 * x5 + 251 * x4 + 284 * x3 + 218 * x2 + 64 * x1 + 319 * x0 + 125 * x13 + 24 * x15 + 267 * x21 + 160 * x23 + 111 * x24 + 33 * x25 + 174 * x29 + 13 * x30 == 480557) solver.add( 87 * x28 + 260 * x27 + 326 * x26 + 210 * x25 + 357 * x24 + 170 * x23 + 315 * x22 + 376 * x21 + 227 * x20 + 43 * x19 + 358 * x18 + 364 * x17 + 309 * x16 + 282 * x15 + 286 * x14 + 365 * x13 + 287 * x12 + 377 * x11 + 74 * x10 + 225 * x9 + 328 * x6 + 223 * x5 + 120 * x4 + 102 * x3 + 162 * x2 + 123 * x1 + 196 * x0 + 29 * x7 + 27 * x8 + 352 * x30 == 666967) solver.add( 61 * x29 + 195 * x28 + 125 * x27 + 64 * x26 + 260 * x25 + 202 * x24 + 116 * x23 + 230 * x22 + 326 * x21 + 211 * x20 + 371 * x19 + 353 * x16 + 124 * x13 + 188 * x12 + 163 * x11 + 140 * x10 + 51 * x9 + 262 * x8 + 229 * x7 + 100 * x6 + 113 * x5 + 158 * x4 + 378 * x3 + 365 * x2 + 207 * x1 + 277 * x0 + 190 * x14 + 320 * x15 + 347 * x17 + 11 * x18 + 137 * x30 == 590534) solver.add( 39 * x28 + 303 * x27 + 360 * x26 + 157 * x25 + 324 * x24 + 77 * x23 + 308 * x22 + 313 * x21 + 87 * x20 + 201 * x19 + 50 * x18 + 60 * x17 + 28 * x16 + 193 * x15 + 184 * x14 + 205 * x13 + 140 * x12 + 311 * x11 + 304 * x10 + 35 * x9 + 356 * x8 + 23 * x5 + 85 * x4 + 156 * x3 + 16 * x2 + 26 * x1 + 157 * x0 + 150 * x6 + 72 * x7 + 58 * x29 == 429108) solver.add( 157 * x29 + 137 * x28 + 71 * x27 + 269 * x26 + 161 * x25 + 317 * x20 + 296 * x19 + 385 * x18 + 165 * x13 + 159 * x12 + 132 * x11 + 296 * x10 + 162 * x7 + 254 * x4 + 172 * x3 + 132 * x0 + 369 * x1 + 257 * x2 + 134 * x5 + 384 * x6 + 53 * x8 + 255 * x9 + 229 * x14 + 129 * x15 + 23 * x16 + 41 * x17 + 112 * x21 + 17 * x22 + 222 * x23 + 96 * x24 + 126 * x30 == 563521) solver.add( 207 * x29 + 83 * x28 + 111 * x27 + 35 * x26 + 67 * x25 + 138 * x22 + 223 * x21 + 142 * x20 + 154 * x19 + 111 * x18 + 341 * x17 + 175 * x16 + 259 * x15 + 225 * x14 + 26 * x11 + 334 * x10 + 250 * x7 + 198 * x6 + 279 * x5 + 301 * x4 + 193 * x3 + 334 * x2 + 134 * x0 + 37 * x1 + 183 * x8 + 5 * x9 + 270 * x12 + 21 * x13 + 275 * x23 + 48 * x24 + 163 * x30 == 493999) solver.add( 393 * x29 + 176 * x28 + 105 * x27 + 162 * x26 + 148 * x25 + 281 * x24 + 300 * x23 + 342 * x18 + 262 * x17 + 152 * x12 + 43 * x11 + 296 * x10 + 273 * x9 + 75 * x6 + 18 * x4 + 217 * x2 + 132 * x1 + 112 * x0 + 210 * x3 + 72 * x5 + 113 * x7 + 40 * x8 + 278 * x13 + 24 * x14 + 77 * x15 + 11 * x16 + 55 * x19 + 255 * x20 + 241 * x21 + 13 * x22 + 356 * x30 == 470065) solver.add( 369 * x29 + 231 * x28 + 285 * x25 + 290 * x24 + 297 * x23 + 189 * x22 + 390 * x21 + 345 * x20 + 153 * x19 + 114 * x18 + 251 * x17 + 340 * x16 + 44 * x15 + 58 * x14 + 335 * x13 + 359 * x12 + 392 * x11 + 181 * x8 + 103 * x7 + 229 * x6 + 175 * x5 + 208 * x4 + 92 * x3 + 397 * x2 + 349 * x1 + 356 * x0 + 64 * x9 + 5 * x10 + 88 * x26 + 40 * x27 + 295 * x30 == 661276) solver.add( 341 * x27 + 40 * x25 + 374 * x23 + 201 * x22 + 77 * x21 + 215 * x20 + 283 * x19 + 213 * x18 + 392 * x17 + 224 * x16 + 1 * x15 + 270 * x12 + 28 * x11 + 75 * x8 + 386 * x7 + 298 * x6 + 170 * x5 + 287 * x4 + 247 * x3 + 204 * x2 + 103 * x1 + 21 * x0 + 84 * x9 + 27 * x10 + 159 * x13 + 192 * x14 + 213 * x24 + 129 * x26 + 67 * x28 + 27 * x29 + 361 * x30 == 555288) solver.add( 106 * x29 + 363 * x28 + 210 * x27 + 171 * x26 + 289 * x25 + 240 * x24 + 164 * x23 + 342 * x22 + 391 * x19 + 304 * x18 + 218 * x17 + 32 * x16 + 350 * x15 + 339 * x12 + 303 * x11 + 222 * x10 + 298 * x9 + 47 * x8 + 48 * x6 + 264 * x4 + 113 * x3 + 275 * x2 + 345 * x1 + 312 * x0 + 171 * x5 + 384 * x7 + 175 * x13 + 5 * x14 + 113 * x20 + 19 * x21 + 263 * x30 == 637650) solver.add( 278 * x29 + 169 * x28 + 62 * x27 + 119 * x26 + 385 * x25 + 289 * x24 + 344 * x23 + 45 * x20 + 308 * x19 + 318 * x18 + 270 * x17 + 1 * x16 + 323 * x15 + 332 * x14 + 287 * x11 + 170 * x10 + 163 * x9 + 301 * x8 + 303 * x7 + 23 * x6 + 327 * x5 + 169 * x3 + 28 * x0 + 365 * x1 + 15 * x2 + 352 * x12 + 72 * x13 + 140 * x21 + 65 * x22 + 346 * x30 == 572609) solver.add( 147 * x29 + 88 * x28 + 143 * x27 + 237 * x26 + 63 * x24 + 281 * x22 + 388 * x21 + 142 * x20 + 208 * x19 + 60 * x18 + 354 * x15 + 88 * x14 + 146 * x13 + 290 * x12 + 349 * x11 + 43 * x10 + 230 * x9 + 267 * x6 + 136 * x5 + 383 * x4 + 35 * x3 + 226 * x2 + 385 * x1 + 238 * x0 + 348 * x7 + 20 * x8 + 158 * x16 + 21 * x17 + 249 * x23 + 9 * x25 + 343 * x30 == 603481) solver.add( 29 * x29 + 323 * x26 + 159 * x25 + 118 * x20 + 326 * x19 + 211 * x18 + 225 * x17 + 355 * x16 + 201 * x15 + 149 * x14 + 296 * x13 + 184 * x12 + 315 * x11 + 364 * x10 + 142 * x9 + 75 * x8 + 313 * x7 + 142 * x6 + 396 * x5 + 348 * x4 + 272 * x3 + 26 * x2 + 206 * x1 + 173 * x0 + 155 * x21 + 144 * x22 + 366 * x23 + 257 * x24 + 148 * x27 + 24 * x28 + 253 * x30 == 664504) solver.add( 4 * x29 + 305 * x28 + 226 * x27 + 212 * x26 + 175 * x25 + 93 * x24 + 165 * x23 + 341 * x20 + 14 * x19 + 394 * x18 + 256 * x17 + 252 * x16 + 336 * x15 + 38 * x14 + 82 * x13 + 155 * x12 + 215 * x11 + 331 * x10 + 230 * x9 + 241 * x8 + 225 * x7 + 186 * x4 + 90 * x3 + 50 * x2 + 62 * x1 + 34 * x0 + 237 * x5 + 11 * x6 + 336 * x21 + 36 * x22 + 29 * x30 == 473092) solver.add( 353 * x29 + 216 * x28 + 252 * x27 + 8 * x26 + 62 * x25 + 233 * x24 + 254 * x23 + 303 * x22 + 234 * x21 + 303 * x20 + 256 * x19 + 148 * x18 + 324 * x17 + 317 * x16 + 213 * x15 + 309 * x14 + 28 * x13 + 280 * x11 + 118 * x10 + 58 * x9 + 50 * x8 + 155 * x7 + 161 * x6 + 64 * x5 + 303 * x4 + 76 * x3 + 43 * x2 + 109 * x1 + 102 * x0 + 93 * x30 == 497492) solver.add( 89 * x29 + 148 * x28 + 82 * x27 + 53 * x26 + 274 * x25 + 220 * x24 + 202 * x23 + 123 * x22 + 231 * x21 + 169 * x20 + 278 * x19 + 259 * x18 + 208 * x17 + 219 * x16 + 371 * x15 + 181 * x12 + 104 * x11 + 392 * x10 + 285 * x9 + 113 * x8 + 298 * x7 + 389 * x6 + 322 * x5 + 338 * x4 + 237 * x3 + 234 * x0 + 261 * x1 + 10 * x2 + 345 * x13 + 3 * x14 + 361 * x30 == 659149) solver.add( 361 * x29 + 359 * x28 + 93 * x27 + 315 * x26 + 69 * x25 + 137 * x24 + 69 * x23 + 58 * x22 + 300 * x21 + 371 * x20 + 264 * x19 + 317 * x18 + 215 * x17 + 155 * x16 + 215 * x15 + 330 * x14 + 239 * x13 + 212 * x12 + 88 * x11 + 82 * x10 + 354 * x9 + 85 * x8 + 310 * x7 + 84 * x6 + 374 * x5 + 380 * x4 + 215 * x3 + 351 * x2 + 141 * x1 + 115 * x0 + 108 * x30 == 629123)
print(solver.check()) print(solver.model())
# x29 = 33, # x18 = 69, # x22 = 116, # x0 = 109, # x3 = 99, # x7 = 121, # x23 = 105, # x11 = 115, # x30 = 125, # x13 = 108, # x20 = 117, # x1 = 111, # x10 = 95, # x16 = 100, # x25 = 110, # x21 = 97, # x26 = 115, # x6 = 123, # x2 = 101, # x12 = 48, # x19 = 113, # x24 = 48, # x9 = 117, # x4 = 116, # x5 = 102, # x17 = 95, # x8 = 48, # x14 = 118, # x28 = 33, # x27 = 33, # x15 = 51
data = { 'x29': 33, 'x18': 69, 'x22': 116, 'x0': 109, 'x3': 99, 'x7': 121, 'x23': 105, 'x11': 115, 'x30': 125, 'x13': 108, 'x20': 117, 'x1': 111, 'x10': 95, 'x16': 100, 'x25': 110, 'x21': 97, 'x26': 115, 'x6': 123, 'x2': 101, 'x12': 48, 'x19': 113, 'x24': 48, 'x9': 117, 'x4': 116, 'x5': 102, 'x17': 95, 'x8': 48, 'x14': 118, 'x28': 33, 'x27': 33, 'x15': 51 }
# # 按照 x 后的数字进行排序 # sorted_data = sorted(data.items(), key=lambda item: int(item[0][1:])) # # # 重组数据 # result = ''.join(chr(value) for key, value in sorted_data) # # print(result)
|