如何在Z3 Solver中结合封闭世界假设求解约束问题？

Z3默认采用开放世界假设（未知命题既不视为真也不视为假），没有内置开关直接切换到封闭世界假设（CWA），必须通过显式编码约束来实现。以下结合你的需求给出具体实现方案和示例：

核心思路 #

CWA的核心是：未被证明为真的命题均视为假。要高效实现，需先将问题限定在有限论域（无限论域无法枚举所有实例，CWA无实际意义），再通过两种方式编码CWA：

1. 对已知部分为真的谓词，直接将其余实例设为假；
2. 对依赖其他谓词的谓词，用逻辑等价式定义其为真的充要条件，自动覆盖所有实例。

代码实现示例 #

假设你的论域包含有限个对象（示例中定义为a、b、c），结合你的约束和事实，代码如下：

from z3 import *

# 1. 定义有限论域（用Z3的Datatype枚举所有可能的对象）
Obj = Datatype('Obj')
Obj.declare('a')
Obj.declare('b')
Obj.declare('c')
Obj = Obj.create()

# 2. 定义谓词：situation和actions（从论域对象映射到布尔值）
situation = Function('situation', Obj, BoolSort())
actions = Function('actions', Obj, BoolSort())

# 3. 初始化求解器
s = Solver()

# 4. 添加给定事实：situation(a) 为真
s.add(situation(Obj.a) == True)

# 5. 添加全称约束：∀x,y (situation(x) ∧ situation(y) → actions(x) ∧ actions(y))
x = Const('x', Obj)
y = Const('y', Obj)
s.add(ForAll([x, y], Implies(And(situation(x), situation(y)), And(actions(x), actions(y)))))

# 6. 编码封闭世界假设（CWA）
all_objs = [Obj.a, Obj.b, Obj.c]

# 6.1 处理situation谓词：未被声明为真的实例均为假
for obj in all_objs:
    if obj != Obj.a:
        s.add(situation(obj) == False)

# 6.2 处理actions谓词：仅当约束要求为真时才为真（用等价式自动覆盖所有实例）
# 逻辑：actions(x)为真 ⇨ 存在y使得situation(x)和situation(y)同时为真（这是约束中能推导actions(x)为真的唯一条件）
s.add(ForAll([x], actions(x) == Exists([y], And(situation(x), situation(y)))))

# 7. 求解并输出结果
if s.check() == sat:
    m = s.model()
    print("满足条件的唯一解：")
    for obj in all_objs:
        print(f"situation({obj}) = {m.eval(situation(obj))}")
        print(f"actions({obj}) = {m.eval(actions(obj))}\n")
else:
    print("无解")

输出结果 #

运行代码后会得到唯一符合CWA的解：

满足条件的唯一解：
situation(a) = True
actions(a) = True

situation(b) = False
actions(b) = False

situation(c) = False
actions(c) = False

关键优化点 #

• 避免手动逐个添加否定约束：通过枚举论域+量化等价式，自动处理所有实例，大幅减少代码冗余；
• 严格遵循CWA原则：仅基于给定事实和约束推导，不引入额外假设，确保解的唯一性。

内容的提问来源于stack exchange，提问作者inferis