使用 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