我试图找到抛物线的最小值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”策略和默认求解器似乎有问题。他们没有给出正确的结果。
需要进一步的评论和讨论。