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

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

Я сформулировал задачу, и 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)

z3 z3py
person SPMP    schedule 06.12.2013    source источник

Ответы (1)


arrow_upward
1
arrow_downward

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

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

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

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

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

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

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

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

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

person Nikolaj Bjorner    schedule 12.12.2013