Formal Methods in Computer-Aided Design 2026
Parallel SMT Solving via Dynamic Partitioning, Core-Guided Pruning, and Backbone Detection Ilana Shapiro1 , Sorin Lerner2,1 , Nikolaj Bjørner3 1 UC San Diego, La Jolla, CA, USA 2 Cornell University, Ithaca, NY, USA 3 Microsoft Research, Redmond, WA, USA [email protected], [email protected], [email protected]
Abstract—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 Z 3 SMT solver and demonstrate that it outperforms both sequential Z 3 and existing state-of-the-art parallel frameworks on challenging benchmarks from six logics in the SMT-COMP 2025 Parallel Track.
I. I NTRODUCTION Scaling distributed SMT to match rapid advances in multicore CPUs, high-performance computing, and cloud platforms is a longstanding challenge. Ideally, solver performance should scale with available physical resources. However, most state-ofthe-art SMT solvers, such as Z 3 [1], CVC 5 [2], O PEN SMT [3], and Y ICES 2 [4], remain largely single-threaded. Consequently, most advances in solver performance have focused on improving the techniques and heuristics of sequential SMT solvers, leaving substantial computational resources underexploited. This limitation constrains the effectiveness of SMT solvers in key domains such as verification [5], model checking [6], security [7], and program synthesis [8]. Existing parallel approaches broadly fall into two categories: portfolio and partitioning. In the portfolio method, multiple solvers are run in parallel under different configurations and/or random seeds and may exchange learned clauses during solving. Portfolio solving has led to substantial improvements over sequential approaches by exploiting the instability of SMT solvers via parallel sampling of the solver configuration space [9–11]. However, because portfolio solving is bounded by the performance of the best sequential solver, the approach is hindered by limited scalability [12, 13]. The partitioning approach addresses scalability via a divideand-conquer strategy: the input formula is decomposed into independent subproblems whose disjunction is a tautology to the original formula. The goal is to shrink the search space of each subproblem such that solving them in parallel is faster
https://doi.org/
than sequential. An optimal search space partitioning has the potential to vastly outperform portfolio solving. However, the partitioning strategy faces several inherent challenges: it is difficult to partition the search space into subproblems that are easier than the original, potentially wasting resources to solve infeasible sub-problems when the original formula is satisfiable. In addition, the runtime of SMT solvers is very unstable and sensitive to seemingly trivial changes, such as randomization during search [13, 14]. A popular approach to partitioning is cube-and-conquer, in which n Boolean atoms are chosen from the input formula and assigned to both polarities. This creates 2n independent cubes (partial assignments) for parallel solving. It is difficult to select good splitting atoms, and badly selected atoms can produce a harder problem than the original. Though techniques such as lookahead have been developed to find good split atoms, cube-and-conquer has had limited success, particularly when the partitions are static [11, 15]. Recent techniques have turned to dynamic partitioning [12, 13, 16], where split atoms are selected during search. This enables more sophisticated heuristics for choosing partitioning variables. A similarly challenging problem is cube scheduling across threads, as the order of subproblem exploration can substantially impact overall performance. The partition tree has shown success as a data structure for dynamic partitioning. Recent architectures have combined it with clause sharing and basic search-space pruning [13, 17]. However, none of these approaches fully leverage the feedback generated during active search. In this paper, we move toward a more robust dynamic partitioning framework by systematically exploiting feedback from active search to guide both partitioning and pruning decisions. We introduce a binary partition tree whose splitting atoms are selected on-the-fly from worker threads’ VSIDS statistics. By leveraging the conflict-driven reasoning of CDCL, we enable non-chronological backjumping across the partition tree, using per-thread unsatisfiable cores to actively prune the search space. Our partition tree also supports cross-thread information sharing and on-demand termination of workers on shared subproblems. We further augment our framework with core minimization and online backbone detection for additional search-space pruning. We implement our approach in Z 3, and show that our approach outperforms both sequential Z 3 and
This article is licensed under a Creative Commons Attribution 4.0 International License
state-of-the-art parallel frameworks on challenging benchmarks from six logics in the SMT-COMP 2025 Parallel Track. In summary, we make the following contributions: 1) We introduce a flexible, generalizable framework for parallel SMT solving that dynamically partitions the input formula with Boolean atoms sampled on-the-fly from VSIDS statistics. 2) We introduce a binary partition tree for cube distribution that harnesses the full power of core-based CDCL-style pruning to dynamically shrink the problem space. 3) We further optimize our architecture by incorporating core minimization and online backbone detection for more powerful search-space pruning. 4) We implement our tool in the SMT solver Z 3 and demonstrate that our approach outperforms sequential Z 3 and existing parallel frameworks on six logics from the SMT-COMP 2025 Parallel Track. Our implementation, data, and results are available at https://zenodo.org/records/ 20129487 II. P RELIMINARIES
A. Definitions and Notations
literals inconsistent with respect to T . The process repeats until a T -consistent satisfying assignment is found (SAT) or an unrecoverable conflict is derived (UNSAT) [18]. B. Portfolio Solving SMT solvers are extremely sensitive to small perturbations to the input formula or configuration heuristics [11]. The portfolio strategy leverages this intrinsic instability by running multiple solvers in parallel with slightly different configurations (e.g. parameter values, random seeds) or with permuted, but logically equivalent, inputs. Solvers exchange information learned during search. The portfolio approach has made substantial gains over sequential solving [9, 10, 21–23]. However, since the fastest solver determines the performance of the portfolio, increasing parallelism leads to diminishing returns. C. Search-Space Partitioning The partitioning approach divides φ into n independent ⋁︁ subproblems φ1 , . . . , φn for parallel solving such that i ≡ φi . Thus, if any one φi is SAT, then φ is SAT, and if all φi are UNSAT, then φ is UNSAT. There are two main partitioning strategies: cube-and-conquer and scattering. In cube-andconquer, a set of n atoms A = {a1 , . . . , an } is selected. A cube is a conjunction of literals over these atoms, that is, a formula of the form C = ℓ1 ∧ · · · ∧ ℓn , where each ℓi ∈ {aj , ¬aj } for some aj ∈ A. The 2n resulting cubes over these atoms yield 2n independent subproblems of the form φ ∧ C, which can be solved in parallel. In contrast, scattering produces a sequence of n partitioning formulae:
Satisfiability Modulo Theories (SMT) seeks to determine the satisfiability of a first-order logic formula with respect to a background theory. A theory is a pair T = (Σ, I) where Σ is a signature and I is a class of Σ-interpretations. We assume a fixed background theory T with signature Σ that includes the Boolean sort BOOL, and assume that all terms are Σp1 = C1 , terms, entailment (|=) is entailment modulo T , equivalence is p2 = ¬C1 ∧ C2 , equivalence modulo T , and interpretations are T -interpretations. p3 = ¬C1 ∧ ¬C2 ∧ C3 , A model of a formula φ is a T -interpretation M such that .. M |= φ. An implicant of φ is a conjunction of literals ν such . that ν |=T φ, i.e. every model of ν is also a model of φ. An pn = ¬C1 ∧ · · · ∧ ¬Cn−1 ∧ Cn , atom is a term of sort BOOL that contains no subterms of this sort. A literal is an atom or its negation. A clause is a where each Ci is a cube (not necessarily over the same set disjunction of literals, and a cube is a conjunction of literals. of atoms). Each partition induces a subproblem of the form A propositional formula in conjunctive normal form (CNF) is φ ∧ pi . By construction, all pi are disjoint and their disjunction a conjunction of clauses. A formula φ is a term of sort BOOL ⋁︁n pi covers the search space. Thus, φ ≡ ⋁︁n (φ ∧ pi ). i=1 i=1 and is satisfiable if it is satisfied by some interpretation in A popular data structure for search-space partitioning is I, and unsatisfiable otherwise. A formula whose negation is the partition tree [17], where the root node represents the unsatisfiable is valid [18]. input formula φ. Given a parent node associated with formula Most SMT solvers follow the CDCL(T ) framework [19], P , its i-th child represents a formula P ∧ Ci produced by a which combines a CDCL SAT solver with one or more theory partitioning function [24] such that for all i, the disjunction solvers. The input formula is first preprocessed into an equisat- ⋁︁ Ci holds, and for all j ̸= i, ¬(Ci ∧ Cj ). Our approach is i isfiable CNF formula ϕ that preserves its T -semantics. The SAT based on this data structure as well. solver then incrementally constructs an assignment α through Search-space partitioning has the potential to vastly outalternating propagation (unit clauses force assignments to perform portfolio if good partitions are chosen. However, literals) and decision (the solver chooses values for unassigned identifying good partitions is challenging, and poorly chosen literals) phases. These assignments and their dependencies are partitions can result in harder problems than the original [15]. tracked in an implication graph [20]. The SAT solver performs III. R ELATED W ORK conflict analysis to learn a clause via resolution and adds it to its clause database to prune the search space. Theory solvers may also contribute lemmas. During conflict analysis, Portfolio Solving. Portfolio solving with clause sharing was the solver may extract an unsatisfiable core: a subset of assigned first introduced in the Z 3 SMT solver [10]. Their strategy was
simple: randomize 4 instances of Z 3, and share globally valid lemmas with at most 8 literals between them. Since Z 3’s initial attempt at portfolio parallelism, several portfolio architectures have been pursued [4, 25]. The most successful frameworks were developed in SMTS [17, 22, 23] and CVC 5 [9]. SMTS adopts a unique client-server architecture that orchestrates an underlying solver. Globally valid lemmas are stored in an external database; these lemmas are scored by frequency and randomly sampled, and lemmas with more than 3 literals are discarded [13]. CVC 5 provides further optimizations such as delayed clause sharing and guided randomization [9]. Although portfolio solving has led to significant speedups (particularly in [9] and [22]), it still suffers from innate lack of scalability. Search-Space Partitioning. The state-of-the-art searchspace partitioning framework is SMTS. It is the first to combine partitioning with clause sharing and per-partition portfolios, and the first to revisit already attempted subproblems with a selection strategy rooted in the solver runtime random distribution [13, 17, 22, 23]. SMTS’s underlyling solver is O PEN SMT2, which uses the scattering strategy to construct partitions from CDCL search branch decision literals [3, 26]. Central to SMTS’s architecture is the partitioning tree ([17]), which is built dynamically during search [13]. In contrast to SMTS, CVC 5-C LOUD does not propose a new framework; rather, it introduces techniques for combining multiple atom sources and partitioning with these atoms [12]. A RI PARTI maintains a dynamic partition tree similar to SMTS, but performs variable-level partitioning tailored to arithmetic theories, simplifying subproblems using Boolean and Interval Constraint Propagation [16]. Unlike SMTS, these works do not support clause sharing or revisit already attempted instances. Finally, other partitioning frameworks either rely on static partitioning trees [22, 27], which are less effective than a carefully constructed dynamic tree, or are tailored to specific logics (B ITWUZLA [28] and PB OOLECTOR [29], which combine cubeand-conquer with bitblasting for QF-BV) and thus have limited generality. While SMTS and A RI PARTI support basic searchspace pruning, more sophisticated strategies remain largely unexplored. Existing frameworks also do not fully incorporate feedback from search. Our addresses both of these gaps.
Fig. 1: Overview of Parallel Architecture
it returns control to the batch manager, which may perform subcubing, and selects a new cube for w (Section IV-A). If the cube is UNSAT, the batch manager prunes the partition tree using the solver’s UNSAT core (Section IV-B) and similarly assigns w a new cube. To mitigate redundant computation when multiple workers are assigned to the same cube, we employ a terminate-on-demand policy (Section IV-D) that aborts workers operating on the now-stale cube. Throughout execution, w accumulates learned lemmas that are reused across cubes. Finally, outside the partition tree, the batch manager coordinates two backbone threads, which prove backbone literals detected during search (Section IV-E) to shrink the search space of the worker threads, as well as a dedicated core minimization thread (Section IV-C), which asynchronously reduces workers’ UNSAT cores for more powerful partition tree pruning. A. Binary Partition Tree At the center of our algorithm is the partitioning tree. Unlike SMTS and A RI PARTI , who support n-ary partition trees, we
find a binary tree gives the best result, likely due to our pruning algorithm (Section IV-B). Each node n in our partition tree contains a split atom of positive or negative polarity (i.e. ℓ or IV. PARALLEL A RCHITECTURE ¬ℓ), and the children of n are the polarities of the next split atom (i.e. ℓ1 and ¬ℓ1 ) (Figure 1). Each node n encodes a cube In this section, we detail our novel parallel architecture and C via the path of literals from n to root. When a worker is the strategies it employs to dynamically leverage information assigned node n, it solves the formula φ ∧ C, where φ is the from search. We use the cube-and-conquer approach: cubes are input formula, under a designated conflict budget. The partition created on-the-fly by sampling split atoms from solver threads’ tree is initialized with the empty cube ∅ at the root (Figure 1). Thus, all workers begin with φ itself. VISIDS statistics. Figure 1 outlines our high-level design. On the main thread, the batch manager coordinates thread Nodes exist in one of three states: open (unsolved and synchronization. It maintains a dynamically evolving binary has no assigned workers), active (has at least 1 assigned partition tree for cube storage, distributes cubes to n worker worker), or closed (was determined UNSAT). After solving threads, and facilitates information exchange between workers. their cube or hitting their conflict budget, workers report one of Each worker w runs a sequential Z 3 instance with a progres- 3 statuses to the batch manager: SAT, UNSAT, and UNDEF. A sively increasing conflict budget and repeatedly requests cubes SAT result terminates the search (φ is SAT). An UNSAT result from the batch manager. If the cube is SAT, the entire problem is marks the node as closed: the batch manager prunes the SAT. If w exhausts its conflict budget without solving the cube, partition tree (Section IV-B), and shares the worker’s UNSAT
Algorithm 1: Tree Expansion (based on [13]) Input: Node n; split literal ℓ; effort effort 1 n.update round max effort(effort); 2 if ¬n.is leaf() then 3 return; numActive ← count active nodes(root); numU nsolved ← count unsolved nodes(root); 6 if numU nsolved ≥ numActive · 2 then 7 return;
4
5
if has unvisited open node(root) then 9 return;
8
if rand() ≥ 0.5 then 11 return ;
Algorithm 2: Node Selection (based on [13]) Input: Root node root; target status target Output: Best node bestNode 1 bestNode ← ⊥; bestEffort ← ∞; bestDepth ← −1; 2 DFS(root) 3 return bestNode; Function DFS(cur) if cur = ⊥ ∨ status(cur) = closed then 6 return;
4
5
7 8 9
10
// 50% rejection
s ← shallowest timedout leaf depth(root); 13 if depth(n) = s then 14 n.split(ℓ, ¬ℓ);
10 11
12
12 13 14 15
if status(cur) = target then e ← effort(cur); d ← depth(cur); update ← false; if bestNode = ⊥ then update ← true; else if e ̸= bestEffort then update ← (e < bestEffort); else update ← (d > bestDepth);
16 if update then core with the other workers. If the entire tree is closed, search 17 bestNode ← cur; is terminated with an UNSAT result. 18 bestEffort ← e; bestDepth ← d; When worker w reports UNDEF on node n, the batch 19 manager decides (1) if n should be split, (governed by the tree DFS(left(cur)); expansion policy), and (2) w’s next node assignment (given 20 21 DFS(right(cur)); by the node selection policy). Unit clauses learned by w on n are shared with the other workers. We do not share larger lemmas at this time; exploring this remains a direction for future work. wi ’s conflict budget (initially 1000) increases B. Core-Guided Backjumping dynamically by a factor of 1.5 after each UNDEF result. Finally, nodes accumulate effort from workers who report UNDEF. A In contrast to prior work [13, 16], when worker w reports worker wi ’s effort is its current conflict budget; thus, effort UNSAT on node n, we do not simply close n and its is scaled dynamically. Multiple workers may act on a node n subtree. Instead, we perform CDCL-style non-chronological in portfolio; in this case, n only records the maximum effort backjumping over the partition tree using UNSAT cores and among its workers. This avoids disproportionately inflating the recursive sibling resolution (Algorithm 3). If n’s UNSAT core accumulated effort of nodes with higher parallelism. Note that is empty, this proves global UNSAT. Otherwise, we maintain such portfolio workers are not redundant as each operates with the invariant that all conflict literals lie on the path from the a distinct random seed and solver state shaped by prior cubes. root to n (i.e., a subset of w’s cube).1 If n’s literal is not in the Each node tracks how many workers have attempted it. core, it is irrelevant to the UNSAT result. Thus, we traverse Our tree expansion policy (Algorithm 1) draws from [13]. upward from n to the nearest ancestor n1 whose decision literal When w reports UNDEF for node n, the batch manager counts does appear in the core.2 It is possible that n1 was already the number of active and unsolved (open or active) closed by another thread with core C. In this case, we perform nodes in the partition tree. We expand n only if there are at a core strengthening check. Let C ′ be the current core. If least twice as many active nodes as unsolved nodes, if all |C ′ | < |C|, we replace C with C ′ . open nodes have been visited at least once, and if the depth We then attempt to propagate this core upward via sibling of n is equal to the depth of the shallowest timed-out leaf. resolution. Let ℓ and ¬ℓ be the complementary decision literals Furthermore, we abort expansion based on random throttling of n1 and its sibling, respectively. If both siblings are closed (50% chance). As noted in [13], such heuristics ensure the tree with cores Cℓ and C¬ℓ , we compute the sibling resolvent:3 remains largely balanced. If expansion proceeds, we split n on the highest scoring atom from wi ’s VSIDS statistics. Our node r = (Cℓ ∪ C¬ℓ ) \ {ℓ, ¬ℓ} selection policy (Algorithm 2) is also inspired by [13]. We 1 This follows from Z3’s assumption-based UNSAT core extraction. Here, prioritize open nodes; if none are available, we select from the assumptions correspond to the cube. active nodes. Among nodes of the chosen status, we select 2 It is certainly possible that n = n. 1 the one with the lowest accumulated effort, with greater depth 3 Both cores are nonempty by construction. An empty core would signal as the tiebreaker. After this, the order is random. global UNSAT and thus is never attached to a node in an unsolved tree.
Algorithm 3: Core-Guided Backjumping Input: Node n; UNSAT core C 1 if C = ∅ then 2 close(root, C) ; // global UNSAT 3 return; while n ̸= ⊥ do if n.literal ∈ C then 6 CloseWithCore(n, C); 7 return;
4
5
8
n ← n.parent;
Function CloseWithCore(n, C) if n.closed then 11 return; 9
10
12 13 14 15 16 17 18 19 20 21 22
p ← n.parent; close(n, C); l ← p.left; r ← p.right; if l.closed ∧ r.closed then R ← (l.core ∪ r.core) \ {l.lit, r.lit}; if R = ∅ then close(root, R) ; // global UNSAT return; a ← highest attach(p, R); close(a, R); PropagateUpward(a);
Function PropagateUpward(cur) 24 while cur.parent ̸= ⊥ do 25 p ← cur.parent; l ← p.left; r ← p.right; 26 if ¬(l.closed ∧ r.closed) then 27 return;
23
28 29 30 31 32 33
R ← (l.core ∪ r.core) \ {l.lit, r.lit}; if R = ∅ then close(root, R) ; // global UNSAT return; close(p, R); cur ← p;
If r = ∅, we conclude global UNSAT. Otherwise, we bubble up to the highest ancestor a such that all literals in r are contained in the path from a to root. We then close a and its subtree, and attach r to a and the newly closed nodes in its subtree. This process is applied recursively: if the sibling of a has already been closed by another thread, we compute a new resolvent and continue propagating upward. The result of this process is non-chronological propagation of cores across the partition tree, enabling integration of independently derived core from different workers and lifting CDCL-style clause resolution to search-space partitioning. We apply this process not only to n, but also to other nodes in the partition tree whose cube contains all literals in the UNSAT core.
Algorithm 4: Partial Core Minimization Input: UNSAT core C, SMT input formula φ Output: Reduced core C or a satisfying model 1 Λ ← C; // literals to test 2 mus ← ∅; // min UNSAT core // Invariant: φ ∧ mus ∧ Λ is UNSAT 3 while Λ ̸= ∅ do 4 ℓ ← last(Λ); 5 Λ ← Λ \ {ℓ}; 6 Γ ← mus ∪ Λ ∪ {¬ℓ} ; // flip ℓ 7 Φ ← φ ∪ {{ℓ} | ℓ ∈ Γ}; 8 r ← check sat(Φ); 9 if r = UNDEF then 10 mus ← mus ∪ {ℓ}; 11 else if r = SAT then 12 set global sat(model(Φ)); 13 return; 14 else if r = UNSAT then 15 C ← UnsatCore(Γ); 16 if ¬ℓ ∈ / C then 17 Λ ← ∅; mus′ ← ∅; 18 foreach c ∈ C do 19 if c ∈ mus then 20 mus′ ← mus′ ∪ {c}; 21 else 22 Λ ← Λ ∪ {c}; 23
24
mus ← mus′ ; C ← mus ∪ Λ;
C. Asynchronous Core Minimization A core returned from the SMT engine is not necessarily minimal, and smaller cores enable more powerful pruning. To that end, we introduce a dedicated asynchronous core minimization thread. When worker w closes node n, it submits the pair (n, C), where C is the unrefined UNSAT core, to the core minimization thread’s pending queue. The minimizer attempts to refine each enqueued core C by iteratively removing literals ℓ: it flips ℓ to ¬ℓ, and checks if this preserves UNSAT in under 5000 conflicts (Algorithm 4). If so, it discards ℓ, since UNSAT does not depend on ℓ. This is the standard deletionbased core (MUS/MUC) extraction paradigm [30], adapted to bounded SMT checks. If C is reduced, the pair (n, C) is sent to the batch manager for additional search tree pruning via core strengthening (Section IV-B). Note that we must enqueue the pair (n, C) rather than C alone, since cores are minimized relative to the cube (node) under which they were derived. To ensure soundness, we store the associated node n with each core and use C to strengthen the core at n (Algorithm 3), which leads to more powerful pruning. Note that using a separate thread to minimize cores unblocks worker threads from exploring the search tree.
D. Terminate on Demand Recall that our node selection policy assigns workers to active nodes when no open nodes remain, resulting in a portfolio of m workers operating on the same node n. If a worker w1 proves n UNSAT, the batch manager closes n and prunes the tree. Consequently, the remaining workers w2 , . . . , wm , as well as any workers exploring pruned regions of the search space, may now be working on stale subproblems. To eliminate such redundant work, similar to [16], we include a terminate-on-demand mechanism based on node leases. When worker w is assigned node n, it acquires a lease that records the node’s current cancel epoch. Each node maintains its own cancel epoch, which is incremented when the node is closed. After pruning, the batch manager terminates all workers with stale leases (i.e. whose recorded cancel epoch no longer matches that of its assigned node), eagerly aborting their current search and reassigning them to new nodes.
clause. Otherwise, all literals in C are removed from ωN , and the refinement loop continues. In our setting, a satisfying assignment under ωN signals immediate termination and global SAT; we do not further refine Λ. Our initial chunk size is 20, and our per-chunk check_sat conflict budget is 1000. Algorithm 5 falls back to testing individual literals in Γ with failed literal probing when ωN = ∅ (i.e. when core refinement exhausts the current assumption set without producing a singleton core) or when the maximum-sized chunk (k = |Λ|) returns undef. A literal ℓ is said to be failed in a CNF formula φ if unit propagation derives a contradiction from φ ∧ ℓ [32]. If ℓ is failed, then its complement ¬ℓ belongs to the backbone of φ. For each ℓ ∈ Γ, our fallback algorithm checks if φ ∧ ℓ is UNSAT in under 10 conflicts; if so, ¬ℓ is a backbone literal. V. E VALUATION
We implemented our approach inside Z 3[1]. All experiments were conducted on a dual-socket server with two AMD EPYC 7763 processors (64 cores per socket, 128 cores, 2.45 GHz We further optimize our architecture with two dedicated clock speed), and 512GB RAM, running Ubuntu 24.04.4 LTS. online backbone detection threads as a lightweight search- We show our approach outperforms several state-of-the-art space pruning mechanism. The backbone of a formula φ is the parallel solvers on a diverse set of difficult benchmarks from the set of literals true in all models of φ [31]. If ℓ is a backbone SMT-COMP 2025 Parallel Track. We then conduct ablations literal, it is a consequence of φ, and thus ¬ℓ can prune the demonstrating that our approach scales with computational partition tree: if ¬ℓ matches node n’s literal, Algorithm 3 can resources and benefits from all system components. close n with singleton core {¬ℓ}. Typical backbone detection A. SMT-COMP 2025 Parallel Track Benchmarks algorithms assume φ is SAT and derive candidates from We evaluate our approach against the state-of-the-art parallel implicants [31]. In contrast, we extract backbone candidates dynamically based on phase age and evaluate them via two solvers SMTS [13], A RI PARTI [16], and CVC 5 in both portfolio parallel threads operating in complementary modes. In negative (SMT- D [9]) and partitioning (CVC 5- P [12]) modes on 6 logics mode, we negate candidates and attempt to quickly prove them from the SMT-COMP 2025 Parallel Track [33]: QF NIA, as backbones by deriving a short UNSAT proof. In positive QF NRA, QF LIA, QF LRA, QF IDL, and QF RDL. The mode, we assume candidates directly and attempt to extend the SMT-COMP Parallel Track curates benchmarks designed to assignment to a full model. Theoretically, the positive mode be challenging for parallel solvers. We run each solver with 8 threads and a 20-minute wall-clock timeout per benchmark. may accelerate search on SAT instances. In line with Figure 1, in addition to the 8 partiThroughout solving, the batch manager stores proven backbone literals and a dynamic ranking of the top 100 candidates tion tree threads that work on the input formula, our from worker threads. Candidates are ranked based on phase Z 3 parallel setup adds a core minimizer thread (Alage (number of assignments since their last phase change) and gorithm 4) and 2 backbone detection threads (Algorithm 5) for a total of 11 threads. For the arithmetic cube hits (number of times worker threads returned them): benchmarks, we set tactic.default_tactic=smt, (︁ )︁ rank(c) = phase age(c) · log2 2 + cube hits(c) smt.auto_config=false. For the difference logics, we Candidates are dispatched in batches Λ to the backbone threads, set smt.auto_config=true, smt.arith_solver=4. who attempt to prove them using a modified version of the We configure each external solver with the parameters specified chunked backbone algorithm [31] (Algorithm 5).4 Given Λ, in the associated paper. A RI PARTI supports three different the procedure repeatedly selects a chunk Γ ⊆ Λ of backbone backend solvers (Z 3, CVC 5, O PEN SMT); for comparison, we candidates of size at most K, and attempts to refute the select Z 3 to best match our own architecture. Precise details simultaneous negation of all literals in Γ (i.e. it invokes the of external solver configurations are specified the appendix. The sequential backend solvers of each parallel architecture solver under the assumptions ωN = {¬ℓ | ℓ ∈ Γ}). If the vary significantly in performance. For a fair evaluation, we thus resulting formula is UNSAT, the UNSAT core C is intersected examine the performance delta between the sequential backend with the current assumptions ωN . If this intersection is a solver and 8-thread parallel mode for each architecture. Specifsingleton {¬ℓ}, then ℓ is a backbone literal. The batch manager ically, we examine the delta in number of examples solved and collects ℓ for search-space pruning and shares it as a unit the delta in PAR-2 scores. PAR-2 is a composite metric that 4 Algorithm 7 in [31] combines runtime and number of solved benchmarks: the sum E. Online Backbone Detection
Algorithm 5: Backbone Detection (based on [31]) Input: Backbone candidate literals Λ; SMT input formula φ; K ∈ N+ (chunk size) 1 k ← min(K, |Λ|); // Initial chunk size 2 while Λ ̸= ∅ do 3 Γ ← pick k literals from Λ; 4 ωN ← {¬ℓ | ℓ ∈ Γ}; 5 while true do 6 Φ ← φ ∪ {{ℓ} | ℓ ∈ ωN }; 7 r ← check sat(Φ); 8 if r = SAT then 9 set global sat(model(Φ)); 10 return; 11 else if r = UNSAT then 12 C ← UnsatCore(ωN ); 13 if C = ∅ then 14 set global unsat(); 15 return; 16 else if C = {ℓ} then 17 collect backbone(¬ℓ); 18 Λ ← Λ \ {¬ℓ}; 19 φ ← φ ∪ {¬ℓ}; 20 Γ ← Γ \ {¬ℓ}; 21 22 23 24 25
26 27 28
29 30
31 32 33
// Remove literals in the core ωN ← ωN \ C; if ωN = ∅ then test all ℓ ∈ Γ with failed literal probing; Λ ← Λ \ Γ; k ← min(K, |Λ|); // reset chunk size break ; // Done with the chunk else // r = UNDEF if k < |Λ| then // retry with larger chunk k ← min(2k, |Λ|); else // Done with the chunk test all ℓ ∈ Γ with failed literal probing; Λ ← Λ \ Γ; break;
of the runtimes for all solved instances, plus twice the timeout value multiplied by the number of unsolved instances [34]. A lower PAR-2 score indicates better performance. The sequential backend solver for our Z 3 parallel architecture is simply the current build of Z 3 in single-threaded mode. SMTS uses O PEN SMT[3] as its backend solver; we build and run the current version of O PEN SMT as the sequential SMTS baseline. O PEN SMT (and thus SMTS) does not support nonlinear arithmetic, and so we cannot report results for these benchmarks with SMTS. Though A RI PARTI also uses Z 3 as its backend solver, it uses a pre-compiled binary from 2023
(v4.12.1); we thus run this baseline separately from our own current Z 3 build. Finally, SMT- D and CVC 5- P both use CVC 5[2] as their backend. We build and run the current version of CVC 5 as the sequential baseline for SMT- D and CVC 5- P. Table I summarizes our results. Note that we cannot report nonlinear arithmetic results for SMTS as O PEN SMT does not support these logics. In QF LRA, we achieve the largest increase in solved instances and the largest PAR-2 reduction by a substantial margin over all competing solvers. In QF NIA, we again achieve the largest PAR-2 reduction and tie with A RI PARTI for the largest gain in solved instances. In QF LIA, our method similarly yields the largest PAR-2 reduction while remaining competitive in solved-instance gains, trailing A RI PARTI by only one benchmark and outperforming all other solvers. On QF IDL, our solved-instance delta is likewise only one lower than SMTS, and our PAR-2 reduction is only slightly smaller. Notably, our architecture substantially improves over sequential performance on QF IDL; however, all other architectures besides SMTS regress relative to their sequential baselines. QF NRA is our weakest logic. A RI PARTI is the clear winner on QF NRA, but our architecture remains competitive with the remaining solvers. Results on QF RDL are inconclusive, as all architectures show negligible changes. Recall that A RI PARTI is specifically designed for arithmetic benchmarks by performing arithmetic-theoretic variable-level partitioning[16]. Our architecture is highly generalized and not tailored to arithmetic; we nonetheless remain competitive with A RI PARTI on arithmetic benchmarks and also deliver strong results on difference logic (QF IDL). Table II confirms our system delivers the strongest overall performance across the benchmark suite. We report overall SAT, UNSAT, and total solved-instance deltas between sequential and 8-thread parallel mode for each architecture. Since SMTS does not support nonlinear arithmetic (2 of the 6 benchmark logics), we additionally report average deltas to enable a fair comparison across all solvers. We also report the average PAR-2 reduction (in thousands) relative to sequential performance. Our architecture achieves both the largest average solved-instance gain and the largest average PAR-2 reduction overall. In particular, we have the largest gain in UNSAT examples (SMTS wins for SAT examples by a small margin; we tie closely behind with A RI PARTI). The strong gains in both our raw and average UNSAT deltas speak to the effectiveness of our core-guided search-space pruning procedure (Algorithm 3). B. Ablations We run ablations of our system on randomly selected subsets from the 2024 and 2025 SMT-LIB QF LIA and QF NIA nonincremental benchmark suites [35]. Each experiment uses a 10minute (600-second) per-benchmark timeout. We demonstrate how our system scales with computational resources and show the importance of the backbone threads, core minimizer thread, and core-guided search-space pruning procedure. 1) Scalability: To show how our system scales with available resources, we run it with 1, 2, 4, and 8 worker threads on two randomly selected subsets from the complete 2024 SMT-LIB
TABLE I: SMT-COMP 2025 Benchmark Results Z 3 (ours)
SMTS
A RI PARTI
SMT- D
CVC 5- P
QF LRA (38)
Solved (Seq) PAR-2 (Seq) Solved (8T) PAR-2 (8T) ∆ Solved ∆ PAR-2
1 89.37 4 83.69 +3 -5.69
22 46.10 22 45.11 +0 -0.99
6 80.70 7 77.82 +1 -2.88
3 85.80 5 82.55 +2 -3.25
3 85.80 4 84.15 +1 -1.66
QF LIA (44)
Solved (Seq) PAR-2 (Seq) Solved (8T) PAR-2 (8T) ∆ Solved ∆ PAR-2
2 102.82 8 89.25 +6 -13.56
10 86.89 14 75.32 +4 -11.57
2 101.19 9 87.83 +7 -13.37
1 103.59 3 100.14 +2 -3.45
1 103.59 2 102.19 +1 -1.40
QF NRA (44)
Solved (Seq) PAR-2 (Seq) Solved (8T) PAR-2 (8T) ∆ Solved ∆ PAR-2
2 100.81 3 98.40 +1 -2.41
† † † † † †
5 94.71 8 86.98 +3 -7.73
1 104.38 2 101.71 +1 -2.68
1 104.38 2 101.26 +1 -3.13
Z 3 (ours)
SMTS
A RI PARTI
SMT- D
CVC 5- P
QF NIA (44)
Solved (Seq) PAR-2 (Seq) Solved (8T) PAR-2 (8T) ∆ Solved ∆ PAR-2
13 76.41 16 69.12 +3 -7.29
† † † † † †
8 89.65 11 82.58 +3 -7.08
4 98.46 4 98.02 +0 -0.44
4 98.46 3 99.58 -1 +1.12
QF RDL (24)
Solved (Seq) PAR-2 (Seq) Solved (8T) PAR-2 (8T) ∆ Solved ∆ PAR-2
1 55.57 1 55.64 +0 +0.07
0 57.60 0 57.60 +0 +0.00
1 55.72 1 56.10 +0 +0.38
0 57.60 0 57.60 +0 +0.00
0 57.60 0 57.60 +0 +0.00
QF IDL (45)
Solved (Seq) PAR-2 (Seq) Solved (8T) PAR-2 (8T) ∆ Solved ∆ PAR-2
14 82.21 18 75.15 +4 -7.06
3 101.80 8 92.78 +5 -9.02
5 98.98 4 100.26 -1 +1.28
2 104.97 1 106.40 -1 +1.43
2 104.97 2 105.51 +0 +0.54
Legend: Solved: number of solved benchmarks (sequential and 8-thread parallel); PAR-2: penalized average runtime (in thousands); ∆: difference between 8-thread and sequential runs; †: solver does not support this logic.
TABLE II: Aggregate SMT-COMP 2025 Deltas Z 3 (ours)
SMTS
A RI PARTI
SMT- D
CVC 5- P
∆ SAT ∆ UNSAT ∆ All
+12 +5 +17
+9* +0* +9*
+12 +1 +13
+3 +1 +4
+3 -1 +2
Avg. ∆ SAT Avg. ∆ UNSAT Avg. ∆ All
+2.00 +0.83 +2.83
+2.25 +0.00 +2.25
+2.00 +0.17 +2.17
+0.50 +0.17 +0.67
+0.50 -0.17 +0.33
Avg. ∆ PAR-2
-5.99
-5.39
-4.90
-1.40
-0.76
*SMTS does not support NIA, NRA; the rest handle all 6 logics. PAR-2 score is in thousands.
nonincremental benchmark suite [36] (consisting of 5000 and 2313 benchmarks, respectively, for QF LIA and QF NIA). Figure 2 summarizes our results via cactus plots. We use a logarithmic x-axis for runtime in seconds (1 to 600), and a y-axis representing the cumulative number of benchmarks each configuration solved under the 600-second timeout. On QF LIA, easy benchmarks do not benefit from parallelization, likely due to concurrency overhead on otherwise simple problems. However, parallelism quickly becomes beneficial on harder instances: the 8-thread configuration consistently leads at 109 seconds and beyond. The advantages of parallelism are even more pronounced in QF NIA. Sequential mode performs substantially worse than all parallel configurations, and performance scales smoothly with thread count: the 8thread configuration takes the lead after only 2 seconds.
(a) QF LIA
(b) QF NIA
Fig. 2: Scaling of Parallel Z3 Using 1 to 8 Solvers 2) Solver Ablations: The remaining ablations use a carefully balanced subset of the 2025 SMT-LIB nonincremental QF LIA benchmark suite [37], consisting of 800 benchmarks (400 SAT / 400 UNSAT) up to 1.2MB in size each. We exclude in the range [0, 600] seconds, where the diagonal denotes equal trivial instance solved by sequential Z 3 in under 10 seconds. runtimes between the two configurations. Results are summarized using scatter plots, where × denotes Backbone Threads. We run our full system with 2 backbone a SAT benchmark solved by either configuration, □ denotes threads (negative+positive mode) and compare to ablations with an UNSAT benchmark, and ∗ denotes a timed-out benchmark. 1 (negative mode only) and 0 backbone threads. Performance The axes use a logarithmic scale over per-benchmark runtimes decreases incrementally with the removal of each backbone
(a) 2 vs 1 Backbone Threads
Fig. 4: Core Minimization Ablation
(b) 2 vs 0 Backbone Threads
Fig. 3: Backbone Thread Ablations
Fig. 5: Core-Guided Pruning Ablation
thread (Figure 3). Compared to 1 backbone thread, the full setup solves 4 more examples and achieves a 2% reduction in the SAT PAR-2 ratio for an overall reduction of 1%. Compared to 0 backbone threads, the full setup solves 3 more examples, but achieves a greater SAT PAR-2 ratio reduction of 6% for an overall reduction of 2%. The backbone threads appear to particularly benefit performance on SAT instances. Core Minimizer Thread. We next ablate the core minimizer thread and compare against the full system (Figure 4). Enabling core minimization solves 12 additional benchmarks (8 of which are UNSAT) and reduces PAR-2 by 9%. Interestingly, the SAT PAR-2 reduction (12%) exceeds the UNSAT reduction (7%), despite the larger UNSAT gains, because many SAT benchmarks solved by both configurations become faster with core minimization enabled (×’s are far above the diagonal), while the additional UNSAT solves tend to occur near the timeout boundary. These UNSAT gains solidify the hypothesis that the core minimizer particularly benefits UNSAT instances by enabling more aggressive search-space pruning. Core-Guided Pruning. To ablate core-guided pruning (Algorithm 3), when closing node n, we ignore the derived core and instead use n’s full cube (path from root to n) as its core. This prunes only n and its subtree, similar to SMTS and A RI PARTI. This ablation also renders the core minimizer thread obsolete, so we disable it. We then compare our full system with the ablated configuration (Figure 5). Enabling core-guided pruning
solves 6 more benchmarks (5 of which are UNSAT) for an overall PAR-2 ratio reduction of 5%. Like the core minimization ablation, the SAT PAR-2 reduction (7%) slightly exceeds the UNSAT reduction (4%) since many SAT benchmarks solved by both configurations run faster with pruning enabled, while most unique UNSAT solves occur near the timeout boundary. Nevertheless, 80% of the additional solved benchmarks are UNSAT, which strongly supports the hypothesis that coreguided pruning particularly benefits UNSAT problems by dynamically shrinking the search space. VI. C ONCLUSION We introduced a novel framework for parallel SMT solving that integrates dynamic VSIDS-based partitioning, core-guided search-space pruning, and online backbone detection for a feedback-driven architecture that uses the evolving search state to steer solving. We showed that our system achieves the strongest overall performance across six challenging SMTCOMP 2025 benchmark suites against four state-of-the-art parallel SMT frameworks, and scales effectively with computational resources. Future work will continue to integrate feedback from search, such as online parameter tuning and improved heuristics for split atom and backbone candidate selection. We also intend to incorporate non-unit clause sharing, particularly subtree-guarded approaches that exploit search-space locality.
R EFERENCES [1] L. M. de Moura and N. S. Bjørner, “Z3: an efficient SMT solver,” in Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, ser. Lecture Notes in Computer Science, C. R. Ramakrishnan and J. Rehof, Eds. Springer, 2008, pp. 337–340. [Online]. Available: https://doi.org/10.1007/978-3-540-78800-3 24 [2] H. Barbosa, C. Barrett, M. Brain, G. Kremer, H. Lachnitt, M. Mann, A. Mohamed, M. Mohamed, A. Niemetz, A. Nötzli, A. Ozdemir, M. Preiner, A. Reynolds, Y. Sheng, C. Tinelli, and Y. Zohar, “cvc5: A versatile and industrialstrength smt solver,” in Tools and Algorithms for the Construction and Analysis of Systems, D. Fisman and G. Rosu, Eds. Cham: Springer International Publishing, 2022, pp. 415–442. [3] A. E. J. Hyvärinen, M. Marescotti, L. Alt, and N. Sharygina, “Opensmt2: An SMT solver for multi-core and cloud computing,” in Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, ser. Lecture Notes in Computer Science, N. Creignou and D. L. Berre, Eds. Springer, 2016, pp. 547–553. [Online]. Available: https://doi.org/10.1007/978-3-319-40970-2 35 [4] B. Dutertre, “Yices 2.2,” in Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, ser. Lecture Notes in Computer Science, A. Biere and R. Bloem, Eds. Springer, 2014, pp. 737–744. [Online]. Available: https://doi.org/10.1007/978-3-319-08867-9 49 [5] L. C. Cordeiro and B. Fischer, “Verifying multi-threaded software using smt-based context-bounded model checking,” in Proceedings of the 33rd International Conference on Software Engineering, ICSE 2011, Waikiki, Honolulu , HI, USA, May 21-28, 2011, R. N. Taylor, H. C. Gall, and N. Medvidovic, Eds. ACM, 2011, pp. 331–340. [Online]. Available: https://doi.org/10.1145/1985793.1985839 [6] A. Komuravelli, A. Gurfinkel, and S. Chaki, “Smt-based model checking for recursive programs,” in Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, ser. Lecture Notes in Computer Science, A. Biere and R. Bloem, Eds. Springer, 2014, pp. 17–34. [Online]. Available: https://doi.org/10.1007/978-3-319-08867-9 2 [7] C. Skalka and J. P. Near, “Smt-boosted security types for low-level MPC,” in Programming Languages and Systems - 34th European Symposium on Programming, ESOP 2025, Held as Part of the International Joint Conferences
on Theory and Practice of Software, ETAPS 2025, Hamilton, ON, Canada, May 3-8, 2025, Proceedings, Part II, ser. Lecture Notes in Computer Science, V. Vafeiadis, Ed. Springer, 2025, pp. 258–285. [Online]. Available: https://doi.org/10.1007/978-3-031-91121-7 11 [8] P. Hozzová and N. Bjørner, “Synthesiz3 this: an smt-based approach for synthesis with uncomputable symbols,” in Proceedings of the 25th Conference on Formal Methods in Computer-Aided Design, FMCAD 2025, Menlo Park, CA, USA, October 6-10, 2025, A. Irfan and D. Kaufmann, Eds. TU Wien Academic Press, 2025. [Online]. Available: https://doi.org/10.34727/ 2025/isbn.978-3-85448-084-6 28 [9] C. W. Barrett, P. Chen, B. Cook, B. Dutertre, R. B. Jones, N. Le, A. Reynolds, K. Sheth, C. Stephens, and M. W. Whalen, “SMT-D: new strategies for portfolio-based SMT solving,” in Formal Methods in Computer-Aided Design, FMCAD 2024, Prague, Czech Republic, October 15-18, 2024, N. Narodytska and P. Rümmer, Eds. IEEE, 2024, pp. 1–10. [Online]. Available: https: //doi.org/10.34727/2024/isbn.978-3-85448-065-5 10 [10] C. M. Wintersteiger, Y. Hamadi, and L. de Moura, “A concurrent portfolio approach to smt solving,” in Computer Aided Verification, A. Bouajjani and O. Maler, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2009, pp. 715–720. [11] A. E. J. Hyvärinen and C. M. Wintersteiger, Parallel Satisfiability Modulo Theories. Cham: Springer International Publishing, 2018, pp. 141–178. [Online]. Available: https://doi.org/10.1007/978-3-319-63516-3 5 [12] A. Wilson, A. Nötzli, A. Reynolds, B. Cook, C. Tinelli, and C. W. Barrett, “Partitioning strategies for distributed SMT solving,” in Formal Methods in Computer-Aided Design, FMCAD 2023, Ames, IA, USA, October 24-27, 2023, A. Nadel and K. Y. Rozier, Eds. IEEE, 2023, pp. 199–208. [Online]. Available: https: //doi.org/10.34727/2023/isbn.978-3-85448-060-0 28 [13] T. Kolárik, A. E. J. Hyvärinen, S. Asadzadeh, and N. Sharygina, “Parallel smt solving via iterative tree partitioning,” in TACAS 2026, 2026. [14] Y. Zhou, J. Bosamiya, Y. Takashima, J. Li, M. Heule, and B. Parno, “Mariposa: Measuring SMT instability in automated program verification,” in Formal Methods in Computer-Aided Design, FMCAD 2023, Ames, IA, USA, October 24-27, 2023, A. Nadel and K. Y. Rozier, Eds. IEEE, 2023, pp. 178–188. [Online]. Available: https: //doi.org/10.34727/2023/isbn.978-3-85448-060-0 26 [15] A. E. J. Hyvärinen, M. Marescotti, and N. Sharygina, “Lookahead in partitioning SMT,” in Formal Methods in Computer Aided Design, FMCAD 2021, New Haven, CT, USA, October 19-22, 2021. IEEE, 2021, pp. 271–279. [Online]. Available: https://doi.org/10.34727/2021/isbn. 978-3-85448-046-4 37 [16] M. Zhao, S. Cai, and Y. Qian, “Distributed smt solving based on dynamic variable-level partitioning,” in Computer Aided Verification, A. Gurfinkel and V. Ganesh, Eds.
Cham: Springer Nature Switzerland, 2024, pp. 68–88. [17] A. E. J. Hyvärinen, M. Marescotti, and N. Sharygina, “Search-space partitioning for parallelizing SMT solvers,” in Theory and Applications of Satisfiability Testing SAT 2015 - 18th International Conference, Austin, TX, USA, September 24-27, 2015, Proceedings, ser. Lecture Notes in Computer Science, M. Heule and S. A. Weaver, Eds. Springer, 2015, pp. 369–386. [Online]. Available: https://doi.org/10.1007/978-3-319-24318-4 27 [18] C. Barrett, R. Sebastiani, S. A. Seshia, and C. Tinelli, “Satisfiability modulo theories,” in Handbook of Satisfiability, 2nd ed., ser. Frontiers in Artificial Intelligence and Applications, A. Biere, M. J. H. Heule, H. van Maaren, and T. Walsh, Eds. IOS Press, Feb. 2021, vol. 336, ch. 33, pp. 825–885. [19] R. Nieuwenhuis, A. Oliveras, and C. Tinelli, “Solving SAT and SAT modulo theories: From an abstract davis–putnam–logemann–loveland procedure to dpll(T),” J. ACM, vol. 53, no. 6, pp. 937–977, 2006. [Online]. Available: https://doi.org/10.1145/1217856.1217859 [20] J. P. M. Silva and K. A. Sakallah, “GRASP: A search algorithm for propositional satisfiability,” IEEE Trans. Computers, vol. 48, no. 5, pp. 506–521, 1999. [Online]. Available: https://doi.org/10.1109/12.769433 [21] T. Balyo, P. Sanders, and C. Sinz, “Hordesat: A massively parallel portfolio SAT solver,” in Theory and Applications of Satisfiability Testing - SAT 2015 - 18th International Conference, Austin, TX, USA, September 24-27, 2015, Proceedings, ser. Lecture Notes in Computer Science, M. Heule and S. A. Weaver, Eds. Springer, 2015, pp. 156–172. [Online]. Available: https://doi.org/10.1007/978-3-319-24318-4 12 [22] M. Marescotti, A. E. J. Hyvärinen, and N. Sharygina, “Clause sharing and partitioning for cloud-based SMT solving,” in Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings, ser. Lecture Notes in Computer Science, C. Artho, A. Legay, and D. Peled, Eds., 2016, pp. 428–443. [Online]. Available: https://doi.org/10.1007/978-3-319-46520-3 27 [23] M. Marescotti, A. E. J. Hyvärinen, and N. Sharygina, “SMTS: distributed, visualized constraint solving,” in LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Awassa, Ethiopia, 16-21 November 2018, 2018. [24] A. E. J. Hyvärinen, T. A. Junttila, and I. Niemelä, “Partitioning search spaces of a randomized search,” Fundam. Informaticae, vol. 107, no. 2-3, pp. 289– 311, 2011. [Online]. Available: https://doi.org/10.3233/ FI-2011-404 [25] T. Weber, “Par4,” Uppsala University, Tech. Rep., 2019. [Online]. Available: http://smt2019.galois.com/papers/ tool paper 9.pdf [26] A. E. J. Hyvärinen, T. A. Junttila, and I. Niemelä, “A distribution method for solving SAT in grids,” in Theory and Applications of Satisfiability Testing - SAT
2006, 9th International Conference, Seattle, WA, USA, August 12-15, 2006, Proceedings, ser. Lecture Notes in Computer Science, A. Biere and C. P. Gomes, Eds. Springer, 2006, pp. 430–435. [Online]. Available: https://doi.org/10.1007/11814948 39 [27] Z. Battleman, J. E. Reeves, and M. J. H. Heule, “Problem partitioning via proof prefixes,” in 28th International Conference on Theory and Applications of Satisfiability Testing, SAT 2025, Glasgow, Scotland, August 12-15, 2025, ser. LIPIcs, J. Berg and J. Nordström, Eds. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025, pp. 3:1–3:18. [Online]. Available: https://doi.org/10.4230/ LIPIcs.SAT.2025.3 [28] D. Schreiber, A. Niemetz, and M. Preiner, “Massively parallel bit-precise verification with bitwuzla and mallob,” in Tools and Algorithms for the Construction and Analysis of Systems, S. Junges and G. Katz, Eds. Cham: Springer Nature Switzerland, 2026, pp. 170–191. [29] C. Reisenberger, “PBoolector: A Parallel SMT Solver for QF BV by Combining Bit-Blasting with LookAhead,” Master’s thesis, Johannes Kepler University Linz, 2014. [Online]. Available: https://fmv.jku.at/master/ Reisenberger-MasterThesis-2014.pdf [30] O. Guthmann, O. Strichman, and A. Trostanetski, “Minimal unsatisfiable core extraction for SMT,” in 2016 Formal Methods in Computer-Aided Design, FMCAD 2016, Mountain View, CA, USA, October 3-6, 2016, R. Piskac and M. Talupur, Eds. IEEE, 2016, pp. 57– 64. [Online]. Available: https://doi.org/10.1109/FMCAD. 2016.7886661 [31] M. Janota, I. Lynce, and J. Marques-Silva, “Algorithms for computing backbones of propositional formulae,” AI Commun., vol. 28, no. 2, pp. 161–177, 2015. [Online]. Available: https://doi.org/10.3233/AIC-140640 [32] J. W. Freeman, “Improvements to propositional satisfiability search algorithms,” Ph.D. dissertation, University of Pennsylvania, 1995. [33] M. Jonáš, F. Bobot, D. Déharbe, and D. Winterer, “SMT-COMP 2025,” 2025, chair: Martin Jonáš, Masaryk University, Czechia. [34] N. Froleyks, M. Heule, A. Iser, M. Järvisalo, and M. Suda, “SAT competition 2020,” Artif. Intell., vol. 301, p. 103572, 2021. [Online]. Available: https://doi.org/10.1016/j.artint.2021.103572 [35] C. Barrett, P. Fontaine, and C. Tinelli, “The smt-lib standard: Version 2.6,” Department of Computer Science, The University of Iowa, Tech. Rep., 2017. [Online]. Available: https://smt-lib.org [36] M. Preiner, H. Schurr, C. W. Barrett, P. Fontaine, A. Niemetz, and C. Tinelli, “SMT-LIB release 2025 (non-incremental benchmarks) (version 2025.08.04),” https://doi.org/10.5281/zenodo.16740866, Aug. 2025, accessed on YYYY-MM-DD. [Online]. Available: https://doi.org/10.5281/zenodo.16740866 [37] ——, “SMT-LIB release 2024 (non-incremental benchmarks),” https://doi.org/10.5281/zenodo.11061097,
Apr. 2024, accessed on YYYY-MM-DD. [Online]. Available: https://doi.org/10.5281/zenodo.11061097 A PPENDIX Our SMTS setup uses the iterative tree partitioning algorithm from [13] using O PEN SMT as the base solver with T = 8 parallel solver instances, and with partitioning and lemma sharing both enabled. The solver timeout TS starts at 32 seconds and doubles whenever the elapsed time reaches 4 · TS . Our A RI PARTI setup runs the dynamic variable-level partitioning framework from [16] using Z 3 (v4.12.1) as the backend solver, with a maximum of T = 8 concurrent worker tasks. Our SMT- D (CVC 5 portfolio mode) setup uses the worker diversity strategy from [9] using a portfolio of T = 8 independent CVC 5 instances. Clause sharing (which requires the full SMT- D gRPC broker) is omitted. Worker diversity follows the guided randomization strategy of [9]: workers are divided into a standard cluster (75%, ⌊ 3T using default randomness, 4 ⌋ ⌊︁workers) ⌋︁ and a noisy cluster (25%, T4 workers) using high randomness to explore parts of the search space that standard workers ignore. Standard workers are populated by cycling through logicspecific base option sets (Table II of [9]) in three passes: (1) base options as-is, (2) base options with flipped decision heuristic (--decision=justification if the logic default is internal, else --decision=internal), and (3) base options with --decision=internal and distinct random seeds. Noisy workers use the same logic-specific base options with --decision=internal, --random-freq=0.75, and distinct random seeds. For logics not covered by Table II (nonlinear arithmetic), our setup falls back to CVC 5 defaults with --decision=internal. Our CVC 5- P (partition mode) setup uses the graduated portfolio approach from [12]. Given T = 8 threads, we use a ranked list of partitioning strategies (default: decision-scatter, decision-cube, following the recommended m = 2 portfolio of [12]) to construct a graduated portfolio: partition batches are allocated greedily in order of increasing size (2, 4, 8, . . .), cycling through the strategy ranking at each size level until we have T partitions. For each batch, CVC 5 is invoked sequentially with delays of t1 = 3s and t2 = 0.1s (following [12]) to generate the partitions. Generated partitions across all batches are then solved concurrently using T CVC 5 solver instances (multijob scheduling).