A Concurrent Portfolio Approach to SMT Solving
A Concurrent Portfolio Approach to SMT Solving
复制标题
解决 SMT 问题的并行组合方法
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
L. D. Moura
中科院分区：
文献类型：
--
作者：
C. Wintersteiger;Y. Hamadi;L. D. Moura
随着多核处理器和大规模计算集群的出现，并行算法的研究在整个业界重新兴起。基于最近 SAT 问题相关算法的成功，我们提出了一种组合方法来确定 SMT 公式的可满足性。我们的 Z3 并行版本的性能优于顺序求解器，在许多基准测试中加速速度远远超过一个数量级。
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.