Последствия в Z3 - PullRequest
Новая
       13

Последствия в Z3

0 голосов
/ 19 февраля 2019

Z3 может вывести логические следствия теории, как объяснено в https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-consequences

Теперь мне интересно, возможно ли это сделать также для числовых значений.Например, учитывая следующую теорию: 

(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(assert (= (+ x y) 10))
(assert (and (>= y 20) (>= x -20)))
(check-sat)
(get-model)

Мне интересно, можно ли получить, что «у» должно лежать между 20 и 30, а х должно лежать между -20 и -10.

Единственный обходной путь, который я могу найти, - максимизировать и минимизировать эти переменные, и тогда я получу диапазон возможностей, но мне кажется, что могут быть лучшие способы сделать это.

1 Ответ

0 голосов
/ 20 февраля 2019

Это очень похоже на предыдущий вопрос о переполнении стека: Использование SMT-LIB для подсчета количества модулей с использованием формулы

Итог: если существует более одной переменнойесли принять участие, то эту проблему вообще трудно решить вообще;если вы не используете конкретные знания о проблеме.Если есть только одна переменная, то вы действительно можете использовать оптимизацию и другие приемы, чтобы дать вам «диапазоны», но в целом такой алгоритм не обязательно будет производительным.(Хотя на практике он может легко обрабатывать самые простые вещи.)

Если вас не интересуют разрывы и вы хотите узнать только максимум / мин, вы можете использовать оптимизатор z3.Обратите внимание, что это не часть стандартного SMTLib, а расширение z3.Вот пример: 

(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(assert (= (+ x y) 10))
(assert (and (>= y 20) (>= x -20)))

(assert (distinct x (- 15)))
(assert (distinct y 25))

(push) (minimize y) (check-sat) (get-objectives) (pop)
(push) (maximize y) (check-sat) (get-objectives) (pop)
(push) (minimize x) (check-sat) (get-objectives) (pop)
(push) (maximize x) (check-sat) (get-objectives) (pop)

Это печатает: 

sat
(objectives
 (y 20)
)
sat
(objectives
 (y 30)
)
sat
(objectives
 (x (- 20))
)
sat
(objectives
 (x (- 10))
)

Итак, вы можете получить границы, но обратите внимание, как я добавил, что требования x != -15 и y != 25 просто внедиапазоны, которые вы получаете.

Обратите внимание, что если ваш тип не ограничен (например, Int), вы также можете получить +/- бесконечность в качестве границы: 

(declare-const x Int)
(assert (< x 10))
(push) (minimize x) (check-sat) (get-objectives) (pop)
(push) (maximize x) (check-sat) (get-objectives) (pop)

Это печатает: 

sat
(objectives
 (x (* (- 1) oo))
)
sat
(objectives
 (x 9)
)

В общем, оптимизация - сложная проблема, и решатель оптимизации в z3 определенно медленнее, чем обычный.Но это может помочь вашему проблемному домену!

...