Поведение z3 меняется по запросу для ненасыщенного ядра

Question

У меня есть несколько примеров SMTLIB2, которые z3 обычно находит ненасыщенными в течение 10 секунд миллисекунд, но когда я добавляю запрос на генерирование несинхронизированных ядер, check-sat продолжает работать в течение нескольких минут, не возвращаясь. Можно ли ожидать такого поведения? Делает ли запрос несогласованных ядер нечто большее, чем просто включение зависимостей записи инструментов и изменение тех процедур и опций, с которыми работает z3? Можно ли установить дополнительные параметры, чтобы я видел то же поведение, когда я использую ненасыщенную генерацию ядра, как я вижу, когда я его не использую?

Я использую Z3 4.3.1 (стабильная ветвь) на Scientific Linux 6.3.

Примеры приведены в AUFNIRA, хотя некоторые из них не содержат реалов и, вероятно, не являются нелинейными.

Спасибо,

Павел.

Answer 1

Несоответствующие ядра отслеживаются с использованием "литералов ответа" (или предположений). Когда мы включаем извлечение ядра в ненасыщенном виде и используем такие утверждения, как

(assert  (! (= x 10) :named a1))

Z3 внутренне создаст новую логическую переменную для имени a1 и утверждать

(assert  (=> a1 (= x 10)))

Когда, check-sat вызывается, предполагается, что все эти вспомогательные переменные являются истиной. То есть Z3 пытается показать, что проблема не удовлетворена / села по модулю этих предположений. Для удовлетворительных случаев это закончится как обычно моделью. Для неудовлетворительных экземпляров он завершается всякий раз, когда генерирует лемму, которая содержит только эти предполагаемые логические переменные. Лемма имеет вид (or (not a_i1) ... (not a_in)) где a_i 's являются подмножеством предполагаемых булевых переменных. Насколько я знаю, этот метод был введен решателем MiniSAT. Это описано здесь (раздел 3). Мне это очень нравится, потому что его легко реализовать, и мы получаем бесплатное генерирование ядра.

Однако у этого подхода есть некоторые недостатки. Во-первых, некоторые этапы предварительной обработки больше не применимы. Если мы просто утверждаем

(assert (= x 10))

Z3 заменит x с 10 везде. Мы говорим, что Z3 выполняет "распространение значения". Этот шаг предварительной обработки не применяется, если утверждение имеет вид

(assert  (=> a1 (= x 10)))

Это всего лишь пример, на него влияют многие другие этапы предварительной обработки. Во время решения некоторые из этапов упрощения также отключены. Если мы проверим исходный файл Z3 smt_context.cpp, мы найдем такой код:

   void context::simplify_clauses() {
        // Remark: when assumptions are used m_scope_lvl >= m_search_lvl > m_base_lvl. Therefore, no simplification is performed.
        if (m_scope_lvl > m_base_lvl)
            return;
        ...
   }

Состояние m_scope_lvl > m_base_lvl) всегда верно, когда используются "ответные литералы" / предположения. Таким образом, когда мы включаем ненасыщенную генерацию ядра, мы можем реально повлиять на производительность. Кажется, что на самом деле ничего не бесплатно:)