在 Z3 中，我无法理解 Exists y 量词消除的结果。 Forall x。 (x>=2) => ((y>1) /\\ (y<=x))答案

【问题标题】：In Z3, I cannot understand result of quantifier elimination of Exists y. Forall x. (x>=2) => ((y>1) /\ (y<=x))在 Z3 中，我无法理解 Exists y 量词消除的结果。 Forall x。 (x>=2) => ((y>1) /\\ (y<=x))
【发布时间】：2023-01-12 03:59:26
【问题描述】：

在 Z3-Py 中，我对以下公式执行量词消除 (QE)：

Exists y. Forall x. (x>=2) => ((y>1) /\ (y<=x))
Forall x. Exists y. (x>=2) => ((y>1) /\ (y<=x)),

x 和 y 都是整数。我通过以下方式进行了量化宽松：

x, y = Ints('x, y')

t = Tactic("qe")

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

#EA

ea = Goal()
ea.add(Exists([y],Implies(negS0, (ForAll([x], And(s1,s2))))))
ea_qe = t(ea)

print(ea_qe)

#AE

ae = Goal()
ae.add(ForAll([x],Implies(negS0, (Exists([y], And(s1,s2))))))
ae_qe = t(ae)

print(ae_qe)

ae 的结果 QE 符合预期：[[]]（即 True）。但是，对于ea，QE 输出：[[Not(x, >= 2)]]，这是一个我不知道如何解释的结果，因为 (1) 它并没有真正执行 QE（注意结果公式仍然包含 x，并且确实如此不包含y，这是最外层的量化变量）和（2）我不明白x, >=中逗号的含义。我也无法获得模型：

phi = Exists([y],Implies(negS0, (ForAll([x], And(s1,s2)))))

s_def = Solver()
s_def.add(phi)
print(s_def.model())

这会导致错误 Z3Exception: model is not available。

我认为重点是：由于(x>=2)是一个蕴涵，所以有两种方法可以满足公式；通过使先行词为False 或满足后因。在第二种情况下，模型将是y=2。但在第一种情况下，QE 的结果将是True，因此我们无法获得单一模型（因为它发生在通用模型中）：

phi = ForAll([x],Implies(negS0, (Exists([y], And(s1,s2)))))

s_def = Solver()
s_def.add(phi)
print(s_def.model())

无论如何，我无法“从哲学上”理解 x 的 QE 的含义，其中 x 是（去除量词的）答案的一部分。

有什么帮助吗？

【问题讨论】：

标签： z3 smt z3py quantifiers satisfiability

【解决方案1】：

这里有两个不同的问题，我将分别解决。

神秘的逗号这是一个常见的问题。你宣布：

x, y = Ints('x, y')

也就是说，您将x 命名为“x”，将y 命名为“y”。请注意名称中 x 后面的逗号。这应该是

x, y = Ints('x y')

我想您可以看出区别：您为变量x 指定的名称是“x”，当您执行第一个操作时；即，逗号是名称的一部分。只需跳过右侧的逗号，这无论如何都不是您想要的。结果将开始变得更有意义。

量化

这是另一个常见问题。当你写：

ea.add(Exists([y],Implies(negS0, (ForAll([x], And(s1,s2))))))

negS0 中存在的 x 是不是由您的ForAll 量化，因为它不在范围内。也许你的意思是：

ea.add(Exists([y],ForAll([x], Implies(negS0, And(s1,s2)))))

很难猜出你想做什么，但我希望上面的内容清楚地表明 x 没有被量化。另外，请记住，公式中的顶级存在量词或多或少是无关紧要的。它等同于所有实际用途的顶级声明。

完成此修复后，我认为事情会变得更加清晰。如果没有，请提出进一步澄清的问题。（作为关于 Stack-overflow 的一个单独问题；因为对现有问题的编辑只会使问题复杂化。）

【讨论】：