См. Публикации на эту тему, например,
1. Николай Бьорнер и Ан-Дунг Фан. νZ - максимальное удовлетворение Z3. В Proc International Symposium по символическим вычислениям в науке о программном обеспечении, Gammart, Тунис, декабрь 2014 г. EasyChair Proceedings in Computing (EPiC). [PDF]
2. Николай Бьорнер, Ан-Дунг Фан и Ларс Флекенштейн. Z3 - Оптимизирующий SMT Solver. In Proc.ТАКАС, объем 9035 LNCS.Springer, 2015 - И, если этого недостаточно, любая другая публикация, связанная с темой теории оптимизации по модулю. [Springer] [[PDF]
Решатель z3 Optimization Modulo Theories (OMT) имеет различные процедуры оптимизации.Некоторые из этих методов более эффективны, чем другие, но могут иметь дело только с определенными классами целевых функций (например, Псевдо-булевых / MaxSMT целей ).В случае функций линейной арифметики , которые нельзя уменьшить до Pseudo-Boolean / MaxSMT , базовый подход к поиску оптимизации, принятый большинством решателей OMT, заключается в запуске либо в linear- или бинарный поиск .Для сравнения двух подходов см.
Роберто Себастьяни и Сильвия Томаси Оптимизация в SMT с функциями затрат LA (Q). В IJCAR, том 7364 из LNAI, стр. 484–498.Springer, июль 2012 г. [PDF]
Роберто Себастьяни и Сильвия Томази . Оптимизация по модулю теории с линейными рациональными затратами. ACM-транзакции по вычислительной логике, 16 (2), март 2015 г. [PDF]
IЯ не уверен, как ответить на вопрос «Как он может эффективно вычислить здесь максимальное / минимальное значение ..?» , потому что сначала нужно определить, что эффективность означает в этом контексте.Как вы можете прочитать из предыдущих двух публикаций, бинарный поиск не всегда является лучшим выбором, потому что шаги поиска в оптимизации не имеют одинаковую "стоимость" .
Определение лексикографическая оптимизация легко доступна по всему Интернету, я использовал ее совсем недавно:
Определение 4.6.4,(Лексикографический OMT [BP14, BPF15, ST15b, ST15c]). Пусть <φ,O> - многоцелевая проблема OMT, где φ - это наземная формула SMT, а O = { obj_1 , ..., obj_N } - отсортированный список Nцелевые функции.Мы называем лексикографической проблемой ОМТ , проблемой нахождения модели M, которая удовлетворяет φ и составляет каждый obj_i минимум¹ в порядке убывания приоритета.
¹:на практике цели не должны быть сведены к минимуму, это просто для простоты определения
AFAIK , процедура лексикографической оптимизации, реализованная в z3, подробно не описанав любой общедоступной газете.Однако тривиальным подходом для lex является запуск N одноцелевых (инкрементальных) оптимизаций, каждый раз фиксируя оптимальное значение, полученное в предыдущем раунде.
Если этого недостаточно дляОтветьте на свои вопросы, пожалуйста, посмотрите на любую другую публикацию, связанную с темой Оптимизация по модулю .