Total tardiness scheduling

AbbreviationInstances of TOTAL TARDINESS#✓fully proved

An instance of TOTAL TARDINESS is a pair \((J, K)\) consisting of a finite list \(J = ((p_0, d_0), \dots, (p_{n-1}, d_{n-1}))\) of jobs, where job \(j\) has processing time \(p_j \in \mathbb{N}\) and due date \(d_j \in \mathbb{N}\), and a bound \(K \in \mathbb{N}\).

abbrev TotalTardinessInstance := List (ℕ × ℕ) × ℕ

Used by 2

Used byThe TOTAL TARDINESS decision problem · Feasible TOTAL TARDINESS instances

DefinitionOne step of the tardiness computation#✓fully proved

Let \(J = ((p_0, d_0), \dots, (p_{n-1}, d_{n-1}))\) be a list of jobs with processing times \(p_i \in \mathbb{N}\) and due dates \(d_i \in \mathbb{N}\), let \(j \in \mathbb{N}\), and let \((p, d) = (p_j, d_j)\) if \(j < n\) and \((p, d) = (0, 0)\) otherwise. Running job \(j\) from the state \((t, s) \in \mathbb{N} \times \mathbb{N}\), where \(t\) is the elapsed time and \(s\) the accumulated tardiness, gives the state \((t + p, \, s + \max(t + p - d, 0))\).

def TardinessStep (jobs : List (ℕ × ℕ)) (state : ℕ × ℕ) (j : ℕ) : ℕ × ℕ :=
  let t := state.1 + (jobs.getD j (0, 0)).1
  (t, state.2 + (t - (jobs.getD j (0, 0)).2))

Used by 1

Used byTotal tardiness of a job order

DefinitionTotal tardiness of a job order#✓fully proved

Let \(J = ((p_0, d_0), \dots, (p_{n-1}, d_{n-1}))\) be a list of jobs with processing times \(p_i \in \mathbb{N}\) and due dates \(d_i \in \mathbb{N}\), and set \((p_i, d_i) = (0, 0)\) for \(i \ge n\). For a list \((j_1, \dots, j_m)\) of natural numbers (job indices), let \(C_k = p_{j_1} + \dots + p_{j_k}\) be the completion time of the \(k\)-th job when the jobs are run in this order. The total tardiness of the order is \(\sum_{k=1}^{m} \max(C_k - d_{j_k}, 0)\).

def TotalTardinessValue (jobs : List (ℕ × ℕ)) (order : List ℕ) : ℕ :=
  (order.foldl (TardinessStep jobs) (0, 0)).2

Uses 1 · Used by 1

Statement usesOne step of the tardiness computation

Used byFeasible TOTAL TARDINESS instances

DefinitionFeasible TOTAL TARDINESS instances#✓fully proved

An instance \((J, K)\) of TOTAL TARDINESS with \(n\) jobs is feasible when some ordering of its jobs, that is, some permutation \((j_1, \dots, j_n)\) of \((0, 1, \dots, n - 1)\), has total tardiness at most \(K\).

def TotalTardinessFeasible
    (i : TotalTardinessInstance) : Prop :=
  ∃ order : List ℕ, order.Perm (List.range i.1.length) ∧
    TotalTardinessValue i.1 order ≤ i.2

Uses 2 · Used by 1

Statement usesInstances of TOTAL TARDINESS · Total tardiness of a job order

Used byThe TOTAL TARDINESS decision problem

DefinitionThe TOTAL TARDINESS decision problem#✓fully proved

The decision problem TOTAL TARDINESS accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding (natural numbers in binary), to an instance of TOTAL TARDINESS that is feasible, that is, whose jobs admit an ordering of total tardiness at most its bound. It rejects every bitstring that does not decode to an instance.

noncomputable def totalTardinessDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := TotalTardinessInstance) x with
  | some i => decide (TotalTardinessFeasible i)
  | none => false

Uses 11 · Used by 1

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Feasible TOTAL TARDINESS instances · Instances of TOTAL TARDINESS · Decision problems

Used byTOTAL TARDINESS is NP-complete

TheoremTOTAL TARDINESS is NP-complete#●ready to prove

The TOTAL TARDINESS decision problem belongs to NP, and every decision problem in NP reduces to it by a polynomial-time many-one reduction.

public theorem_wanted totalTardiness_npComplete :
    totalTardinessDec ∈ MetaMathlibExt.ComplexityTheory.NP ∧
      ∀ L : MetaMathlibExt.ComplexityTheory.DecisionProblem,
        L ∈ MetaMathlibExt.ComplexityTheory.NP →
          Cslib.CookLevin.PolyManyOneRed L totalTardinessDec

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), TOTAL TARDINESS (1||sum T_j); J. Du and J. Y.-T. Leung, "Minimizing total tardiness on one machine is NP-hard" (1990).

Uses 5

Statement usesPolynomial-time many-one reduction · The TOTAL TARDINESS decision problem · Complexity classes · Decision problems · The complexity class NP

5 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.