Какова теория Z3 Оптимизация максимальной и минимальной функциональности? - PullRequest
Новая
       16

Какова теория Z3 Оптимизация максимальной и минимальной функциональности?

0 голосов
/ 29 января 2019

Я пишу, чтобы узнать теорию / алгоритм, лежащие в основе функции Z3 Optimize, особенно для ее функций maximum и minimum.Это кажется довольно волшебным для меня.Это как-то бинарный поиск или так?Как он может эффективно определить максимальное / минимальное значение здесь?

Я пытался найти исходный код связанных функций (например, функцию execute_min_max), но без глубокого понимания терминов, он не делает слишком многосмысл для меня ... В основном, что означает lex здесь?Кажется, что решения каким-то образом поддерживаются в стеке.

Любые предложения или советы будут очень благодарны.Спасибо.

1 Ответ

0 голосов
/ 03 февраля 2019

См. Публикации на эту тему, например,

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 одноцелевых (инкрементальных) оптимизаций, каждый раз фиксируя оптимальное значение, полученное в предыдущем раунде.

Если этого недостаточно дляОтветьте на свои вопросы, пожалуйста, посмотрите на любую другую публикацию, связанную с темой Оптимизация по модулю .

...