z3 SMT 求解器在不同平台上的性能

【问题标题】：z3 SMT solver performance on different platformsz3 SMT 求解器在不同平台上的性能
【发布时间】：2015-08-08 14:35:42
【问题描述】：

我有使用 z3py 编写的逻辑问题。我在我的电脑（intel core i5 + 8GB RAM）和集群（32 AMD Operaton 6320 cpus + 500GB RAM）上运行它们。运行时没有太大区别，有时远程服务器需要更长的时间，这让我感到困惑。有谁知道 z3 求解器在多核机器上是否更高效？

【问题讨论】：

标签： concurrency z3 multicore smt z3py

【解决方案1】：

默认情况下，Z3 不使用多个内核或 CPU。

但是，它带有 par-or 和 par-and 策略，可用于制定利用并行性的自定义策略。

【讨论】：

谢谢，克里斯托夫。这真的很有帮助。但是在Z3 python api中可以使用这两种策略吗？
是的，它们被称为 ParAndThen 和 ParOr，请参见此处：z3prover.github.io/api/html/…
谢谢。欣赏！