Неправильная модель максимального значения в Z3Py

Я хочу найти максимальный интервал, в котором выражение e верно для всех x. Способ написания такой формулы должен быть: Exists d : ForAll x in (-d,d) . e and ForAll x not in (-d,d) . !e.

Чтобы получить такое d, формула f в Z3 (если смотреть на приведенную выше) может быть следующей:

from __future__ import division
from z3 import *

x = Real('x')
delta = Real('d')
s = Solver()

e = And(1/10000*x**2 > 0, 1/5000*x**3 + -1/5000*x**2 < 0)

f = ForAll(x,
And(Implies(And(delta > 0,
                -delta < x, x < delta, 
                x != 0),
            e),
    Implies(And(delta > 0,
                Or(x > delta, x < -delta),
                x != 0),
            Not(e))
    )
)

s.add(Not(f))
s.check()
print s.model()

Что выводит [d = 1/4].

Чтобы проверить это, я устанавливаю delta = RealVal('1/4'), сбрасываю квантификатор ForAll с f и получаю x = 1/2. Я заменяю delta на 1/2 и получаю 3/4, затем 7/8 и так далее. Граница должна быть 1. Могу ли я заставить Z3 выводить это немедленно?


z3 z3py
person yokke    schedule 20.06.2018    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Если вы посчитаете сами, то увидите, что решение x != 0, x < 1. Или вы можете просто спросить Wolfram Alpha, чтобы сделать это за вас. Значит, нет такого delta.

Проблема, с которой вы столкнулись, заключается в том, что вы утверждаете:

s.add(Not(f))

Это превращает универсальную количественную оценку x в экзистенциальную; просят z3 найти delta такое, что существует некоторый x, отвечающий всем требованиям. (То есть вы отрицаете всю свою формулу.) Вместо этого вы должны сделать:

s.add(delta > 0, f)

что также гарантирует, что delta положителен. С этим изменением z3 будет правильно реагировать:

unsat

(И тогда вы получите сообщение об ошибке для вызова s.model(), вы должны вызывать s.model() только в том случае, если предыдущий вызов s.check() возвращает sat.)

person alias    schedule 20.06.2018
comment
В чем разница между s.add(d > 0, f) и f = ForAll(x, Implies(d > 0, ...) в Z3? - person yokke; 25.06.2018
comment
Первое — это соединение, второе — импликация. В первом случае вы говорите z3 найти вам модель, убедившись, что d является строго положительным, а также f соблюдается. В последнем случае вы говорите z3 найти модель, в которой вы заботитесь о f только тогда, когда d положителен. То есть он может найти вам модель с d <= 0 и полностью проигнорировать то, что происходит с f, а это не то, что вам нужно. Обратите внимание, что это не имеет ничего общего с z3, а просто с обычной логикой предикатов. Разница между p /\ forall x. q и forall x. p => q, когда p не упоминает x. - person alias; 25.06.2018