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

Question

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

是否有任何方法将多个服务器聚类，以加入计算能力并以分布式方式解决SMT公式？运行Z3的系统的推荐特性是什么，以尽可能快的速度(对于硬件)？

谢谢你！！

Answer 1

由于缓存命中率低，SMT/SMT解算器的内存通常很重。因此，您不能在CPU上运行多个进程，否则它们很快就会降低彼此的性能(也就是说，如果要对每个内核运行一个进程，则不是一个好主意)。

我不能给出任何具体的推荐，但我会选择有较少的核心(例如4)和高内存带宽的CPU。现在CPU有一个固定的TDP，CPU越少，每个CPU的功能就越强大--对内存的争夺也就越少。

此外，您还想坚持使用小终端架构。目前，Z3与大端建筑(如许多武器、MIPS、SPARCs等)打得不太好。此外，据我所见，64位通常是有帮助的。