Это ошибка в Z3? Неправильный ответ на применение Real и ForAll

Я пытаюсь найти минимальное значение Параболы y=(x+2)**2-3, видимо, ответ должен быть y==-3, когда x ==-2. Но z3 дает ответ [x = 0, y = 1], который не соответствует утверждению ForAll.

Я что-то неправильно предполагаю?

Вот код питона:

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 — 4.3.2 для Mac.


optimization z3 z3py quantifiers
person wsysuper    schedule 14.11.2014    source источник

Ответы (1)


arrow_upward
0
arrow_downward

Я ссылался на Как 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» и решатель по умолчанию кажутся ошибочными. Они не дают правильного результата. Необходимы дополнительные комментарии и обсуждения.

person wsysuper    schedule 14.11.2014
comment
Спасибо за создание этих примеров. Однако я не могу воспроизвести эти ошибки, используя последнюю нестабильную ветку. Я исправил некоторые ошибки в модуле qe, основываясь на отчете Monniaux несколько месяцев назад. - person Nikolaj Bjorner; 14.11.2014
comment
@NikolajBjorner Значит, в следующем релизе проблема выше будет в порядке? - person wsysuper; 15.11.2014