Parallel SMT Solving via Dynamic Partitioning, Core-Guided Pruning, and Backbone Detection

Abstract

Exploiting parallelism in modern CPU architectures remains a longstanding challenge in optimizing SMT solvers. We introduce a novel framework for parallel SMT solving that uses feedback from active search to steer solving. We dynamically build a binary partition tree of the search space by sampling from workers' VSIDS statistics during solving. We introduce a novel search-space pruning mechanism that harnesses the full power of core-based CDCL-style pruning to continuously shrink the partition tree. We further optimize our architecture by incorporating online backbone detection into worker threads, as well as a terminate-on-demand mechanism to eagerly eliminate work on pruned subproblems. The resulting algorithm is highly generalizable and scales effectively with available resources. We implement our approach in the Z3 SMT solver and demonstrate that it outperforms both sequential Z3 and existing state-of-the-art parallel frameworks on challenging benchmarks from six logics in the SMT-COMP 2025 Parallel Track.

Accepted to FMCAD 2026