# Three machines and five jobs

KL-FCS-025 · Scheduling · version 1.0.0

## Problem

Minimize makespan for independent jobs on identical machines.

## Context

Attach feasibility and optimality to an explicit scheduling model, including resource assumptions and the objective.

## Definitions

- **Makespan**: The completion time of the last job.
- **Non-preemptive job**: A job runs continuously once it starts.
- **Identical machine model**: Every machine has the same processing rate, and independent jobs are available at time zero.

## Checked result

Minimum makespan: 4.

The witness lists one machine per job. Feasibility follows from sequential execution on each machine, and enumeration establishes the minimum load ceiling.

## Checker reasoning

1. Enumerate every job-to-machine assignment.
2. Sum the durations assigned to each machine.
3. Evaluate makespan as the maximum load.
4. Check that the witness achieves the minimum across all assignments.

## Dataset construction

{
  "family": "scheduling",
  "task": "Minimize makespan for independent jobs on identical machines.",
  "input_encoding": "Structured JSON; field meanings are stated in the specification.",
  "coverage": "Complete assignment space · 243 schedules",
  "acceptance": [
    "Enumerate every job-to-machine assignment.",
    "Sum the durations assigned to each machine.",
    "Evaluate makespan as the maximum load.",
    "Check that the witness achieves the minimum across all assignments."
  ],
  "generation": "Deterministic finite fixture; full enumeration or witness replay as stated.",
  "split_policy": "Reference corpus for exposition and reproduction; no train/test evaluation split is claimed."
}

## Formal payload

```json
{
  "specification": {
    "durations": [
      4,
      3,
      2,
      2,
      1
    ],
    "machines": 3,
    "constraints": "Non-preemptive; all available at time zero; no precedence or setup times."
  },
  "claim": {
    "minimum_makespan": 4
  },
  "witness": {
    "assignment": [
      0,
      1,
      2,
      2,
      1
    ]
  }
}
```

## Complexity

m machines and n jobs produce mⁿ assignments. In this model, job order within a machine does not change the load.

## Limits

The model excludes release delays, precedence, heterogeneous machines, and setup costs.

## Common error and further work

A balanced-looking schedule need not be optimal; release dates and precedence change the problem.

Add precedence-constrained schedules and dual or lower-bound certificates.

## Verification

Complete assignment space · 243 schedules. 243 checker units.
Replay with `python3 tools/verify.py`. Mechanical status: checked; human review
has not yet been recorded. Custom Python verification, not a proof-assistant
claim. Checker 1.0.0 and exact source hashes are in `verification.json`.

## Provenance and references

Original Kenton Labs reference instance, authored with Codex assistance on 2026-10-11.
No external dataset or model-generation experiment. Reuse-license selection
remains pending.

- [Conceptual reference](https://developers.google.com/optimization/assignment/linear_assignment)