ListBound

Graham's 1966 bound for list scheduling.

theorem GrahamLPT.lb_mul_le {m n : ℕ} (p : Fin n → ℝ) (hp : ∀ (j : Fin n), 0 ≤ p j) (σ : Fin n → Fin m) (hσ : IsListSchedule p σ) (k : Fin n) : ↑m * (loadBefore p σ (↑k) (σ k) + p k) ≤ ∑ j : Fin n, p j + (↑m - 1) * p k

The makespan of a list schedule, through the last job k of a heaviest machine: m · (L_k + p_k) ≤ Σ p + (m − 1) · p_k.

theorem GrahamLPT.listSchedule_bound {m n : ℕ} [NeZero m] (p : Fin n → ℝ) (hp : ∀ (j : Fin n), 0 ≤ p j) (σ : Fin n → Fin m) (hσ : IsListSchedule p σ) (τ : Fin n → Fin m) : ↑m * makespan p σ ≤ (2 * ↑m - 1) * makespan p τ

Graham's bound for list scheduling: for nonnegative lengths, every list schedule σ and every assignment τ satisfy m · C(σ) ≤ (2m − 1) · C(τ).

theorem GrahamLPT.listSchedule_le_optMakespan {m n : ℕ} [NeZero m] (p : Fin n → ℝ) (hp : ∀ (j : Fin n), 0 ≤ p j) (σ : Fin n → Fin m) (hσ : IsListSchedule p σ) : makespan p σ ≤ (2 - 1 / ↑m) * optMakespan m p

Every list schedule is within the factor 2 − 1/m of the optimum.