z3 模块

创建未知变量

  • 声明整型 Int

    1
    2
    3
    x = Int('x')
    a, s, d = Ints('a s d')     # 一次全部列出
    v = [Int(f'v{i}') for i in range(len(s))]   # 参数较多，则建议使用循环，批量声明

  • 声明布尔型 Bool

    1
    x = Bool('x')

  • 声明实数型 Real

    1
    x = Real('x')

创建约束器

1
solver = Solver()

添加约束

1
2
3
4
5
6
7
8
solver.add(v[0] * 7 == 546)
solver.add(v[1] * 2 == 166)
solver.add(v[2] * 6 + v[3] * 1 + v[5] * 7 == 1055)
solver.add(v[4] * 4 == 336)
solver.add(v[1] * 2 + v[5] * 7 == 656)
solver.add(v[7] * 6 == 606)
solver.add(v[8] + v[14] * 5 == 652)
solver.add(v[9] * 5 + v[10] * 16 + v[12] * 6 == 3213)

注意：z3 中的整数除法为 / ，使用 // 会报错

判断是否有解

1
if solver.check() == sat:

求解

1
2
f = solver.model()
print(f)

当问题有多个解时，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
from z3 import *
result = 'v0b9n1nkajz@j0c4jjo3oi1h1i937b395i5y5e0e$i'
s = 'wesyvbniazxchjko1973652048@$+-&*<>'

v = [Int(f'v{i}') for i in range(len(result)//2)]
vv =v
solver = Solver()

for i in range(0,len(result)//2):
    str=result[i*2:(i+1)*2]
    s1 = str[0]
    s2 = str[1]
    ind1 = s.index(s1)
    ind2 = s.index(s2)
    solver.add(v[i]>0,v[i]<130,(v[i]/17+i)%34 == ind1)
    solver.add(v[i]>0,v[i]<130,-(v[i]%17+i+1)%34 == ind2)

print(solver.check())
f = solver.model()
flag  = ""
for i in vv:
    print(f[i])
    flag += chr(f[i].as_long())
print(flag)