Three-machine scheduling model and solver assurance

Edition: 9 October 2026 Australia/Brisbane. Decision: Prototype a bounded assurance adapter; defer a direct production scheduler or source-algorithm speedup. Buyer demand and profitability remain hypotheses.

Research finding

Family 124 claims a uniform deterministic fixed finite machine that finds the minimum makespan and exactly decides a deadline for explicitly listed nonempty unit-job DAGs on exactly three identical parallel machines. Jobs are nonpreemptive, with no release dates, communication delays, eligibility restrictions or additional resources. Its binary-input runtime is O((L+2)^150020), with no practical running-time claim.

The new source reading covers the seven principal TeX argument files, including the full 541-line driver, bounded global predicates, separator/list/boundary invariants and complexity accounting. The finite family permits up to 10,000 leaves and O(N^(3K)) formula instances before deduplication. The structural claim uses fewer than 500 leaves, five upset-list entries and fewer than 40 leaves per entry; this establishes a complexity argument, not a measured compact production backend. The selected Comparator states existence of one fixed finite machine and positive constant C; the 90-line solution entry point and its immediate statement were read, but imported proofs, compilation and executable extraction remain unverified.

Problem and buyer

A scheduling researcher or engineering team may need to distinguish a valid schedule, an optimality claim, an exact deadline answer and a theorem guarantee for a particular model. A three-station unit-time workflow fits only when stations are interchangeable and all real constraints match the stated model. Unequal jobs, setups, machine availability and eligibility are common reasons the source result cannot be applied directly.

The candidate recurring task is review of proposed schedules and unsupported guarantees around an existing solver. There is no evidence yet that this bounded adapter catches important operational mistakes often enough to support a paid product.

What the finding could enable

An assurance module can require an explicit model, independently check each supplied schedule, provide elementary capacity/critical-path bounds, compute exact tiny optima and document the gap between source theorem and implementation. The structural proof suggests a research direction for compressing inherited interval descriptions, but a general-purpose bounded-state framework does not follow from this three-machine argument.

three_machine_reference.py uses conventional breadth-first search over completed-job ideals. It is exponential and bounded, not the source polynomial algorithm. solve_and_audit_three_machine.py proposes schedules with existing CP-SAT and checks them separately. A checked schedule attaining an elementary lower bound is a finite optimality witness; otherwise the exact search must complete before independent optimality is asserted.

Technical and commercial limits

The references cap 18 jobs, 50,000 ideal states and two million transitions. The proposer uses one worker, seed 124 and a default two-second limit, capped at ten seconds. The strict model rejects missing fields and extra features. On search exhaustion, exact optimum and optimal slots remain unknown. An independently checked witness can still prove a deadline feasible, or an elementary lower bound can prove it impossible; solver status alone does not fill an unresolved independent result.

Splitting a longer job into unit vertices can permit interleaving or preemption; it needs a separate model bridge. Restricting the leaf allowance or pruning the source enumeration would need a completeness argument. No production latency, source-machine extraction, certified CP-SAT proof log, scalability or practical theorem-derived advantage is established.

Minimal architecture

Explicit source-model declarations and stable job IDs -> DAG/encoding validation -> existing solver proposal -> direct slot capacity and strict precedence audit -> elementary lower/checked upper bound -> bounded exact ideal search when necessary -> distinct feasible/optimal/deadline/unknown evidence -> versioned source/implementation report. Retain original candidate audit separately from any new solver proposal.

Existing alternatives and differentiation

OR-Tools already provides CP-SAT interval, cumulative-resource and scheduling modeling. The implemented baseline uses one-unit intervals, cumulative capacity three, precedence inequalities and a makespan objective. It is the same narrow mathematical model, rather than silently importing the broader public job-shop example. Primary scheduling recipes, existing job-shop model.

Live OR-Tools 9.15.6755 reaches independently checked optima on all eight generated controls. Therefore no solver-quality advantage is demonstrated. Potential differentiation is explicit model correspondence and reproducible evidence within the shared assurance workflow; if existing practice already supplies this adequately, reject the module.

Monetization hypothesis

Hypothesis: AUD 5,000 for a tightly scoped model/solver assessment as one module of the evidence platform. At 20 assumed specialist hours at AUD 180/hour, AUD 1,400 remains before sales, support and overhead; 30 hours cost AUD 5,400 and exceed the fee. No quote, customer, revenue or verified delivery cost exists. Do not count the adapter as an additional independent customer or assume a subscription from a complexity result.

Validation experiment

3,346 controls compare all 1,099 topologically ordered DAG edge sets through five jobs with a separate per-job slot-assignment oracle; they check witnesses, bounds, invalid models and budget states. Every finite DAG admits a topological numbering, but testing these sizes establishes no unrestricted implementation theorem.

The generated nine-job control has a four-slot longest-tail priority schedule and exact optimum three. The six-job bottleneck has capacity/critical-path lower bound two but exact optimum three. These distinguish heuristic output and elementary bounds from completed exact evidence.

40 live baseline controls compare CP-SAT against finite optima on eight self-authored models. In the 18 independent-job case CP-SAT reports FEASIBLE at its two-second limit, while the checked six-slot witness attains the capacity lower bound and independently proves optimality. A deliberately exhausted independent reference leaves its optimum unknown even when CP-SAT reports OPTIMAL on a different case. Saved runtime and results. Timings are single-run diagnostics, not a performance study or customer benchmark.

Conditions to reject or defer

Defer the full source backend without a practical extracted implementation, reviewed constants and useful benchmarks. Reject generalized scheduling guarantees from this result, source proof badges for the reference/CP-SAT wrapper and a production speedup from polynomial classification. Reject the commercial module if model preparation/support cost exceeds its value or the existing solver/review workflow suffices.

Next concrete action

Use the two saved controls to review whether a real recurring unit-job workflow needs independent schedule/model evidence. Measure preparation, material mistakes caught and correction effort before proposing a fee. Inspect extracted source-machine construction and bounded-descriptor pruning only as separate research tasks, with explicit proof and performance obligations. Current documentary contract, self-authored gap report.

Pinned source evidence

Source revision fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb. Paper driver and exact model, selected scope, Comparator statement, solution entry point. Main argument text was read; figures/bibliography, imported formal proofs and independent acceptance were not completed. Exact ledger.