Z3 solver是由微软开发的可满足性模理论求解器（Satisfiability Modulo Theory solver， 即 SMT solver），用于检查逻辑表达式的可满足性，并可以找到一组约束中的其中一个可行解（无法找出所有的可行解）

注意这一关键点，只能给出一个可行解，无法列出所有的可行解。

在 CTF 逆向题中，我们有的时候会遇到一些较为复杂的约束条件，此时可以使用 z3 来辅助求解。之前在广州大学的2023年网安学会第一次内部赛当中，我就遇到了一道解方程组的Crypto方向的题目，我使用了Python的其他库来解决问题，过程十分复杂，我想那道题目的正常做法应该是用到z3约束求解器。

安装没啥好说的，python的库安装不要太简单，网上一搜索一大把。

我在学习了一下之后对z3约束求解器的理解就是可以用来求解方程，至于其他的用途，以后遇到再说吧。

在Python中使用z3模块，有以下几种类型的变量：

Int #整型
Real #实数类型
BitVec #位向量
Bool #布尔类型
Array #数组类型

这里的Int可不是 C/C++ 里面包含上下界的 Int，Z3 中的 Int 对应的就是数学中的整数，而Real声明的变量则可能是包含小数点的实数，Bool则声明的自变量只能是0或者1。我不完全了解BitVec，我的理解就是可以创建一个二进制数，因为看的文章里面说Z3 中的 BitVector 才对应到 C/C++ 中的 Int，并且C语言中的int型可以用BitVec(‘a’,32)表示，又有其中BitVec可以是特定大小的数据类型，BitVec可以(‘a’,8)可以代表char型，有一些疑问我们在后面的代码调试里面再看看。

先看看如何使用z3来解决问题，抛出一个方程组

30x+15y=675
12x+5y=265

很明显这个方程组只有一个解,且解是整型，解题代码如下

from z3 import *   #导入z3模块
x=Int('x')
y=Int('y')    #设未知量
s=Solver()    #创建约束求解器
s.add(30*x+15*y==675)
s.add(12*x+5*y==265)   #添加约束条件
if s.check()==sat:     #判断是否有解
    print(s.model())    #若有解则得出解，得出的解是等式
else:
    print('error')      #若无解则打印error

第一步导入z3模块，我一开始还用import z3导入，但是在后面写代码的时候就要多次申明z3模块，太麻烦了。

第二步就是设未知量，解很明显是整数，当然用Real或者BitVec来都是可以运行的，BitVec必须要给多一个bv参数，即位向量的大小。

第三步即创建一个约束求解器，Solver()命令会创建一个通用求解器

第四步就是添加约束条件，add()命令用来添加约束条件，通常在solver()命令之后，添加的约束条件通常是一个逻辑等式，当然不等式也是可以的。

这里的check()命令通常用来判断在添加完约束条件后，来检测解的情况，有解的时候会回显sat，无解的时候会回显unsat

所有利用check()函数进行判断，若有解model()命令会给出方程组的解，是多个等式组成的列表，如图

我们再来看看解多解方程式的情况，如下图

解x**2+y**2=2的方程组，重复运行代码，输出的结果依旧不变，所以多解的情况下，z3约束求解器输出的只是其中一解，并且重复运行，输出的解不变。

这里的文章只是讲讲z3的使用，具体原理肯定复杂，我就不深究了。

下面是一道例题

[MoeCTF 2023]EQUATION – Arnold’s Blog (arnold66.top)