A Concurrent Portfolio Approach to SMT Solving

With the availability of multi-core processors and large-scale computing clusters, the study of parallel algorithms has been revived throughout the industry. We present a portfolio approach to deciding the satisfiability of SMT formulas, based on the recent success of related algorithms for the SAT problem. Our parallel version of Z3 outperforms the sequential solver, with speedups of well over an order of magnitude on many benchmarks.

• Type: Conference
• Year: 2009
• Where: CAV
• Authors: Christoph M. Wintersteiger, Leonardo Mendonça de Moura, Youssef Hamadi
• Keywords: CAV 2009, Formal Methods, Large-scale Computing Clusters, Parallel Algorithms, SMT Formulas