Job sequencing with deadlines and profits

AbbreviationJob-sequencing instances#✓fully proved

An instance of job sequencing with deadlines, processing times and profits is a pair \((J, K)\) of a finite list \(J\) of jobs, each a triple \((p, d, w)\) of natural numbers giving its processing time \(p\), deadline \(d\) and profit \(w\), and a natural number \(K\), the profit bound.

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

Used by 2

Used byJob sequencing with deadlines, processing times and profits as a decision problem · Feasible job-sequencing instances

DefinitionFeasible job-sequencing instances#✓fully proved

Let \((J, K)\) be a job-sequencing instance with jobs \(J = (p_0, d_0, w_0), \dots, (p_{n-1}, d_{n-1}, w_{n-1})\). The instance is feasible when there are distinct indices \(j_1, \dots, j_m < n\), for some \(m \ge 0\), such that \(w_{j_1} + \dots + w_{j_m} \ge K\) and, for every \(t\) with \(1 \le t \le m\), \(p_{j_1} + \dots + p_{j_t} \le d_{j_t}\): the selected jobs, run one after another in this order from time \(0\), each finish by their deadlines, and their total profit is at least \(K\).

def JobSequencingWithProcessingTimesFeasible
    (i : JobSequencingWithProcessingTimesInstance) : Prop :=
  ∃ order : List ℕ, order.Nodup ∧ (∀ j ∈ order, j < i.1.length) ∧
    i.2 ≤ (order.map (fun j => (i.1.getD j (0, 0, 0)).2.2)).sum ∧
    ∀ t < order.length,
      ((order.take (t + 1)).map (fun j => (i.1.getD j (0, 0, 0)).1)).sum ≤
        (i.1.getD (order.getD t 0) (0, 0, 0)).2.1

Uses 1 · Used by 1

Statement usesJob-sequencing instances

Used byJob sequencing with deadlines, processing times and profits as a decision problem

DefinitionJob sequencing with deadlines, processing times and profits as a decision problem#✓fully proved

This decision problem accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to a job-sequencing instance that is feasible; bitstrings that do not decode to an instance are rejected.

noncomputable def jobSequencingWithProcessingTimesDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := JobSequencingWithProcessingTimesInstance) x with
  | some i => decide (JobSequencingWithProcessingTimesFeasible 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 job-sequencing instances · Job-sequencing instances · Decision problems

Used byJOB SEQUENCING WITH DEADLINES, PROCESSING TIMES, AND PROFITS is NP-complete

TheoremJOB SEQUENCING WITH DEADLINES, PROCESSING TIMES, AND PROFITS is NP-complete#●ready to prove

The decision problem of job sequencing with deadlines, processing times and profits on bitstrings is NP-complete: it belongs to NP, and every decision problem in NP has a polynomial-time many-one reduction to it.

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), SEQUENCING WITH DEADLINES AND PROFITS (arbitrary processing times); R. M. Karp, "Reducibility among combinatorial problems" (1972).

Uses 5

Statement usesPolynomial-time many-one reduction · Job sequencing with deadlines, processing times and profits 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.