Как эффективно решать комбинации теорий в Z3

Question

Я пытаюсь решить проблему, которая включает пропозициональную выполнимость (с квантификаторами) и линейную арифметику.

Я сформулировал проблему, и Z3 может решить ее, но это занимает неоправданно много времени.

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

Ниже приводится очень упрощенная проблема, которая отражает суть того, что я пытаюсь решить. Кто-нибудь может дать предложения?

Я пытался прочитать такие вещи, как метод Нельсона Оппена, но было много незнакомых нотаций, и потребуется много времени, чтобы выучить его.

Кроме того, Z3 позволяет пользователям настраивать эти конфигурации? Наконец, как я могу использовать эту тактику с z3py?

(declare-datatypes () ((newtype (item1) (item2) (item3))))

(declare-fun f (newtype newtype) Bool)

(declare-fun cost (newtype newtype) Real)

(assert (exists ((x newtype)(y newtype)) (f x y)))

(assert (forall ((x newtype)(y newtype)) (=> (f x y) (> (cost x y) 0))))

(assert (forall ((x newtype) (y newtype)) (<= (cost x y) 5)))

(check-sat)

(get-model)

Answer 1

В примере задачи, которую вы закодировали, используется количественная оценка. Z3 использует особую процедуру для определения выполнимости класса количественных формул, называемых основанным на модели инстанцированием квантификатора (опция mbqi). Он работает путем расширения модели-кандидата для части ваших формул, не содержащей кванторов, в модель для квантификаторов. Этот процесс может включать в себя много поиска. Вы можете извлечь статистику из процесса поиска, запустив Z3 с параметром /st, и он покажет выбранную статистику процесса поиска и даст приблизительное представление о том, что происходит во время поиска. Не существует конкретной комбинации тактик, которая специализировалась бы на классах формул с арифметикой и квантификаторами (есть класс формул, которые используют битовые векторы и квантификаторы, которые обрабатываются тактикой по умолчанию для таких формул).

Я пытался прочитать такие вещи, как метод Нельсона Оппена, но было много незнакомых нотаций, и потребуется много времени, чтобы выучить его.

Это будет немного касательно понимания проблемы поиска с квантификаторами.

Кроме того, Z3 позволяет пользователям настраивать эти конфигурации?

Да, вы можете настроить Z3 из командной строки. Например, вы можете отключить MBQI с помощью командной строки:

z3 tt.smt2 -st smt.auto_config = false smt.mbqi = false

Z3 теперь возвращает "неизвестно", потому что более слабый механизм квантификатора, который выполняет выбранные экземпляры, не сможет определить, что формула выполнима. Вы можете узнать параметры командной строки, следуя инструкциям из "z3 -?"

Наконец, как я могу использовать эту тактику с z3py?

Вы можете использовать тактику от z3py. Файл z3.py содержит краткую информацию о том, как сочетать тактику. Тем не менее, я ожидаю, что сложность вашего класса задач действительно связана с трудностью поиска, связанной с квантификаторами. Очень легко сформулировать формулы с квантификаторами, в которых доказательства теорем расходятся, поскольку эти классы формул, как правило, в высшей степени неразрешимы.