Resource-constrained project scheduling

AbbreviationInstances of resource-constrained project scheduling#✓fully proved

An instance of resource-constrained project scheduling (an RCPSP instance) is a quadruple \((J, P, C, D)\): a list \(J\) of jobs, each a pair \((p, r) \in \mathbb{N} \times \mathbb{N}\) of a duration \(p\) and a resource demand \(r\); a list \(P\) of precedence pairs \((a, b) \in \mathbb{N} \times \mathbb{N}\) of job indices; a resource capacity \(C \in \mathbb{N}\); and a deadline \(D \in \mathbb{N}\).

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

Used by 3

Used byResource-constrained project scheduling as a decision problem · Feasible RCPSP instances · Well-formed RCPSP instances

DefinitionWell-formed RCPSP instances#✓fully proved

An RCPSP instance \((J, P, C, D)\) 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\), and there is a listing of \(0, 1, \dots, n-1\), each exactly once, in which \(a\) comes before \(b\) for every \((a, b) \in P\).

def WellFormed (i : RCPSPInstance) : 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 resource-constrained project scheduling

Used byResource-constrained project scheduling as a decision problem

DefinitionFeasible RCPSP instances#✓fully proved

Let \((J, P, C, D)\) be an RCPSP instance with \(n\) jobs, where job \(j < n\) has duration \(p_j\) and resource demand \(r_j\), and set \(p_j = 0\) for \(j \ge n\). The instance is feasible when there are start times \(s_0, \dots, s_{n-1} \in \mathbb{N}\), with \(s_j = 0\) for \(j \ge n\), such that every job finishes by the deadline (\(s_j + p_j \le D\) for all \(j < n\)), every precedence pair \((a, b) \in P\) satisfies \(s_a + p_a \le s_b\), and at every time \(t < D\) the total demand of the jobs active at \(t\) (the jobs \(j < n\) with \(s_j \le t < s_j + p_j\)) is at most \(C\).

def RCPSPFeasible
    (i : RCPSPInstance) : Prop :=
  ∃ start : List ℕ, start.length = i.1.length ∧
    (∀ j < i.1.length, start.getD j 0 + (i.1.getD j (0, 0)).1 ≤ i.2.2.2) ∧
    (∀ p ∈ i.2.1, start.getD p.1 0 + (i.1.getD p.1 0).1 ≤ start.getD p.2 0) ∧
    ∀ t < i.2.2.2, ¬ ∃ active : List ℕ, active.Nodup ∧
      (∀ j ∈ active, j < i.1.length ∧ start.getD j 0 ≤ t ∧
        t < start.getD j 0 + (i.1.getD j (0, 0)).1) ∧
      i.2.2.1 < (active.map (fun j => (i.1.getD j (0, 0)).2)).sum

Uses 1 · Used by 1

Statement usesInstances of resource-constrained project scheduling

Used byResource-constrained project scheduling as a decision problem

DefinitionResource-constrained project scheduling as a decision problem#✓fully proved

RESOURCE-CONSTRAINED PROJECT SCHEDULING is the decision problem that accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding of RCPSP instances, to an RCPSP instance that is well formed and feasible. Bitstrings that do not decode to an instance are rejected.

noncomputable def rcpspDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := RCPSPInstance) x with
  | some i => decide (WellFormed i ∧ RCPSPFeasible 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 RCPSP instances · Instances of resource-constrained project scheduling · Well-formed RCPSP instances · Decision problems

Used byRESOURCE-CONSTRAINED PROJECT SCHEDULING is NP-complete

TheoremRESOURCE-CONSTRAINED PROJECT SCHEDULING is NP-complete#●ready to prove

The decision problem RESOURCE-CONSTRAINED PROJECT SCHEDULING belongs to NP, and every decision problem in NP has a polynomial-time many-one reduction to it.

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), BIN PACKING; J. Blazewicz, J. K. Lenstra, and A. H. G. Rinnooy Kan, "Scheduling subject to resource constraints: classification and complexity", Discrete Applied Mathematics 5 (1983), 11-24 (classification).

Uses 5

Statement usesPolynomial-time many-one reduction · Resource-constrained project scheduling as a 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.