分佈式Z3和每個節點的最佳硬件

我在考慮啓動一個服務器集羣，它將獨家運行Z3來解決SMT公式。分佈式Z3和每個節點的最佳硬件

有沒有什麼辦法可以將幾臺服務器集羣化來加入計算能力並以分佈式方式解決SMT公式？系統的推薦特性是什麼？Z3的運行速度會盡可能快（關於硬件）？

謝謝！

由於緩存命中率低，SAT/SMT解算器通常在內存上佔用很大的內存。因此，你不能在CPU上運行很多進程，否則它們很快就會降低對方的性能（例如，如果你想進行基準測試，每個內核運行一個進程並不是一個好主意）。

我不能給出任何具體的推薦，但我會選擇核心較少（比如說4）和高內存帶寬的CPU。如今，CPU擁有固定的TDP，而CPU越少，每個CPU越強大 - 對內存的爭用也越少。

另外你想堅持小端架構。目前，Z3並不適合用於大端（如ARM，MIPS，SPARC等）。而且，就我所見，64位通常有幫助。

2015-10-21 08:45:14

謝謝。你知道我是否可以以分佈式方式使用Z3？謝謝 – user1618465

你不能。雖然有一個並行模式（使用OpenMP），但加速可以介於<1％到幾％之間，這取決於您想要解決的問題類型。如果您有足夠的問題來保持設備繁忙，則不值得。 –

回答