Day16:Z3求解器

z3求解器

基本数据类型

• Int：整数
• BitVec：二进制数据（如BitVec(‘a’,8)：8个比特位的一个变量a）
• Real：有理数
• Bool：布尔值
• Array：数组

基本流程

设变量

• 使用基本数据类型来声明变量，如：x=Int(‘x’)

创建求解器

• 使用函数Solve()创建一个求解器：s=Solver()

添加约束条件

• 使用函数add()添加约束条件：s.add(一个方程/不等式)

判断是否有解

• 使用函数check()检查是否有解，有解返回’sat’，无解返回’unsat’

取解的交集

• 使用函数model()取满足每个条件的解的交集，返回的是字典，用model[变量名]可以得到变量的解

示例

解方程{x,y|30x+15y=675,12x+5y=265}

from z3 import *

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())
#得到解[x = 20, y = 5]