关于Z3 solver中PartialOrder不满足自反性的技术疑问

Z3内置的PartialOrder(IntSort(), 0)生成的关系仅保证传递性和反对称性，并不强制全域自反性——这就是你的代码返回sat的原因。偏序的标准定义要求自反、传递、反对称，但Z3的这个内置函数默认不满足全域自反，允许存在元素x使得R(x,x)不成立。

而LinearOrder生成的全序关系天然满足全域自反性，因此添加Not(R(x,x))后会返回unsat，符合预期。

解决方法 #

如果需要严格符合定义的偏序，手动添加全域自反性约束即可：

from z3 import *

s = Solver()
R = PartialOrder(IntSort(), 0)
x = Int('x')
# 强制所有元素满足自反性
s.add(ForAll([x], R(x, x)))
# 验证自反性
s.add(Not(R(x, x)))
print(s.check())  # 输出 unsat

模型解析 #

你拿到的模型中，partial-order的定义包含Var(0) == Var(1)分支，理论上R(x,x)应为True，但由于未显式约束全域自反，Z3可以构造出一个模型，其中部分元素的自反性不成立——这是Z3在满足现有约束下的合法解。

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