Strategy Scheduling
Strategy scheduling runs multiple Prover9 search strategies concurrently using a sliding-window scheduler and takes the first proof found. Each strategy uses different search parameters drawn from a machine-learned portfolio of 96 strategies.
The scheduler is designed for TPTP competition use. It is enabled by -cores N or -comp N and is completely inert in LADR mode.
Command-Line Flags
-cores <N>
Enable the sliding-window scheduler with N concurrent children (1 to 64). Each child runs a different strategy from the ML portfolio. Auto-enables TPTP mode features (SInE, multi-ordering trial, fast predicate elimination).
prover9 -cores 4 -t 300 -f problem.p
-comp <N>
Competition mode. Shorthand for -cores <cpus> -fastPE -t N. Uses all available CPUs and sets a time limit of N seconds.
prover9 -comp 60 problem.p
-strategy <N>
Force a single strategy index N from the ML portfolio (0 to 95). Runs a deterministic single-core search with that strategy's parameters. No forking, no scheduling. Overrides -cores.
prover9 -strategy 5 -t 60 -f problem.p
-strategies <N>
Override Phase 1 breadth cap. Limits how many strategies are tried in Phase 1 of the sliding-window scheduler. Clamped to [1, 96]. See Two-Phase Scheduling.
ML Strategy Portfolio
The portfolio contains 96 strategies: 95 specialist strategies trained on problems that auto_default fails on, plus auto_default itself (the standard Prover9 automatic mode with no parameter overrides).
Each specialist strategy specifies values for up to 27 search parameters:
| Category | Parameters |
|---|---|
| Term ordering | LPO, RPO, KBO |
| Given-clause selection | age_part, weight_part |
| Weight limits | max_weight |
| SInE | tolerance, depth, max_axioms, weight |
| Demodulation | back_demod, factor, unit_deletion |
| Inference rules | binary_resolution, hyper_resolution, ur_resolution, paramodulation |
| Resolution modes | ordered_res, ordered_para, para_units_only |
| Preprocessing | multi_order_trial, process_initial_sos |
| Subsumption/search | back_subsume, lightest_first, breadth_first, safe_unit_conflict |
| Penalty functions | literal_selection, nest_penalty, depth_penalty |
A parameter value of -1 means "keep Prover9's default." auto_default has all parameters set to -1.
The portfolio was generated by greedy set cover over a 1000-strategy grid evaluated on hard TPTP problems.
Decision Tree Classifier
A decision tree classifies each input problem into a leaf node based on syntactic features (symbol counts, clause counts, formula structure). Each leaf node has a ranking of all 96 strategies, ordered by how often each strategy solved problems at that leaf during training.
The classifier runs in microseconds and adds no measurable overhead. When -cores N is used, the per-leaf ranking determines which strategies to try and in what order.
Two-Phase Scheduling
Phase 1: Breadth
Try as many different strategies as possible. Each child gets a fixed time slice, and when it expires, the child is suspended and a new strategy is spawned.
- Roughly half the total time budget is allocated to breadth.
- Per-child slice: at least 8 seconds.
- The -strategies flag overrides the automatic breadth cap.
Phase 1 ends when all selected strategies have been started.
Phase 2: Depth
Resume the most promising suspended children using priority scores. Children that made the most progress in Phase 1 are resumed first.
Priority scoring:
- Children still in preprocessing (stuck in predicate elimination or clausification): score 0 (low priority).
- Children that reached the main search loop: score based on given clauses processed and progress since last suspend.
- auto_default (slot 0): bonus +10000 when searching — always resumed first.
Phase 2 continues until the time limit expires, cycling through suspended children in priority order.
auto_default (Slot 0)
auto_default always occupies slot 0 and receives special treatment:
- It is the first strategy started.
- It is never suspended. While other children cycle through sleep/wake, auto_default runs continuously on its dedicated core.
- It uses Prover9's standard automatic mode with no parameter overrides, which is the strongest single strategy.
Two Fork Modes
The scheduler uses two different fork points depending on the number of axioms in the input.
Fork-Before-SInE (>5000 axioms)
For problems with more than 5000 axioms, the scheduler forks before SInE premise selection and clausification. Each child gets its own SInE parameters and independently selects a different subset of axioms.
This provides diversity at both the premise selection level and the search strategy level.
Fork-After-Clausification (≤5000 axioms)
For problems with 5000 or fewer axioms, the scheduler forks after full preprocessing (SInE, parsing, clausification). All children share the same clause set and differ only in search parameters.
This avoids redundant preprocessing, which is expensive for FOF problems.
Shared-Memory Progress
Children communicate their progress to the parent via shared memory. Each child writes to a dedicated slot containing:
- stage — current processing phase (init through done)
- given — total given clauses processed
- kept — total kept clauses
- sos_size — current SOS list size
- usable_size — current usable list size
- megs_used — current memory consumption
The parent reads these slots to make Phase 2 priority decisions and to detect children that are stuck or consuming too much memory.
Memory Ejection
When max_megs is set to 8192 or less (competition mode), the parent enforces a per-child memory budget:
budget = max_megs / max(num_strats, N)
Children whose memory usage exceeds the budget are killed to prevent a single child from consuming all available memory.
Winner Selection
The first child to exit with a proof-found status (exit code 0) is declared the winner.
- All other children are woken (SIGCONT) then killed (SIGTERM).
- The winner's proof output is printed to stdout.
- The parent exits with the winner's exit code.
If no child finds a proof, the parent reports the best exit status: GaveUp, Timeout, or MemoryOut.
Examples
Example 1: 4-core scheduling, 5-minute timeout
prover9 -cores 4 -t 300 -f problem.p
Four concurrent children, sliding window over 96 strategies. Phase 1 tries as many strategies as fit in ~150 seconds, then Phase 2 resumes the most promising.
Example 2: Competition mode, 60 seconds
prover9 -comp 60 problem.p
Uses all available CPUs, fast predicate elimination, 60-second time limit.
Example 3: Force a specific strategy
prover9 -strategy 5 -t 60 -f problem.p
Runs strategy index 5 as a single-core deterministic search. No forking.
Example 4: Override Phase 1 breadth
prover9 -cores 4 -strategies 20 -t 300 -f problem.p
Limits Phase 1 to 20 strategies instead of the automatic cap.
Example 5: Single search (no scheduling)
prover9 -t 60 -f problem.p
Without -cores or -comp, TPTP mode runs a single deterministic search with auto_default parameters.
Notes
- CPU usage
- With -cores N, N child processes run concurrently. On a machine with N+ cores, each child gets a full core. On machines with fewer cores, children share CPU time but still get the full wall-clock budget.
- Memory usage
- Each child gets its own memory space. The max_megs limit applies per child. For large inputs, N children each using 1–2 GB means N × 1–2 GB total.
- Interaction with user options
- User-specified options (via magic comments or command-line) are applied before strategy overrides. Strategy children then modify specific parameters. User settings for parameters not touched by the strategy are preserved.
- Checkpointing
- Checkpointing is automatically disabled in strategy children to avoid checkpoint file collisions.
- LADR mode
- The -cores and -comp flags are only meaningful with TPTP input. LADR-mode searches are completely unaffected.