Search papers, labs, and topics across Lattice.
This paper presents a novel parallel framework for SMT solving that utilizes a dynamic binary partition tree constructed from workers' VSIDS statistics, enhancing the efficiency of the solving process. By integrating core-based CDCL-style pruning and online backbone detection, the approach significantly reduces the search space and optimizes resource allocation. Experimental results show that the new algorithm implemented in the Z3 SMT solver outperforms both sequential Z3 and existing parallel frameworks across multiple challenging benchmarks in the SMT-COMP 2025 Parallel Track.
A new parallel SMT solving framework achieves superior performance by dynamically optimizing search space partitioning and pruning strategies.
Exploiting parallelism in modern CPU architectures remains a longstanding challenge in optimizing SMT solvers. We introduce a novel parallel framework that dynamically builds a binary partition tree of the search space by sampling from workers' VSIDS statistics during solving. We leverage 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.
Microsoft Research