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

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

Поскольку ваша формула состоит из квантификаторов, я не думаю, что 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) && target(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, который полностью соответствует вашим предпочтениям.

Целевая функция использует нелинейную целочисленную арифметику и квантификаторы. Нелинейная целочисленная арифметика уже сложна (неразрешима) без кванторов, а добавление кванторов делает ее еще хуже. Если вы измените сортировку с 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, которые должны иметь отношение к делу. Они довольно близко подходят к решению такого рода проблем. Последние несколько слайдов в этой колоде иллюстрируют, как использовать Z3 API для поиска по моделям. Конечно, вы также можете использовать текстовый API, если хотите написать парсер для выходного формата. Есть много других способов взаимодействия с Z3 для решения проблем оптимизации, но все они требуют, чтобы вы запрограммировали поиск оптимизации поверх Z3. Это все еще может быть полезно, когда у вас есть логические комбинации ограничений по арифметике и другим областям, поддерживаемым Z3, но стандартные задачи оптимизации лучше решать с помощью специальных инструментов оптимизации.

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

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