Сокращение количества используемых предложений с использованием цели доказательства в Z3

Question

Я экспериментирую с оптимизацией использования Z3 для доказательства фактов о теории первого порядка. В настоящее время я задаю теорию первого порядка в Python, обосновываю квантификаторы и отправляю все предложения вместе с отрицанием цели доказательства в Z3. У меня есть следующая идея, которая, как я надеюсь, может оптимизировать результат: я хочу только отправить формулы из теории в Z3, которые имеют отношение к доказательной цели. Я не буду подробно обсуждать эту концепцию, но я думаю, что интуиция проста: моя теория представляет собой совокупность формул, и я хочу только посылать конъюнкты, которые могут повлиять на истинное значение цели доказательства.

Мой вопрос заключается в следующем: может ли это привести к повышению эффективности, или Z3 уже использует подобный метод? Я думаю, нет, потому что я не думаю, что Z3 всегда предполагает, что последнее утверждение является целью доказательства, поэтому у него нет способа оптимизировать это.

Answer 1

Да, удаление не относящихся к делу фактов может иметь большое значение. Предположим, что у нас есть неудовлетворительная формула вида F_1 and F_2 and (not G), Более того, допустим, что F_1 and (not G) неудовлетворительно, и F_2 выполнимо. F_2 это то, что вы называете не имеет значения. Если есть дешевый способ удалить F_2 перед отправкой формулы в Z3, это, вероятно, будет иметь большое значение.

У Z3 есть эвристика для "игнорирования" не относящихся к делу фактов, но это всего лишь эвристика. Для нашего примера наихудший сценарий F_2 это действительно трудно для Z3 удовлетворить. Z3, по сути, пытается построить интерпретацию / решение, которое удовлетворяет формуле ввода (формула F_1 an F_2 and (not G) в нашем рабочем примере). Формула является неудовлетворительной, когда Z3 может показать, что невозможно построить интерпретацию. На практике формула F_2 не имеет значения для Z3, только если он может быстро показать, что он выполним, и интерпретация / решение для F_2 не конфликтует F_1 and (not G), Если это не так, Z3 может тратить много ресурсов с F_2,