Z3求解器

Ra1N 发布于 2024-10-19 58 次阅读

参考文献：z3求解器(SMT)

🔦简介🔫

z3-solver是由Microsoft Research(微软)开发的SMT求解器，它用于检查逻辑表达式的可满足性，可以找到一组约束中的其中一个可行解，缺点是无法找出所有的可行解（

以下是对Python接口的详解

z3可直接通过pip安装：

pip install z3-solver

Z3API文件

变量类型

整型(Int)，实型(Real)和向量(BitVec)。

整型

  1. Int(name, ctx=None)，创建一个整数变量，name是名字
  2. Ints (names, ctx=None)，创建多个整数变量，names是名字，以空格分隔
  3. IntVal (val, ctx=None)，创建一个整数常量，有初始值，没有名字。

Real型的API与Int一致，向量稍有区别

  1. Bitvec(name,bv,ctx=None)，创建一个位向量，name是他的名字，bv表示大小
  2. BitVecs(name,bv,ctx=None)，创建一个有多变量的位向量，name是名字，bv表示大小
  3. BitVecVal(val,bv,ctx=None)，创建一个位向量，有初始值，没名字。

Solver求解器

用于取出指定变量的结果

直接solver终端会直接以序列打印出解

  1. s=solver()，创建一个解的对象。
  2. s.add(条件)，为解增加一个限制条件
  3. s.check()，检查解是否存在，如果存在，会返回"sat"
  4. modul()，输出解得结果

可以通过solver.assertions()查看求解器已经添加的约束和约束的个数：

assertions = solver.assertions()
print(assertions) # 已添加的约束条件
print(len(assertions)) # 已添加的约束条件的个数

⚠️注意：没有push过的约束条件时直接pop会导致报出Z3Exception: b'index out of bounds'错误。

🚦线性多项式约束🚧

x, y = Reals('x y')
solver = Solver()
solve([x > 2, y < 10, x + 2*y == 7])

xy都约束为整数，我们需要找到一个可行解

结果:

Python
x, y = Reals('x y')
solve([x > 2, y < 10, x + 2*y == 7])
​
x, y = Ints('x y')
solve([x > 2, y < 10, x + 2*y == 7])
# [y = 2, x = 3]
# [y = 0, x = 7]

💧非线性多项式约束🌌

约束条件为：

[math]x^2 + y^2 >3 \\x^3 +y <5[/math]

一样的直接写进去就行，

高中物理匀变速直线运动相关问题📰

使用高中物理的匀变速公式

举个例子，以30m/s的速度前进时踩下刹车，如果减速的加速度为− 8 m / s 2 -8m/s^2−8m/s2，求刹车完毕时，汽车的刹车距离是多少？

直接解

Python
from z3 import *
solver = Solver()
s, v_i, a, t, v_f = Reals('s v__i a t v__f')

equations = [
    s == v_i * t + (a * t ** 2) / 2,
    v_f == v_i + a * t,
]

variables = [
    v_i ==30,
    v_f == 0,
    a == -8
]
print("参数变量：",variables)
print("结果:",)
solve(equations + variables)
# 获取指定变量的结果
solver.add(equations + variables)
if solver.check() == sat:
    result = solver.model()
print(f"刹车距离：{result[s].as_decimal(2)}m，刹车时间：{result[t].as_decimal(4)}s")

参数变量： [vi == 30, vf == 0, a == -8]

结果: [s = 225/4, vf = 0, vi = 30, a = -8, t = 15/4]

刹车距离：56.25m，刹车时间：3.75s