Scheduling with release times and deadlines

AbbreviationInstances of single-machine scheduling with release times and deadlines#✓fully proved

A release-deadlines instance is a list of jobs \((p_0, r_0, d_0), \dots, (p_{n-1}, r_{n-1}, d_{n-1})\) of triples of natural numbers, where \(p_j\) is the processing time, \(r_j\) the release time and \(d_j\) the deadline of job \(j\).

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

Used by 2

Used bySingle-machine scheduling with release times and deadlines as a decision problem · Feasible single-machine schedules with release times and deadlines

DefinitionFeasible single-machine schedules with release times and deadlines#✓fully proved

A release-deadlines instance with jobs \((p_j, r_j, d_j)\) for \(j < n\) is feasible when there are start times \(s_0, \dots, s_{n-1} \in \mathbb{N}\) such that \(r_j \le s_j\) and \(s_j + p_j \le d_j\) for every \(j < n\), and for all \(a < b < n\) either \(s_a + p_a \le s_b\) or \(s_b + p_b \le s_a\).

def ReleaseDeadlinesSchedulingFeasible
    (i : ReleaseDeadlinesSchedulingInstance) : Prop :=
  ∃ start : List ℕ, start.length = i.length ∧
    (∀ j < i.length, (i.getD j (0, 0, 0)).2.1 ≤ start.getD j 0 ∧
      start.getD j 0 + (i.getD j (0, 0, 0)).1 ≤ (i.getD j (0, 0, 0)).2.2) ∧
    ∀ a < i.length, ∀ b < i.length, a < b →
      start.getD a 0 + (i.getD a (0, 0, 0)).1 ≤ start.getD b 0 ∨
      start.getD b 0 + (i.getD b (0, 0, 0)).1 ≤ start.getD a 0

Uses 1 · Used by 1

Statement usesInstances of single-machine scheduling with release times and deadlines

Used bySingle-machine scheduling with release times and deadlines as a decision problem

DefinitionSingle-machine scheduling with release times and deadlines as a decision problem#✓fully proved

SINGLE-MACHINE SCHEDULING WITH RELEASE TIMES AND DEADLINES is the decision problem that accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding of release-deadlines instances, to a feasible instance. Bitstrings that do not decode to an instance are rejected.

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

abbrev DecisionProblem := List Bool → Bool

MathlibExt/Computability/Complexity.lean:170

def bitDecode [BitstringEncoding α] (l : List Bool) : Option α := toEncoding.decode l

MathlibExt/Computability/Complexity.lean:58

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

WantedExt/Complexity/NPComplete/ReleaseDeadlinesSchedulingWanted.lean:48

def ReleaseDeadlinesSchedulingFeasible
    (i : ReleaseDeadlinesSchedulingInstance) : Prop :=
  ∃ start : List ℕ, start.length = i.length ∧
    (∀ j < i.length, (i.getD j (0, 0, 0)).2.1 ≤ start.getD j 0 ∧
      start.getD j 0 + (i.getD j (0, 0, 0)).1 ≤ (i.getD j (0, 0, 0)).2.2) ∧
    ∀ a < i.length, ∀ b < i.length, a < b →
      start.getD a 0 + (i.getD a (0, 0, 0)).1 ≤ start.getD b 0 ∨
      start.getD b 0 + (i.getD b (0, 0, 0)).1 ≤ start.getD a 0

WantedExt/Complexity/NPComplete/ReleaseDeadlinesSchedulingWanted.lean:51

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 single-machine schedules with release times and deadlines · Instances of single-machine scheduling with release times and deadlines · Decision problems

Used bySINGLE-MACHINE SCHEDULING WITH RELEASE TIMES AND DEADLINES is NP-complete

TheoremSINGLE-MACHINE SCHEDULING WITH RELEASE TIMES AND DEADLINES is NP-complete#●ready to prove

The decision problem SINGLE-MACHINE SCHEDULING WITH RELEASE TIMES AND DEADLINES belongs to NP, and every decision problem in NP has a polynomial-time many-one reduction to it.

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

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

WantedExt/Complexity/NPComplete/ReleaseDeadlinesSchedulingWanted.lean:63

def NP : DecisionComplexityClass :=
  { L | ∃ (p : Polynomial ℕ), ∃ R : (List Bool × List Bool) → Bool,
      IsPolyTime R ∧
      ∀ x, L x ↔ ∃ w : List Bool, w.length ≤ p.eval x.length ∧ R (x, w) }

MathlibExt/Computability/Complexity.lean:200

abbrev DecisionProblem := List Bool → Bool

MathlibExt/Computability/Complexity.lean:170

def PolyManyOneRed (L₁ L₂ : MetaMathlibExt.ComplexityTheory.DecisionProblem) : Prop :=
  ∃ reduce : List Bool → List Bool,
    MetaMathlibExt.ComplexityTheory.IsPolyTime reduce ∧ ∀ x, L₁ x = L₂ (reduce x)

CSLibExt/Computability/CookLevin.lean:396

Sources

J. K. Lenstra, A. H. G. Rinnooy Kan, and P. Brucker, "Complexity of machine scheduling problems", Annals of Discrete Mathematics 1 (1977), 343-362 (strong NP-hardness of nonpreemptive 1|r_j|L_max; feasibility is L_max <= 0).

Uses 5

Statement usesPolynomial-time many-one reduction · Single-machine scheduling with release times and deadlines as a 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.