Z3中y=2模型唯一，为何生成多个Skolem函数模型？

实验背景 #

我测试Z3里两种量化公式的模型表现，做了两组实验：

• 基于ExistsForall构造的公式，唯一满足的模型是y=2，运行代码后只会输出这一个模型；
• 基于ForallExists构造的公式，预期唯一模型是不依赖x的Skolem函数f(x)=2，但实际运行后输出了多个看似重复的Skolem函数模型。

疑问 #

为什么y=2的模型是唯一的，而Skolem函数却会生成多个不同形式的模型？从逻辑上看，[skolem = [else -> 2]]应该是唯一不依赖x的Skolem模型才对。

解答 #

这本质是Z3对两种量化公式的模型生成策略差异导致的：

1. ExistsForall公式的常量模型：对于∃y ∀x. P(y,x)这类公式，y是全局常量，Z3会直接找到唯一满足所有x的常量赋值，不存在其他等价的表示形式，所以只会输出y=2这一个模型。
2. ForallExists公式的Skolem函数模型：对于∀x ∃y. P(x,y)这类公式，y被表示为依赖x的Skolem函数f(x)。当f(x)的取值恒为2时，Z3的模型生成器可能会用多种等价的语法形式来描述这个函数：
   • 直接输出[else -> 2]，表示无论x取何值结果都是2；
   • 也可能拆分x的取值范围（比如按整数区间、符号分支等），但每个分支的结果都是2，看起来是不同的模型，但逻辑上和[else -> 2]完全等价。

Z3在生成Skolem函数模型时，会根据内部的求解策略、约束拆分方式输出不同的语法表示，但这些模型在语义上是等价的——它们都表示f(x)恒等于2。而常量模型没有这种语法上的等价变体，所以只会输出唯一形式。

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