Найти возможные значения - PullRequest
Новая
       14

Найти возможные значения

0 голосов
/ 17 мая 2018

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

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

Все переменные являются действительными.

Как предложено здесь , я добавляю этот список в решатель: 

[ForAll([x0, x1],
    Implies(Or(x0 != 0, x1 != 0),
        And(P0*x0*x0 + P1*x0*x1 + P2*x0*x1 + P3*x1*x1 > 0,
            -2*P0*x0*x1 + P1*x0*x0 - P1*x0*x1 - P1*x1*x1 + P2*x0*x0 - P2*x0*x1 - P2*x1*x1 + 2*P3*x0*x1 - 2*P3*x1*x1 < 0
            )
        )
    )
]

Решатель с приведенной выше формулой возвращает unsat. Возможное решение для P должно быть [[1.5, -0.5], [-0.5, 1]], и фактически, подставляя эти значения, формула удовлетворяется: 

And(3/2*x0*x0 - 1*x0*x1 + x1*x1 > 0,
    -1*x0*x0 - 1*x1*x1 < 0)

Есть ли способ на самом деле вычислить такой p? Если для z3 сложно, есть ли альтернатива для этой проблемы?

1 Ответ

0 голосов
/ 17 мая 2018

Когда вы говорите «Exists», а затем «Forall», вы говорите, что формула должна быть истинной для каждого такого x0, x1. И Z3 говорит вам, что это просто не так.

Если вы заинтересованы в поиске одного такого P и соответствующих x значений, просто отбросьте квантификацию и сделайте все переменной верхнего уровня: 

from z3 import *

def f(x0, x1, P0, P1, P2, P3):
    return P0*x0*x0 + P1*x0*x1 + P2*x0*x1 + P3*x1*x1

def g(x0, x1, P0, P1, P2, P3):
    return -2*P0*x0*x1 + P1*x0*x0 - P1*x0*x1 - P1*x1*x1 + P2*x0*x0 - P2*x0*x1 - P2*x1*x1 + 2*P3*x0*x1 - 2*P3*x1*x1

p0, p1, p2, p3  = Reals('p0 p1 p2 p3')

x0, x1 = Reals('x0 x1')
fmls = [Implies(Or(x0 != 0, x1 != 0), And(f(x0, x1, p0, p1, p2, p3) > 0, g(x0, x1, p0, p1, p2, p3) < 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

Когда я запускаю это, я получаю: 

sat
[x0 = 1/8, p0 = -1/2, p1 = -1/2, x1 = 1/2, p2 = 1, p3 = 1]

и многие другие; что я верю, что вы после.

Обратите внимание, что вы также можете заняться программированием, чтобы избавиться от экзистенциального количественного определения в зависимости от того, где вы находитесь; то есть, начните с количественной версии, если вы получите unsat, затем переключитесь на новый решатель и используйте не количественную версию, чтобы автоматизировать этот процесс. Конечно, это всего лишь программирование, и на данный момент оно не имеет ничего общего с z3.

...