Z3三值逻辑支持实现方法详解

Z3 本身不直接支持“未知”语义，但可通过双重可满足性检查（验证命题及其否定是否均可满足）来模拟三值逻辑判断，从而准确区分“必然为真”、“必然为假”和“无法判定”。

在形式化推理任务中，用户常需判断某命题在给定前提下是 必然为真（True）、必然为假（False），还是 无法确定（Unknown） ——这本质上是逻辑蕴涵（entailment）与反蕴涵（anti-entailment）的联合判定问题。而 Z3 作为 SMT 求解器，其核心返回值仅有 sat（存在模型满足断言）、unsat（无模型满足，即矛盾）和 unknown（求解器未完成判定，如超时或逻辑超出可判定片段）。注意：Z3 的 unknown 是求解器能力限制信号，而非用户语义中的“知识不充分”。

要正确实现 True/False/Unknown 三值判定，关键在于：

✅ True：前提 ∧ ¬P 不可满足 → 即 ¬P 与前提矛盾 ⇒ P 必然成立
✅ False：前提 ∧ P 不可满足 → 即 P 与前提矛盾 ⇒ P 必然不成立
✅ Unknown：前提 ∧ P 可满足 且 前提 ∧ ¬P 也可满足 → P 既非必然真，也非必然假

因此，必须对同一前提集分别尝试添加 P 和 ¬P，并独立检查可满足性。为避免相互干扰，需使用 Z3 的增量求解接口（push() / pop()） 管理断言栈。

以下为完整、健壮的三值判定实现：

from z3 import *

# 定义枚举类型与谓词
ThingsSort, (charlie, erin, fiona, harry) = EnumSort('ThingsSort', ['charlie', 'erin', 'fiona', 'harry'])
green = Function('green', ThingsSort, BoolSort())
kind  = Function('kind',  ThingsSort, BoolSort())
blue  = Function('blue',  ThingsSort, BoolSort())
smart = Function('smart', ThingsSort, BoolSort())
rough = Function('rough', ThingsSort, BoolSort())
quiet = Function('quiet', ThingsSort, BoolSort())
nice  = Function('nice',  ThingsSort, BoolSort())
x = Const('x', ThingsSort)

# 构建前提知识库
s = Solver()
s.add(green(charlie))
s.add(kind(charlie))
s.add(nice(charlie))
s.add(rough(charlie))
s.add(kind(erin))
s.add(nice(erin))
s.add(quiet(erin))
s.add(quiet(fiona))
s.add(rough(fiona))
s.add(smart(harry))
s.add(ForAll([x], Implies(And(rough(x), green(x)), quiet(x))))
s.add(ForAll([x], Implies(And(green(x), rough(x)), nice(x))))
s.add(ForAll([x], Implies(And(kind(x), smart(x)), green(x))))
s.add(ForAll([x], Implies(And(green(erin), blue(erin)), quiet(erin))))
s.add(ForAll([x], Implies(quiet(x), smart(x))))
s.add(ForAll([x], Implies(kind(x), green(x))))
s.add(ForAll([x], Implies(smart(x), kind(x))))
s.add(ForAll([x], Implies(And(rough(x), nice(x)), blue(x))))

# 辅助函数：安全检查某命题是否与当前前提一致
def is_consistent(solver, formula):
    solver.push()           # 保存当前状态
    solver.add(formula)
    result = solver.check()
    solver.pop()            # 恢复原始状态，避免污染
    if result == sat:
        return True
    elif result == unsat:
        return False
    else:
        raise RuntimeError(f"Z3 returned 'unknown'; check logic fragment or set timeout. Got: {result}")

# 执行三值判定：Erin is rough?
p = rough(erin)
is_p_possible   = is_consistent(s, p)
is_not_p_possible = is_consistent(s, Not(p))

if is_p_possible and is_not_p_possible:
    print("Unknown")  # 前提既不推出 p，也不推出 ¬p
elif is_p_possible:
    print("True")     # 前提 ⊨ p
elif is_not_p_possible:
    print("False")    # 前提 ⊨ ¬p
else:
    print("Inconsistent")  # 前提自身已矛盾（应提前检测）

关键注意事项：

• ✅ 必须使用 push()/pop()：否则连续 add() 会累积断言，导致第二次检查受第一次影响；
• ⚠️ 避免重复调用 check() 而不重置：原问题中两次 s.check() 未清理，第二次实际检查的是 precond ∧ ¬rough(erin)，而非独立验证；
• ? 警惕 unknown 返回值：若 Z3 返回 unknown（如因量化公式复杂），应显式报错或降级处理，不可默认为 Unknown 语义；
• ? 量化逻辑需谨慎：Z3 对含 ForAll 的一阶逻辑支持有限，建议启用 s.set('mbqi', True) 启用模型构建实例化（Model-Based Quantifier Instantiation），提升量化推理能力；
• ? 扩展性提示：该模式可封装为通用函数 evaluate_truth(solver, formula) → Literal['True','False','Unknown']，便于批量处理多命题。

综上，Z3 完全胜任三值逻辑推理任务，但需正确建模——它不是“内置 Unknown 类型”，而是通过双侧可满足性分析还原人类推理中的不确定性。这一方法兼具理论严谨性与工程实用性，是将 SMT 求解器用于知识推理的典型范式。