使用 Z3 Solver 求解逻辑题

Z3 是一个由 Microsoft Research 开发的定理求解器。它可以用在很多方面,如软/硬件的验证与测试、约束求解、混合系统的分析、安全、生物,以及求解几何等问题[1]。Z3 主要由 C++ 开发,但它支持被 .NET、C、C++、Java、Python 等语言调用。本文使用其 Python binding。

在网上看到有不少解方程和约束条件的使用,我在此补充它在命题逻辑方面的例子。

安装

非Windows平台可尝试直接安装:

pip install z3-solver

Windows平台由于编译环境比较复杂,Pypi 中只有没这么新的版本,指定旧版本安装:

pip install z3-solver==4.5.1.0.post2

例题 1

一军用仓库被窃,公安部门已掌握如下线索:①甲、乙、丙三人至少有一个是窃贼;②如甲是窃贼,则乙一定是同案犯;③盗窃发生时,乙正在影剧院看电影。由此可以推出( )。

A.甲、乙、丙都是窃贼
B.甲和乙都是窃贼
C.丙是窃贼
D.甲是窃贼

注意在下面的代码中,使用了反证法。

运行代码后,第3条的结果为 unsat,即对应原选项 C 是正确的。

例题 2

某大型煤矿发生了一起重大事故,事发现场的人有以下的断定:

矿工甲:发生事故的原因是设备问题;
矿工乙:有人违反了操作规程,但发生事故的原因不是设备问题;
矿工丙:如果发生事故的原因是设备问题,那么有人违反操作规程;
矿工丁:发生事故的原因是设备问题,但没有人违反操作规程。

如果上述四人的断定中只有一个人为真,则以下可能为真的一项是( )。

A.矿工甲的断定为真
B.矿工乙的断定为真
C.矿工丁的断定为真
D.矿工丙的断定为真,有人违反了操作规程
E.矿工丙的断定为真,没有人违反操作规程

对应的代码为:

由运行结果可见选项 E 是正确的。

相关参考

1. https://ericpony.github.io/z3py-tutorial/guide-examples.htm
2. https://blog.csdn.net/qq_33438733/article/details/82011892

发表评论

验证码 *