Z3 Forall с массивом

Z3 предоставляет неизвестное для простой задачи:

(assert
(forall ((y (Array Int Int)))
   (= (select y 1) 0))
 )
(check-sat)

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

Это вызывает проблемы, потому что класс проблем, которые я хочу решить, больше похож на:

(declare-fun u () Int)
(assert
 (forall ((y (Array Int Int)) )
     (=> 
        (= u 0) (<= (select y 1) 0))
 )
)
(check-sat)

Где отрицание одного только forall не является той же проблемой, так что здесь этого сделать нельзя. Есть ли какой-нибудь способ задать этот стиль проблемы Z3, чтобы получить результат un/sat?


arrays z3 quantifiers
person Dval    schedule 26.08.2020    source источник

Ответы (2)


arrow_upward
3
arrow_downward

Проблемы с квантификаторами всегда проблематичны с решателями SMT, особенно если они включают массивы и чередующиеся квантификаторы, как в вашем примере. По сути, у вас есть exits u. forall y. P(u, y). Z3 или любой другой SMT-решатель с трудом справляется с подобными проблемами.

Когда у вас есть количественное утверждение, подобное тому, когда у вас есть forall либо на верхнем уровне, либо вложенные с exists, логика становится полуразрешимой. Z3 использует MBQI (установление квантификатора на основе модели) для эвристического решения таких проблем, но чаще всего это не удается. Проблема не только в том, что z3 не способна: для таких проблем нет процедуры решения, и z3 делает все возможное.

Вы можете попробовать дать шаблоны квантификаторов для таких проблем, чтобы помочь z3, но я не вижу простого способа применить это к вашей проблеме. (Шаблоны квантификаторов применяются, когда у вас есть неинтерпретированные функции и количественные аксиомы. См. https://rise4fun.com/z3/tutorialcontent/guide#h28). Так что я не думаю, что это сработает для вас. Даже если бы это было так, шаблоны очень привередливы в программировании и не устойчивы к изменениям в вашей спецификации, которые в противном случае могли бы выглядеть безобидными.

Если вы имеете дело с такими квантификаторами, решатели SMT, вероятно, просто не подходят. Обратите внимание на полуавтоматические средства доказательства теорем, такие как Lean, Isabelle, Coq и т. д., которые предназначены для работы с квантификаторами гораздо более дисциплинированным способом. Конечно, вы теряете полную автоматизацию, но большинство этих инструментов могут использовать решатель SMT для выполнения достаточно простых подцелей. Таким образом, вы по-прежнему выполняете тяжелую работу вручную, но большинство подцелей автоматически обрабатывается z3. (Особенно в случае Lean см. здесь: https://leanprover.github.io/)

person alias    schedule 26.08.2020

arrow_upward
0
arrow_downward

Есть одна лишняя закрывающая (правая) скобка, которую нужно удалить. Кроме того, добавьте assert перед оператором forall.

(assert ( forall ( (y (Array Int Int) ) ) 
   (= (select y 1) 0) 
))
(check-sat)

Запустите приведенный выше код, и вы должны получить unsat в качестве ответа.

Для второй программы вам может быть полезен ответ псевдонима.

person user8616916    schedule 31.08.2020
comment
rise4fun.com/Z3/FKO1b Из онлайн-решателя это приводит к неизвестному. - person Dval; 01.09.2020
comment
Я запустил его на своем терминале. Я не знаю, почему это показывает - неизвестно на его сайте. - person user8616916; 01.09.2020
comment
Несмотря на это, в вашем вопросе есть одна лишняя правая скобка, которую необходимо удалить. - person user8616916; 01.09.2020