Можно ли найти оптимальное решение для булевой формулы с помощью SMT-решателей?

Question

У меня есть большая логическая формула для решения, из-за причины редактирования, я должен вставить изображение здесь:

Кроме того, у меня уже есть функция area для измерения размера 4 целых чисел: area(c,d,e,f)=|c−d|×|e−f|

Я хотел бы сделать больше, чем просто выяснить, является ли формула выполнимой: я ищу оптимальный 6-кортеж (a,b,c,d,e,f), в котором большая формула TRUE и area(c,d,e,f) больше или равна измерению любого другого кортежа 6, который также удовлетворяет формуле.

Другими словами, найдите Max(area(c,d,e,f)) подстановку для большой формулы.

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

У кого-нибудь есть идеи? Будем благодарны за любые комментарии по поводу SMT solver, Z3 или других алгоритмов ...

Answer 1

Короче говоря, да.

Поскольку ваша формула состоит из квантификаторов, я не думаю, что Microsoft Solver Foundation является подходящим выбором.Как вы сказали, Z3 поддерживает кванторы, теорию целых чисел и используется для проверки выполнимости.Хотя Z3 напрямую не поддерживает оптимизацию, вы можете легко кодировать задачи оптимизации с помощью универсальных квантификаторов:

sat (a, b, c, d, e, f) => (для всех a1, b1, c1, d1, e1, f1. sat (a1, b1, c1, d1, e1, f1) && goal (a, b, c, d, e, f)> = цель (a1, b1, c1, d1, e1,f1))

где: sat - это ваше логическое выражение для проверки выполнимости, а goal - это функция area, ваша цель оптимизации.

Как видите,Формулировка буквально переводится с вашего требования в вопросе.Назначение для (a, b, c, d, e, f) - это оптимальное решение, которое вам нужно найти.

Кроме того, Z3 имеет дистрибутив Linux и предоставляет OCaml API, который полностью соответствует вашим предпочтениям.

Answer 2

Целевая функция использует нелинейную целочисленную арифметику и квантификаторы. Уже нелинейная целочисленная арифметика жесткая (неразрешимая) без квантификаторов, а добавление квантификаторов делает его еще хуже. Если вы измените вид с Int на Real, то у нас очень ограниченное исключение квантификаторов для нелинейных вещественных чисел ((set-option: ELIM_QUANTIFIERS true) (set-option: ELIM_NLARITH_QUANTIFIERS true)) Но это кажется не совсем подходящим для проблемы, которую вы, кажется, решаете. Попробуйте посмотреть, можно ли сформулировать ее как линейную или квадратичную задачу оптимизации. Есть много инструментов, которые настроены на квадратичную оптимизацию (и, возможно, они менее настроены на, скажем, логический поиск Z3). Попробуйте, например, Solver Foundation, который включает плагины для нескольких инструментов оптимизации.

Возможно использовать Z3 для решения задач оптимизации, но типичный подход заключается в том, чтобы петля снаружи из Z3. Сначала вы ставите задачу, которую вы хотите проверить, выполнимо, а затем вы ищете следующее удовлетворяющее задание, которое улучшает текущий (который вы извлекаете из удовлетворительной модели). Для поиска следующего удовлетворительного задания вы будете утверждать, что «цель», назначенная следующему значению, которое вы ищете, улучшает «цель» присваивается текущее наилучшее значение.

Вот несколько слайдов http://research.microsoft.com/en-us/people/nbjorner/lecture1.pptx это должно быть актуально. Они очень близки к решению этой проблемы. Последние несколько слайдов в этой колоде показывают, как использовать API Z3 для поиска по моделей. Конечно, вы также можете использовать текстовый API, если вы хотите написать парсер для выходной формат. Есть еще много способов взаимодействия с Z3 для оптимизации проблемы, но все они требуют, чтобы вы запрограммировали поиск оптимизации поверх Z3. Это все еще может быть полезно, когда у вас есть логические комбинации ограничений над арифметические и другие области, поддерживаемые Z3, но стандартные проблемы оптимизации может быть решена лучше с помощью специальных инструментов оптимизации.

Answer 3

Я считаю, эта страница была бы чрезвычайно полезна.Пример хорошо объяснен, и он поможет прочитать весь пост.

Answer 4

Ваша проблема не совсем в удовлетворенности, а скорее в оптимизации или, более конкретно, в смешанном целочисленном программировании. Это не должно быть слишком сложно решить с помощью любого решателя, такого как (поскольку вы пометили свой вопрос Z3 и, похоже, используете Windows) Microsoft Solver Foundation , который также предлагает бесплатную версию.