Получение «хорошего» unsat-core с z3 (логика QF_BV)

Question

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

Модель неудовлетворительна, и я пытаюсь получить решатель для создания unsat-core.

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

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

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

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

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

Answer 1

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

EDIT: по умолчанию Z3 использует несколько шагов предварительной обработки, прежде чем пытается решить проблему. Некоторые из этих шагов могут повлиять на генерацию ненасыщенного ядра. В частности, он устраняет константы, используя уравнения в задаче. Мы говорим, что Z3 «решает» уравнения и исключает переменные. В вашем script вы можете получить меньшее ядро, отключив этот шаг. Мы можем это сделать, используя опцию

(set-option :auto-config false) 

Z3 выполнит очень общую конфигурацию. Для битовых векторных задач обычно это хорошая идея, чтобы отключить «распространение relevacy»:

(set-option :relevancy 0) 

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

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