3

我试图找到抛物线 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。

4

1 回答 1

0

我参考 了 Z3 如何处理非线性整数算术？ 并使用“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' 策略和默认求解器仍然看起来有问题。他们没有给出正确的结果。需要进一步的评论和讨论。

于 2014-11-14T09:39:55.227 回答