Parallel machine scheduling with deadlines

AbbreviationParallel machine scheduling instances#✓fully proved

An instance of parallel machine scheduling with deadlines is a pair consisting of a finite list of jobs, each a pair \((p, d)\) of natural numbers giving its processing time \(p\) and deadline \(d\), and a natural number \(m\), the number of machines.

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

Used by 2

Used byThe PARALLEL MACHINES WITH DEADLINES decision problem · Feasible schedules on parallel machines with deadlines

DefinitionFeasible schedules on parallel machines with deadlines#✓fully proved

An instance consisting of jobs \((p_1, d_1), \dots, (p_k, d_k)\), where job \(j\) has processing time \(p_j\) and deadline \(d_j\), and a number \(m\) of machines is feasible when there are start times \(s_1, \dots, s_k \in \mathbb{N}\) and machines \(\mu_1, \dots, \mu_k \in \{0, \dots, m - 1\}\) such that \(s_j + p_j \le d_j\) for every \(j\), and for all \(a \ne b\) with \(\mu_a = \mu_b\), either \(s_a + p_a \le s_b\) or \(s_b + p_b \le s_a\).

def ParallelMachinesDeadlinesFeasible
    (i : ParallelMachinesDeadlinesInstance) : 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) ∧
      (∀ j < i.1.length, start.getD j 0 + (i.1.getD j (0, 0)).1 ≤ (i.1.getD j (0, 0)).2) ∧
      ∀ 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, 0)).1 ≤ start.getD b 0 ∨
        start.getD b 0 + (i.1.getD b (0, 0)).1 ≤ start.getD a 0

Uses 1 · Used by 1

Statement usesParallel machine scheduling instances

Used byThe PARALLEL MACHINES WITH DEADLINES decision problem

DefinitionThe PARALLEL MACHINES WITH DEADLINES decision problem#✓fully proved

This decision problem accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to jobs \((p_1, d_1), \dots, (p_k, d_k)\) of natural numbers (processing times and deadlines) and a number \(m\) of machines for which there are start times \(s_1, \dots, s_k \in \mathbb{N}\) and machines \(\mu_1, \dots, \mu_k \in \{0, \dots, m - 1\}\) such that \(s_j + p_j \le d_j\) for every \(j\), and for all \(a \ne b\) with \(\mu_a = \mu_b\), either \(s_a + p_a \le s_b\) or \(s_b + p_b \le s_a\). It rejects every bitstring that does not decode.

noncomputable def parallelMachinesDeadlinesDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := ParallelMachinesDeadlinesInstance) x with
  | some i => decide (ParallelMachinesDeadlinesFeasible 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 schedules on parallel machines with deadlines · Parallel machine scheduling instances · Decision problems

Used byPARALLEL MACHINES WITH DEADLINES is NP-complete

TheoremPARALLEL MACHINES WITH DEADLINES is NP-complete#●ready to prove

The PARALLEL MACHINES WITH DEADLINES decision problem belongs to NP, and every decision problem in NP reduces to it by a polynomial-time many-one reduction.

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), PARALLEL MACHINE SCHEDULING WITH DEADLINES.

Uses 5

Statement usesPolynomial-time many-one reduction · The PARALLEL MACHINES WITH DEADLINES decision problem · Complexity classes · Decision problems · The complexity class NP

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.