A Concurrent Portfolio Approach to SMT Solving
- Youssef Hamadi ,
- Leonardo de Moura ,
- Christoph M. Wintersteiger
Proceedings of the 21st International Conference on Computer Aided Verification (CAV) |
Published by Springer
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.