Получение "хорошего" несат-ядра с z3 (логика QF_BV)

Question

Я использую решатель Z3 SMT для решения проблемы, которую я выразил в логике QF_BV, используя язык SMTLIB 2.

Модель неудовлетворительна, и я пытаюсь заставить решатель создать ядро ​​ненадежности.

Моя модель состоит из нескольких "обязательных" ограничений, которые я определяю, используя assert заявления.

Утверждения, которые я хочу рассмотреть для генерации ненасыщенных ядер, были определены с использованием (assert (! (EXPR) :named NAME)) построить.

Z3 дает мне unsat, как и ожидалось. Тем не менее, Z3 всегда, кажется, сбрасывает "тривиальное" ядро ​​ненасыщенности, состоящее из ВСЕХ названных утверждений.

Я знаю, что существует подмножество моих именованных утверждений, которое является несоответствующим ядром. Я нашел это ядро ​​с помощью Yices SMT Solver, который часто дает мне относительно меньшие ненасыщенные ядра. Модель Yices такая же, как модель Z3 (в значительной степени построчный перевод с SMT2 на язык ввода Yices).

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

Answer 1

Z3 и Yices 1.x используют один и тот же подход для вычисления ненасыщенных ядер. Отслеживайте все утверждения, которые были использованы при доказательстве неудовлетворенности. Однако доказательства, построенные каждой системой, могут быть совершенно разными. Существуют алгоритмы для вычисления минимальных ненасыщенных ядер на основе возможностей, предоставляемых Z3 и Yices. Вот ссылка.

РЕДАКТИРОВАТЬ: по умолчанию Z3 использует несколько этапов предварительной обработки, прежде чем он пытается решить проблему. Некоторые из этих шагов могут повлиять на генерацию ненасыщенного ядра. В частности, он устраняет константы, используя уравнения в задаче. Мы говорим, что Z3 "решает" уравнения и исключает переменные. В вашем скрипте вы можете получить меньшее ядро, отключив этот шаг. Мы можем сделать это, используя опцию

(set-option :auto-config false)

Z3 выполнит очень общую конфигурацию. Для задач с битовыми векторами обычно рекомендуется отключить "распространение релевантности":

(set-option :relevancy 0)

Наконец, теперь мы можем включить / отключить шаг исключения переменных и увидеть влияние на размер ядра без ответа.

(set-option :solver true) ;; Z3 will generate the core C0 C1 C2
(set-option :solver false) ;; Z3 will generate the core C1 C2