optimization - 这是Z3中的错误吗？对 Real 和 ForAll 应用的答案不正确

Question

我试图找到抛物线 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，尽管它并不总是正确的。这就是解算器给出错误答案的原因吗？我应该编写什么代码来找到此类表达式的最小(或最大值)值？

顺便说一句，Z3 的 Mac 版本是 4.3.2。

Answer 1

我引用了 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' 策略和默认求解器仍然存在问题。他们没有给出正确的结果。需要进一步的评论和讨论。