Time reversal
Lax434175.TimeReversal · concepts/Lax434175/TimeReversal.lean · lax-434175
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Running a schedule backwards from a horizon turns a piece processing an operation during into one processing it during . A job that completes at then starts at , and a precedence constraint becomes the constraint of the reversed relation.
Hence the maximum lateness without release dates and the makespan with release dates are equivalent:
- for due dates exactly if the reversed problem with release dates , , has makespan at most (if some is negative, or there are no jobs and is negative, the threshold is );
- for release dates exactly if the reversed problem without release dates and with due dates has maximum lateness at most (if is negative or some exceeds , the answer is no, and the reduction asks whether the maximum lateness for due dates is at most ).
This is shown for the problems of the family with operations that have one operation per job, no restarts, a reversible precedence class, no deadlines, and none of the communication delays, server, forbidden times, transportation delays, no-idle and batch setups, whose meaning changes under reversal. The reversed specification has the reversed precedence class, the release dates or none, and the makespan or the maximum lateness.
A specification reduces to by reversal if it is of this kind, and either minimizes the maximum lateness without release dates and its reversal with release dates and the makespan is field by field a special case of , or minimizes the makespan with release dates or none and its reversal without release dates and with the maximum lateness is so. The relation is decidable.
Theorem. A specification that reduces to another by reversal describes a problem whose decision version reduces to that of the other.
Concept map
Evidence
Each proof establishes this claim relative to its assumptions.
Lean source view on GitHub
| 1 | import Lax434175.DeadlineSteps |
| 2 | import Lax434175.PrecedenceReversal |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Time reversal |
| 7 | type: theorem |
| 8 | --- |
| 9 | Running a schedule backwards from a horizon turns a piece processing an |
| 10 | operation during into one processing it during . A |
| 11 | job that completes at then starts at , and a precedence |
| 12 | constraint becomes the constraint |
| 13 | of the reversed relation. |
| 14 | |
| 15 | Hence the maximum lateness without release dates and the makespan with |
| 16 | release dates are equivalent: |
| 17 | |
| 18 | - for due dates exactly if the reversed problem with |
| 19 | release dates , , has makespan |
| 20 | at most (if some is negative, or there are no jobs and is |
| 21 | negative, the threshold is ); |
| 22 | - for release dates exactly if the reversed problem |
| 23 | without release dates and with due dates has maximum lateness at |
| 24 | most (if is negative or some exceeds , the answer is no, |
| 25 | and the reduction asks whether the maximum lateness for due dates is at |
| 26 | most ). |
| 27 | |
| 28 | This is shown for the problems of the family with operations that have one |
| 29 | operation per job, no restarts, a reversible precedence class, no deadlines, |
| 30 | and none of the communication delays, server, forbidden times, transportation |
| 31 | delays, no-idle and batch setups, whose meaning changes under reversal. The |
| 32 | reversed specification has the reversed precedence class, the release dates |
| 33 | or none, and the makespan or the maximum lateness. |
| 34 | |
| 35 | A specification reduces to by reversal if it is of this kind, and |
| 36 | either minimizes the maximum lateness without release dates and its reversal |
| 37 | with release dates and the makespan is field by field a special case of , |
| 38 | or minimizes the makespan with release dates or none and its reversal without |
| 39 | release dates and with the maximum lateness is so. The relation is decidable. |
| 40 | |
| 41 | **Theorem.** A specification that reduces to another by reversal describes a |
| 42 | problem whose decision version reduces to that of the other. |
| 43 | -/ |
| 44 | |
| 45 | namespace Lax434175.TimeReversal |
| 46 | open Lax434175.Problems Lax434175.Assembly |
| 47 | open Lax434175 Lax434175.Operations Lax434175.OperationsFamily |
| 48 | |
| 49 | def isSingle : Structure → Bool |
| 50 | | .single => true |
| 51 | | _ => false |
| 52 | |
| 53 | def notRestarts : Interruption.Mode → Bool |
| 54 | | .restarts => false |
| 55 | | _ => true |
| 56 | |
| 57 | def noDelays : CommunicationDelays.Value → Bool |
| 58 | | .none => true |
| 59 | | _ => false |
| 60 | |
| 61 | def noServer : Servers.Value → Bool |
| 62 | | .none => true |
| 63 | | _ => false |
| 64 | |
| 65 | def noForbidden : ForbiddenTimes.Value → Bool |
| 66 | | .none => true |
| 67 | | _ => false |
| 68 | |
| 69 | def noTransport (v : Transportation.Value) : Bool := |
| 70 | (match v.shape with |
| 71 | | .none => true |
| 72 | | _ => false) && !v.robot |
| 73 | |
| 74 | def noIdling : ShopExtras.NoIdle → Bool |
| 75 | | .none => true |
| 76 | | _ => false |
| 77 | |
| 78 | def noSetups : ShopExtras.BatchSetups → Bool |
| 79 | | .none => true |
| 80 | | _ => false |
| 81 | |
| 82 | def releaseNone : ReleaseDates.Value → Bool |
| 83 | | .none => true |
| 84 | | _ => false |
| 85 | |
| 86 | def releaseKnown : ReleaseDates.Value → Bool |
| 87 | | .online => false |
| 88 | | _ => true |
| 89 | |
| 90 | /-- The specification can be reversed. -/ |
| 91 | def Reversible (s : Spec family) : Bool := |
| 92 | notRestarts (s.module .interruption) && isSingle (s.module .jobStructure) && |
| 93 | PrecedenceReversal.reversible (s.module .precedence).order && DeadlineSteps.noDeadlines (s.module .deadlines) && |
| 94 | noDelays (s.module .communicationDelays) && noServer (s.module .server) && |
| 95 | noForbidden (s.module .forbiddenTimes) && noTransport (s.module .transportation) && |
| 96 | noIdling (s.module .noIdle) && noSetups (s.module .batchSetups) |
| 97 | |
| 98 | /-- The reversed specification, with given release dates and objective. -/ |
| 99 | def reversed (s : Spec family) (release : ReleaseDates.Value) (objective : Objectives.Value) : |
| 100 | Spec family where |
| 101 | module |
| 102 | | .precedence => (⟨PrecedenceReversal.reverse (s.module .precedence).order, (s.module .precedence).lags⟩ : |
| 103 | Precedence.Value) |
| 104 | | .releaseDates => release |
| 105 | | i => s.module i |
| 106 | objective := objective |
| 107 | |
| 108 | /-- `s` reduces to `t` by reversal. -/ |
| 109 | def ReducesByReversal (s t : Spec family) : Prop := |
| 110 | Reversible s = true ∧ |
| 111 | ((Thresholds.objectiveOf s = .lmax ∧ releaseNone (s.module .releaseDates) = true ∧ |
| 112 | (reversed s .releaseDates .makespan).le t) ∨ |
| 113 | (Thresholds.objectiveOf s = .makespan ∧ releaseKnown (s.module .releaseDates) = true ∧ |
| 114 | (reversed s .none .lmax).le t)) |
| 115 | |
| 116 | instance (s t : Spec family) : Decidable (ReducesByReversal s t) := by |
| 117 | unfold ReducesByReversal |
| 118 | infer_instance |
| 119 | |
| 120 | axiom reducible_of_reducesByReversal {s t : Spec family} : |
| 121 | ReducesByReversal s t → Reducible (problem family s) (problem family t) |
| 122 | |
| 123 | end Lax434175.TimeReversal |
| 124 |
Used by
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments