# Challenge 4 sat-solver using Z3 - jiva

import z3

# Define z3 variables
pw0 = z3.Int('pw0')
pw1 = z3.Int('pw1')
pw2 = z3.Int('pw2')
pw3 = z3.Int('pw3')
pw4 = z3.Int('pw4')
pw5 = z3.Int('pw5')
pw6 = z3.Int('pw6')
pw7 = z3.Int('pw7')
pw8 = z3.Int('pw8')
pw9 = z3.Int('pw9')
pw10 = z3.Int('pw10')
pw11 = z3.Int('pw11')
pw12 = z3.Int('pw12')
pw13 = z3.Int('pw13')
pw14 = z3.Int('pw14')
pw15 = z3.Int('pw15')
pw16 = z3.Int('pw16')
pw17 = z3.Int('pw17')
pw18 = z3.Int('pw18')
pw19 = z3.Int('pw19')
pw20 = z3.Int('pw20')
pw21 = z3.Int('pw21')
pw22 = z3.Int('pw22')

# Store variables in a list for printing purposes later
chars = [pw0,pw1,pw2,pw3,pw4,pw5,pw6,pw7,pw8,pw9,pw10,pw11,pw12,pw13,pw14,pw15,pw16,pw17,pw18,pw19,pw20,pw21,pw22]

# Initialize the solver
s = z3.Solver()

