Identical-machine scheduling

Machine loads and makespans, list schedules with arbitrary tie breaking, LPT schedules, and the two families attaining Graham's bounds. Processing times are real numbers; nonnegativity and positivity are imposed by the individual results that require them.

def GrahamLPT.loadBefore {m n : ℕ} (p : Fin n → ℝ) (σ : Fin n → Fin m) (k : ℕ) (i : Fin m) : ℝ

The load of machine i from the jobs of index below k under the assignment σ.

Equations

• GrahamLPT.loadBefore p σ k i = ∑ j : Fin n with ↑j < k ∧ σ j = i, p j

def GrahamLPT.load {m n : ℕ} (p : Fin n → ℝ) (σ : Fin n → Fin m) (i : Fin m) : ℝ

The load of machine i: the total length of the jobs assigned to it.

Equations

• GrahamLPT.load p σ i = ∑ j : Fin n with σ j = i, p j

def GrahamLPT.makespan {m n : ℕ} [NeZero m] (p : Fin n → ℝ) (σ : Fin n → Fin m) : ℝ

The makespan of an assignment: its largest machine load.

Equations

• GrahamLPT.makespan p σ = Finset.univ.sup' ⋯ (GrahamLPT.load p σ)

def GrahamLPT.optMakespan (m : ℕ) [NeZero m] {n : ℕ} (p : Fin n → ℝ) : ℝ

The optimal makespan: the least makespan over all assignments of the n jobs to the m machines.

Equations

• GrahamLPT.optMakespan m p = Finset.univ.inf' ⋯ fun (σ : Fin n → Fin m) => GrahamLPT.makespan p σ

def GrahamLPT.IsListSchedule {m n : ℕ} (p : Fin n → ℝ) (σ : Fin n → Fin m) : Prop

A list schedule in the index order: each job k goes to a machine whose load from the jobs before k is least, under any tie-breaking.

Equations

• GrahamLPT.IsListSchedule p σ = ∀ (k : Fin n) (i : Fin m), GrahamLPT.loadBefore p σ (↑k) (σ k) ≤ GrahamLPT.loadBefore p σ (↑k) i

def GrahamLPT.IsLPTSchedule {m n : ℕ} (p : Fin n → ℝ) (σ : Fin n → Fin m) : Prop

An LPT schedule: a list schedule of the jobs taken in some nonincreasing order of length.

Equations

• GrahamLPT.IsLPTSchedule p σ = ∃ (π : Equiv.Perm (Fin n)), Antitone (p ∘ ⇑π) ∧ GrahamLPT.IsListSchedule (p ∘ ⇑π) (σ ∘ ⇑π)

def GrahamLPT.grahamJobs (m : ℕ) : Fin (2 * m + 1) → ℝ

Graham's instance for LPT: the 2m + 1 lengths 2m − 1, 2m − 1, 2m − 2, 2m − 2, …, m + 1, m + 1, m, m, m.

Equations

• GrahamLPT.grahamJobs m j = if ↑j < 2 * m then 2 * ↑m - 1 - ↑(↑j / 2) else ↑m

def GrahamLPT.grahamOrder (m : ℕ) (i : Fin (2 * m + 1)) : Fin (2 * m + 1)

The order 2m − 1, …, m + 1, m, m, 2m − 1, …, m + 1, m of Graham's instance, as the job at each position: position i < m − 1 holds job 2i (length 2m − 1 − i), positions m − 1 and m hold jobs 2m − 2 and 2m − 1 (length m), position m + 1 + a with a < m − 1 holds job 2a + 1 (length 2m − 1 − a), and position 2m holds job 2m (length m).

Equations

• One or more equations did not get rendered due to their size.

def GrahamLPT.unitJobs (m : ℕ) : Fin (m * (m - 1) + 1) → ℝ

Graham's instance for list scheduling: m(m − 1) unit jobs followed by one job of length m.

Equations

• GrahamLPT.unitJobs m j = if ↑j < m * (m - 1) then 1 else ↑m