from
z3
import
*
arr1
=
[
0X7A
,
0XCF
,
0X8C
,
0X95
,
0X8E
,
0XA8
,
0X5F
,
0XC9
,
0X7A
,
0X91
,
0X88
,
0XA7
,
0X70
,
0XC0
,
0X7F
,
0X89
,
0X86
,
0X93
,
0X5F
,
0XCF
,
0X6E
,
0X86
,
0X85
,
0XAD
,
0X88
,
0XD4
,
0XA0
,
0XA2
,
0X98
,
0XB3
,
0X79
,
0XC1
,
0X7E
,
0X7E
,
0X77
,
0X93
]
arr2
=
[
0x10
,
0x08
,
0X08
,
0x0E
,
0X06
,
0X0B
,
0X5
,
0X17
,
0X05
,
0X0A
,
0X0C
,
0X17
,
0X0E
,
0X17
,
0X13
,
0X07
,
0X08
,
0X0A
,
0X04
,
0X0D
,
0X16
,
0X11
,
0X0B
,
0X16
,
0X06
,
0X0E
,
0X02
,
0X0B
,
0X12
,
0X09
,
0X05
,
0X08
,
0X08
,
0X0A
,
0X10
,
0X0D
]
arr3
=
[
8
,
1
,
7
,
1
,
1
,
0
,
4
,
8
,
1
,
2
,
3
,
9
,
3
,
8
,
6
,
6
,
4
,
8
,
3
,
5
,
7
,
8
,
8
,
7
,
0
,
9
,
0
,
2
,
3
,
4
,
2
,
3
,
2
,
5
,
4
,
0
]
temp
=
[BitVec(
'%d'
%
i,
8
)
for
i
in
range
(
36
)]
s
=
Solver()
for
i
in
range
(
36
):
s.add(temp[i] <
127
)
s.add(temp[i] >
=
32
)
ptr
=
[
0
]
*
36
v7
=
[
0
]
*
36
one
=
[
0
]
*
36
two
=
[
0
]
*
36
for
i
in
range
(
36
):
ptr[i]
=
temp[i] >>
4
v7[i]
=
temp[i] &
15
for
i
in
range
(
6
):
for
j
in
range
(
6
):
for
k
in
range
(
6
):
one[
6
*
i
+
j]
+
=
ptr[
6
*
i
+
k]
*
arr3[
6
*
k
+
j]
for
i
in
range
(
6
):
for
j
in
range
(
6
):
two[
6
*
i
+
j]
=
v7[
6
*
i
+
j]
+
arr3[
6
*
i
+
j]
for
i
in
range
(
36
):
s.add(one[i]
=
=
arr1[i])
s.add(two[i]
=
=
arr2[i])
flag
=
[]
strflag
=
''
if
s.check()
=
=
sat:
result
=
s.model()
for
i
in
temp:
flag.append(result[i])
print
(flag)
else
:
print
(
'无解'
)
result
=
[
104
,
103
,
97
,
109
,
101
,
123
,
49
,
95
,
116
,
104
,
105
,
110
,
107
,
95
,
77
,
97
,
116
,
114
,
49
,
120
,
95
,
105
,
115
,
95
,
118
,
101
,
114
,
121
,
95
,
117
,
115
,
101
,
102
,
53
,
108
,
125
]
for
i
in
range
(
36
):
strflag
+
=
chr
(result[i])
print
(strflag)