Formal Computer Science / Optimization

Kenton Labs / Optimization

Scheduling

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

The vocabulary.

These definitions state the objects and properties used by the dataset. The complete instance specification remains the authority for each result.

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.

How the dataset works.

Three deterministic instances define this family. Each includes its input model, a checked result, evidence, and an acceptance procedure. Download the complete dataset JSON ↘ or the area’s readable source ↘.

Acceptance procedure

  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.

Cost and scope

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

A common failure

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

Explore the mechanics.

Change a local input or follow the steps. The stored result and its scope remain attached to the downloadable record.

Worked records.

Three instances expose concrete claims and the artifacts that establish or refute them. Expand a record for the problem, checker reasoning, formal payload, and verification metadata.

KL-FCS-010
SchedulingAn optimal two-machine scheduleComplete assignment enumeration · 8 schedules

The problem

Schedule independent, non-preemptive jobs with durations [2, 2, 1] on two identical machines, all available at time zero, to minimize makespan.

The checked result

Minimum makespan: 3.

Assign the first and third jobs to machine 0 and the second to machine 1. Loads are 3 and 2. Enumeration of every assignment establishes the optimum; job order does not affect loads in this model.

Why the checker accepts it

  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.

Formal specification

{
  "durations": [
    2,
    2,
    1
  ],
  "machines": 2,
  "constraints": "No precedence, setup time, release delay, or preemption; each machine runs its assigned jobs sequentially."
}

Claim and evidence

{
  "claim": {
    "minimum_makespan": 3
  },
  "witness": {
    "assignment": [
      0,
      1,
      0
    ]
  }
}

Dataset construction

Deterministic finite fixture; full enumeration or witness replay as stated. Structured JSON; field meanings are stated in the specification. Acceptance covers 8 checker units for this record; the unit type is stated in its verification scope.

Complexity and limits

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

Only this job set and scheduling model; additional constraints require a new specification and checker.

A boundary to investigate

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 and provenance metadata

Mechanical status: checked. Human review: not yet recorded. Checker version 1.0.0, Python 3.9.6. The report contains source hashes. The trust boundary includes Python and the custom checker implementations; no proof-assistant validation is claimed.

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

Replay from the source bundle: python3 tools/verify.py.

Readable source ↘Record JSON ↘Full area ↗Related KL-FCS-024 ↘Related KL-FCS-025 ↘
KL-FCS-024
SchedulingA perfectly balanced four-job scheduleComplete assignment space · 16 schedules

The problem

Minimize makespan for independent jobs on identical machines.

The 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.

Why the checker accepts it

  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.

Formal specification

{
  "durations": [
    3,
    2,
    2,
    1
  ],
  "machines": 2,
  "constraints": "Non-preemptive; all available at time zero; no precedence or setup times."
}

Claim and evidence

{
  "claim": {
    "minimum_makespan": 4
  },
  "witness": {
    "assignment": [
      0,
      1,
      1,
      0
    ]
  }
}

Dataset construction

Deterministic finite fixture; full enumeration or witness replay as stated. Structured JSON; field meanings are stated in the specification. Acceptance covers 16 checker units for this record; the unit type is stated in its verification scope.

Complexity and limits

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

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

A boundary to investigate

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 and provenance metadata

Mechanical status: checked. Human review: not yet recorded. Checker version 1.0.0, Python 3.9.6. The report contains source hashes. The trust boundary includes Python and the custom checker implementations; no proof-assistant validation is claimed.

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

Replay from the source bundle: python3 tools/verify.py.

Readable source ↘Record JSON ↘Full area ↗Related KL-FCS-010 ↘Related KL-FCS-025 ↘
KL-FCS-025
SchedulingThree machines and five jobsComplete assignment space · 243 schedules

The problem

Minimize makespan for independent jobs on identical machines.

The 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.

Why the checker accepts it

  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.

Formal specification

{
  "durations": [
    4,
    3,
    2,
    2,
    1
  ],
  "machines": 3,
  "constraints": "Non-preemptive; all available at time zero; no precedence or setup times."
}

Claim and evidence

{
  "claim": {
    "minimum_makespan": 4
  },
  "witness": {
    "assignment": [
      0,
      1,
      2,
      2,
      1
    ]
  }
}

Dataset construction

Deterministic finite fixture; full enumeration or witness replay as stated. Structured JSON; field meanings are stated in the specification. Acceptance covers 243 checker units for this record; the unit type is stated in its verification scope.

Complexity and limits

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

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

A boundary to investigate

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 and provenance metadata

Mechanical status: checked. Human review: not yet recorded. Checker version 1.0.0, Python 3.9.6. The report contains source hashes. The trust boundary includes Python and the custom checker implementations; no proof-assistant validation is claimed.

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

Replay from the source bundle: python3 tools/verify.py.

Readable source ↘Record JSON ↘Full area ↗Related KL-FCS-010 ↘Related KL-FCS-024 ↘

Go further.

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

Questions to investigate

  1. A balanced-looking schedule need not be optimal; release dates and precedence change the problem.
  2. Which assumption in the specification can be changed to make the current evidence insufficient?
  3. Add precedence-constrained schedules and dual or lower-bound certificates.

Conceptual references

These sources explain the surrounding theory. The linked material was not imported as a dataset, and these records do not claim checking by the source’s software.

Primary conceptual reference ↗

Related areas

Circuit minimizationCombinatorial optimizationConstraint satisfaction