CoffmanSethi

Chen's property of LPT schedules (Chen 1993, as Della Croce–Scatamacchia 2020 restate it, Proposition 2): in an LPT schedule the j-th job placed on a machine has length at most C(τ)/j for every assignment τ; hence, when a machine attaining the makespan holds k jobs, k·m·C(σ) ≤ ((k + 1)m − 1)·C(τ) (the Coffman–Sethi form). Helpers carry the prefix cs_.

The route (this development). Fix P > 0 below every job placed so far and weigh a job x by ⌊x/P⌋. For two machines h, g write D for the load of h minus the load of g, Φ for the weight of h minus the number of jobs on g, and y for the last job placed. The invariant loadDifferenceInvariant (D ≥ 0 → ⌊D/P⌋ ≤ Φ; D < 0 → −1 ≤ Φ ∧ ⌊(D + y)/P⌋ − 1 ≤ Φ) holds at every step of a list schedule in nonincreasing order, since a job joins a least-loaded machine. With g the machine receiving job k, every machine weighs at least the number of jobs on g before k; summing over the machines and comparing with τ, where a machine's weight is below j when its load is below j·p_k, gives j · p_k ≤ C(τ).

def GrahamLPT.prefixJobCount {m n : ℕ} (σ : Fin n → Fin m) (k : ℕ) (i : Fin m) : ℤ

The number of jobs of index below k on machine i, as an integer.

Equations

• GrahamLPT.prefixJobCount σ k i = ∑ _j : Fin n with ↑_j < k ∧ σ _j = i, 1

noncomputable def GrahamLPT.prefixJobWeight {m n : ℕ} (p : Fin n → ℝ) (P : ℝ) (σ : Fin n → Fin m) (k : ℕ) (i : Fin m) : ℤ

The weight Σ ⌊p_j / P⌋ of the jobs of index below k on machine i.

Equations

• GrahamLPT.prefixJobWeight p P σ k i = ∑ j : Fin n with ↑j < k ∧ σ j = i, ⌊p j / P⌋

def GrahamLPT.loadDifferenceInvariant (P D y : ℝ) (Φ : ℤ) : Prop

The two-machine invariant: D a load difference, y the last job, Φ a weight minus a count.

Equations

• GrahamLPT.loadDifferenceInvariant P D y Φ = ((0 ≤ D → ⌊D / P⌋ ≤ Φ) ∧ (D < 0 → -1 ≤ Φ ∧ ⌊(D + y) / P⌋ - 1 ≤ Φ))

theorem GrahamLPT.cs_inv_mono {P D y y' : ℝ} {Φ : ℤ} (hP : 0 < P) (h : loadDifferenceInvariant P D y Φ) (hy : y' ≤ y) : loadDifferenceInvariant P D y' Φ

theorem GrahamLPT.cs_inv_self {P y : ℝ} {Φ : ℤ} (hΦ : 0 ≤ Φ) : loadDifferenceInvariant P 0 y Φ

theorem GrahamLPT.cs_inv_istep {P D y x : ℝ} {Φ : ℤ} (hP : 0 < P) (hx : P ≤ x) (hD : 0 ≤ D) (h : loadDifferenceInvariant P D y Φ) : loadDifferenceInvariant P (D - x) x (Φ - 1)

The receiving machine is the second of the pair (D ≥ 0): it gains a job of length x ≥ P.

theorem GrahamLPT.cs_inv_hstep {P D y x : ℝ} {Φ : ℤ} (hP : 0 < P) (hx : P ≤ x) (hxy : x ≤ y) (hD : D ≤ 0) (h : loadDifferenceInvariant P D y Φ) : loadDifferenceInvariant P (D + x) x (Φ + ⌊x / P⌋)

The receiving machine is the first of the pair (D ≤ 0): it gains a job x with P ≤ x ≤ y.

theorem GrahamLPT.cs_cnt_le_fl {m n : ℕ} (p : Fin n → ℝ) {P : ℝ} (hP : 0 < P) (σ : Fin n → Fin m) (k : ℕ) (hk : ∀ (j : Fin n), ↑j < k → P ≤ p j) (i : Fin m) : prefixJobCount σ k i ≤ prefixJobWeight p P σ k i

