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.

翻译：利用现代CPU架构中的并行性一直是优化SMT求解器面临的长久挑战。我们提出了一种新颖的并行框架，该框架在求解过程中通过采样工作线程的VSIDS统计数据，动态构建搜索空间的二叉划分树。我们充分利用基于核心的CDCL风格剪枝的全部能力，持续缩小划分树。我们进一步通过将在线主干检测融入工作线程，并引入按需终止机制以积极消除已剪枝子问题上的工作量，从而优化了架构。所得到的算法具有高度通用性，并能随可用资源有效扩展。我们在Z3 SMT求解器中实现了该方法，并在SMT-COMP 2025并行赛道中来自六个逻辑的具有挑战性的基准测试上证明，其性能优于串行Z3以及现有最先进的并行框架。