Z3Py 中最大值的模型不正确

Question

我想找到一个表达式e对所有 x 都为真的最大间隔。编写此类公式的方法应该是：Exists d : ForAll x in (-d,d) . e and ForAll x not in (-d,d) . !e。

为了得到这样的d，Z3 中f的公式(查看上面的公式(可能如下：

from __future__ import division
from z3 import *
x = Real('x')
delta = Real('d')
s = Solver()
e = And(1/10000*x**2 > 0, 1/5000*x**3 + -1/5000*x**2 < 0)
f = ForAll(x,
And(Implies(And(delta > 0,
-delta < x, x < delta, 
x != 0),
e),
Implies(And(delta > 0,
Or(x > delta, x < -delta),
x != 0),
Not(e))
)
)
s.add(Not(f))
s.check()
print s.model()

其中输出[d = 1/4].

为了检查它，我设置了delta = RealVal('1/4')，从f中删除ForAll量词，我得到x = 1/2。我用1/2替换delta并得到3/4，然后7/8等等。绑定应1。我可以让 Z3 立即输出吗？

Answer 1

如果你自己做数学，你可以看到解决方案是x != 0, x < 1.或者你可以简单地让 Wolfram Alpha 为你做这件事。所以，没有这样的delta.

您遇到的问题是您断言：

s.add(Not(f))

这就把x的普遍量化变成了存在主义的;要求z3找到一个delta，这样就有一些符合要求的x。(也就是说，你否定了你的整个公式。相反，您应该执行以下操作：

s.add(delta > 0, f)

这也确保了delta是积极的。通过该更改，z3 将正确响应：

unsat

(然后你会得到一个错误，调用s.model()，你应该只在上一个调用s.check()返回sat时调用s.model()。