编程语言
首页 > 编程语言> > 【python环境下Z3约束求解器学习笔记】基础语法

【python环境下Z3约束求解器学习笔记】基础语法

作者:互联网

一个简单的实例

问题描述:解不等式a+b<2,a>=0,b>=0的整数a和b

from z3 import *

a = Int('a')#定义一个整形 a
b = Int('b')#定义一个整形 b
s = Solver()#生成一个约束求解器
s.add(a+b<2)#添加约束条件 a+b<2
s.add(a>=0)#添加约束条件 a>=0
s.add(b>=0)#添加约束条件 b>=0

print(s.check())#检查约束求解器是否有解,如果有,返回sat; 如果不满足,返回unsat
print(s.model())#输出结果

执行结果:
在这里插入图片描述

  • 在Z3中,除了整形(Int),还可求取实数型(Real),浮点型(Float16、Float32、Float64、Float128),布尔型(Bool)等
  • 运算符有<,<=,>,> =,==和!=
  • 虽然这个不等式的结果有很多,但约束求解器只能求出一个结果,后续会讲到求解多种结果的方法

另一种求解方法:solver

问题描述:求解满足下列条件:a+b<2,a>=0,b>=0的整数a和b

from z3 import *

a = Int('a')#定义一个整形 a
b = Int('b')#定义一个整形 b

solve(a+b<2,a>=0,b>=0)#将a和b的约束条件写在括号里用逗号分割

执行结果:
在这里插入图片描述

这种方法虽然书写简单,但在约束条件太多的情况,不容易理解

Real类型的简单使用

问题描述:求解3x=1时,x的值

from z3 import *

x = Real('x')
solve(3*x == 1)

set_option(rational_to_decimal=True)
solve(3*x == 1)

执行结果:
在这里插入图片描述

Real类型的数据求解默认为分数形式,如果设置rational_to_decimal=True则结果位小数形式,默认显示小数点后10位,10位后用?表示后面还有

实数型小数保留问题:precision

问题描述:求解满足下列条件:a+b<2,a>=0,b>=0的整数a和b

from z3 import *

x = Real('x')
y = Real('y')
s = Solver( ) #生成一个约束求解器
s.add(x**2 + y**2 == 3) #添加约束条件:x的平方加y的平方等于3
s.add(x**3 == 2) #添加约束条件:x的三次方等于2

set_option(precision=30)#输出结果保留小数点后30位

print(s.check())#检查约束求解器是否有解,如果有,返回sat; 如果不满足,返回unsat
print(s.model())#输出结果

执行结果:
在这里插入图片描述

Not和Or的简单使用

公式简化:Simplify

问题描述:简化公式x + y + 2*x + 3

from z3 import *

x = Int('x')
y = Int('y')
print (simplify(x + y + 2*x + 3))
print (simplify(x < y + x + 2))
print (simplify(And(x + 1 >= 3, x**2 + x**2 + y**2 + 2 >= 5)))

执行结果:
在这里插入图片描述

主要用于对复杂公式的自动化简化

标签:Real,约束条件,求解,python,语法,Int,print,import,Z3
来源: https://blog.csdn.net/qq_37400312/article/details/112268489