在 Z3 Python 中使用量词消除答案

【问题标题】：Using quantifer elimination with Z3 Python在 Z3 Python 中使用量词消除
【发布时间】：2013-02-19 01:18:27
【问题描述】：

我尝试使用 solve(g) 找到满足公式 g = And(ForAll([i, j, k], Implies(And(k <= 0, A * i + B * j + C * k + D <= 0), k + i - j <= 0)),Not(And(A==0,B==0,C==0))) 的 A、B、C、D 的值。这有很多可能的解决方案，一个是A=1,B=-1,C=D=0，但 Z3 似乎无法做到这一点（solve(g) 不会终止）。

Z3 可以做这种非线性（但简单）的公式吗？也许我可以为此指定一些量化宽松策略或其他东西？

【问题讨论】：

标签： z3 z3py

【解决方案1】：

Z3 有一个量词消除策略。我们可以通过使用以下方法创建求解器来启用它：

s = Then('qe', 'smt').solver()

此命令将创建一个求解器，该求解器首先应用量词消除，然后调用 SMT 求解器。但是，Z3 对非线性公式的量词消除的支持非常有限。您的示例是非线性的，因为它包含：A * i + B * j + C * k + D <= 0。因此，qe 策略将无法消除量词。

如果您可以为非线性算术实现更好的 QE 支持，那就太好了。

【讨论】：

感谢 Leonardo，如果不支持非线性算术的 QE，那么为什么不让 solve(g) 在看到这类公式时返回未知或不支持？相反，它似乎在尝试做某事？此外，Z3 是否支持非线性 equalities 或任何其他非线性算术类？您知道是否有任何其他 SMT 求解器提供对非线性算术的支持？再次感谢
Z3 使用启发式实例化和基于模型的量词实例化。这些方法并不完整，但可以解决很多问题。请注意，发送给 Z3 的大多数问题（包含量词）都在一个不可判定的片段中，但这并不妨碍 Z3 解决其中的一个子集。
据我所知，Z3对非线性算法的支持最好。它在（无量词）非线性算术问题中非常有效。对比见文末research.microsoft.com/en-us/um/people/leonardo/files/…
顺便说一句，我们可以使用超时来中断 Z3 的执行。因此，我们可以使用启发式方法来量化 Z3 将花费的时间来处理量词。