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