Job sequencing
Lax799700.JobSequencing · concepts/Lax799700/JobSequencing.lean · lax-799700
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
SEQUENCING: given jobs with execution times, deadlines and penalties, and a bound, is there a one-processor schedule whose jobs missing their deadline carry a total penalty at most the bound? Numbers are written in binary, as for Knapsack. A schedule is a linear order on the universe, which a certificate can guess and a first-order kernel can constrain; a job's completion time is the total execution time of the jobs at or before it (JSCompletion), it is late when that exceeds its deadline, and the schedule is good when the late jobs' penalties sum to at most the bound. Membership is by an existential second-order definition, hardness by an ordered first-order reduction from NAE-3SAT.
Concept map
Evidence
Lean source view on GitHub
| 1 | import Mathlib.Algebra.BigOperators.Finprod |
| 2 | import Mathlib.ModelTheory.Semantics |
| 3 | import Mathlib.ModelTheory.Complexity |
| 4 | import Mathlib.Tactic.FinCases |
| 5 | import Mathlib.Data.Set.Finite.Lemmas |
| 6 | import Mathlib.Data.Fintype.EquivFin |
| 7 | import Mathlib.Data.Set.Card |
| 8 | import Mathlib.SetTheory.Cardinal.Finite |
| 9 | import Mathlib.Logic.Equiv.Prod |
| 10 | import Mathlib.ModelTheory.Syntax |
| 11 | import Lax799700.Common |
| 12 | import Lax904597.Machines |
| 13 | import Lax904597.Classes |
| 14 | import Lax799700.Problems |
| 15 | |
| 16 | /-! |
| 17 | --- |
| 18 | title: Job sequencing |
| 19 | type: theorem |
| 20 | --- |
| 21 | SEQUENCING: given jobs with execution times, deadlines and penalties, and |
| 22 | a bound, is there a one-processor schedule whose jobs missing their |
| 23 | deadline carry a total penalty at most the bound? Numbers are written in |
| 24 | binary, as for Knapsack. A schedule is a linear order on the universe, |
| 25 | which a certificate can guess and a first-order kernel can constrain; a |
| 26 | job's completion time is the total execution time of the jobs at or |
| 27 | before it (JSCompletion), it is late when that exceeds its deadline, and |
| 28 | the schedule is good when the late jobs' penalties sum to at most the |
| 29 | bound. Membership is by an existential second-order definition, hardness |
| 30 | by an ordered first-order reduction from NAE-3SAT. |
| 31 | |
| 32 | -/ |
| 33 | |
| 34 | namespace Lax799700.JobSequencing |
| 35 | |
| 36 | open Lax799700.Common Lax904597.Machines |
| 37 | |
| 38 | open FirstOrder |
| 39 | |
| 40 | open FirstOrder.Language |
| 41 | |
| 42 | /-- The relation symbols of the language. -/ |
| 43 | inductive jobSeqRel : ℕ → Type where |
| 44 | /-- `job j`: `j` is a job. -/ |
| 45 | | job : jobSeqRel 1 |
| 46 | /-- `posn p`: `p` is a bit position. -/ |
| 47 | | posn : jobSeqRel 1 |
| 48 | /-- `time j p`: the execution time of `j` has bit 1 at position `p`. -/ |
| 49 | | time : jobSeqRel 2 |
| 50 | /-- `dline j p`: the deadline of `j` has bit 1 at position `p`. -/ |
| 51 | | dline : jobSeqRel 2 |
| 52 | /-- `pen j p`: the penalty of `j` has bit 1 at position `p`. -/ |
| 53 | | pen : jobSeqRel 2 |
| 54 | /-- `bnd p`: the penalty bound has bit 1 at position `p`. -/ |
| 55 | | bnd : jobSeqRel 1 |
| 56 | /-- `le a b`: the linear order carrying the place values. -/ |
| 57 | | le : jobSeqRel 2 |
| 58 | deriving DecidableEq |
| 59 | |
| 60 | /-- The relational language of job-sequencing instances: jobs and bit |
| 61 | positions, the bits of each job's execution time, deadline and penalty, the |
| 62 | bits of the penalty bound, and a linear order. -/ |
| 63 | def jobSeq : FirstOrder.Language := |
| 64 | ⟨fun _ => Empty, jobSeqRel⟩ |
| 65 | |
| 66 | instance instIsRelationalJobSeq : FirstOrder.Language.IsRelational jobSeq := fun _ => |
| 67 | (inferInstance : IsEmpty Empty) |
| 68 | |
| 69 | /-- `job j`: `j` is a job. -/ |
| 70 | abbrev jsJob : jobSeq.Relations 1 := |
| 71 | .job |
| 72 | |
| 73 | /-- `posn p`: `p` is a bit position. -/ |
| 74 | abbrev jsPosn : jobSeq.Relations 1 := |
| 75 | .posn |
| 76 | |
| 77 | /-- `time j p`: the execution time of `j` has bit 1 at position `p`. -/ |
| 78 | abbrev jsTime : jobSeq.Relations 2 := |
| 79 | .time |
| 80 | |
| 81 | /-- `dline j p`: the deadline of `j` has bit 1 at position `p`. -/ |
| 82 | abbrev jsDline : jobSeq.Relations 2 := |
| 83 | .dline |
| 84 | |
| 85 | /-- `pen j p`: the penalty of `j` has bit 1 at position `p`. -/ |
| 86 | abbrev jsPen : jobSeq.Relations 2 := |
| 87 | .pen |
| 88 | |
| 89 | /-- `bnd p`: the penalty bound has bit 1 at position `p`. -/ |
| 90 | abbrev jsBnd : jobSeq.Relations 1 := |
| 91 | .bnd |
| 92 | |
| 93 | /-- `le a b`: the linear order carrying the place values. -/ |
| 94 | abbrev jsLe : jobSeq.Relations 2 := |
| 95 | .le |
| 96 | |
| 97 | open FirstOrder |
| 98 | |
| 99 | open Language Structure |
| 100 | |
| 101 | section Shorthands |
| 102 | |
| 103 | variable {A : Type} [jobSeq.Structure A] |
| 104 | |
| 105 | /-- `job j`: `j` is a job. -/ |
| 106 | def JSJob {A : Type} [jobSeq.Structure A] (a0 : A) : Prop := |
| 107 | FirstOrder.Language.Structure.RelMap jsJob ![a0] |
| 108 | |
| 109 | /-- `posn p`: `p` is a bit position. -/ |
| 110 | def JSPosn {A : Type} [jobSeq.Structure A] (a0 : A) : Prop := |
| 111 | FirstOrder.Language.Structure.RelMap jsPosn ![a0] |
| 112 | |
| 113 | /-- `time j p`: the execution time of `j` has bit 1 at position `p`. -/ |
| 114 | def JSTime {A : Type} [jobSeq.Structure A] (a0 : A) (a1 : A) : Prop := |
| 115 | FirstOrder.Language.Structure.RelMap jsTime ![a0, a1] |
| 116 | |
| 117 | /-- `dline j p`: the deadline of `j` has bit 1 at position `p`. -/ |
| 118 | def JSDline {A : Type} [jobSeq.Structure A] (a0 : A) (a1 : A) : Prop := |
| 119 | FirstOrder.Language.Structure.RelMap jsDline ![a0, a1] |
| 120 | |
| 121 | /-- `pen j p`: the penalty of `j` has bit 1 at position `p`. -/ |
| 122 | def JSPen {A : Type} [jobSeq.Structure A] (a0 : A) (a1 : A) : Prop := |
| 123 | FirstOrder.Language.Structure.RelMap jsPen ![a0, a1] |
| 124 | |
| 125 | /-- `bnd p`: the penalty bound has bit 1 at position `p`. -/ |
| 126 | def JSBnd {A : Type} [jobSeq.Structure A] (a0 : A) : Prop := |
| 127 | FirstOrder.Language.Structure.RelMap jsBnd ![a0] |
| 128 | |
| 129 | /-- `le a b`: the linear order carrying the place values. -/ |
| 130 | def JSLe {A : Type} [jobSeq.Structure A] (a0 : A) (a1 : A) : Prop := |
| 131 | FirstOrder.Language.Structure.RelMap jsLe ![a0, a1] |
| 132 | |
| 133 | /-- The execution time of a job, decoded. -/ |
| 134 | noncomputable def JSTimeVal (j : A) : ℕ := binNum JSLe JSPosn (JSTime j) |
| 135 | |
| 136 | /-- The deadline of a job, decoded. -/ |
| 137 | noncomputable def JSDlineVal (j : A) : ℕ := binNum JSLe JSPosn (JSDline j) |
| 138 | |
| 139 | /-- The penalty of a job, decoded. -/ |
| 140 | noncomputable def JSPenVal (j : A) : ℕ := binNum JSLe JSPosn (JSPen j) |
| 141 | |
| 142 | end Shorthands |
| 143 | |
| 144 | /-- The penalty bound of an instance, decoded. -/ |
| 145 | noncomputable def JSBound (A : Type) [jobSeq.Structure A] : ℕ := |
| 146 | binNum (JSLe (A := A)) JSPosn JSBnd |
| 147 | |
| 148 | section Schedule |
| 149 | |
| 150 | variable {A : Type} [jobSeq.Structure A] |
| 151 | |
| 152 | /-- The completion time of a job under a schedule: the total execution time of |
| 153 | the jobs scheduled at or before it. -/ |
| 154 | noncomputable def JSCompletion (sched : A → A → Prop) (j : A) : ℕ := |
| 155 | ∑ᶠ i ∈ {i : A | JSJob i ∧ sched i j}, JSTimeVal i |
| 156 | |
| 157 | /-- A job is late under a schedule when it completes after its deadline. -/ |
| 158 | def JSLate (sched : A → A → Prop) (j : A) : Prop := |
| 159 | JSDlineVal j < JSCompletion sched j |
| 160 | |
| 161 | /-- The total penalty of the jobs a schedule leaves late. -/ |
| 162 | noncomputable def JSPenalty (sched : A → A → Prop) : ℕ := |
| 163 | ∑ᶠ j ∈ {j : A | JSJob j ∧ JSLate sched j}, JSPenVal j |
| 164 | |
| 165 | end Schedule |
| 166 | |
| 167 | section Problem |
| 168 | |
| 169 | variable (A : Type) [jobSeq.Structure A] |
| 170 | |
| 171 | /-- A job-sequencing instance is a yes-instance when its order is a linear |
| 172 | order and some schedule – some linear order on the universe – leaves late only |
| 173 | jobs whose penalties sum to at most the bound. -/ |
| 174 | def HasGoodSchedule : Prop := |
| 175 | Finite A ∧ IsLinOrd (JSLe (A := A)) ∧ |
| 176 | ∃ sched : A → A → Prop, IsLinOrd sched ∧ JSPenalty sched ≤ JSBound A |
| 177 | |
| 178 | end Problem |
| 179 | |
| 180 | open Lax904597.Problems Lax904597.Classes Lax799700.Problems |
| 181 | |
| 182 | /-- The property `HasGoodSchedule` is isomorphism-invariant. -/ |
| 183 | axiom hasGoodSchedule_iso : ∀ {A B : Type} [Lax799700.JobSequencing.jobSeq.Structure A] [Lax799700.JobSequencing.jobSeq.Structure B], |
| 184 | (A ≃[Lax799700.JobSequencing.jobSeq] B) → (HasGoodSchedule A ↔ HasGoodSchedule B) |
| 185 | |
| 186 | /-- The problem JobSequencing: does the structure satisfy `HasGoodSchedule`? -/ |
| 187 | def JobSequencing : DecisionProblem Lax799700.JobSequencing.jobSeq := |
| 188 | DecisionProblem.ofPred HasGoodSchedule |
| 189 | |
| 190 | /-- The yes-instances of JobSequencing are exactly the structures satisfying |
| 191 | `HasGoodSchedule`. -/ |
| 192 | axiom jobSequencing_iff : ∀ (A : Type) [Lax799700.JobSequencing.jobSeq.Structure A], JobSequencing A ↔ HasGoodSchedule A |
| 193 | |
| 194 | /-- JobSequencing is NP-complete. -/ |
| 195 | axiom jobSequencing_NP_complete : NP.Complete JobSequencing |
| 196 | |
| 197 | end Lax799700.JobSequencing |
| 198 |
Used by
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments