For many users of Satisfiability Modulo Theories (SMT) solvers, the solver's performance is the main bottleneck in their application. One promising approach for improving performance is to leverage the increasing availability of parallel and cloud computing. However, despite many efforts, the best parallel approach to date consists of running a portfolio of solvers, meaning that performance is still limited by the best possible sequential performance. In this paper, we revisit divide-and-conquer approaches to parallel SMT, in which a challenging problem is partitioned into several subproblems. We introduce several new partitioning strategies and evaluate their performance, both alone as well as within portfolios, on a large set of difficult SMT benchmarks. We show that hybrid portfolios that include our new strategies can significantly outperform traditional portfolios for parallel SMT.

翻译：对于许多可满足性模理论（SMT）求解器的用户而言，求解器的性能是其应用中的主要瓶颈。提升性能的一个有前景的方法是充分利用日益普及的并行计算和云计算资源。然而，尽管已有诸多努力，目前最佳的并行方法仍局限于运行求解器组合（portfolio），这意味着性能仍然受限于最优的串行性能。在本文中，我们重新审视并行SMT中的分治方法，即通过将难题分解为若干子问题进行求解。我们提出了若干新的分区策略，并在大规模困难SMT基准测试集上，分别评估了这些策略单独使用及嵌入组合中的性能。实验表明，包含我们新策略的混合组合能够显著超越传统并行SMT的组合方案。