我试图找到抛物线的最小值y =(x + 2)** 2-3,显然,当x ==-2时,答案应该是y ==-3。
但是z3给出了答案[x = 0,y = 1],不符合ForAll断言。

我误以为是什么东西吗?

这是python代码:

from z3 import *

x, y, z = Reals('x y z')

print(Tactic('qe').apply(And(y == (x + 2) ** 2 - 3,
                             ForAll([z], y <= (z + 2) ** 2 - 3))))

solve(y == x * x + 4 * x +1,
      ForAll([z], y <= z * z + 4 * z +1))


结果:

[[y == (x + 2)**2 - 3, True]]
[x = 0, y = 1]


结果表明,“ qe”策略将ForAll断言消除为True,尽管并不总是如此。
那是求解器给出错误答案的原因吗?
我应该如何编码才能找到此类表达式的最小值(或最大值)?

顺便说一句,对于Mac,Z3版本是4.3.2。

最佳答案

我提到了
How does Z3 handle non-linear integer arithmetic?
并使用“ qfnra-nlsat”和“ smt”策略找到了部分解决方案。

from z3 import *

x, y, z = Reals('x y z')

s1 = Then('qfnra-nlsat','smt').solver()
print s1.check(And(y == (x + 2) ** 2 - 3,
                             ForAll([z], y <= (z + 2) ** 2 - 3)))
print s1.model()

s2 = Then('qe', 'qfnra-nlsat','smt').solver()
print s2.check(And(y == (x + 2) ** 2 - 3,
                             ForAll([z], y <= (z + 2) ** 2 - 3)))
print s2.model()


结果:

sat
[x = -2, y = -3]
sat
[x = 0, y = 1]


仍然,“ qe”策略和默认求解器似乎有问题。他们没有给出正确的结果。
需要进一步的评论和讨论。

08-25 12:49
查看更多