Weighted number of tardy jobs

AbbreviationWeighted tardy jobs instances#✓fully proved

An instance of WEIGHTED NUMBER OF TARDY JOBS is a pair consisting of a finite list of jobs, each a triple \((p, d, w)\) of natural numbers giving its processing time \(p\), due date \(d\) and weight \(w\), and a natural number \(K\), the bound.

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

Used by 2

Used byThe weighted number of tardy jobs decision problem · Feasible weighted tardy jobs instances

DefinitionOne step of the weighted tardy jobs computation#✓fully proved

Let \(J\) be a list of jobs, each a triple \((p, d, w)\) of natural numbers (processing time, due date, weight). Given a state \((t, s)\) and a natural number \(j\), let \((p, d, w)\) be the job at position \(j\) of \(J\), counting from \(0\), or \((0, 0, 0)\) if \(J\) has no position \(j\), and let \(t' = t + p\). The step returns \((t', s + w)\) if \(d < t'\), and \((t', s)\) otherwise.

def WeightedTardyStep (jobs : List (ℕ × ℕ × ℕ)) (state : ℕ × ℕ) (j : ℕ) : ℕ × ℕ :=
  let t := state.1 + (jobs.getD j (0, 0, 0)).1
  (t, state.2 + if (jobs.getD j (0, 0, 0)).2.1 < t then (jobs.getD j (0, 0, 0)).2.2 else 0)

Used by 1

Used byWeighted number of tardy jobs of an ordering

DefinitionWeighted number of tardy jobs of an ordering#✓fully proved

Let \(J\) be a list of jobs, each a triple of natural numbers (processing time, due date, weight), and write \((p_i, d_i, w_i)\) for the job at position \(i\) of \(J\), counting from \(0\), with \((p_i, d_i, w_i) = (0, 0, 0)\) when \(J\) has no position \(i\). For a list \((j_1, \dots, j_m)\) of natural numbers, the weighted number of tardy jobs of this order is the sum of \(w_{j_k}\) over all \(k\) with \(d_{j_k} < C_k\), where \(C_k = p_{j_1} + \dots + p_{j_k}\) is the completion time of the \(k\)-th job.

def WeightedTardy (jobs : List (ℕ × ℕ × ℕ)) (order : List ℕ) : ℕ :=
  (order.foldl (WeightedTardyStep jobs) (0, 0)).2

Uses 1 · Used by 1

Statement usesOne step of the weighted tardy jobs computation

Used byFeasible weighted tardy jobs instances

DefinitionFeasible weighted tardy jobs instances#✓fully proved

A weighted tardy jobs instance, consisting of a list of \(n\) jobs and a bound \(K\), is feasible when there is an ordering of its jobs, that is, a list of the job indices \(0, 1, \dots, n - 1\) in which each index occurs exactly once, whose weighted number of tardy jobs is at most \(K\).

def WeightedTardyJobsFeasible
    (i : WeightedTardyJobsInstance) : Prop :=
  ∃ order : List ℕ, order.Perm (List.range i.1.length) ∧
    WeightedTardy i.1 order ≤ i.2

Uses 2 · Used by 1

Statement usesWeighted number of tardy jobs of an ordering · Weighted tardy jobs instances

Used byThe weighted number of tardy jobs decision problem

DefinitionThe weighted number of tardy jobs decision problem#✓fully proved

WEIGHTED NUMBER OF TARDY JOBS is the decision problem that accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding of weighted tardy jobs instances, to a feasible instance, that is, an instance having an ordering of its jobs whose weighted number of tardy jobs is at most its bound. A bitstring that decodes to no instance is rejected.

noncomputable def weightedTardyJobsDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := WeightedTardyJobsInstance) x with
  | some i => decide (WeightedTardyJobsFeasible 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 weighted tardy jobs instances · Weighted tardy jobs instances · Decision problems

Used byWEIGHTED NUMBER OF TARDY JOBS is NP-complete

TheoremWEIGHTED NUMBER OF TARDY JOBS is NP-complete#●ready to prove

The weighted number of tardy jobs decision problem lies in NP, and every decision problem in NP has a polynomial-time many-one reduction to it.

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), WEIGHTED NUMBER OF TARDY JOBS (1||sum w_j U_j).

Uses 5

Statement usesPolynomial-time many-one reduction · The weighted number of tardy jobs 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.