theorem GrahamLPT.cs_cnt_zero {m n : ℕ} (σ : Fin n → Fin m) (i : Fin m) : prefixJobCount σ 0 i = 0

theorem GrahamLPT.cs_fl_zero {m n : ℕ} (p : Fin n → ℝ) (P : ℝ) (σ : Fin n → Fin m) (i : Fin m) : prefixJobWeight p P σ 0 i = 0

theorem GrahamLPT.cs_inv_all {m n : ℕ} (p : Fin n → ℝ) (hanti : Antitone p) (σ : Fin n → Fin m) (hσ : IsListSchedule p σ) {P : ℝ} (hP : 0 < P) (k : ℕ) : k ≤ n → (∀ (j : Fin n), ↑j < k → P ≤ p j) → ∀ (h g : Fin m) (y : ℝ), (∀ (j : Fin n), ↑j + 1 = k → y ≤ p j) → loadDifferenceInvariant P (loadBefore p σ k h - loadBefore p σ k g) y (prefixJobWeight p P σ k h - prefixJobCount σ k g)

The invariant along a list schedule in nonincreasing order, for every pair of machines.

theorem GrahamLPT.cs_cnt_le_fl_of_min {m n : ℕ} (p : Fin n → ℝ) (hanti : Antitone p) (σ : Fin n → Fin m) (hσ : IsListSchedule p σ) {P : ℝ} (hP : 0 < P) (k : Fin n) (hk : ∀ (j : Fin n), ↑j < ↑k → P ≤ p j) (h : Fin m) : prefixJobCount σ (↑k) (σ k) ≤ prefixJobWeight p P σ (↑k) h

Every machine weighs at least the number of jobs on the machine that receives job k, before k.

theorem GrahamLPT.lpt_job_position_le {m n : ℕ} [NeZero m] (p : Fin n → ℝ) (hp : ∀ (j : Fin n), 0 ≤ p j) (hanti : Antitone p) (σ : Fin n → Fin m) (hσ : IsListSchedule p σ) (k : Fin n) (τ : Fin n → Fin m) : (↑{j : Fin n | ↑j < ↑k ∧ σ j = σ k}.card + 1) * p k ≤ makespan p τ

Chen's property, sorted form: job k is the (c + 1)-th job on its machine, c the jobs of smaller index there; then (c + 1) · p_k ≤ C(τ) for every assignment τ.

theorem GrahamLPT.cs_bound {m n : ℕ} [NeZero m] (p : Fin n → ℝ) (hp : ∀ (j : Fin n), 0 ≤ p j) (hanti : Antitone p) (σ : Fin n → Fin m) (hσ : IsListSchedule p σ) (τ : Fin n → Fin m) (i : Fin m) (hi : load p σ i = makespan p σ) : ↑{j : Fin n | σ j = i}.card * ↑m * makespan p σ ≤ ((↑{j : Fin n | σ j = i}.card + 1) * ↑m - 1) * makespan p τ

The Coffman–Sethi form, sorted: a machine i attaining the makespan of a list schedule in nonincreasing order, holding k jobs, gives k·m·C(σ) ≤ ((k + 1)m − 1)·C(τ) for every assignment τ.

theorem GrahamLPT.lpt_bound_of_card {m n : ℕ} [NeZero m] (p : Fin n → ℝ) (hp : ∀ (j : Fin n), 0 ≤ p j) (σ : Fin n → Fin m) (hσ : IsLPTSchedule p σ) (τ : Fin n → Fin m) (i : Fin m) (hi : load p σ i = makespan p σ) : ↑{j : Fin n | σ j = i}.card * ↑m * makespan p σ ≤ ((↑{j : Fin n | σ j = i}.card + 1) * ↑m - 1) * makespan p τ

The Coffman–Sethi form of the LPT bound: if a machine i attaining the makespan of an LPT schedule holds q jobs, then q·m · C(σ) ≤ ((q + 1)m − 1) · C(τ) for every assignment τ (Coffman–Sethi 1976 as corrected by Chen 1993, as Della Croce and Scatamacchia restate it; the literature states it for q ≥ 3; for m ≥ 2 it is weaker than lpt_bound at q ≤ 2, and its attainment is not proved here).