Получение моделей для задач с количественными булевыми переменными

Question

Я использую Z3 для проверки выполнимости в логике с линейной целочисленной арифметикой, неинтерпретируемыми функциями и квантификаторами над булевыми переменными.Z3 не предоставляет моделей для удовлетворительных проблем, я полагаю, это из-за квантификаторов (или логики, которую я выбрал: AUFLIA).

Есть ли способ заставить Z3 давать мне модели для таких проблем, кромедля создания всех логических переменных самостоятельно?

Answer 1

Z3 может в принципе решить этот фрагмент.Я говорю «в принципе», потому что сложность решения задачи для этого фрагмента очень высока.Например, он включает в себя фрагмент Бернайса-Шенфинкеля (он же EPR), который является NEXPTIME-полным.Список фрагментов, которые могут быть определены Z3, можно найти по адресу: http://rise4fun.com/z3/tutorial/guide

. Мы должны убедиться, что основанное на модели создание экземпляров квантификатора (MBQI) включено в Z3.Это можно сделать с помощью параметра командной строки MBQI=true или команды SMT2

(set-option :mbqi true)

Z3 также имеет пороговое значение для числа итераций шагов MBQI.Мы можем изменить порог, используя параметр командной строки MBQI_MAX_ITERATIONS=<value> или команду

(set-option :mbqi-max-iterations 1000000)

. Для каждого шага MBQI мы можем попросить Z3 показать, какие квантификаторы не были удовлетворены текущей моделью-кандидатом.Опция MBQI_TRACE=true

При этом я недавно исправил ошибку (сбой), обнаруженную в сценарии SMT2, который вы мне прислали.Исправление будет доступно в Z3 3.2.