Ненулевой вектор в квантификаторе

Я хочу проверить формулу вида:

Exists p . ForAll x != 0 . f(x, p) > 0

Реализация (которая не работает) следующая:

def f0(x0, x1, x, y):
    return x1 ** 2 * y + x0 ** 2 * x

s = Solver()
x0, x1 = Reals('x0 x1')
p0, p1 = Reals('p0 p1')

s.add(Exists([p0, p1], 
                ForAll([x0, x1], 
                          f0(x0, x1, p0, p1) > 0
                      )
            ))
#s.add(Or(x0 != 0, x1 != 0))

while s.check() == sat:
    m = s.model()
    m.evaluate(x0, model_completion=True)
    m.evaluate(x1, model_completion=True)
    m.evaluate(p0, model_completion=True)
    m.evaluate(p1, model_completion=True)
    print m
    s.add(Or(x0 != m[x0], x1 != m[x1]))

Формула не выполняется.

С f0() >= 0 единственный выход - (0, 0).

Я хочу иметь f0() > 0 и ограничивать (x0, x1) != (0, 0).

Я ожидал, что это: p0, p1 = 1, 1 или 2, 2, например, но я не знаю, как удалить 0, 0 из возможных значений для x0, x1.


solver z3 z3py
person nyuw    schedule 10.05.2018    source источник

Ответы (2)


arrow_upward
1
arrow_downward

Продолжая ответ Левента. Во время первой проверки Z3 использует специальную процедуру принятия решения, которая работает с квантификаторами. В инкрементальном режиме он возвращается к чему-то, что не является процедурой принятия решения. Чтобы заставить одноразовый решатель, попробуйте следующее:

from z3 import *

def f0(x0, x1, x, y):
    return x1 * x1 * y + x0 * x0 * x

p0, p1 = Reals('p0 p1')

x0, x1 = Reals('x0 x1')
fmls = [ForAll([x0, x1], Implies(Or(x0 != 0, x1 != 0), f0(x0, x1, p0, p1) > 0))]

while True:
    s = Solver()
    s.add(fmls)
    res = s.check()
    print res
    if res == sat:
        m = s.model()
        print m
        fmls += [Or(p0 != m[p0], p1 != m[p1])]
    else:
       print "giving up"
       break
person Nikolaj Bjorner    schedule 11.05.2018
comment
Это круто! Я не осознавал, что инкрементный режим переключился на другой решатель. Хорошо знать! - person alias; 12.05.2018
comment
Спасибо! Могу ли я получить контрпример, если есть пара x0, x1, для которой он ложен? - person nyuw; 12.05.2018

arrow_upward
0
arrow_downward

Вы бы просто написали это как следствие внутри количественной оценки. Я думаю, вы также смешиваете здесь некоторые переменные. Следующее, кажется, отражает ваше намерение:

from z3 import *

def f0(x0, x1, x, y):
    return x1 * x1 * y + x0 * x0 * x

s = Solver()
p0, p1 = Reals('p0 p1')

x0, x1 = Reals('x0 x1')
s.add(ForAll([x0, x1], Implies(Or(x0 != 0, x1 != 0), f0(x0, x1, p0, p1) > 0)))

while True:
    res = s.check()
    print res
    if res == sat:
        m = s.model()
        print m
        s.add(Or(p0 != m[p0], p1 != m[p1]))
    else:
        print "giving up"
        break

Конечно, z3 не гарантирует, что найдет вам какие-либо решения; хотя кажется, что он управляет одним:

$ python a.py
sat
[p1 = 1, p0 = 1]
unknown
giving up

Как только вы используете кванторы, все ставки отменяются, поскольку логика становится полуразрешимой. Z3 здесь хорошо справляется и возвращает одно решение, а потом сдаётся. Я не думаю, что вы можете ожидать чего-то лучшего, если не используете какие-то специальные процедуры принятия решений.

person alias    schedule 10.05.2018