形式化⽅法SATProblemsSolving——使⽤Z3来验证问题的可
满⾜性
⼀、SAT
1、SAT 问题
宝马迷你酷派2、SAT Solver
解决 SAT 问题的程序或⼯具就叫做 SAT Solver。
此处使⽤到的 Z3 Theorem Solver/Prover 就是⼀款 SAT Solver。
⼆、Z3的安装与使⽤
1、Z3在Windows平台上的安装
推荐使⽤Z3的Python绑定，因此在安装Z3之前需要保证⾃⼰电脑上已经安装了Python 3及以上的标准。
此处也提供⼀个Z3的安装包：
下载之后，解压到⾃⼰合适的⽬录下，进⾏环境变量的配置。
右击“我的电脑”-⾼级系统设置-环境变量-系统变量栏
在Path变量后添加：z3的安装⽬录\bin，我的是 D:\Program Files\z3-4.8.7-x64-win\bin
新增变量PYTHONPATH，并将其值设置为：z3的安装⽬录\bin\python，我的是 D:\Program Files\z3-4.8.7-x64-
win\bin\python
2、Warm-up Test
打开python的编辑框，输⼊如下的代码，看结果是否与预期相符。
（1）测试代码1
获取简单逻辑命题：P /\ Q 的可满⾜性的解决⽅案。
测试代码如下：z3_test.py
#!/usr/bin/python3
# -*- coding: utf-8 -*-
# @Author : exiahan@exiahan
# @Time : 2020/03/26
# @File : z3_test.py
import z3
# Find Solution Set That Can Make Logical Expression P/\Q be True P, Q = z3.Bools('P Q')
F = z3.And(P, Q)
宝马培训solver = z3.Solver()
solver.add(F)
print(solver.check())
del())
执⾏结果如下：
此时，表明z3安装成功。
（2）测试代码2
测试代码如下：
from z3 import *
x = Real('x')
y = Real('y')
一汽丰田普拉多报价s = Solver()
s.add(x + y > 5, x > 1, y > 1)
print(s.check())
del())
测试结果如下：
3、语法规范
1、调⽤z3：import z3
2、声明命题：P, Q = z3.Bools('P Q')
3、使⽤连接词建⽴命题：F = z3.And(P, Q)
4、创建solver()：solver = z3.Solver()
5、将所要验证的命题添加到solver()中：solver.add(F)
6、输出命题的验证结果（是否为SAT）：print(solver.check())
7、输出命题为TRUE时的model：del())
三、基础命题逻辑（Basic Propositional Logic）
1、声明命题
在Z3中，我们可以将命题声明为布尔量。
举个栗⼦：声明两个命题 P 和 Q
//⽅法1
P = Bool('P')
Q = Bool('Q')
//⽅法2
P, Q = Bool('P Q')
2、⽤连接词建⽴命题
Z3⽀持的连接词有：/\（And） \/（Or） ~（Not） ->（Implies）等
可以通过直接编写Lisp风格的抽象语法树来构建命题。
举个栗⼦：析取符 P \/ Q
F = Or(P, Q)
3、Solve的⽤法
Solve() 函数的作⽤
solve() 函数创建⼀个solver实例，检查命题的可满⾜性，并且在该命题可满⾜的情况下输出model（即变量的取值情况，使得命题在该model下为TRUE）
举个栗⼦1：
from z3 import *
P, Q = Bools('P Q')
F = Or(P,Q)
solve(F)
结果为：
日产特黄极日产输出为：
[P=True, Q=False]
表明这是⼀个分配给P和Q的模型，使得命题F可以满⾜；这只是可能的⼏种模型之⼀。
举个栗⼦2：
from z3 import *
P = Bool('P')
F = And(P,Not(P))
solve(F)
结果为：
输出为：
no solution
表明该命题是不可满⾜的，即对于任何可能的P值，命题F都不可能为TRUE。
4、获取更多的解决⽅案
对于前⾯的栗⼦：证明 P \/ Q 的可满⾜性，z3 只会输出真值表的⼀⾏。
P \/ Q 真值表如下所⽰：
P Q P \/Q
T T T
T F T
F T T
F F F
如果我们需要输出所有使得该命题可满⾜的model类型（在本例中，需要输出的是真值表的前三⾏），则我们在获取到答案时，将答案取反，与原始命题交，然后再次检查可满⾜性。
操作如下：
from z3 import *
P, Q = Bools('P Q')
F = Or(P, Q)
东风日产天籁公爵solve(F)
结果为：
[P = True, Q = False]
因为 P 是True，Q 为False，所以在构造下⼀个 F 时：
（1）P保持原型，Q取反：P Not(Q)
（2）将⼆者相交之后，再进⾏取反：Not(And(P, Not(Q)))
（3）将上述式⼦与原始命题 F 做交运算：And(F, Not(And(P, Not(Q))))（4）再次检查可满⾜性
代码如下：
F = And(F, Not(And(P, Not(Q))))
solve(F)
结果为：
[P = False, Q = True]
因为 P 是False，Q 为True，所以在构造下⼀个 F 时：
（1）P取反，Q保持原型：Not(P) Q
（2）将⼆者相交之后，再进⾏取反：Not(And(Not(P), Q))
（3）将上述式⼦与原始命题 F 做交运算：And(F, Not(And(Not(P), Q)))（4）再次检查可满⾜性350
代码如下：
F = And(F, Not(And(Not(P), Q)))
solve(F)
结果为：
[P = True, Q = True]
因为 P 是True，Q 为True，所以在构造下⼀个 F 时：
（1）P，Q均保持原型：P Q
（2）将⼆者相交之后，再进⾏取反：Not(And(P, Q))
（3）将上述式⼦与原始命题 F 做交运算：And(F, Not(And(P, Q)))（4）再次检查可满⾜性
代码如下：
F = And(F, Not(And(P, Q)))
solve(F)
发布评论