Z3Py 中的最大值模型不正确 [英] Incorrect model of max value in Z3Py

问题描述

我想找到一个最大区间，其中表达式 e 对所有 x 都为真.编写这样一个公式的方法应该是: Exists d : ForAll x in (-d,d) .e 和 ForAll x 不在 (-d,d) 中.!e.

I want to find a maximal interval in which an expression e is true for all x. A way to write such a formula should be: Exists d : ForAll x in (-d,d) . e and ForAll x not in (-d,d) . !e.

要得到这样的 d，Z3 中的公式 f(看上面的那个)可能如下:

To get such a d, the formula f in Z3 (looking at the one above) could be the following:

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 立即输出吗?

To check it, I set delta = RealVal('1/4'), drop the ForAll quantifier from f and I get x = 1/2. I replace delta with 1/2 and get 3/4, then 7/8 and so on. The bound should be 1. Can I get Z3 to output that immediately?

推荐答案

如果你自己算一下，你可以看到解决方案是 x != 0, x

1.或者你可以简单地问 Wolfram Alpha 为您做这件事.所以，没有这样的delta.

If you do the math yourself, you can see that the solution is x != 0, x < 1. Or you can simply ask Wolfram Alpha to do it for you. So, there's no such delta.

您遇到的问题是您在断言:

The issue you're having is that you're asserting:

s.add(Not(f))

这将 x 上的通用量化变成了存在主义；要求 z3 找到一个 delta，这样 有一些 x 符合要求.(也就是说，您否定了整个公式.)相反，您应该这样做:

This turns the universal quantification on x into an existential; asking z3 to find a delta such that there is some x that fits the bill. (That is, you're negating your whole formula.) Instead, you should do:

s.add(delta > 0, f)

这也确保 delta 是正数.随着这一变化，z3 将正确响应:

which also makes sure that delta is positive. With that change, z3 will correctly respond:

unsat

(然后你会得到一个调用 s.model() 的错误，你应该只调用 s.model() 如果之前调用s.check() 返回 sat.)

(And then you'll get an error for the call to s.model(), you should only call s.model() if the previous call to s.check() returns sat.)

这篇关于Z3Py 中的最大值模型不正确的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！