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

Alpha-Beta剪枝用于裁剪搜索树中不需要搜索的树枝，以提高运算速度。它基本的原理是：

• 当一个 Min 节点的 β值≤任何一个父节点的α值时 ，剪掉该节点的所有子节点
• 当一个 Max 节点的 α值≥任何一个父节点的β值时 ，剪掉该节点的所有子节点

下面为只使用 MiniMax 和使用 Alpha-Beta 剪枝的简单对比。

需要注意的是，剪枝的效果与树节点的访问顺序有关。

Alpha-Beta剪枝的伪代码如下：

Initialize MAX_VALUE(node,game,-∞,∞)

function MAX_VALUE(state,game,α,β) returns the minimax value of state
    inputs: state, current state in game
            game, game description
            α, the best score for MAX along the path to state
            β, the best score for MIN along the path to state

    if CUTOFF_TEST(state) then return EVAL(state)
    for each s in SUCCESSORS(state) do
        α = MAX(α, MIN_VALUE(s,game,α,β))
        if α ≥ β then return β
    end
    return α

function MIN_VALUE(state,game,α,β) returns the minimax value of state
    if CUTOFF-TEST(state) then return EVAL(state)
    for each s in SUCCESSORS(state) do
        β = MIN(β, MAX_VALUE(s,game,α,β))
        if α ≥ β then return α
    end
    return β

下面用一个例子说明。规定从左节点开始展开。原搜索树为：