python - 使用 Z3Py 相同约束集的不同运行时间

Question

我正在使用 z3py API 使用 Z3 求解器对调度问题进行编码。除了每次运行中求解器的运行时间有所不同(有时相差 10/100)之外，它的工作效果非常好。如果求解器花费太长时间，我经常做的就是终止查询并重新启动它。

在我看来，求解器(每次运行)采用某种不同的路径来寻找解决方案，这会导致不同的运行时间。

所以我的问题是，我是否可以强制求解器每次针对同一组约束(问题)采取相同(相似)的路径？

经过一些研究后，我偶然发现了手动设置随机种子的概念。这对我有帮助吗？有更多信息如何使用 python api 做到这一点吗？

最佳

珍妮

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 函数从 Python API 设置此选项，请参阅:https://z3prover.github.io/api/html/namespacez3py.html#a54767807c828563030b9400332f81d48