Skip to main content

run_minion_work_steal

Function run_minion_work_steal 

Source
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).