【发布时间】：2015-10-20 20:25:24
【问题描述】：
我正在考虑启动一个专门运行 Z3 的服务器集群来解决 SMT 公式。
有没有什么方法可以集群化多台服务器以加入计算能力并以分布式方式解决 SMT 公式？ 将尽可能快地运行 Z3 的系统的推荐特征是什么（关于硬件）？
谢谢！！
【问题讨论】：
标签： hardware z3 distributed-computing smt
【发布时间】：2015-10-20 20:25:24
【问题描述】：
由于缓存命中率低，SAT/SMT 求解器通常占用大量内存。因此，您不能在 CPU 上运行多个进程，否则它们很快就会开始降低彼此的性能（即，如果您想进行基准测试，每个内核运行一个进程并不是一个好主意）。
我不能给出任何具体的建议，但我会选择内核更少（比如 4 个）和高内存带宽的 CPU。如今，CPU 具有固定的 TDP，并且 CPU 越少，每个 CPU 的功能就越强大 - 内存争用也就越少。
您还想坚持使用小端架构。目前，Z3 不能很好地与大端拱（例如许多 ARM、MIPS、SPARC 等）配合使用。此外，就我所见，64 位通常会有所帮助。
【讨论】：
-
谢谢。你知道我是否可以以分布式方式使用 Z3 吗？谢谢
-
你不能。不过，有一个并行模式（使用 OpenMP），但加速可以在