使用Z3Py的同一约束集的不同运行时间

Question

我正在使用z3pyapi用Z3解算器编码一个调度问题。除了解算器的运行时在每次运行中的时间不同（有时相差10/100倍）之外，它工作得非常好。 如果解算器花费太长时间，我通常会停止查询并重新启动它。你知道吗

在我看来，解算器（每次运行）采用不同的路径来找到解决方案，这会导致不同的运行时间。你知道吗

所以我的问题是，对于同一组约束（问题），我是否可以强制解算器每次都采用相同的（相似的）路径？你知道吗

在做了一些研究之后，我偶然发现了手动设置随机种子的概念。那对我有帮助吗？关于如何使用pythonapi实现这一点，还有更多的信息吗？你知道吗

最好的

珍妮

Answer 1

除非你提前知道哪个随机种子最有效。但是，您确实可以在回归场景中设置种子，以获得可重复的行为。你知道吗

检查z3 -p的输出，我看到了许多可能性：

fixedpoint.spacer.random_seed (unsigned int) (default: 0)
sat.random_seed (unsigned int) (default: 0)
nlsat.seed (unsigned int) (default: 0)
fp.spacer.random_seed (unsigned int) (default: 0)
smt.random_seed (unsigned int) (default: 0)
sls.random_seed (unsigned int) (default: 0)

（注。0告诉“自己挑选”给解算器。）您想要的最有可能是smt.或sat.一个；也许两者都是。你知道吗

您可以使用set_param函数从pythonapi设置此选项，请参见：https://z3prover.github.io/api/html/namespacez3py.html#a54767807c828563030b9400332f81d48