Sequencing with deadlines and penalties

JobSequencing is Karp's problem JOB SEQUENCING [Kar72], the problem SEQUENCING TO MINIMIZE TARDY TASK WEIGHT of Garey and Johnson, Problem SS3: given jobs with (time, deadline, penalty) (Cslib.Complexity.JobSequencing.Job) and a bound (Cslib.Complexity.JobSequencingInstance), some order of the jobs, run one after another from time 0 without idle time, has total penalty at most bound, where a job pays its penalty when it completes after its deadline. All numbers are natural numbers in binary (encNat); orders are permutations (List.Perm) of the list of jobs, so repeated jobs are scheduled with multiplicity.

Karp's reduction from SubsetSum (his KNAPSACK) maps the numbers a and target t to jobs of time and penalty a and common deadline t, with penalty bound a.sum - t (SubsetSum.toJobSequencing). The jobs completed on time in an order hold numbers of total at most t, and the others pay their whole time as penalty, so the bound is met exactly when the jobs on time sum to t. A target above a.sum is mapped to a fixed instance without a feasible order, since then the subtraction would truncate.

NP membership uses the order itself as the witness (Turing.MultiTapeTM.Decoder.list): the verifier checks that it is a permutation of the jobs by counting occurrences, and computes its total penalty in closed form from prefix sums.

Main definitions

• Cslib.Complexity.JobSequencing.Job, Cslib.Complexity.JobSequencing.encJob: jobs with processing time, deadline, and penalty, and their binary encoding.
• Cslib.Complexity.JobSequencing.penaltyFrom, Cslib.Complexity.JobSequencing.totalPenalty: the total penalty of an order.
• Cslib.Complexity.JobSequencingInstance, Cslib.Complexity.JobSequencing, Cslib.Complexity.encJobSequencing.
• Cslib.Complexity.SubsetSum.toJobSequencing: Karp's reduction.

Main results

• Cslib.Complexity.JobSequencing.penaltyFrom_append: penalties of consecutive runs add up.
• Cslib.Complexity.JobSequencing.computableInPolyTime_totalPenalty: the total penalty of an order is polynomial-time.
• Cslib.Complexity.JobSequencing.mem_NP: JobSequencing ∈ NP encJobSequencing.
• Cslib.Complexity.SubsetSum.toJobSequencing_mem_iff: correctness of the reduction.
• Cslib.Complexity.polyTimeReducible_SubsetSum_JobSequencing, Cslib.Complexity.JobSequencing_npHard, Cslib.Complexity.JobSequencing_npComplete: JobSequencing is NP-complete.

References

• M. R. Garey and D. S. Johnson, Computers and Intractability
• R. M. Karp, Reducibility among combinatorial problems

structure Cslib.Complexity.JobSequencing.Job : Type

A job in JobSequencing, with processing time, deadline, and tardiness penalty.

• time : ℕ

  The processing time required by the job.

• deadline : ℕ

  The deadline by which the job must complete to avoid paying its penalty.

• penalty : ℕ

  The penalty incurred if the job completes strictly after its deadline.

theorem Cslib.Complexity.JobSequencing.Job.ext {x y : Job} (time : x.time = y.time) (deadline : x.deadline = y.deadline) (penalty : x.penalty = y.penalty) : x = y

theorem Cslib.Complexity.JobSequencing.Job.ext_iff {x y : Job} : x = y ↔ x.time = y.time ∧ x.deadline = y.deadline ∧ x.penalty = y.penalty

@[instance_reducible]

instance Cslib.Complexity.JobSequencing.instDecidableEqJob : DecidableEq Job

def Cslib.Complexity.JobSequencing.instDecidableEqJob.decEq (x✝ x✝¹ : Job) : Decidable (x✝ = x✝¹)

def Cslib.Complexity.JobSequencing.instReprJob.repr : Job → ℕ → Std.Format

@[instance_reducible]

instance Cslib.Complexity.JobSequencing.instReprJob : Repr Job

theorem Cslib.Complexity.JobSequencing.encJob_time_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Job} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encJob S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).time) encIn✝ Turing.MultiTapeTM.encNat S✝