# Add the constraints
s.add(pw22 * 0xba5 + pw0 * 0xb02 + pw1 * 0x2253 + pw2 * 0x1fa7 + pw3 * 0x1ab0 + pw4 * -0x1ec2 + pw5 * -0x1957 + pw6 * 0x12ec + pw7 * -0x175e + pw8 * -0x1170 + pw9 * 0x250f + pw10 * 0x566 + pw11 * 0x153e + pw12 * 0xa2f + pw13 * -0x2567 + pw14 * -0x200f + pw15 * 0x13f8 + pw16 * 0x17ec + pw17 * 0x1b43 + pw18 * 0x260b + pw19 * 0xd58 + pw20 * -0x176b + pw21 * -0xbbd == 0x25ddae)
s.add(pw22 * 0x441 + pw0 * 0x144a + pw1 * 0xd38 + pw2 * 0x23a3 + pw3 * 0x3ac + pw4 * 0x5f4 + pw5 * 0xfce + pw6 * 0x1dcb + pw7 * 0x137d + pw8 * 0x1bba + pw9 * -0x128 + pw10 * 0x2157 + pw11 * -0xa79 + pw12 * 0xef0 + pw13 * 0x17ec + pw14 * 0x1eee + pw15 * 0x22a + pw16 * -0x198f + pw17 * 0x765 + pw18 * 0x16c8 + pw19 * 0x24b9 + pw20 * 0x76e + pw21 * -0x1e3e == 0x58dc8a)
s.add(pw22 * -0x1d2 + pw0 * 0x14ae + pw1 * -0x25a9 + pw2 * -0x1697 + pw3 * -0x2152 + pw4 * 0x9b + pw5 * 0xa4e + pw6 * 0x1f3c + pw7 * 0x1ca9 + pw8 * -0x1e67 + pw9 * 0x9c4 + pw10 * 0x1e49 + pw11 * -0x20b2 + pw12 * -0x24c9 + pw13 * 0x1f06 + pw14 * 0xdf5 + pw15 * 0x10c4 + pw16 * 0x1917 + pw17 * 0x1112 + pw18 * 0x48e + pw19 * 0x7b5 + pw20 * 0x19d0 + pw21 * 0xa11 == 0x1d4940)
s.add(pw22 * 0x12b4 + pw0 * 0x529 + pw1 * 0x22c9 + pw2 * 0x1ae5 + pw3 * 0xd74 + pw4 * -0x21a4 + pw5 * 0x376 + pw6 * 0x1193 + pw7 * 0xa21 + pw8 * -0x540 + pw9 * 0x225 + pw10 * -0xdb2 + pw11 * 0x408 + pw12 * 0xeb5 + pw13 * -0x2ff + pw14 * 0x5d8 + pw15 * -0x110a + pw16 * -0x2377 + pw17 * 0x2303 + pw18 * 0x2153 + pw19 * -0x3da + pw20 * -0x6af + pw21 * 0xea == 0x122acb)
s.add(pw22 * 0x6e4 + pw0 * 0x77a + pw1 * 0x2369 + pw2 * 0x159e + pw3 * 0x1be8 + pw4 * 0x13d + pw5 * 0xe7 + pw6 * -0xe6f + pw7 * 0xd3c + pw8 * -0x14f7 + pw9 * -0x1cfd + pw10 * 0x20cb + pw11 * 0x1e + pw12 * 0x40b + pw13 * 0x3c6 + pw14 * -0x2167 + pw15 * 0x13a6 + pw16 * 0x20e6 + pw17 * 0x19e9 + pw18 * 0xf3d + pw19 * 0xd1e + pw20 * 0xeb7 + pw21 * 0x347 == 0x49ee81)
s.add(pw22 * 0x13b5 + pw0 * 0x2033 + pw1 * 0x102f + pw2 * 0xd38 + pw3 * -0x16d9 + pw4 * 0x1181 + pw5 * 0x15f6 + pw6 * -0x1219 + pw7 * -0x1aa6 + pw8 * -0xb23 + pw9 * -0x1dd1 + pw10 * 0x5df + pw11 * -0x1a08 + pw12 * 0x1df6 + pw13 * -0x247f + pw14 * 0xa96 + pw15 * 0x1624 + pw16 * -0x562 + pw17 * -0x1b65 + pw18 * -0x287 + pw19 * -0xd2f + pw20 * 0x1f49 + pw21 * -0x11bb == 0x62b11)
s.add(pw22 * 0x25d5 + pw0 * 0x228a + pw1 * 0x1306 + pw2 * 0x368 + pw3 * 0x1bdd + pw4 * 0xb5c + pw5 * -0x241 + pw6 * 0xa1a + pw7 * -0x14d7 + pw8 * 0x65b + pw9 * 0xadc + pw10 * 0x1a17 + pw11 * 0xdd4 + pw12 * 0x25f0 + pw13 * -0xad1 + pw14 * -0x4c1 + pw15 * -0x256 + pw16 * 0x449 + pw17 * 0x197c + pw18 * -0x1d3f + pw19 * 0x131d + pw20 * 0xa2b + pw21 * 0xcb9 == 0x4a508d)
s.add(pw22 * -0x1df0 + pw0 * 0x1d82 + pw1 * 0x270a + pw2 * 0x19c4 + pw3 * -0x237 + pw4 * -0x2254 + pw5 * 0x267e + pw6 * 0x98d + pw7 * 0xd9b + pw8 * 0x1145 + pw9 * -0x24c0 + pw10 * 0x389 + pw11 * 0x1a9e + pw12 * 0x996 + pw13 * 0x1385 + pw14 * 0xadd + pw15 * -0x1cb5 + pw16 * 0x1526 + pw17 * 0x40e + pw18 * 0x1ee1 + pw19 * 0x1a47 + pw20 * 0xbbd + pw21 * 0x253f == 0x42d8a4)
s.add(pw22 * 0x1d02 + pw0 * 0xe5d + pw1 * 0x8d + pw2 * 0x13a8 + pw3 * 0x4ab + pw4 * -0x10ee + pw5 * 0x207 + pw6 * -0x1c34 + pw7 * 0x15ab + pw8 * 0xeec + pw9 * 0xce5 + pw10 * 0x280 + pw11 * -0x1cc9 + pw12 * 0x1b9a + pw13 * 0x871 + pw14 * 0x2ba + pw15 * 0xd76 + pw16 * -0x590 + pw17 * -0x167f + pw18 * 0xbe + pw19 * 0x130b + pw20 * 0x8fe + pw21 * -0x1d7f == 0x1d7b0d)
s.add(pw22 * -0xc7d + pw0 * 0x21ca + pw1 * 0x3e6 + pw2 * 0x347 + pw3 * 0x24f1 + pw4 * -0x1940 + pw5 * 0x2f + pw6 * -0x2002 + pw7 * -0x1a2d + pw8 * -0x1882 + pw9 * 0xffb + pw10 * 0xb40 + pw11 * 0xadf + pw12 * -0x11cb + pw13 * 0x129e + pw14 * 0x232b + pw15 * 0xbc3 + pw16 * -0xf53 + pw17 * -0x1e23 + pw18 * 0x13b1 + pw19 * 0x64f + pw20 * -0x23 + pw21 * -0x2304 == -0x88e13)
s.add(pw22 * -0x16e1 + pw0 * 0x1950 + pw1 * 0x681 + pw2 * -0x217c + pw3 * -0x2671 + pw4 * 0xc7c + pw5 * 0x26ec + pw6 * -0x108e + pw7 * 0xb77 + pw8 * -0x1408 + pw9 * 0x2342 + pw10 * -0x2501 + pw11 * 0x1bf2 + pw12 * -0x1864 + pw13 * -0x1bed + pw14 * -0x21f8 + pw15 * 0x1dc + pw16 * -0x6c2 + pw17 * 0x66e + pw18 * 0x1b42 + pw19 * -0x613 + pw20 * 0x1bcc + pw21 * -0x21ec == -0x219469)
s.add(pw22 * 0xa02 + pw0 * 0x7c4 + pw1 * -0xda5 + pw2 * 0x1abc + pw3 * 0x72f + pw4 * 0x126d + pw5 * 0x25f3 + pw6 * 0x20c + pw7 * 0x612 + pw8 * -0x818 + pw9 * -0xa29 + pw10 * -0x512 + pw11 * 0x1098 + pw12 * 0xd1 + pw13 * -0x705 + pw14 * 0x1ddc + pw15 * 0x1a9a + pw16 * 0x1b7b + pw17 * 0xf46 + pw18 * 0x17ce + pw19 * 0x2038 + pw20 * 0x71a + pw21 * 0x217b == 0x5ca54b)
s.add(pw22 * 0x26e0 + pw0 * 0x10bf + pw1 * -0x1cf7 + pw2 * -0x7df + pw3 * 0x1b3b + pw4 * -0xf35 + pw5 * -0x6d0 + pw6 * 0x9ec + pw7 * 0x847 + pw8 * 0xfde + pw9 * -0x23ce + pw10 * 0x1078 + pw11 * -0x24f4 + pw12 * 0x4ec + pw13 * 0xe79 + pw14 * 0x972 + pw15 * -0x1ef9 + pw16 * -0xf06 + pw17 * 0xa33 + pw18 * 0x1448 + pw19 * 0x186e + pw20 * -0xb13 + pw21 * 0x16af == 0xb9934)
s.add(pw22 * 0x14e8 + pw0 * 0x1e07 + pw1 * -0x17da + pw2 * 0x36a + pw3 * 0xe6c + pw4 * 0x7cd + pw5 * 0x12fb + pw6 * 0x484 + pw7 * 0x10f4 + pw8 * 0x8f6 + pw9 * -0x160f + pw10 * -0x21ad + pw11 * 0x1ab4 + pw12 * 0x23df + pw13 * 0x11e9 + pw14 * 0x5f6 + pw15 * -0x1e74 + pw16 * -0x2658 + pw17 * -0xfe3 + pw18 * 0x1952 + pw19 * 0x260a + pw20 * -0x1280 + pw21 * -0x1e6a == 0x7bac7)
s.add(pw22 * 0x10bc + pw0 * 0x199e + pw1 * 0xd17 + pw2 * -0xeaa + pw3 * -0x435 + pw4 * 0xbe + pw5 * -0xcb3 + pw6 * 0x8a3 + pw7 * 0x9ff + pw8 * 0x560 + pw9 * 0x389 + pw10 * -0xc49 + pw11 * 0x1adf + pw12 * -0x1398 + pw13 * 0x7f0 + pw14 * -0x1cb1 + pw15 * -0x1830 + pw16 * 0x1abc + pw17 * 0x21d8 + pw18 * 0x263a + pw19 * 0x1f6f + pw20 * 300 + pw21 * -0xbce == 0x171bef)
s.add(pw22 * -0x730 + pw0 * 0x2008 + pw1 * -0x21c2 + pw2 * -0x1dc + pw3 * 0x9dc + pw4 * 0x56a + pw5 * 0x5c1 + pw6 * 0x1a0a + pw7 * -0x10b5 + pw8 * -0x154b + pw9 * 0xbef + pw10 * -0x21b5 + pw11 * 0x209e + pw12 * 1999 + pw13 * -0xec5 + pw14 * 0x18ac + pw15 * 0x1405 + pw16 * -0x3c1 + pw17 * -0x2690 + pw18 * -0x8e9 + pw19 * 0x205f + pw20 * 0x212b + pw21 * 0x115 == 0x374bd)
s.add(pw22 * -0x695 + pw0 * 0x5ff + pw1 * 0x1831 + pw2 * 0x26f7 + pw3 * -0x53a + pw4 * 0x1863 + pw5 * 0x2278 + pw6 * -0x21a8 + pw7 * 0x1361 + pw8 * 0xc8e + pw9 * 0x358 + pw10 * 0x3e4 + pw11 * -0x899 + pw12 * 0x1419 + pw13 * 0x16b7 + pw14 * -0x1da5 + pw15 * 0x1b0c + pw16 * -0xafb + pw17 * 0x920 + pw18 * 0xa57 + pw19 * 0x26f4 + pw20 * 0x637 + pw21 * 0x25dd == 0x5767ea)
s.add(pw22 * -0x1944 + pw0 * 0x1373 + pw1 * 0x1bb4 + pw2 * -0x1f97 + pw3 * -0x14c1 + pw4 * -0x6fb + pw5 * 0xa8b + pw6 * -0x669 + pw7 * 0xfbc + pw8 * -0x14e3 + pw9 * 0x1c00 + pw10 * 0x1a44 + pw11 * 0xfc7 + pw12 * -0x231a + pw13 * 0x624 + pw14 * 0xf92 + pw15 * -0xaa0 + pw16 * 0x1ab1 + pw17 * -0x1ee6 + pw18 * -0x3f4 + pw19 * 0x1462 + pw20 * 0x1fd1 + pw21 * 0x65e == 0x279a0)
s.add(pw22 * -0x1c3b + pw0 * 0x25ec + pw1 * 0x18ff + pw2 * 0x215d + pw3 * 0x1332 + pw4 * 0xe63 + pw5 * 0x2634 + pw6 * 0x8dc + pw7 * 0x2655 + pw8 * -0x7db + pw9 * -0xd40 + pw10 * -0x3f4 + pw11 * 0xf19 + pw12 * 0x3f9 + pw13 * -0xd85 + pw14 * -0x230c + pw15 * 0x2207 + pw16 * -0x2670 + pw17 * 0x1577 + pw18 * 0x1b66 + pw19 * 0x7c + pw20 * 0x1db + pw21 * 0x1095 == 0x498a62)
s.add(pw22 * 0x251d + pw0 * 0x22e6 + pw1 * 0x26a6 + pw2 * 0x14cc + pw3 * 0x261a + pw4 * -0xe1e + pw5 * -0xf54 + pw6 * 0x312 + pw7 * 0x18fe + pw8 * 0x26c4 + pw9 * 0x1fa8 + pw10 * 0x1fcc + pw11 * -0x1572 + pw12 * 0x25c + pw13 * 0x52f + pw14 * 0x65 + pw15 * 0x923 + pw16 * 0x259c + pw17 * -0xf98 + pw18 * 0x24e9 + pw19 * 0xd16 + pw20 * 0x12c2 + pw21 * 0x19f2 == 0x739b84)
s.add(pw22 * -0x158e + pw0 * 0x7c8 + pw1 * -0x17c4 + pw2 * -0x6fa + pw3 * -0x1ed7 + pw4 * 0xe2d + pw5 * 0x3c6 + pw6 * 0xfc3 + pw7 * 0x1e14 + pw8 * 0x73 + pw9 * -0x19ee + pw10 * 0x15f + pw11 * 0x80a + pw12 * -0xc46 + pw13 * 0x24c + pw14 * -0x69b + pw15 * -0xdb2 + pw16 * 0x738 + pw17 * 0x21cc + pw18 * 0x1f1c + pw19 * 0x174d + pw20 * 0x303 + pw21 * 0x14dc == 0x110941)
s.add(pw22 * 0x1ab4 + pw0 * 0x1fb9 + pw1 * -0x1e0d + pw2 * 0x338 + pw3 * -0x1596 + pw4 * 0x810 + pw5 * 0x18d6 + pw6 * 0x8d + pw7 * -0x466 + pw8 * 0x268e + pw9 * -0x1449 + pw10 * 0x446 + pw11 * 0x16e8 + pw12 * -0xdd6 + pw13 * -0x153f + pw14 * 0xc5f + pw15 * 0xfae + pw16 * 0x10f1 + pw17 * -0x41b + pw18 * 0x15b9 + pw19 * 0x207c + pw20 * 0x1527 + pw21 * 0x257b == 0x3b34df)
s.add(pw22 * 0x1dc8 + pw0 * 0x1dfc + pw1 * -0x1580 + pw2 * 0x1e9d + pw3 * 0xa5c + pw4 * 0xc62 + pw5 * 0x22f8 + pw6 * -0xdc8 + pw7 * 0x2397 + pw8 * -0x8b1 + pw9 * 0x4c7 + pw10 * -0xf6f + pw11 * 0x5d + pw12 * -0x7b4 + pw13 * -0x1d12 + pw14 * -0x91f + pw15 * 0x1689 + pw16 * 0xbc1 + pw17 * 600 + pw18 * 0xede + pw19 * 0xb4f + pw20 * 0x2229 + pw21 * 0x232a == 0x49d71b)

# Check if the constraints are satisfiable
if s.check().r != 1:
    print('not sat')
else:
    m = s.model()
    print(''.join(chr(m[c].as_long()) for c in chars))