有什么方法可以让 Z3 使用多核（多线程）来解决大问题？

Question

我正在尝试从商业求解器转移到 Z3 以解决大整数可满足性问题。 “大”是指我要解决的模型大约有 300,000 个整数和 300,000 个 (assert (=... 语句，每个语句可能包含 8-16 个变量。

我们的商业求解器用了 1353 秒来解决这个大问题。我们的商业求解器实际上是一个优化器，它作为一个混合整数优化问题来解决。该问题转化为具有 5,093,121 个变量、9901 个约束、63,450,472 个零、5,093,120 个整数的整数问题，并在 4690 次迭代中求解。但是，这是一个简单的 SAT 问题，所以我希望将其移至 Z3 并放弃商业优化器。

正如我所指出的，商业优化器花费了 1353 秒，但它也被允许使用 32 个内核，并且表明我使用了其中的许多（我没有跟踪它最终使用了多少个内核）。

我希望 Z3 能够使用多个内核。目前看来还没有。有没有办法让它这样做？如果做不到这一点，还有其他 SMT 求解器可以吗？

Answer 1

Z3 确实支持并行处理，见：https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-parallel-z3

可以在命令行上设置参数。所以要让z3使用4个线程并处理文件solve.z3，使用：

z3 parallel.enable=true parallel.threads.max=4 solve.z3

请注意，如果parallel.enable 设置为true，Z3 将默认为处理器数量。

不幸的是，此功能的文档记录相当差。如果您尝试一下，请务必报告您的发现！