Использование исключения квантифера с Z3 Python

Я пытаюсь найти значения для A,B,C,D, удовлетворяющие формуле g = And(ForAll([i, j, k], Implies(And(k <= 0, A * i + B * j + C * k + D <= 0), k + i - j <= 0)),Not(And(A==0,B==0,C==0))), используя solve(g) . У этого есть много возможных решений, одно из них A=1,B=-1,C=D=0, но Z3, похоже, не может этого сделать (solve(g) не завершается).

Может ли Z3 использовать такую ​​нелинейную (но простую) формулу? Возможно, я могу указать некоторые стратегии количественного смягчения или что-то в этом роде?


z3 z3py
person Vu Nguyen    schedule 19.02.2013    source источник

Ответы (1)


arrow_upward
4
arrow_downward

Z3 использует тактику исключения квантификаторов. Мы можем включить его, создав решатель, используя:

s = Then('qe', 'smt').solver()

Эта команда создаст решатель, который сначала применяет исключение квантификатора, а затем вызывает решатель SMT. Однако Z3 имеет очень ограниченную поддержку исключения квантификаторов нелинейных формул. Ваши примеры нелинейны, потому что они содержат: A * i + B * j + C * k + D <= 0. Таким образом, тактика qe не сможет устранить квантификатор.

Было бы здорово, если бы вы могли реализовать лучшую поддержку QE для нелинейной арифметики.

person Leonardo de Moura    schedule 19.02.2013
comment
Спасибо, Леонардо, если QE для нелинейной арифметики не поддерживается, то почему бы просто не сделать так, чтобы solve(g) возвращал неизвестное или неподдерживаемое значение при виде таких формул? Вместо этого кажется, что он пытается что-то сделать? Кроме того, поддерживает ли Z3 QE нелинейные равенства или любой другой нелинейный арифметический класс? Знаете ли вы, поддерживает ли какой-либо другой SMT-решатель нелинейную арифметику? Спасибо еще раз - person Vu Nguyen; 19.02.2013
comment
В Z3 используется эвристическая реализация и реализация квантификатора на основе модели. Эти методы не являются полными, но они могут решить многие проблемы. Обратите внимание, что большинство задач (содержащих кванторы), отправляемых в Z3, находятся в неразрешимом фрагменте, но это не мешает Z3 решать часть из них. - person Leonardo de Moura; 19.02.2013
comment
Насколько мне известно, в Z3 лучшая поддержка нелинейной арифметики. Он очень эффективен в нелинейных арифметических задачах (без кванторов). См. сравнение в конце этой статьи research.microsoft. com/en-us/um/people/leonardo/files/ - person Leonardo de Moura; 19.02.2013
comment
Кстати, мы можем использовать тайм-ауты, чтобы прервать выполнение Z3. Таким образом, мы можем количественно определить количество времени, которое Z3 потратит, используя эвристические методы обработки квантификаторов. - person Leonardo de Moura; 19.02.2013