z3/comparison-report.md

Comparison Report: Case Splits in smt_parallel.cpp vs. AriParti

Overview

This report compares how Z3's src/smt/smt_parallel.cpp and AriParti (src/partitioner/src/math/subpaving/subpaving_t_def.h + orchestrated by src/AriParti.py) perform case splits in parallel arithmetic SMT solving.

---

Architecture

Aspect	Z3 smt_parallel.cpp	AriParti
Parallelism model	Shared-memory multi-threaded (C++ threads, one smt::context per worker)	Process-based distributed (partitioner process + N solver sub-processes, IPC via named pipes)
Where splits happen	Inside each SMT worker thread, using the live SMT context state	In a standalone subpaving partitioner process, before handing off to external solvers
Split representation	expr_ref atom (e.g., x ≤ mid) passed to batch_manager, which builds a search tree	Bound pair (x ≤ mid / x > mid) installed on two child nodes in the subpaving tree
Sub-problem dispatch	Workers pull cubes from a shared search_tree via batch_manager::get_cube()	Child nodes are serialised to .smt2 files and dispatched to external solver processes

---

Case Split Flow

Z3 (smt_parallel.cpp)

worker::run()
  → check_cube()     [run SMT check with current cube]
  → l_undef result
  → get_split_atom()
      1. get_arith_split_atom()   ← AriParti-style arithmetic split
      2. VSIDS Boolean fallback   ← if no arithmetic atom found
  → batch_manager::split()        ← insert atom into search tree (binary split)
  → simplify()                    ← optional inprocessing

AriParti (subpaving_t_def.h / AriParti.py)

context_t::operator()()           ← main partitioner loop
  → create_new_task()             ← if a leaf is ready, emit it as an .smt2 task
  → select_split_node()           ← pick highest-priority leaf from heap
  → split_node(n)
      → select_best_var(n)        ← multi-key heuristic
      → compute midpoint
      → mk_node(left), mk_node(right)
      → propagate(left/right)     ← BICP immediately
      → emit "unsat-task" or "new-task" messages to master

---

Variable Selection Heuristic

Z3 get_arith_split_atom()

Iterates over all 0-arity arithmetic enodes visible in the current SMT context. For each variable it records:

• occ: count of arithmetic-comparison parent enodes (≤, ≥, <, >, =)
• has_lo, has_up, lo, up: current theory bounds from arith_value

Ranking (highest priority first):

1. Higher occurrence count – more active in constraint network
2. Fully bounded preferred over half-bounded or unbounded
3. Wider interval (for fully-bounded variables)
4. Interval contains zero – as tiebreaker

Variables whose interval is already a point (lo == up) are skipped.

AriParti select_best_var()

Uses a var_info struct with five keys and a dynamic key ordering (key_rank) that rotates per node to break ties diversely:

Key index	Criterion	Better is…
0	m_split_cnt – global split count	Lower (less-split variables preferred)
1	m_cz – interval contains zero	true preferred
2	m_deg – max polynomial degree	Higher preferred (prioritises nonlinear vars)
3	m_occ – occurrence in undecided clauses	Higher preferred
4	m_width – interval width (with penalties for unbounded)	Wider preferred

Key ordering for a child node is derived from its parent's key_rank by rotating one position whenever the parent's ranking had consecutive equal keys; this diversifies splits across the tree.

Variables that are fully determined (lower == upper), Boolean (m_is_bool), or defined (m_defs[x] != nullptr) are excluded.

Unbounded width penalties (AriParti only):

• Fully unbounded: width = 1024²
• Half-bounded ((-∞, u]): width = 1024 + u (if u ≥ 0), or width = 1024 / max(1, -u) (if u < 0)
• Half-bounded ([l, ∞)): symmetric formula

---

Midpoint Computation

Both implementations agree on the core zero-split heuristic (AriParti Section 4.2): if the interval straddles zero, split at 0.

Case	Z3 get_arith_split_atom()	AriParti split_node()
Interval contains 0	mid = 0	mid = 0
Fully bounded [lo, up]	mid = (lo + up) / 2; floor(mid) for integers	mid = (lo + up) / 2; ceiling applied if width > 10
Half-bounded [lo, ∞)	mid = lo (split at lower bound)	mid = lo + delta (delta = 128)
Half-bounded (-∞, up]	mid = up - 1 (int) or up - 0.5 (real)	mid = floor(up) - delta
Fully unbounded	mid = 0	mid = 0 (via m_cz = true)

The split produces two branches: x ≤ mid and x > mid in both cases.

---

Node / Leaf Selection

Z3

Workers call batch_manager::get_cube(), which calls search_tree::activate_node() and find_active_node(). The search tree uses a simple work-stealing model: each worker tries to continue the node it last worked on; if unavailable, it picks any open node. There is no explicit priority between open nodes.

AriParti

Uses a priority heap (m_leaf_heap, ordered by node_info::operator<):

1. Lowest depth first – broader, shallower problems are split first
2. Most undecided clauses – more constrained nodes processed first
3. Most undecided literals
4. Lowest node ID (earlier-created nodes preferred as tiebreaker)

This gives AriParti more control over the shape of the partitioning tree.

---

Post-Split Processing

Aspect	Z3	AriParti
Bound propagation after split	None immediately; full SMT check on next check_cube()	Immediate BICP (propagate()) on both children; inconsistent children are pruned at once
Inprocessing simplification	Optional simplify() after split (configurable, one-shot)	None; each sub-task is a fresh SMT instance
Learned clause sharing	Yes: units and clauses shared via batch_manager::collect_clause()	None: each solver instance is independent
Backtracking	batch_manager::backtrack() annotates nodes in search tree with unsat-cores	Master (AriParti.py) propagates unsat upward and downward via push_up / push_down

---

Boolean Variables

• Z3: When get_arith_split_atom() finds no arithmetic variable, it falls back to a VSIDS-style Boolean heuristic: selects the unassigned Boolean variable with the highest product of positive/negative literal activity scores (m_lit_scores[0][v] * m_lit_scores[1][v]), then halves both scores.
• AriParti: select_best_var() explicitly skips Boolean variables (if (m_is_bool[x]) continue). Boolean case splits are not performed by the partitioner; they occur only inside each external solver instance.

---

Shared Origins and Similarities

Both implementations are directly inspired by the AriParti paper (Section 4.2):

1. Zero-split heuristic: both preferentially split at 0 when the interval straddles zero.
2. Midpoint bisection: both use (lo + up) / 2 for fully-bounded intervals.
3. Occurrence count: both use the number of arithmetic constraints that mention a variable as a key factor.
4. Interval width: both prefer variables with wider intervals as a heuristic for "less constrained" variables.
5. Binary tree structure: both build a binary case-split tree where each split adds exactly two child nodes.
6. Arithmetic-only primary heuristic: both focus exclusively on arithmetic (Int/Real) variables for the primary split decision.

The Z3 implementation (get_arith_split_atom()) was explicitly added to smt_parallel.cpp as an "AriParti-style arithmetic interval split" (see comment at line 543–549), making it a direct re-implementation of the core idea from the AriParti paper within Z3's parallel SMT framework.

---

Key Differences Summary

Dimension	Z3 smt_parallel.cpp	AriParti
Architecture	Shared-memory threads inside Z3	Distributed processes with IPC
Variable selection keys	3 (occ, width, cz)	5 (split_cnt, cz, deg, occ, width) with dynamic ordering
Split-count tracking	Not tracked	Tracked globally; fewer-split vars preferred
Polynomial degree	Not considered	Considered (key 2: higher degree preferred)
Boolean fallback	VSIDS-style score-based	None (Boolean vars skipped entirely)
Unbounded width	Sentinel −1; fully-bounded strictly preferred	Penalty values (1024, 1024²) enable ranking across all cases
Split delta (semi-unbounded)	1 (int) / 0.5 (real)	128 (fixed m_split_delta)
Node priority	Work-stealing, no explicit ordering	Priority heap (depth, undecided clauses, undecided literals)
Post-split propagation	None until full SMT check	Immediate BICP; infeasible children pruned instantly
Clause learning across workers	Yes (shared via batch_manager)	No (each solver is isolated)
Inprocessing	Optional (m_inprocessing flag)	None (whole new sub-task per child)
SLS portfolio	Yes (optional parallel SLS worker)	No

---

Source Locations

Component	File
Z3 arithmetic split	src/smt/smt_parallel.cpp, worker::get_arith_split_atom() (lines 414–534)
Z3 Boolean split fallback	src/smt/smt_parallel.cpp, worker::get_split_atom() (lines 537–570)
Z3 search tree split	src/smt/smt_parallel.cpp, batch_manager::split() (lines 342–358)
AriParti variable selection	src/partitioner/src/math/subpaving/subpaving_t_def.h, select_best_var() (lines 2354–2421)
AriParti var_info ranking	src/partitioner/src/math/subpaving/subpaving_t.h, struct var_info, operator< (lines 453–519)
AriParti split_node	src/partitioner/src/math/subpaving/subpaving_t_def.h, split_node() (lines 2516–2610)
AriParti node priority	src/partitioner/src/math/subpaving/subpaving_t.h, struct node_info, operator< (lines 430–451)
AriParti master orchestration	src/AriParti.py, ArithPartition::solve() and push_up() / push_down()