Precedence-constrained multiprocessor scheduling

AbbreviationInstances of precedence-constrained multiprocessor scheduling#✓fully proved

An instance is a tuple \((d, P, m, D)\) in which \(d = (d_0, \dots, d_{n-1})\) is a list of natural numbers, \(d_j\) being the duration of job \(j\); \(P\) is a list of pairs \((a, b)\) of natural numbers, each read as the precedence constraint that job \(a\) precedes job \(b\); \(m\) is a natural number, the number of machines; and \(D\) is a natural number, the deadline.

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

Used by 3

Used byThe precedence-constrained multiprocessor scheduling decision problem · Feasible precedence-multiprocessor scheduling instances · Well-formed precedence-multiprocessor scheduling instances

DefinitionWell-formed precedence-multiprocessor scheduling instances#✓fully proved

An instance \((d, P, m, D)\) whose list of job durations \(d\) has length \(n\) is well formed when every precedence pair \((a, b) \in P\) satisfies \(a < n\), \(b < n\) and \(a \ne b\), and there is an ordering of the jobs \(0, \dots, n-1\) (a permutation of this list) in which \(a\) comes before \(b\) for every \((a, b) \in P\).

def WellFormed (i : PrecedenceMultiprocessorSchedulingInstance) : Prop :=
  ∀ p ∈ i.2.1, p.1 < i.1.length ∧ p.2 < i.1.length ∧ p.1 ≠ p.2 ∧
    ∃ ord : List ℕ, ord.Perm (List.range i.1.length) ∧
      ∀ p ∈ i.2.1, ord.idxOf p.1 < ord.idxOf p.2

Uses 1 · Used by 1

Statement usesInstances of precedence-constrained multiprocessor scheduling

Used byThe precedence-constrained multiprocessor scheduling decision problem

DefinitionFeasible precedence-multiprocessor scheduling instances#✓fully proved

An instance \((d, P, m, D)\) with job durations \(d = (d_0, \dots, d_{n-1})\) is feasible when there are start times \(s_0, \dots, s_{n-1} \in \mathbb{N}\) and machines \(\mu_0, \dots, \mu_{n-1} \in \mathbb{N}\) such that \(\mu_j < m\) and \(s_j + d_j \le D\) for every \(j < n\), \(s_a + d_a \le s_b\) for every precedence pair \((a, b) \in P\), and for all jobs \(a < b < n\) with \(\mu_a = \mu_b\), either \(s_a + d_a \le s_b\) or \(s_b + d_b \le s_a\). Here \(s_j\) and \(d_j\) are read as \(0\) when \(j \ge n\).

def PrecedenceMultiprocessorSchedulingFeasible
    (i : PrecedenceMultiprocessorSchedulingInstance) : Prop :=
  ∃ start : List ℕ, start.length = i.1.length ∧
    ∃ machine : List ℕ, machine.length = i.1.length ∧
      (∀ j < i.1.length, machine.getD j 0 < i.2.2.1) ∧
      (∀ j < i.1.length, start.getD j 0 + i.1.getD j 0 ≤ i.2.2.2) ∧
      (∀ p ∈ i.2.1, start.getD p.1 0 + i.1.getD p.1 0 ≤ start.getD p.2 0) ∧
      ∀ a < i.1.length, ∀ b < i.1.length, a < b → machine.getD a 0 = machine.getD b 0 →
        start.getD a 0 + i.1.getD a 0 ≤ start.getD b 0 ∨
        start.getD b 0 + i.1.getD b 0 ≤ start.getD a 0

Uses 1 · Used by 1

Statement usesInstances of precedence-constrained multiprocessor scheduling

Used byThe precedence-constrained multiprocessor scheduling decision problem

DefinitionThe precedence-constrained multiprocessor scheduling decision problem#✓fully proved

The decision problem that accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to a precedence-multiprocessor scheduling instance that is well formed and feasible. Bitstrings that do not decode to an instance are rejected.

noncomputable def precedenceMultiprocessorSchedulingDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := PrecedenceMultiprocessorSchedulingInstance) x with
  | some i => decide (WellFormed i ∧ PrecedenceMultiprocessorSchedulingFeasible 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 precedence-multiprocessor scheduling instances · Instances of precedence-constrained multiprocessor scheduling · Well-formed precedence-multiprocessor scheduling instances · Decision problems

Used byPRECEDENCE-CONSTRAINED MULTIPROCESSOR SCHEDULING is NP-complete

TheoremPRECEDENCE-CONSTRAINED MULTIPROCESSOR SCHEDULING is NP-complete#●ready to prove

The precedence-constrained multiprocessor scheduling decision problem is in NP, and every decision problem in NP has a polynomial-time many-one reduction to it.

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), PRECEDENCE-CONSTRAINED MULTIPROCESSOR SCHEDULING; J. D. Ullman, "NP-complete scheduling problems" (1975).

Uses 5

Statement usesPolynomial-time many-one reduction · The precedence-constrained multiprocessor scheduling decision problem · Complexity classes · Decision problems · The complexity class NP

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.