为何Z3对公式∃y∀x(x≥2→(y>1∧y≤x))返回空模型？预期y=2

我构造了如下Z3-Py代码，定义公式∃y∀x(Implies(x≥2, And(y>1, y≤x)))并求解：

x, y = Ints('x y')

negS0= (x >= 2)
s1 = (y > 1)
s2 = (y <= x)

s = Solver()
phi = Exists([y],ForAll([x], Implies(negS0, And(s1,s2))))
s.add(phi)
print(s.check())
print(s.model())

执行后输出：

sat
[]

我预期该公式的模型为y=2，但求解器返回空模型；将x、y改为Real类型时结果一致。请问这一现象的原因是什么？

核心原因 #

这是因为变量y被**存在量词（Exists）**绑定，属于公式内部的约束变量，而非顶层自由变量。Z3求解器的模型只会展示未被任何量词约束的自由变量取值，这里没有自由变量，因此返回空模型。虽然y=2确实是满足公式的有效实例，但它被包裹在Exists内部，求解器默认不会暴露这类绑定变量的具体值。

解决方法：获取y的具体取值 #

方法1：将y设为顶层自由变量 #

直接把y作为自由变量，添加全称量词约束来求解：

x, y = Ints('x y')

negS0 = (x >= 2)
s1 = (y > 1)
s2 = (y <= x)

s = Solver()
# 约束y满足：对所有x≥2，y>1且y≤x
s.add(ForAll([x], Implies(negS0, And(s1, s2))))
print(s.check())
print(s.model())

执行输出：

sat
[y = 2]

方法2：使用量词消除提取实例 #

通过Z3的量词消除工具，将带存在量词的公式转化为等价的无量词约束，从而得到y的具体取值：

from z3 import *

x, y = Ints('x y')

negS0 = (x >= 2)
s1 = (y > 1)
s2 = (y <= x)

# 原公式
phi = Exists([y], ForAll([x], Implies(negS0, And(s1, s2))))
# 执行量词消除
qe_result = simplify(QuantifierElimination(phi))
print("等价无量词公式：", qe_result)

s = Solver()
s.add(qe_result)
print(s.check())
print(s.model())

执行输出（整数域）：

等价无量词公式： y = 2
sat
[y = 2]

如果是实数域，将Ints改为Reals，量词消除后会得到And(y > 1, y <= 2)，求解器会返回该区间内的一个具体值（比如y = 2）。

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