Как использовать пошаговое решение с z3py

Question

Я использую Python API решателя Z3 для поиска оптимизированных расписаний. Он работает довольно хорошо, за исключением того, что иногда он очень медленный даже для небольших графиков (иногда очень быстрый). Причиной этого, вероятно, является то, что ограничения моей задачи планирования довольно сложны. Я пытаюсь ускорить процесс и наткнулся на некоторые статьи о пошаговом решении. Насколько я понял, вы можете использовать инкрементное решение, чтобы обрезать часть пространства поиска, применяя только части ограничений.

Итак, мой оригинальный код выглядел так:

for constraint in constraint_set:
    self._opt_solver.add(constraint)
self._opt_solver.minimize(some_objective)
self._opt_solver.check()
model = self._opt_solver.mode()

Я изменил это сейчас на следующее:

for constraint in constraint_set:
    self._opt_solver.push(constraint)
    self._opt_solver.check()
self._opt_solver.minimize(some_objective)
self._opt_solver.check()
model = self._opt_solver.mode()

Я в основном заменил команду "add" командой "push" и добавил check() после каждого нажатия.

Итак, прежде всего: правильный ли мой общий подход? Кроме того, я получаю исключение, от которого не могу избавиться:

self._opt_solver.push(constraint) TypeError: push() takes 1 positional argument but 2 were given

Может ли кто-нибудь дать мне подсказку, что я делаю не так. Также есть, возможно, руководство по z3py, которое объясняет (возможно, с некоторыми примерами), как использовать инкрементальное решение с API Python.

Мой последний вопрос: это вообще правильный способ минимизации времени выполнения решателя или есть другой / лучший способ?

Answer 1

Функция push не принимает аргумент Это создает точку "возврата", которую вы можете pop позже. Смотрите здесь: http://z3prover.github.io/api/html/classz3py_1_1_solver.html

Ну, это похоже push не совсем то, что вы хотите / нужно здесь вообще. Вы должны просто добавить свои ограничения один за другим и вызвать check, Тем не менее, я очень сомневаюсь, что проверка после каждого добавления может значительно ускорить процесс. В частности, оптимизатор (в отличие от обычного) обычно решает все с нуля. (См. Соответствующее обсуждение здесь: https://github.com/Z3Prover/z3/issues/1577)

Относительно добавочного: Python API автоматически "добавочный". Инкрементальный означает просто возможность вызова команды check() несколько раз, без решателя, забыв, что он видел раньше. (т.е. звоните checkУтверждай больше фактов, звони check снова; второй check будет принимать во внимание все утверждения с самого начала.) Вы не должны делать никаких предположений относительно этого, это даст вам скорость по сравнению с вызовом check только один раз в самом конце: это полностью зависит от эвристики и процедур принятия решений, которые зависят от рассматриваемой проблемы.