theorem Cslib.Complexity.JobSequencing.encJob_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 T0 S0 x1 T1 S1 x2 T2 S2 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInO x0 encIn Turing.MultiTapeTM.encNat T0 S0) (h1 : Turing.MultiTapeTM.ComputableInO x1 encIn Turing.MultiTapeTM.encNat T1 S1) (h2 : Turing.MultiTapeTM.ComputableInO x2 encIn Turing.MultiTapeTM.encNat T2 S2) : Turing.MultiTapeTM.ComputableInO (fun (x : γ) => { time := x0 x, deadline := x1 x, penalty := x2 x }) encIn encJob (fun (x : γ) => T0 x + (T1 x + T2 x)) fun (x : γ) => S0 x + (S1 x + S2 x)

theorem Cslib.Complexity.JobSequencing.encJob_penalty_deg : Turing.MultiTapeTM.ComputableInDegree Job.penalty encJob Turing.MultiTapeTM.encNat 1 1

theorem Cslib.Complexity.JobSequencing.encJob_penalty_inO : Turing.MultiTapeTM.ComputableInO Job.penalty encJob Turing.MultiTapeTM.encNat (fun (a : Job) => (encJob a).length) fun (a : Job) => (encJob a).length

@[reducible, inline]

abbrev Cslib.Complexity.JobSequencing.encJobFields : ℕ × ℕ × ℕ ↪ List Bool

The tuple of the fields of encJob.

theorem Cslib.Complexity.JobSequencing.encJob_deadline_inO : Turing.MultiTapeTM.ComputableInO Job.deadline encJob Turing.MultiTapeTM.encNat (fun (a : Job) => (encJob a).length) fun (a : Job) => (encJob a).length

theorem Cslib.Complexity.JobSequencing.encJob_mk_deg : Turing.MultiTapeTM.ComputableInDegree (fun (p : ℕ × ℕ × ℕ) => { time := p.1, deadline := p.2.1, penalty := p.2.2 }) encJobFields encJob 1 1

theorem Cslib.Complexity.JobSequencing.encJob_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget x0 x1 x2 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInSpace x0 encIn Turing.MultiTapeTM.encNat budget) (h1 : Turing.MultiTapeTM.ComputableInSpace x1 encIn Turing.MultiTapeTM.encNat budget) (h2 : Turing.MultiTapeTM.ComputableInSpace x2 encIn Turing.MultiTapeTM.encNat budget) : Turing.MultiTapeTM.ComputableInSpace (fun (x : γ) => { time := x0 x, deadline := x1 x, penalty := x2 x }) encIn encJob budget

theorem Cslib.Complexity.JobSequencing.encJob_penalty_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Job} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encJob S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).penalty) encIn✝ Turing.MultiTapeTM.encNat S✝

theorem Cslib.Complexity.JobSequencing.encJob_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : Job) => (a.time, a.deadline, a.penalty)) encJob encJobFields 1 1

theorem Cslib.Complexity.JobSequencing.encJob_time_deg : Turing.MultiTapeTM.ComputableInDegree Job.time encJob Turing.MultiTapeTM.encNat 1 1

def Cslib.Complexity.JobSequencing.encJob : Job ↪ List Bool

Binary encoding of a job as (time, (deadline, penalty)).

theorem Cslib.Complexity.JobSequencing.encJob_deadline_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → Job} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encJob S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).deadline) encIn✝ Turing.MultiTapeTM.encNat S✝

theorem Cslib.Complexity.JobSequencing.encJob_deadline_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Job} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encJob → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).deadline) encIn✝ Turing.MultiTapeTM.encNat

theorem Cslib.Complexity.JobSequencing.encJob_time_inO : Turing.MultiTapeTM.ComputableInO Job.time encJob Turing.MultiTapeTM.encNat (fun (a : Job) => (encJob a).length) fun (a : Job) => (encJob a).length

theorem Cslib.Complexity.JobSequencing.encJob_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 x1 x2 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInPolyTime x0 encIn Turing.MultiTapeTM.encNat) (h1 : Turing.MultiTapeTM.ComputableInPolyTime x1 encIn Turing.MultiTapeTM.encNat) (h2 : Turing.MultiTapeTM.ComputableInPolyTime x2 encIn Turing.MultiTapeTM.encNat) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { time := x0 x, deadline := x1 x, penalty := x2 x }) encIn encJob

theorem Cslib.Complexity.JobSequencing.encJob_penalty_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Job} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encJob → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).penalty) encIn✝ Turing.MultiTapeTM.encNat

theorem Cslib.Complexity.JobSequencing.encJob_deadline_deg : Turing.MultiTapeTM.ComputableInDegree Job.deadline encJob Turing.MultiTapeTM.encNat 1 1

