Как оптимизировать кусок кода в Z3? (связано с PI_NON_NESTED_ARITH_WEIGHT)

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

1. Найдите одно решение (в вашем случае решение (sat c d e f)

2. Вычислите значение этого решения (если ваше решение c0, d0, e0, f0, оцените (goal c0 d0 e0 f0). Назовите это значение v0.

3. Найдите решение новой проблемы (and (sat c1 d1 e1 f1) (> (goal c1 d1 e1 f1) v0)).

4. Если пункт 3. возвращает UNSAT, v0 является вашим максимумом. Если нет, используйте новое решение как v0 и вернитесь к пункту 3.

Иногда вы можете ускорить процесс, угадывая сначала верхнюю границу (т. е. значения cu, du, eu, fu, такие, что (and (sat c d e f) (<= (goal cu du eu fu)) является UNSAT), а затем действуя по дихотомии.

По моему опыту, итеративный способ намного быстрее, чем использование квантификаторов для задач оптимизации.

SoftTimur: Так как ваша проблема связана с нелинейной арифметикой (в функции цели) над целыми числами, Z3, скорее всего, ответит "неизвестно" на вашу проблему, даже если вы сможете решить другие проблемы, с которыми вы столкнулись. Нелинейная целочисленная арифметика неразрешима, и маловероятно, что текущий решатель в Z3 сможет эффективно справиться с вашей задачей при наличии квантификаторов. (Конечно, замечательные ребята из Z3 могут «правильно» настроить свой решатель для решения этой конкретной проблемы, но в целом проблема неразрешимости остается.) Решатели SMT, и вы вряд ли далеко пойдете с количественным подходом.

Итак, вы, по сути, остались с идеей Филиппа об использовании итерации. Однако я хочу подчеркнуть, что эти два метода (итерация и количественная оценка) не эквивалентны! Теоретически количественный подход более эффективен. Например, если вы попросите Z3 дать вам наибольшее целочисленное значение (простая задача максимизации, где стоимость является значением самого целого числа), он правильно скажет вам, что такого целого числа не существует. Однако если вы будете следовать итеративному подходу, вы зациклитесь навсегда. Как правило, итеративный подход не работает в тех случаях, когда в задаче оптимизации нет глобального максимума/минимума. В идеале подход, основанный на квантификаторах, может иметь дело с такими случаями, но тогда он подвержен другим ограничениям, как вы сами заметили.

Какими бы замечательными ни были Z3 (и SMT-решатели в целом), программировать их с помощью SMT-Lib довольно сложно. Вот почему многие люди создают более простые в использовании интерфейсы. Например, если вы готовы использовать Haskell, вы можете попробовать привязки SBV, которые позволят вам создавать сценарии Z3 из Haskell. На самом деле, я закодировал вашу проблему на Haskell: http://gist.github.com/1485092. (Имейте в виду, что я мог неправильно понять ваш код SMTLib или допустил ошибку в коде, поэтому проверьте еще раз.)

Библиотека Haskell SBV допускает как количественный, так и итеративный подходы к оптимизации. Когда я пробую z3 с квантификаторами, Z3 действительно возвращает «неизвестно», что означает, что проблема неразрешима. (См. функцию «test1» в программе.) Когда я попытался использовать итеративную версию (см. функцию «test2»), она продолжала находить все лучшие и лучшие решения, я убил ее примерно через 10 минут, найдя следующее решение:

*** Round 3128 ****************************
*** Solution: [4,42399,-1,0]
*** Value   : 42395 :: SInteger

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

Дайте мне знать, если вы решите изучить путь Haskell и если у вас возникнут какие-либо проблемы с ним.