Я экспериментирую с Z3 (используя Python API), где я строю модель планирования для назначения класса, где я должен использовать по модулю довольно часто (потому что это периодическое). Кажется, что Modulo уже сильно замедляет работу z3, но если я попытаюсь провести некоторую оптимизацию сверху (минимизировать функцию стоимости, которая является суммой), то для довольно небольших задач потребуется довольно много времени.
Без оптимизации работает нормально (несколько секунд для небольшой проблемы). Так что, как говорится, у меня сейчас 2 вопроса:
1) Есть ли уловка с функцией по модулю, как ее использовать? Я уже назначил значение по модулю функции. Или есть какой-то другой способ выразить периодическое / кольцевое поведение?
2) Я не заинтересован в поиске наилучшего решения. Хороший, будет достаточно хорош. Есть ли способ установить некоторые границы для функции стоимости. Мол, если знать верхнюю и нижнюю границы этого? Любые другие приемы, где я мог бы использовать знания предметной области, чтобы быстро находить решения.
Кроме того, я подумал, что, если я буду использовать опцию тайм-аута solver.set («тайм-аут» 10000), тогда решатель покажет время с лучшим решением. Это не похоже на случай. Это просто время ожидания.