[HGAME 2023 week2]math yj233的WriteUp

from z3 import *
v10=[0]*25
v12=[0]*25
v11=[0]*25
v10[0] = 126
v10[1] = 225
v10[2] = 62
v10[3] = 40
v10[4] = 216
v10[5] = 253
v10[6] = 20
v10[7] = 124
v10[8] = 232
v10[9] = 122
v10[10] = 62
v10[11] = 23
v10[12] = 100
v10[13] = 161
v10[14] = 36
v10[15] = 118
v10[16] = 21
v10[17] = 184
v10[18] = 26
v10[19] = 142
v10[20] = 59
v10[21] = 31
v10[22] = 186
v10[23] = 82
v10[24] = 79
v12[0] = 63998
v12[1] = 33111
v12[2] = 67762
v12[3] = 54789
v12[4] = 61979
v12[5] = 69619
v12[6] = 37190
v12[7] = 70162
v12[8] = 53110
v12[9] = 68678
v12[10] = 63339
v12[11] = 30687
v12[12] = 66494
v12[13] = 50936
v12[14] = 60810
v12[15] = 48784
v12[16] = 30188
v12[17] = 60104
v12[18] = 44599
v12[19] = 52265
v12[20] = 43048
v12[21] = 23660
v12[22] = 43850
v12[23] = 33646
v12[24] = 44270

x = Solver()
flag = [Real('%d'%i) for i in range(32)]
for i in range(5):
    for j in range(5):
        for k in range(5):
            v11[5 * i + j] += flag[5 * i + k] * v10[5 * k + j]
for i in range(25):
    x.add(v11[i] == v12[i])
if x.check() == sat:
    model = x.model()
    s = ''
    for i in range(25):
        s += chr((model[flag[i]].as_long().real) & 0x7f)#0-127(0x00-0x7f)
    print(s)