Three-machine flow shop scheduling

AbbreviationFlow-shop instances#✓fully proved

A flow-shop instance is a pair consisting of a finite list of jobs, each a finite list of natural numbers (its processing times on machines 1, 2 and 3, in that order), and a natural number \(D\), the deadline. The type does not force a job to have exactly three entries; that is part of well-formedness.

abbrev FlowShopInstance := List (List ℕ) × ℕ

Used by 3

Used byThe 3-machine flow shop scheduling decision problem · Feasible flow-shop schedules · Well-formed flow-shop instances

DefinitionWell-formed flow-shop instances#✓fully proved

A flow-shop instance is well formed when every job in it is a list of exactly three natural numbers.

def WellFormed (i : FlowShopInstance) : Prop :=
  ∀ job ∈ i.1, job.length = 3

Uses 1 · Used by 1

Statement usesFlow-shop instances

Used byThe 3-machine flow shop scheduling decision problem

DefinitionFeasible flow-shop schedules#✓fully proved

Let an instance consist of jobs \(1, \dots, n\), where job \(j\) is a list of natural numbers whose \(k\)-th entry \(p_{j,k}\) is its processing time on machine \(k\) (read as \(0\) if the list has fewer than \(k\) entries), and a deadline \(D\). The instance is feasible when there are natural numbers \(s_{j,k}\), for each job \(j\) and each \(k \in \{1, 2, 3\}\), such that for every job \(j\) we have \(s_{j,1} + p_{j,1} \le s_{j,2}\), \(s_{j,2} + p_{j,2} \le s_{j,3}\) and \(s_{j,3} + p_{j,3} \le D\), and for every machine \(k \in \{1, 2, 3\}\) and all jobs \(a < b\) we have \(s_{a,k} + p_{a,k} \le s_{b,k}\) or \(s_{b,k} + p_{b,k} \le s_{a,k}\).

Here \(s_{j,k}\) is the start time of job \(j\) on machine \(k\): each job visits machines 1, 2, 3 in that order, no machine processes two jobs at once, and every job finishes by \(D\).

def FlowShopFeasible
    (i : FlowShopInstance) : Prop :=
  ∃ start : List (List ℕ), start.length = i.1.length ∧
    (∀ row ∈ start, row.length = 3) ∧
    (∀ j < i.1.length, (start.getD j []).getD 0 0 + (i.1.getD j []).getD 0 0 ≤
        (start.getD j []).getD 1 0 ∧
      (start.getD j []).getD 1 0 + (i.1.getD j []).getD 1 0 ≤
        (start.getD j []).getD 2 0 ∧
      (start.getD j []).getD 2 0 + (i.1.getD j []).getD 2 0 ≤ i.2) ∧
    ∀ k < 3, ∀ a < i.1.length, ∀ b < i.1.length, a < b →
      (start.getD a []).getD k 0 + (i.1.getD a []).getD k 0 ≤
          (start.getD b []).getD k 0 ∨
        (start.getD b []).getD k 0 + (i.1.getD b []).getD k 0 ≤
          (start.getD a []).getD k 0

Uses 1 · Used by 1

Statement usesFlow-shop instances

Used byThe 3-machine flow shop scheduling decision problem

DefinitionThe 3-machine flow shop scheduling decision problem#✓fully proved

The decision problem 3-MACHINE FLOW SHOP SCHEDULING accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding of flow-shop instances, to an instance that is well formed and feasible. Bitstrings that do not decode to an instance are rejected.

noncomputable def flowShopDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := FlowShopInstance) x with
  | some i => decide (WellFormed i ∧ FlowShopFeasible 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 flow-shop schedules · Flow-shop instances · Well-formed flow-shop instances · Decision problems

Used by3-MACHINE FLOW SHOP SCHEDULING is NP-complete

Theorem3-MACHINE FLOW SHOP SCHEDULING is NP-complete#●ready to prove

The 3-machine flow shop scheduling decision problem belongs to NP, and every decision problem in NP reduces to it by a polynomial-time many-one reduction.

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

Sources

• M. R. Garey, D. S. Johnson, and R. Sethi, "The complexity of flowshop and jobshop scheduling", Mathematics of Operations Research 1 (1976), 117-129; T. F. Gonzalez and S. Sahni, "Flowshop and jobshop schedules: complexity and approximation", Operations Research 26 (1978), 36-52.

Uses 5

Statement usesPolynomial-time many-one reduction · The 3-machine flow shop 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.