分布式Z3和每个节点的最佳硬件

Question

我在考虑启动一个服务器集群，它将独家运行Z3来解决SMT公式。

有没有什么办法可以将几台服务器集群化来加入计算能力并以分布式方式解决SMT公式？ 系统的推荐特性是什么？Z3的运行速度会尽可能快（关于硬件）？

谢谢！

Answer 1

由于缓存命中率低，SAT/SMT解算器通常在内存上占用很大的内存。因此，你不能在CPU上运行很多进程，否则它们很快就会降低对方的性能（例如，如果你想进行基准测试，每个内核运行一个进程并不是一个好主意）。

我不能给出任何具体的推荐，但我会选择核心较少（比如说4）和高内存带宽的CPU。如今，CPU拥有固定的TDP，而CPU越少，每个CPU越强大 - 对内存的争用也越少。

另外你想坚持小端架构。目前，Z3并不适合用于大端（如ARM，MIPS，SPARC等）。而且，就我所见，64位通常有帮助。