首页
社区
课程
招聘
[原创]2022 KCTF春季赛 第7题
2022-5-23 15:30 3980

[原创]2022 KCTF春季赛 第7题

2022-5-23 15:30
3980

Z3求解

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
from z3 import *
 
flag = [Int("flag_%d" % i) for i in range(16)]
 
s = Solver()
s.add(flag[1] == 3)
s.add(flag[2] == 1)
s.add(flag[4] == 1)
s.add(flag[7] == 3)
s.add(flag[8] == 2)
s.add(flag[10] == 3)
s.add(flag[11] == 4)
s.add(flag[13] == 4)
s.add(flag[14] == 2)
 
s.add(flag[3] + flag[2] + flag[1] + flag[0] == 10)
s.add(flag[7] + flag[6] + flag[5] + flag[4] == 10)
s.add(flag[11] + flag[10] + flag[9] + flag[8] == 10)
s.add(flag[15] + flag[14] + flag[13] + flag[12] == 10)
s.add(flag[12] + flag[8] + flag[4] + flag[0] == 10)
s.add(flag[13] + flag[9] + flag[5] + flag[1] == 10)
s.add(flag[14] + flag[10] + flag[6] + flag[2] == 10)
s.add(flag[15] + flag[11] + flag[7] + flag[3] == 10)
s.add(flag[5] + flag[1] + flag[0] + flag[4] == 10)
s.add(flag[7] + flag[6] + flag[2] + flag[3] == 10)
s.add(flag[13] + flag[12] + flag[9] + flag[8] == 10)
s.add(flag[15] + flag[14] + flag[11] + flag[10] == 10)
 
 
assert s.check() == sat
print("OK")
m = s.model()
c = [m[flag[i]].as_long() for i in range(16)]
for i in [0, 3, 5, 6, 9, 12, 15]:
    print(c[i], end="")

[培训]科锐软件逆向50期预科班报名即将截止,速来!!! 50期正式班报名火爆招生中!!!

收藏
免费 1
打赏
分享
最新回复 (0)
游客
登录 | 注册 方可回帖
返回