我正在考虑启动一个服务器集群，它将专门运行Z3来解决SMT公式。
是否有办法将多个服务器集群起来，以分布式方式加入计算能力并解决SMT公式?运行Z3以尽可能快(就硬件而言)的系统的推荐特性是什么?
谢谢! !
由于缓存命中率低，SAT/SMT求解器通常对内存的占用非常大。因此，你不能在一个CPU上运行许多进程，否则它们很快就会开始降低彼此的性能(也就是说，如果你想要基准测试，每个核心运行一个进程并不是一个好主意)。
我不能给出任何具体的建议，但我会选择内核较少(比如4个)和内存带宽高的cpu。现在cpu有一个固定的TDP, cpu越少，每个cpu就越强大——对内存的争用也就越少。
你还想坚持使用小端架构。目前，Z3不能很好地与大端arch(如许多arm、MIPS、sparc等)配合使用。此外，据我所见，64位通常有用。