Z3 是一个微软出品的开源约束求解器，能够解决很多种情况下的给定部分约束条件寻求一组满足条件的解的问题（可以简单理解为解方程的感觉，虽然这么比喻其实还差距甚远，请勿吐槽），功能强大且易于使用。

Z3 内置了多种变量类型，基本能覆盖常见计算机数据结构。包括整数、浮点数、BitVector、数组等。

from z3 import *
 x = Int('x')
 y = Int('y')
 solve(x > 2, y < 10, x + 2*y == 7) 

运行一下结果：

(z3env) $ python example.py 
[y = 0, x = 7] 

调用了 solve 函数求解三个条件下的满足模型，这三个条件分别是 x 大于 2，y 小于 10，并且 x 加 2 个 y 等于 7

Z3 在默认情况下，只寻找满足所有条件的一组解，而不是找出所有解

 from  z3 import *
a=[Int('a[%d]'%i) for i in range(26)]  #添加变量：使用Z3 Solver创建了一个包含26个整数变量的列表。每个变量的名称都是'a[i]'，其中'i'是从0到25的整数
solver = Solver()                    #Solver对象是Z3的一个核心组件，它允许你描述和解决逻辑和算术约束
solver.add(len(a[])==26)    
solver.add(a[0] - a[20] == -10)
solver.add(a[6] + a[1] == 208)
solver.add(a[2] - a[4] == 10)
solver.add(a[3] - a[14] == -2)
solver.add(a[25] * a[4] == 10100)
solver.add(a[17] + a[5] == 219)
solver.add(a[6] - a[10] == -11)
solver.add(a[7] - a[20] == -10)
solver.add(a[17] * a[8] == 11845)
solver.add(a[9] - a[18] == -7)
solver.add(a[10] - a[24] == 1)
solver.add(a[4] * a[11] == 9797)
solver.add(a[12] - a[3] == 3)
solver.add(a[11] * a[13] == 11252)
solver.add(a[14] - a[13] == -2)
solver.add(a[15] == a[23])
solver.add(a[16] - a[8] == -5)
solver.add(a[7] * a[17] == 10815)
solver.add(a[18] - a[14] == -2)
solver.add(a[19] - a[0] == -8)
solver.add(a[20] - a[23] == 4)
solver.add(a[7] + a[21] == 220)
solver.add(a[22] - a[1] == 15)
solver.add(a[23] == a[15])
solver.add(a[2] * a[24] == 12654)
solver.add(a[25] - a[12] == -15)
solver.add(a[0] - a[20] == -10)
solver.add(a[6] + a[1] == 208)
solver.add(a[2] - a[4] == 10)
solver.add(a[3] - a[14] == -2)
solver.add(a[25] * a[4] == 10100)
solver.add(a[17] + a[5] == 219)
solver.add(a[6] - a[10] == -11)
solver.add(a[7] - a[20] == -10)
solver.add(a[17] * a[8] == 11845)
solver.add(a[9] - a[18] == -7)
solver.add(a[10] - a[24] == 1)
solver.add(a[4] * a[11] == 9797)
solver.add(a[12] - a[3] == 3)
solver.add(a[11] * a[13] == 11252)
solver.add(a[14] - a[13] == -2)
solver.add(a[15] == a[23])
solver.add(a[16] - a[8] == -5)
solver.add(a[7] * a[17] == 10815)
solver.add(a[18] - a[14] == -2)
solver.add(a[19] - a[0] == -8)
solver.add(a[20] - a[23] == 4)
solver.add(a[7] + a[21] == 220)
solver.add(a[22] - a[1] == 15)
solver.add(a[23] == a[15])
solver.add(a[2] * a[24] == 12654)
solver.add(a[25] - a[12] == -15)
if solver.check() == sat:
    model = solver.model()
    result = ''
    for i in range(26):
        result += chr(model[a[i]].as_long())
    print('[+] found:{}'.format(result))
else:
    print('[-]not fount')

2543 sudo apt install build-essential python3-dev 
2544 git clone https://github.com/Z3Prover/z3.git 
2545 cd z3 2546 python3 scripts/mk_make.py --python 
2547 cd build 2548 make 
2549 sudo make install 
2550 ipython3