Каковы пределы рассуждений в количественной арифметике в SMT?

Question

Я попробовал несколько решателей SMT (CVC3, CVC4 и Z3) на следующем, казалось бы, тривиальном тесте:

(set-logic LIA)
(set-info :smt-lib-version 2.0)
(assert (forall (( x Int)) (forall ((y Int)) (= y x))))
(check-sat)
(exit)

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

Есть ли способ решить эти проблемы и каковы пределы аргументации в количественной арифметике в SMT?

Answer 1

Колодка правильная, qe Препроцессор может быть довольно дорогим. Более того, он неэффективен в формулах, исходящих от инструментов проверки программного обеспечения, таких как VCC, Poirot, Dafny, VeriFast, Why3 и ESCJava2. Это не эффективно, потому что формулы, создаваемые этими приложениями, также содержат неинтерпретированные функции, массивы и т. Д.

Как следует из ответа Пада, Z3 - это набор двигателей. Он предоставляет API и команды, которые позволяют пользователям выбирать, какой механизм (или комбинация двигателей) будет использоваться для решения проблемы. Когда пользователь просто говорит (check-sat) is пытается угадать, что является лучшим двигателем для решения формулы ввода. Предположение основано на структуре формулы ввода и аннотациях, предоставленных пользователем (пример: set-logic команда). Мы постоянно расширяем набор фрагментов, которые автоматически обнаруживаются, и набор движков, которые мы предоставляем.

Это, как говорится, смущает, что Z3 пропустил такой фрагмент, как LIA и не применял автоматически qe процедура к нему. За LIA формулы, qe обычно лучший вариант. Альтернативы, основанные на E-match или MBQI, не эффективны, поскольку они предназначены для совершенно разных фрагментов.

Я просто зафиксировал код, который обнаруживает LIA (даже когда set-logic не используется). Изменение уже доступно в unstable (незавершенное) филиал. Он будет доступен завтра в ночных сборках и в следующем официальном релизе.

Answer 2

Ваш пример относится к категории Linear Integer Arithmetic (LIA).

LIA, т. Е. Арифметика Presburger, допускает исключение квантификаторов (qe), хотя временная сложность процедур qe чрезмерно высока.

Я не уверен, что CVC3 и CVC4 поддерживают устранение квантификаторов для LIA, но в Z3 вы можете сделать

(set-logic LIA)
(set-info :smt-lib-version 2.0)
(assert (forall (( x Int)) (forall ((y Int)) (= y x))))
(check-sat-using (then qe smt))

От исполнения Rise4Fun у меня есть unsat результат.

Здесь qe тактика - шаг предварительной обработки перед применением тактики конца игры smt,