Асимметричное поведение в ctx-solver-simplify

Я вижу довольно неожиданное поведение ctx-solver-simplify, где порядок параметров для z3.And(), кажется, имеет значение, используя последнюю версию Z3 из основной ветки https://git01.codeplex.com/z3 (89c1785b):

#!/usr/bin/python
import z3

a, b = z3.Bools('a b')
p = z3.Not(a)
q = z3.Or(a, b)
for e in z3.And(p, q), z3.And(q, p):
  print e, '->', z3.Tactic('ctx-solver-simplify')(e)

производит:

And(Not(a), Or(a, b)) -> [[Not(a), Or(a, b)]]
And(Or(a, b), Not(a)) -> [[b, Not(a)]]

Это ошибка в Z3?


z3
person user1861926    schedule 29.11.2012    source источник

Ответы (2)


arrow_upward
2
arrow_downward

Нет, это не ошибка. Тактика ctx-solver-simplify очень затратна и по своей сути асимметрична. То есть порядок посещения подформул влияет на конечный результат. Эта тактика реализована в файле src/smt/tactic/ctx_solver_simplify_tactic.cpp. Код вполне читаем. Обратите внимание, что он использует решатель «SMT» (m_solver) и делает несколько вызовов m_solver.check() при обходе входной формулы. Каждый из этих звонков может быть довольно дорогим. Для конкретных проблемных доменов мы можем реализовать версию этой тактики, которая еще дороже и позволяет избежать асимметрии, описанной в вашем вопросе.

ИЗМЕНИТЬ:

Вы также можете рассмотреть тактику ctx-simplify, она дешевле, чем ctx-solver-simplify, но симметрична. Тактика ctx-simplify по существу применяет такие правила, как:

A \/ F[A] ==> A \/ F[false]
x != c \/ F[x] ==> F[c]

Где F[A] — формула, которая может содержать A. Он дешевле, чем ctx-solver-simplify, поскольку не вызывает SMT-решатель при обходе формулы. Вот пример использования этой тактики (также доступен онлайн):

a, b = Bools('a b')
p = Not(a)
q = Or(a, b)
c = Bool('c')
t = Then('simplify', 'propagate-values', 'ctx-simplify')
for e in Or(c, And(p, q)), Or(c, And(q, p)):
  print e, '->', t(e)

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

person Leonardo de Moura    schedule 29.11.2012
comment
Спасибо! Если я хочу создать краткую удобочитаемую версию формулы, а время вычисления менее важно, есть ли API или тактика, которую я могу использовать в Z3, чтобы попытаться упростить выражение? Или нужно модифицировать ctx_solver_simplify_tactic.cpp/писать свою тактику? - person user1861926; 29.11.2012
comment
Действительно, propagate-values очень помогает в моем случае - еще раз спасибо! - person user1861926; 30.11.2012

arrow_upward
2
arrow_downward

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

Кроме того, ctx_solver_simplify_tactic делает некоторые компромиссы при упрощении формул: он позволяет избежать многократного упрощения одной и той же подформулы. Если бы это было так, это могло бы значительно (экспоненциально) увеличить размер результирующей формулы.

person Nikolaj Bjorner    schedule 29.11.2012