What a schedule can achieve

The one semantic fact about job sequencing that a reduction into it needs: when every job carries the same deadline and its penalty equals its execution time, a schedule is nothing but a choice of the jobs that meet the deadline. Two halves:

• DescriptiveComplexity.finsum_onTime_le – the jobs a schedule leaves on time weigh at most the deadline. They are exactly the jobs at or before the last of them, so their total execution time is that job's completion time, and that job is on time;
• DescriptiveComplexity.exists_schedule_onTime – conversely, any set of jobs weighing at most the deadline can be put first, by ordering the universe through the key “not chosen, then the ambient order” (DescriptiveComplexity.isLinOrd_of_key), and then all of it is on time.

Together they give DescriptiveComplexity.hasGoodSchedule_iff_exists_subset and, when the jobs weigh twice the deadline and the bound is the deadline, DescriptiveComplexity.hasGoodSchedule_iff_exists_half: the instance is a yes-instance exactly when some set of jobs weighs exactly the deadline. That last form is Partition's condition, which is why a reduction into job sequencing can be built out of a balanced-split gadget – provided it also writes the deadline, its double and the bound, which is what constrains the gadget.

Sums over sets of jobs

Completion times along a schedule

theorem DescriptiveComplexity.jsCompletion_mono {A : Type} [Finite A] [FirstOrder.Language.jobSeq.Structure A] {sched : A → A → Prop} (hs : IsLinOrd sched) {i j : A} (hij : sched i j) : JSCompletion sched i ≤ JSCompletion sched j

Completion times grow along the schedule.

theorem DescriptiveComplexity.not_jsLate_of_sched {A : Type} [Finite A] [FirstOrder.Language.jobSeq.Structure A] {D : ℕ} {sched : A → A → Prop} (hs : IsLinOrd sched) (hdl : ∀ (j : A), JSJob j → JSDlineVal j = D) {i j : A} (hi : JSJob i) (hj : JSJob j) (hij : sched i j) (hnl : ¬JSLate sched j) : ¬JSLate sched i

With a common deadline, being on time is inherited backwards along the schedule: the on-time jobs form a prefix.

theorem DescriptiveComplexity.finsum_onTime_le {A : Type} [Finite A] [FirstOrder.Language.jobSeq.Structure A] {D : ℕ} {sched : A → A → Prop} (hs : IsLinOrd sched) (hdl : ∀ (j : A), JSJob j → JSDlineVal j = D) : ∑ᶠ (j : A) (_ : j ∈ {j : A | JSJob j ∧ ¬JSLate sched j}), JSTimeVal j ≤ D

The jobs a schedule leaves on time weigh at most the deadline: they are the jobs at or before the last of them, so their total execution time is that job's completion time.

Putting a set of jobs first

theorem DescriptiveComplexity.exists_schedule_onTime {A : Type} [Finite A] [FirstOrder.Language.jobSeq.Structure A] {D : ℕ} [LinearOrder A] {S : A → Prop} (hsum : ∑ᶠ (j : A) (_ : j ∈ {j : A | S j}), JSTimeVal j ≤ D) (hdl : ∀ (j : A), JSJob j → JSDlineVal j = D) : ∃ (sched : A → A → Prop), IsLinOrd sched ∧ ∀ (j : A), JSJob j → S j → ¬JSLate sched j

Any set of jobs weighing at most the deadline can be scheduled first, by ordering the universe through the key “not chosen, then the ambient order”. Everything chosen is then on time.

The characterization

theorem DescriptiveComplexity.hasGoodSchedule_iff_exists_subset {A : Type} [Finite A] [FirstOrder.Language.jobSeq.Structure A] {D : ℕ} [LinearOrder A] (hlin : IsLinOrd JSLe) (hdl : ∀ (j : A), JSJob j → JSDlineVal j = D) (hpt : ∀ (j : A), JSJob j → JSPenVal j = JSTimeVal j) : HasGoodSchedule A ↔ ∃ (S : A → Prop), (∀ (j : A), S j → JSJob j) ∧ ∑ᶠ (j : A) (_ : j ∈ {j : A | S j}), JSTimeVal j ≤ D ∧ ∑ᶠ (j : A) (_ : j ∈ {j : A | JSJob j ∧ ¬S j}), JSTimeVal j ≤ JSBound A

A schedule is a choice of the jobs that meet the deadline: when all deadlines agree and each penalty is its job's execution time, the instance is a yes-instance exactly when some set of jobs fits in the deadline while the jobs it leaves out fit in the bound.

theorem DescriptiveComplexity.hasGoodSchedule_iff_exists_half {A : Type} [Finite A] [FirstOrder.Language.jobSeq.Structure A] {D : ℕ} [LinearOrder A] (hlin : IsLinOrd JSLe) (hdl : ∀ (j : A), JSJob j → JSDlineVal j = D) (hpt : ∀ (j : A), JSJob j → JSPenVal j = JSTimeVal j) (htot : ∑ᶠ (j : A) (_ : j ∈ {j : A | JSJob j}), JSTimeVal j = 2 * D) (hbnd : JSBound A = D) : HasGoodSchedule A ↔ ∃ (S : A → Prop), (∀ (j : A), S j → JSJob j) ∧ ∑ᶠ (j : A) (_ : j ∈ {j : A | S j}), JSTimeVal j = D

The balanced form: when the jobs weigh twice the deadline and the bound is the deadline, a good schedule is a set of jobs weighing exactly the deadline. This is Partition's condition, and it is what a reduction into job sequencing has to produce – together with the deadline, its double and the bound, all three written in binary.