SoftTimur: Поскольку ваша задача связана с нелинейной арифметикой (в целевой функции) над целыми числами, Z3, скорее всего, ответит «неизвестно» на вашу проблему, даже если вы можете решить другие проблемы, с которыми вы столкнулись.Нелинейная целочисленная арифметика неразрешима, и маловероятно, что текущий решатель в Z3 может эффективно решить вашу проблему при наличии квантификаторов.(Конечно, удивительные люди Z3 могут настроить свой решатель просто «правильно» для решения этой конкретной проблемы, но проблема неразрешимости остается в целом.) Даже если у вас не было нелинейных конструкций, квантификаторы - это мягкое место дляРешатели SMT, и вам вряд ли удастся далеко продвинуться с количественным подходом.
Итак, вы по сути остались с идеей Филиппа об использовании итерации.Я хочу подчеркнуть, однако, что эти два метода (итерация против количественного определения) не эквивалентны!Теоретически, количественный подход является более мощным.Например, если вы попросите Z3 дать вам наибольшее целочисленное значение (простая задача максимизации, где стоимость - это значение самого целого числа), он правильно скажет вам, что такого целого числа не существует.Однако, если вы будете следовать итеративному подходу, вы будете работать бесконечно.В общем, итеративный подход потерпит неудачу в тех случаях, когда для задачи оптимизации не существует глобального максимума / минимума.В идеале, подход, основанный на квантификаторе, может иметь дело с такими случаями, но тогда он подвержен и другим ограничениям, как вы уже сами наблюдали.Lib немного болит.Вот почему многие люди создают более простые в использовании интерфейсы.Если вы открыты для использования Haskell, например, вы можете попробовать привязки SBV, которые позволят вам написать скрипт Z3 из Haskell.Фактически, я закодировал вашу проблему в Haskell: http://gist.github.com/1485092. (Имейте в виду, что, возможно, я неправильно понял ваш код SMTLib или, возможно, допустил ошибку кодирования, поэтому, пожалуйста, проверьте еще раз.)
Библиотека SBV Haskell допускает количественные и итеративные подходы к оптимизации.Когда я пробую z3 с квантификаторами, Z3 действительно возвращает «неизвестно», что означает, что проблема не решаема.(См. Функцию «test1» в программе.) Когда я попробовал итеративную версию (см. Функцию «test2»), она все время находила все более и более лучшие решения, я убил ее примерно через 10 минут, найдя следующее решение:
*** Round 3128 ****************************
*** Solution: [4,42399,-1,0]
*** Value : 42395 :: SInteger
Вы случайно не знаете, имеет ли данный конкретный случай вашей проблемы оптимальное решение?Если это так, вы можете позволить программе работать дольше, и она в конечном итоге найдет ее, в противном случае она будет работать вечно.
Дайте мне знать, если вы решите исследовать путь Haskell и если у вас есть какие-либопроблемы с этим.