z3 使用笔记

发表于 更新于 本文字数： 1.3k 阅读时长 ≈ 1 分钟
z3&python 的用法简要笔记

z3 简介

z3 是 Microsoft Research 开发的一个定理证明器，支持位向量、布尔值、数组、浮点数、字符串和其他数据类型，可以用来自动化证明定理、线性规划求解和方程求解。

但方程求解效率过低，不建议使用 z3 求解方程 (少量未知数可以使用)。

z3 安装

可以使用 pip 进行安装

1
pip install z3-solver

若出现 pip 安装超时或安装失败的情况，请在 https://github.com/Z3Prover/z3/releases 中下载 release 版本包。

这里以 Windows 为例，下载 z3-x64-win.zip 后解压在合适的目录中。

然后将解压目录下的 ./bin 目录添加进入环境变量 Path ；解压目录下的 ./bin/python 添加进入环境变量 PYTHONPATH 即可。

z3 使用

求解过程

  1. 定义若干某种类型的未知数
  2. 创建求解器 Solver()
  3. 添加约束条件 add()
  4. 进行检查问题是否有解 check()
  5. 创建解决问题后的模型对象 model()
  6. 得到解

定义若干某种类型的未知数

1
2
3
4
5
6
7
8
9
10
from z3 import *

x = Int('x')				# 创建数据类型为整数的未知数
y = Real('y')				# 创建数据类型为实数的未知数
z = BitVec('z', 64)			# 创建数据类型为 64 位向量的未知数 (通常用于求解位运算问题)

# 创建数据类型为整数的三个未知数
# 同理存在 Reals, BitVecs 等
x, y, z = Ints('x y z')
# 以上 'x', 'y', 'z' 均为 z3 内部的未知数名，可更改，但不能重复

二元一次方程求解

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
from z3 import *

# 定义若干某种类型的未知数
x, y = Ints('x y')
# 创建求解器
s = Solver()
# 添加约束条件
s.add(x+3*y == 4)
s.add(3*x+y == 4)
# 以上两行代码可以归并成一行代码 s.add(x+3*y == 4, 3*x+y == 4)

# 判断是否问题有解，有解则返回 sat ；无解则返回 unsat
if s.check() == sat:
    # 创建解决问题后的模型对象
    m = s.model()
    # 获得 x 未知数对应的模型值
    varX = m[x]
    # 输出
    print(varX)
else:
    print("unsat!")

位运算求解

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
from z3 import *

# 定义若干某种类型的未知数
x = BitVec('x', 64)
# 创建求解器
s = Solver()
# 添加约束条件
s.add(x ^ 0xff == 0x12)
# 判断是否问题有解，有解则返回 sat ；无解则返回 unsat
if s.check() == sat:
    # 创建解决问题后的模型对象
    m = s.model()
    # 获得 x 未知数对应的模型值
    varX = m[x]
    # 输出
    print(varX)
else:
    print("unsat!")