The stacked scheduling instance
Lax391470.StackedConstruction · concepts/Lax391470/StackedConstruction.lean · lax-391470
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
The scheduling instance built from an instance of , in which the two deadlines of a pending job are expressed by ordinary availability intervals. The construction buys the second deadline with room on the time line before time .
Let and let for . For every connected pair the instance contains five jobs:
- a separator with availability interval and length , which is thereby pinned in place;
- an inner long job and an outer long job ;
- an inner short job and an outer short job .
The ordinary jobs are kept unchanged. The separators cut the time before into bins , each with room for exactly one long and one short job. The availability intervals of the four jobs of a pair are nested, the inner ones carrying the early deadlines. A feasible schedule parks two jobs of each pair in its bin and runs the other two, one long and one short, after time . The inner long job and the inner short job of a pair do not fit into its bin together, so one of the two jobs running after is an inner job and meets an early deadline — the condition on connected pairs.
Concept map
Evidence
Lean source view on GitHub
| 1 | import Lax391470.AuxiliaryProblem |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: The stacked scheduling instance |
| 6 | type: definition |
| 7 | --- |
| 8 | The scheduling instance built from an instance of , in which the two |
| 9 | deadlines of a pending job are expressed by ordinary availability intervals. The |
| 10 | construction buys the second deadline with room on the time line before time . |
| 11 | |
| 12 | Let and let for . For every connected |
| 13 | pair the instance contains five jobs: |
| 14 | |
| 15 | - a *separator* with availability interval and length |
| 16 | , which is thereby pinned in place; |
| 17 | - an *inner* long job and an *outer* long job |
| 18 | ; |
| 19 | - an *inner* short job and an *outer* short job |
| 20 | . |
| 21 | |
| 22 | The ordinary jobs are kept unchanged. The separators cut the time before into |
| 23 | *bins* , each with room for exactly one long and one short job. The |
| 24 | availability intervals of the four jobs of a pair are nested, the inner ones carrying |
| 25 | the early deadlines. A feasible schedule parks two jobs of each pair in its bin and runs |
| 26 | the other two, one long and one short, after time . The inner long job and the inner |
| 27 | short job of a pair do not fit into its bin together, so one of the two jobs running |
| 28 | after is an inner job and meets an early deadline — the condition on connected |
| 29 | pairs. |
| 30 | |
| 31 | # Formalization notes |
| 32 | |
| 33 | The source leaves the separator length free; it is fixed to here. |
| 34 | |
| 35 | Jobs are numbered: the ordinary jobs keep their numbers, and the five jobs of pair |
| 36 | (counted from ) follow at positions in the order |
| 37 | separator, inner long, outer long, inner short, outer short. With pairs counted from |
| 38 | the left end of bin is . |
| 39 | -/ |
| 40 | |
| 41 | namespace Lax391470.StackedConstruction |
| 42 | |
| 43 | open Lax391470.Scheduling Lax391470.AuxiliaryProblem |
| 44 | |
| 45 | variable (p q : ℕ) (A : AuxiliaryProblem.Instance) |
| 46 | |
| 47 | /-- The left end `tᵢ` of the bin of pair `i`, pairs counted from `0`. -/ |
| 48 | def binStart (i : ℕ) : ℤ := -(((p + 2 * q) * (i + 1) : ℕ) : ℤ) |
| 49 | |
| 50 | /-- The number of jobs: the ordinary ones and five for every connected pair. -/ |
| 51 | def numJobs : ℕ := A.ordinary + 5 * A.pairs |
| 52 | |
| 53 | /-- The pair a job beyond the ordinary ones belongs to. -/ |
| 54 | def pairOf (j : ℕ) : ℕ := (j - A.ordinary) / 5 |
| 55 | |
| 56 | /-- Which of the five jobs of its pair a job is: `0` the separator, `1` the inner long |
| 57 | job, `2` the outer long job, `3` the inner short job, `4` the outer short job. -/ |
| 58 | def partOf (j : ℕ) : ℕ := (j - A.ordinary) % 5 |
| 59 | |
| 60 | /-- **The stacked instance** built from `A` at the lengths `p` and `q`. -/ |
| 61 | def inst : Scheduling.Instance where |
| 62 | jobs := numJobs A |
| 63 | r j := |
| 64 | if h : (j : ℕ) < A.ordinary then A.r ⟨j, h⟩ |
| 65 | else |
| 66 | binStart p q (pairOf A j) + |
| 67 | match partOf A j with |
| 68 | | 0 => (p + q : ℕ) |
| 69 | | 1 => (q : ℕ) |
| 70 | | 2 => 0 |
| 71 | | 3 => (p : ℕ) |
| 72 | | _ => 0 |
| 73 | d j := |
| 74 | if h : (j : ℕ) < A.ordinary then A.d ⟨j, h⟩ |
| 75 | else |
| 76 | have hi : pairOf A j < A.pairs := by |
| 77 | have := j.isLt |
| 78 | simp only [pairOf, numJobs] at * |
| 79 | omega |
| 80 | match partOf A j with |
| 81 | | 0 => binStart p q (pairOf A j) + (p + 2 * q : ℕ) |
| 82 | | 1 => A.longEarly ⟨pairOf A j, hi⟩ |
| 83 | | 2 => A.longDue ⟨pairOf A j, hi⟩ |
| 84 | | 3 => A.shortEarly ⟨pairOf A j, hi⟩ |
| 85 | | _ => A.shortDue ⟨pairOf A j, hi⟩ |
| 86 | p j := |
| 87 | if h : (j : ℕ) < A.ordinary then (if A.long ⟨j, h⟩ then p else q) |
| 88 | else |
| 89 | match partOf A j with |
| 90 | | 1 => p |
| 91 | | 2 => p |
| 92 | | _ => q |
| 93 | |
| 94 | /-- The stacked instance is on the lengths `{p, q}`. -/ |
| 95 | axiom lengthsIn : (inst p q A).LengthsIn p q |
| 96 | |
| 97 | /-- **The construction is correct.** For job lengths `p > q ≥ 1`, an ordered instance of |
| 98 | `AUX(p, q)` has a solution exactly when the stacked instance has a feasible schedule. -/ |
| 99 | axiom correct (hq : 0 < q) (hqp : q < p) (hA : A.Ordered) : |
| 100 | A.Solvable p q ↔ (inst p q A).Schedulable |
| 101 | |
| 102 | /-- **The numbers of the stacked instance are small**: if every release time and every |
| 103 | deadline of an ordered instance `A` is at most `T`, every release time and deadline of the |
| 104 | stacked instance lies within `T + (p + 2q)N` of `0`, where `N` is the number of pairs. |
| 105 | Together with `SatConstruction.times_le`, this bounds every number of the composed |
| 106 | reduction by a polynomial in the size of the formula. -/ |
| 107 | axiom times_le (hA : A.Ordered) (T : ℕ) |
| 108 | (hT : (∀ o, A.r o ≤ T ∧ A.d o ≤ T) ∧ |
| 109 | (∀ i, A.longDue i ≤ T ∧ A.shortDue i ≤ T)) : |
| 110 | ∀ j, |(inst p q A).r j| ≤ ((T + (p + 2 * q) * A.pairs : ℕ) : ℤ) ∧ |
| 111 | |(inst p q A).d j| ≤ ((T + (p + 2 * q) * A.pairs : ℕ) : ℤ) |
| 112 | |
| 113 | end Lax391470.StackedConstruction |
| 114 |
Formalization notes
The source leaves the separator length free; it is fixed to here.
Jobs are numbered: the ordinary jobs keep their numbers, and the five jobs of pair (counted from ) follow at positions in the order separator, inner long, outer long, inner short, outer short. With pairs counted from the left end of bin is .
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments