pub fn run_minion_work_steal(
num_threads: usize,
model: Model,
callback: ParallelCallback<'_>,
) -> Result<WorkStealStats, MinionError>Expand description
Run Minion with thread-based work-stealing: N workers cooperatively split the search tree. Worker 0 starts at the root; idle workers wait on a shared queue. Busy workers, on each search node, donate one stealable left-branch (encoded as a path-from-root) to the queue when other workers are idle. Idle workers fast-forward via worldPush + propagate replay and continue search from there.
Unlike run_minion_parallel (pure portfolio), this divides the
search tree across workers and so speeds up UNSAT proving roughly with
1/N. Wdeg counters drift between workers — intended as a diversity
source.
Mid-search mutation is not supported. See run_minion_parallel for
the concurrency caveat (don’t call this from multiple host threads
concurrently — the underlying alarm/ctrl-C handler state is
process-global).