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 に削除したことを示していますが、常に 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 に答える