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.
From: Ilana Shapiro [view email]
[v1]
Sun, 7 Jun 2026 21:45:08 UTC (1,211 KB)
[v2]
Sun, 2 Aug 2026 07:18:06 UTC (2,039 KB)
此内容由惯性聚合(RSS阅读器)自动聚合整理，仅供阅读参考。 原文来自 — 版权归原作者所有。