Distributed Z3 and best hardware for each node

Question

I'm thinking on starting a cluster of servers which will be running exclusively Z3 to solve SMT formulas.

Is there any way to clusterize several servers to join computational power and solve SMT formulas in a distributed fashion? What are the recommendation characteristics of an system that will be running Z3 to be as fast as possible (regarding to hardware)?

Thank you!!

Answer 1

SAT/SMT solvers are usually very heavy on memory due to low cache hits. Therefore you can't run many processes on a CPU, otherwise they soon start degrading the performance of each other (i.e., running one process per core is not a good idea if you want to benchmark).

I can't give any specific recomendation, but I would choose CPUs that have fewer cores (say 4) and high memory bandwidth. These days CPUs have a fixed TDP and the fewer the CPUs the more powerful each one is -- and less contention for the memory.

Also you want to stick with little-endian architectures. At the moment, Z3 doesn't play well with big-endian archs (such as many ARMs, MIPS, SPARCs, etc). Moreover, for what I've seen, 64 bits usually helps.