-
-
[原创]第二题 南冥神功 z3约束求解
-
发表于: 2021-5-12 13:44 6095
-
最后几分钟没提交上。
题目比较明确
迷宫问题,需要将所有0都遍历成1。然后用z3约束求解一下得到答案
table1和table2表示每个字符需要约束的结果v10和v7
from
z3
import
*
x
=
Int
(
'x'
)
table1
=
[
1
,
3
,
3
,
1
,
3
,
3
,
1
,
0
,
2
,
0
,
5
,
5
,
3
,
5
,
5
,
1
,
1
,
1
,
1
,
3
,
3
,
2
,
2
]
table2
=
[
2
,
4
,
2
,
2
,
4
,
2
,
1
,
1
,
1
,
0
,
0
,
4
,
4
,
0
,
0
,
2
,
0
,
2
,
2
,
4
,
2
,
3
,
1
]
idx2
=
[]
for
i
in
range
(
len
(table1)):
solve(
5
-
(i
+
x)
%
6
=
=
table1[i],(i
+
x
/
6
)
%
6
=
=
table2[i],x>
=
0
,x<
=
36
)
str
=
"0123456789ABCDEFGHIJKLMNOPQRSTUVWXYZ"
idx
=
[
16
,
19
,
0
,
31
,
4
,
21
,
10
,
4
,
31
,
20
,
14
,
31
,
26
,
35
,
28
,
31
,
12
,
23
,
16
,
19
,
0
,
0
,
23
]
for
i
in
range
(
len
(idx)):
print
(
str
[idx[i]],end
=
'')
from
z3
import
*
x
=
Int
(
'x'
)
table1
=
[
1
,
3
,
3
,
1
,
3
,
3
,
1
,
0
,
2
,
0
,
5
,
5
,
3
,
5
,
5
,
1
,
1
,
1
,
1
,
3
,
3
,
2
,
2
]
table2
=
[
2
,
4
,
2
,
2
,
4
,
2
,
1
,
1
,
1
,
0
,
0
,
4
,
4
,
0
,
0
,
2
,
0
,
2
,
2
,
4
,
2
,
3
,
1
]
[培训]内核驱动高级班,冲击BAT一流互联网大厂工作,每周日13:00-18:00直播授课
赞赏
他的文章
- KCTF 迷失丛林 18343
- [原创]office病毒分析资料整理 15425
- [原创] 初入门径 --- 护网钓鱼样本分析 10683
- [原创]2021年第四届红帽杯Re ezRev和file_store题解 11096
- [原创]第二题 南冥神功 z3约束求解 6096
看原图
赞赏
雪币:
留言: