Z3(Py)中Skolem函数交集结果不符合预期的技术咨询

问题背景 #

假设存在包含进程A、B的系统，由环境选择激活A或B：

• 激活A时，系统需求解P1：Exists y. Forall x. (x>=2) --> (y>1) /\ (y<=x)
• 激活B时，系统需求解P2：Exists y. Forall x. (x<2) --> (y>1) /\ (y>x)

在Exists-Forall量词形式下：

• P1的唯一模型为y=2
• P2的模型包括y=2、3、4……
• 二者合取的模型为y=2，符合预期

但转换为Forall-Exists量词形式、用Skolem函数建模时，合取两个公式得到的Skolem函数模型（如[skolem = [else -> 3/2]]）不符合预期的[skolem = [else -> 2]]，且整数域中出现实数结果，同时P1的Skolem函数输出存在多种形式，由此产生以下疑问：

1. 如何在Z3中正确计算n个Skolem函数的交集？
2. 为何当前合取公式得到的Skolem函数模型不符合预期？
3. 整数域中出现实数结果3/2的原因是什么？
4. P1的Skolem函数输出存在多种形式的原因是什么？

问题解答 #

1. 如何正确计算n个Skolem函数的交集？ #

Skolem函数的“交集”本质是找到同时满足所有约束的Skolem函数，核心是统一域定义+合取所有约束，步骤如下：

• 统一变量与Skolem函数的排序：所有相关公式必须使用相同的域（如全用整数域IntSort()，禁止混合实数与整数）
• 明确每个Skolem函数的约束：将原问题的Exists-Forall公式转换为对应的Forall约束（即Forall x. 触发条件 -> Skolem(x)满足对应性质）
• 合取所有约束并求解：将所有约束合并后交给Z3求解器，得到的模型就是满足所有条件的Skolem函数

修正后的示例代码：

x = Int('x')
skolem = Function('skolem', IntSort(), IntSort())

# P1的Skolem约束：x>=2时，skolem(x)需满足>1且<=x
ct_p1 = ForAll([x], Implies(x >= 2, And(skolem(x) > 1, skolem(x) <= x)))
# P2的Skolem约束：x<2时，skolem(x)需满足>1且>x
ct_p2 = ForAll([x], Implies(x < 2, And(skolem(x) > 1, skolem(x) > x)))

s = Solver()
s.add(ct_p1, ct_p2)
print(s.check())
print(s.model())  # 输出符合预期的skolem = [else -> 2]

2. 当前合取公式模型不符合预期的原因 #

当前代码存在两个关键错误：

• 域不统一：P2的Skolem代码误用了Real('x')和RealSort()，而P1使用整数域，混合域会导致Z3优先满足实数域约束，得到非预期解
• 约束逻辑未对齐：交集部分的变量定义与Skolem函数域未统一，导致约束没有正确覆盖所有整数x的情况

修正后统一使用整数域，Z3会输出skolem = [else -> 2]，因为2同时满足：

• 对所有整数x>=2，2>1且2<=x
• 对所有整数x<2，2>1且2>x（整数x只能是1、0、-1等，均满足）

3. 整数域中出现实数3/2的原因 #

完全是因为代码混合了整数域与实数域：P2的Skolem定义中，x被声明为实数类型，Skolem函数的域也用了实数排序。Z3处理混合域约束时，会将整数视为实数子集，求解器会优先寻找满足所有约束的实数解，而3/2（1.5）在实数域中满足：

• 对x>=2，1.5<=x且1.5>1
• 对x<2，1.5>x（x在[1,2)区间时成立）且1.5>1
  只要统一使用IntSort()，就不会出现实数结果。

4. P1的Skolem函数输出存在多种形式的原因 #

P1的约束是Forall x. (x>=2) -> (skolem(x) >1 ∧ skolem(x) <=x)，这个约束存在多个合法的Skolem函数，Z3会返回任意一个满足条件的解，因此输出形式多样：

• 当x>=2时，Skolem函数可以固定返回2（对所有x>=2都成立），也可以返回x本身，或者定义分段函数（如x=2时返回2，x>2时返回3）
• x<2时的Skolem函数值不影响P1约束（因为P1只约束x>=2的情况），所以这部分可以是任意整数
• Z3的求解器会根据内部启发式算法选择解，不同状态或版本可能返回不同模型，但所有解都满足P1的约束

比如以下都是P1的合法Skolem函数：

• skolem(x) = 2（对所有x）
• skolem(x) = If(x >=2, x, 0)（x<2时的值任意）
• skolem(x) = If(x ==2, 2, x-1)（x>2时返回x-1，满足x-1>1且x-1<=x）

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