theorem Cslib.Complexity.JobSequencing.encJob_time_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → Job} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encJob → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).time) encIn✝ Turing.MultiTapeTM.encNat

@[simp]

theorem Cslib.Complexity.JobSequencing.encJob_apply (a : Job) : encJob a = encJobFields (a.time, a.deadline, a.penalty)

def Cslib.Complexity.JobSequencing.penaltyFrom : ℕ → List Job → ℕ

The total penalty of the jobs run in the given order, one after another without idle time, from time s: a job pays its penalty when it completes after its deadline.

def Cslib.Complexity.JobSequencing.totalPenalty (σ : List Job) : ℕ

The total penalty of the jobs run in the given order from time 0.

theorem Cslib.Complexity.JobSequencing.penaltyFrom_append (s : ℕ) (σ τ : List Job) : penaltyFrom s (σ ++ τ) = penaltyFrom s σ + penaltyFrom (s + (List.map Job.time σ).sum) τ

The penalties of two consecutive runs add up; the second starts when the first ends.

structure Cslib.Complexity.JobSequencingInstance : Type

An instance of JobSequencing: a list of jobs to schedule and a penalty bound.

• jobs : List JobSequencing.Job

  The jobs to schedule consecutively without idle time starting at time 0.

• bound : ℕ

  The maximum allowed total tardiness penalty.

theorem Cslib.Complexity.JobSequencingInstance.ext_iff {x y : JobSequencingInstance} : x = y ↔ x.jobs = y.jobs ∧ x.bound = y.bound

theorem Cslib.Complexity.JobSequencingInstance.ext {x y : JobSequencingInstance} (jobs : x.jobs = y.jobs) (bound : x.bound = y.bound) : x = y

def Cslib.Complexity.instDecidableEqJobSequencingInstance.decEq (x✝ x✝¹ : JobSequencingInstance) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Complexity.instDecidableEqJobSequencingInstance : DecidableEq JobSequencingInstance

@[instance_reducible]

instance Cslib.Complexity.instReprJobSequencingInstance : Repr JobSequencingInstance

def Cslib.Complexity.instReprJobSequencingInstance.repr : JobSequencingInstance → ℕ → Std.Format

theorem Cslib.Complexity.encJobSequencing_bound_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → JobSequencingInstance} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encJobSequencing → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).bound) encIn✝ Turing.MultiTapeTM.encNat

theorem Cslib.Complexity.encJobSequencing_bound_inO : Turing.MultiTapeTM.ComputableInO JobSequencingInstance.bound encJobSequencing Turing.MultiTapeTM.encNat (fun (a : JobSequencingInstance) => (encJobSequencing a).length) fun (a : JobSequencingInstance) => (encJobSequencing a).length

theorem Cslib.Complexity.encJobSequencing_jobs_deg : Turing.MultiTapeTM.ComputableInDegree JobSequencingInstance.jobs encJobSequencing (Turing.MultiTapeTM.encList JobSequencing.encJob) 1 1

@[simp]

theorem Cslib.Complexity.encJobSequencing_apply (a : JobSequencingInstance) : encJobSequencing a = encJobSequencingFields (a.jobs, a.bound)

theorem Cslib.Complexity.encJobSequencing_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → List JobSequencing.Job} {x1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInPolyTime x0 encIn (Turing.MultiTapeTM.encList JobSequencing.encJob)) (h1 : Turing.MultiTapeTM.ComputableInPolyTime x1 encIn Turing.MultiTapeTM.encNat) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { jobs := x0 x, bound := x1 x }) encIn encJobSequencing

theorem Cslib.Complexity.encJobSequencing_jobs_inO : Turing.MultiTapeTM.ComputableInO JobSequencingInstance.jobs encJobSequencing (Turing.MultiTapeTM.encList JobSequencing.encJob) (fun (a : JobSequencingInstance) => (encJobSequencing a).length) fun (a : JobSequencingInstance) => (encJobSequencing a).length

theorem Cslib.Complexity.encJobSequencing_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : JobSequencingInstance) => (a.jobs, a.bound)) encJobSequencing encJobSequencingFields 1 1

theorem Cslib.Complexity.encJobSequencing_jobs_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → JobSequencingInstance} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encJobSequencing → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).jobs) encIn✝ (Turing.MultiTapeTM.encList JobSequencing.encJob)

theorem Cslib.Complexity.encJobSequencing_bound_deg : Turing.MultiTapeTM.ComputableInDegree JobSequencingInstance.bound encJobSequencing Turing.MultiTapeTM.encNat 1 1

