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
| from z3 import *
v4, SBYTE1v4, SBYTE2v4, SBYTE3v4, SBYTE4v4, SBYTE5v4, SBYTE6v4, SHIBYTEv4 = Ints( 'v4 SBYTE1v4 SBYTE2v4 SBYTE3v4 SBYTE4v4 SBYTE5v4 SBYTE6v4 SHIBYTEv4') v5, SBYTE1v5, SBYTE2v5, SBYTE3v5, SBYTE4v5, SBYTE5v5, SBYTE6v5, SHIBYTEv5 = Ints( 'v5 SBYTE1v5 SBYTE2v5 SBYTE3v5 SBYTE4v5 SBYTE5v5 SBYTE6v5 SHIBYTEv5') v6, SBYTE1v6, SBYTE2v6, SBYTE3v6, SBYTE4v6, SBYTE5v6, SBYTE6v6, SHIBYTEv6 = Ints( 'v6 SBYTE1v6 SBYTE2v6 SBYTE3v6 SBYTE4v6 SBYTE5v6 SBYTE6v6 SHIBYTEv6') v7, SBYTE1v7, SBYTE2v7, SBYTE3v7, SBYTE4v7, SBYTE5v7, SBYTE6v7, SHIBYTEv7 = Ints( 'v7 SBYTE1v7 SBYTE2v7 SBYTE3v7 SBYTE4v7 SBYTE5v7 SBYTE6v7 SHIBYTEv7') v8, SBYTE1v8, SBYTE2v8, SBYTE3v8, SBYTE4v8, SBYTE5v8, SBYTE6v8, SHIBYTEv8 = Ints( 'v8 SBYTE1v8 SBYTE2v8 SBYTE3v8 SBYTE4v8 SBYTE5v8 SBYTE6v8 SHIBYTEv8') v9, SBYTE1v9, SBYTE2v9 = Ints('v9 SBYTE1v9 SBYTE2v9')
s = Solver() s.add(v4 + 293 + 682 * SBYTE1v4 == 56972, 582 * SBYTE1v4 + 211 * SBYTE2v4 == 62443, SBYTE2v4 - 246 - 940 * SBYTE3v4 == -79139, SBYTE3v4 - 612 + 399 - SBYTE4v4 == -199, SBYTE4v4 + 709 - (200 - SBYTE5v4) == 702, SBYTE5v4 + 818 + 281 - SBYTE6v4 == 1169, 295 * SBYTE6v4 - 122 * SHIBYTEv4 == 9535, SHIBYTEv4 + 577 + 369 * v5 == 19815, v5 - 530 + 488 * SBYTE1v5 == 22946, 578 * SBYTE1v5 + 232 - SBYTE2v5 == 27921, SBYTE2v5 - 266 + 168 - SBYTE3v5 == -91, SBYTE4v5 + 591 + 610 * SBYTE3v5 == 29919, SBYTE4v5 + 322 + 257 * SBYTE5v5 == 13477, SBYTE6v5 + 368 + 206 * SBYTE5v5 == 10919, SBYTE6v5 + 815 - (350 - SHIBYTEv5) == 562, 266 * SHIBYTEv5 + 400 * v6 == 52632, v6 - 651 - (SBYTE1v6 + 303) == -957, SBYTE1v6 + 889 + SBYTE2v6 + 980 == 2019, SBYTE2v6 - 968 + 730 * SBYTE3v6 == 31932, SBYTE3v6 + 254 - (676 - SBYTE4v6) == -325, SBYTE4v6 - 969 + SBYTE5v6 + 950 == 86, SBYTE5v6 + 597 - (SBYTE6v6 + 120) == 478, SBYTE6v6 - 412 + 861 - SHIBYTEv6 == 450, 722 * SHIBYTEv6 - 697 * v7 == 5457, v7 + 871 - 741 * SBYTE1v7 == -40580, 805 * SBYTE1v7 - 838 * SBYTE2v7 == -172, SBYTE3v7 + 636 + 646 * SBYTE2v7 == 35573, 889 * SBYTE3v7 + 688 * SBYTE4v7 == 115917, SBYTE5v7 + 830 + 462 * SBYTE4v7 == 47075, SBYTE5v7 + 556 - (118 - SBYTE6v7) == 532, SBYTE6v7 - 783 + 840 * SHIBYTEv7 == 84946, SHIBYTEv7 + 964 + v8 + 990 == 2109, v8 + 698 + SBYTE1v8 + 923 == 1774, 384 * SBYTE1v8 + 847 * SBYTE2v8 == 79056, SBYTE2v8 + 358 + 637 * SBYTE3v8 == 62195, SBYTE4v8 + 693 + 818 * SBYTE3v8 == 80089, SBYTE4v8 - 638 + 348 - SBYTE5v8 == -292, SBYTE5v8 + 425 - (828 - SBYTE6v8) == -295, SBYTE6v8 - 941 + SHIBYTEv8 + 331 == -453, SHIBYTEv8 - 826 - 370 * v9 == -19595, v9 - 857 - (818 - SBYTE1v9) == -1527, 999 * SBYTE1v9 + 616 * SBYTE2v9 == 173903, 498 * SBYTE2v9 + 206 * v4 == 77288)
if s.check() == sat: m = (s.model()) sorted_model = sorted(m, key=lambda x: str(x)) for variable in sorted_model: print(f"{variable} = {m[variable]}")
else: print("无解")
|