Weighted completion time with precedence constraints

AbbreviationInstances of single-machine weighted completion with precedence#✓fully proved

An instance of the scheduling problem \(1 \mid \mathrm{prec} \mid \sum w_j C_j\) (one machine, precedence constraints, objective the sum over jobs \(j\) of the weight \(w_j\) times the completion time \(C_j\)) is a triple \((J, P, K)\): a list \(J\) of jobs, each a pair \((p, w)\) of natural numbers giving its processing time and weight; a list \(P\) of pairs of natural numbers, read as precedence constraints between job indices; and a natural number bound \(K\).

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

Used by 3

Used bySINGLE-MACHINE WEIGHTED COMPLETION WITH PRECEDENCE as a decision problem · Feasible weighted completion instances · Well-formed weighted completion instances

DefinitionOne step of the weighted completion time computation#✓fully proved

Let \(J\) be a list of jobs, each a pair (processing time, weight), let \((t, s)\) be a state consisting of the elapsed time \(t\) and the accumulated weighted completion time \(s\), and let \(j\) be a job index. With \((p, w)\) the job at position \(j\) of \(J\) counting from \(0\), or \((0, 0)\) if \(J\) has no such position, the step sends \((t, s)\) to \((t + p, s + w (t + p))\).

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

Used by 1

Used byTotal weighted completion time of a job order

DefinitionTotal weighted completion time of a job order#✓fully proved

Let \(J\) be a list of jobs, each a pair \((p_i, w_i)\) of processing time and weight indexed from \(0\), with \((p_i, w_i) = (0, 0)\) for \(i\) outside the list. For a list \(j_1, \dots, j_m\) of job indices, the total weighted completion time is \(\sum_{k=1}^{m} w_{j_k} C_k\), where \(C_k = p_{j_1} + \dots + p_{j_k}\) is the completion time of the \(k\)-th job in the order.

def WeightedCompletion (jobs : List (ℕ × ℕ)) (order : List ℕ) : ℕ :=
  (order.foldl (WeightedCompletionStep jobs) (0, 0)).2

Uses 1 · Used by 1

Statement usesOne step of the weighted completion time computation

Used byFeasible weighted completion instances

DefinitionWell-formed weighted completion instances#✓fully proved

An instance \((J, P, K)\) whose job list \(J\) has \(n\) jobs is well formed when every precedence pair \((a, b)\) in \(P\) satisfies \(a < n\), \(b < n\) and \(a \ne b\).

def WellFormed (i : PrecedenceWeightedCompletionInstance) : Prop :=
  ∀ p ∈ i.2.1, p.1 < i.1.length ∧ p.2 < i.1.length ∧ p.1 ≠ p.2

Uses 1 · Used by 1

Statement usesInstances of single-machine weighted completion with precedence

Used bySINGLE-MACHINE WEIGHTED COMPLETION WITH PRECEDENCE as a decision problem

DefinitionFeasible weighted completion instances#✓fully proved

Let \((J, P, K)\) be an instance whose job list \(J\) consists of \(n\) jobs \((p_0, w_0), \dots, (p_{n-1}, w_{n-1})\) (processing time, weight). It is feasible when there is an ordering \(j_1, \dots, j_n\) of the indices \(0, \dots, n-1\), each listed exactly once, such that for every pair \((a, b)\) in \(P\) the position of \(a\) in the ordering is smaller than the position of \(b\), where an index that does not occur gets position \(n + 1\), and \(\sum_{k=1}^{n} w_{j_k} (p_{j_1} + \dots + p_{j_k}) \le K\).

def PrecedenceWeightedCompletionFeasible
    (i : PrecedenceWeightedCompletionInstance) : Prop :=
  ∃ order : List ℕ, order.Perm (List.range i.1.length) ∧
    (∀ p ∈ i.2.1, order.idxOf p.1 < order.idxOf p.2) ∧
    WeightedCompletion i.1 order ≤ i.2.2

Uses 2 · Used by 1

Statement usesInstances of single-machine weighted completion with precedence · Total weighted completion time of a job order

Used bySINGLE-MACHINE WEIGHTED COMPLETION WITH PRECEDENCE as a decision problem

DefinitionSINGLE-MACHINE WEIGHTED COMPLETION WITH PRECEDENCE as a decision problem#✓fully proved

The decision problem accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to an instance \((J, P, K)\) that is well formed and feasible: every precedence pair in \(P\) consists of two distinct job indices of \(J\), and some ordering of all the jobs that puts the first job of every precedence pair before the second has total weighted completion time at most \(K\). Bitstrings that do not decode to an instance are rejected.

noncomputable def precedenceWeightedCompletionDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := PrecedenceWeightedCompletionInstance) x with
  | some i => decide (WellFormed i ∧ PrecedenceWeightedCompletionFeasible i)
  | none => false

Uses 12 · 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 completion instances · Instances of single-machine weighted completion with precedence · Well-formed weighted completion instances · Decision problems

Used bySINGLE-MACHINE WEIGHTED COMPLETION WITH PRECEDENCE is NP-complete

TheoremSINGLE-MACHINE WEIGHTED COMPLETION WITH PRECEDENCE is NP-complete#●ready to prove

The decision problem SINGLE-MACHINE WEIGHTED COMPLETION WITH PRECEDENCE on bitstrings belongs to NP, and every decision problem in NP reduces to it by a polynomial-time many-one reduction.

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), 1|prec|sum w_j C_j; E. L. Lawler, "Sequencing jobs to minimize total weighted completion time subject to precedence constraints", Annals of Discrete Mathematics 2 (1978), 75-90; J. K. Lenstra and A. H. G. Rinnooy Kan, "Complexity of scheduling under precedence constraints", Operations Research 26 (1978), 22-35.

Uses 5

Statement usesPolynomial-time many-one reduction · SINGLE-MACHINE WEIGHTED COMPLETION WITH PRECEDENCE as a decision problem · Complexity classes · Decision problems · The complexity class NP

6 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.