@[reducible, inline]

abbrev Cslib.Complexity.encJobSequencingFields : List JobSequencing.Job × ℕ ↪ List Bool

The tuple of the fields of encJobSequencing.

theorem Cslib.Complexity.encJobSequencing_mk_deg : Turing.MultiTapeTM.ComputableInDegree (fun (p : List JobSequencing.Job × ℕ) => { jobs := p.1, bound := p.2 }) encJobSequencingFields encJobSequencing 1 1

theorem Cslib.Complexity.encJobSequencing_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget : γ → ℕ} {x0 : γ → List JobSequencing.Job} {x1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInSpace x0 encIn (Turing.MultiTapeTM.encList JobSequencing.encJob) budget) (h1 : Turing.MultiTapeTM.ComputableInSpace x1 encIn Turing.MultiTapeTM.encNat budget) : Turing.MultiTapeTM.ComputableInSpace (fun (x : γ) => { jobs := x0 x, bound := x1 x }) encIn encJobSequencing budget

theorem Cslib.Complexity.encJobSequencing_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → List JobSequencing.Job} {T0 S0 x1 T1 S1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInO x0 encIn (Turing.MultiTapeTM.encList JobSequencing.encJob) T0 S0) (h1 : Turing.MultiTapeTM.ComputableInO x1 encIn Turing.MultiTapeTM.encNat T1 S1) : Turing.MultiTapeTM.ComputableInO (fun (x : γ) => { jobs := x0 x, bound := x1 x }) encIn encJobSequencing (fun (x : γ) => T0 x + T1 x) fun (x : γ) => S0 x + S1 x

theorem Cslib.Complexity.encJobSequencing_jobs_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → JobSequencingInstance} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encJobSequencing S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).jobs) encIn✝ (Turing.MultiTapeTM.encList JobSequencing.encJob) S✝

def Cslib.Complexity.encJobSequencing : JobSequencingInstance ↪ List Bool

Instances of JobSequencing are encoded as a list of jobs and a penalty bound, all in binary.

theorem Cslib.Complexity.encJobSequencing_bound_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → JobSequencingInstance} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encJobSequencing S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).bound) encIn✝ Turing.MultiTapeTM.encNat S✝

def Cslib.Complexity.JobSequencing : Set JobSequencingInstance

Sequencing with deadlines and penalties [Kar72]: some order of the jobs has total penalty at most the bound.

theorem Cslib.Complexity.JobSequencing.computableInPolyTime_totalPenalty : Turing.MultiTapeTM.ComputableInPolyTime totalPenalty (Turing.MultiTapeTM.encList encJob) Turing.MultiTapeTM.encNat

The total penalty of an order is polynomial-time computable.

theorem Cslib.Complexity.JobSequencing.mem_NP : JobSequencing ∈ NP encJobSequencing

JobSequencing belongs to NP, with the order as the witness; a permutation of the jobs is encoded with the length of the encoded list of jobs.

def Cslib.Complexity.SubsetSum.toJobSequencing (x : SubsetSumInstance) : JobSequencingInstance

Karp's reduction from SubsetSum to JobSequencing [Kar72]: each number a becomes a job of time and penalty a with the target t as deadline, and the penalty bound is a.sum - t. A target above the total is mapped to a single job that is always late.

theorem Cslib.Complexity.SubsetSum.toJobSequencing_mem_iff (x : SubsetSumInstance) : toJobSequencing x ∈ JobSequencing ↔ x ∈ SubsetSum

Correctness of the reduction to JobSequencing.

theorem Cslib.Complexity.SubsetSum.computableInPolyTime_toJobSequencing : Turing.MultiTapeTM.ComputableInPolyTime toJobSequencing encSubsetSum encJobSequencing

The reduction toJobSequencing is computable in polynomial time.

theorem Cslib.Complexity.polyTimeReducible_SubsetSum_JobSequencing : PolyTimeReducible encSubsetSum encJobSequencing SubsetSum JobSequencing

SubsetSum reduces to JobSequencing in polynomial time.

theorem Cslib.Complexity.JobSequencing_npHard : NPHard encJobSequencing JobSequencing

JobSequencing is NP-hard.

theorem Cslib.Complexity.JobSequencing_npComplete : NPComplete encJobSequencing JobSequencing

Sequencing with deadlines and penalties is NP-complete, with the numbers in binary [Kar72].