使用 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.甲是窃贼

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

#!/usr/bin/python3
# -*- encoding:utf-8 -*-

from z3 import Solver, Bool, If, Not, Or, And, Implies

a = Bool('a')  # 若甲是窃贼 则a为真
b = Bool('b')
c = Bool('c')

def build_solver():
    solver = Solver()

    # 给solver添加约束条件
    solver.add(If(a, 1, 0) + If(b, 1, 0) + If(c, 1, 0) >= 1)  # 三人至少有一个是窃贼
    solver.add(Implies(a, b))  # 如甲是窃贼 则乙一定是同案犯
    solver.add(Not(b))  # 乙一定不是

    return solver


if __name__ == '__main__':
    solver = build_solver()
    # 采用反证法 把各选项的 *否定* 添加进solver中 若冲突将返回unsat 原选项正确
    solver.add(Not(And(a, b, c)))  # 甲、乙、丙都是窃贼
    print(solver.check())  # will output "sat"

    solver = build_solver()
    solver.add(Not(And(a, b)))  # 甲和乙都是窃贼
    print(solver.check())  # will output "sat"

    solver = build_solver()
    solver.add(Not(c))  # 丙是窃贼
    print(solver.check())  # will output "unsat"

    solver = build_solver()
    solver.add(Not(a))  # 甲是窃贼
    print(solver.check())  # will output "sat"

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

例题 2

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

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

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

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

对应的代码为:

#!/usr/bin/python3
# -*- encoding:utf-8 -*-

from z3 import Solver, Bool, If, Not, Or, And, Implies

equipment = Bool('shebei')  # 设备是否有问题
violation = Bool('weifan')  # 是否违反操作规程

s1 = equipment  # 甲:发生事故的原因是设备问题
s2 = And(violation, Not(equipment))  # 乙:违反了操作规程,但不是设备问题
s3 = Implies(equipment, violation)  # 丙:如果事故的原因是设备问题,那么违反操作规程
s4 = And(equipment, Not(violation))  # 丁:发生事故的原因是设备问题,但没有人违反操作规程

def build_solver():
    solver = Solver()
    solver.add(If(s1, 1, 0) + If(s2, 1, 0) + If(s3, 1, 0) + If(s4, 1, 0) == 1)  # 四人的断定中只有一个人为真
    return solver


if __name__ == '__main__':
    solver = build_solver()
    # 采用反证法 把各选项的 *否定* 添加进solver中 若冲突将返回unsat 原选项正确
    solver.add(Not(s1))  # 甲的断定为真
    print(solver.check())

    solver = build_solver()
    solver.add(Not(s2))  # 乙的断定为真
    print(solver.check())

    solver = build_solver()
    solver.add(Not(s4))  # 丁的断定为真
    print(solver.check())

    solver = build_solver()
    solver.add(Not(And(s3, violation)))  # 丙的断定为真 并且有人违反了操作规程
    print(solver.check())

    solver = build_solver()
    solver.add(Not(And(s3, Not(violation))))  # 丙的断定为真 并且没有人违反操作规程
    print(solver.check())

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

相关参考

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


仅有1条评论 发表评论

  1. 伪善 /

    谢谢博主,一下子明白了好多

发表评论