如何在 Z3 中正确建模封闭世界假设（CWA）约束问题-Python教程-PHP中文网

如何在 Z3 中正确建模封闭世界假设（CWA）约束问题

z3 等 smt 求解器默认采用开放世界语义，不支持内置的封闭世界假设（cwa）；若需 cwa 效果，必须通过显式建模实现——例如使用有限域枚举、函数外延化或显式否定补集，而非依赖求解器自动推断“未声明即为假”。

z3 等 smt 求解器默认采用开放世界语义，不支持内置的封闭世界假设（cwa）；若需 cwa 效果，必须通过显式建模实现——例如使用有限域枚举、函数外延化或显式否定补集，而非依赖求解器自动推断“未声明即为假”。

在逻辑编程（如 Prolog）中，封闭世界假设是默认行为：所有未被断言为真的原子公式均被视为假。但 Z3 作为基于一阶逻辑的 SMT 求解器，严格遵循模型存在性语义——只要存在某个解释满足全部约束，即返回 sat；对未约束的谓词或变量，Z3 可自由赋予任意合法值（真或假），不作隐式否定。

因此，不存在启用 CWA 的开关（如 set_option(:closed_world true)），也无法通过修改求解策略间接实现。任何试图“全局启用 CWA”的尝试（如遍历所有可能项并添加 ¬P(t)）在理论上不可行、实践中低效——尤其当论域无限或规模较大时，会导致约束爆炸。

✅ 正确路径是重构建模方式，将 CWA 需求内化为显式、有限、可编码的约束。以下是三种典型可行策略：

1. 限定有限论域 + 外延化谓词

若 x, y 实际取值来自有限集合（如 ['s1', 's2', 's3']），可将其声明为枚举类型，并显式定义谓词行为：

from z3 import *

# 定义有限情境集合
Situation = EnumSort('Situation', ['s1', 's2', 's3'])
x, y = Consts('x y', Situation)

situation = Function('situation', Situation, BoolSort())
actions = Function('actions', Situation, BoolSort())

# 已知事实：situation(s1) 为真
facts = [situation('s1') == True]

# 封闭世界建模：仅 s1 是 situation；其余必为假
cwa_situation = And(
    situation('s1') == True,
    situation('s2') == False,
    situation('s3') == False
)

# 约束：∀x,y. (situation(x) ∧ situation(y)) → (actions(x) ∧ actions(y))
constraint = ForAll([x, y], 
    Implies(And(situation(x), situation(y)), 
            And(actions(x), actions(y))))

# 推出 actions 在所有 situation 实例上必须为真
# （因仅 s1 满足 situation，故只需 actions('s1') == True）
solver = Solver()
solver.add(facts + [cwa_situation] + [constraint])
print(solver.check())  # sat
print(solver.model())   # actions('s1') = True；actions('s2'), actions('s3') 自由（除非额外约束）

⚠️ 注意：此处 actions 未施加 CWA，因其语义独立；若也需 CWA，则同样需显式枚举赋值。

2. 使用代数数据类型（ADT）替代未解释谓词

当逻辑结构具有明确分类时（如“只有这几种 situation 类型”），ADT 能天然排除未定义项：

S = Datatype('Situation')
S.declare('s1')
S.declare('s2')
S.declare('s3')
Situation = S.create()

# now x can *only* be s1/s2/s3 — no "unknown" values possible
x = Const('x', Situation)
# situation(x) becomes a selector or case analysis — no open-world gap

3. 函数外延性 + 唯一模型约束（高级技巧）

对小规模问题，可强制谓词为“完全由已知事实决定”：

# 假设 situation 仅在显式列出的常量上为真，其余全假
known_sits = ['s1']
all_sits = ['s1', 's2', 's3']

cwa_full = And([
    Or([situation(s) == True for s in known_sits]),  # 至少一个为真（可选）
    And([Implies(situation(s), s in known_sits) for s in all_sits]),  # 若为真，则必在已知集
    And([Implies(Not(Or([s == k for k in known_sits])), situation(s) == False) 
         for s in all_sits])  # 若不在已知集，则必为假
])