如何使用 z3py 进行增量求解

我正在使用 Z3 求解器的 python API 来搜索优化的时间表。它工作得很好，除了有时即使对于小图也非常慢（但有时非常快）。原因可能是我的调度问题的约束相当复杂。 我试图加快速度，并偶然发现了一些关于增量解决方案的文章。 据我了解，您可以使用增量求解来通过仅应用部分约束来修剪一些搜索空间。

所以我原来的代码看起来像这样：

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()

我基本上用“push”命令替换了“add”命令，并在每次推送后添加了一个 check() 。

首先：我的总体方法正确吗？ 此外，我遇到了一个无法摆脱的异常：

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

谁能给我一个提示，我做错了什么。另外可能还有一个 z3py 教程解释（可能有一些示例）如何通过 python api 使用增量求解。

我的最后一个问题是：这是否是最小化求解器执行时间的正确方法，或者是否有不同/更好的方法？

功能push不需要争论。它创建了一个“回溯”点，您可以pop到后来。看这里：http://z3prover.github.io/api/html/classz3py_1_1_solver.html#abc4ae989afee7ad164844640537107d9 http://z3prover.github.io/api/html/classz3py_1_1_solver.html#abc4ae989afee7ad164844640537107d9

所以它看起来push根本不是您真正想要/需要的。您应该简单地一一添加约束并调用check。然而，我非常怀疑每次添加后的检查是否会显着加快速度。特别是优化求解器（与常规求解器相反）通常从头开始解决所有问题。 （参见此处的相关讨论：https://github.com/Z3Prover/z3/issues/1577 https://github.com/Z3Prover/z3/issues/1577)

关于增量：Python API 是自动“增量”的。增量只是意味着调用命令的能力check()多次，解算器不会忘记之前看到的内容。 （即，调用check，断言更多事实，致电check再次;第二check将从一开始就考虑到所有断言。）您不应该对此做出任何假设，这会给您带来比调用更快的速度check最后一次：这完全取决于启发法和所涉及的决策程序，这取决于手头的问题。