# Partitioning Strategies for Distributed SMT Solving

arXiv: https://arxiv.org/abs/2306.05854 · HTML: https://mlsanity.com/paper/2306.05854/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 8 Jun 2023.

## Built on by (most cited first, 1 of 1)

- [Smart Cubing for Graph Search: A Comparative Study](https://mlsanity.com/paper/2501.17201/) (2025)

## Abstract (arXiv)

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.