While this submission is a draft, it cannot be used by other submissions.

The stacked scheduling instance

Lax391470.StackedConstruction · concepts/Lax391470/StackedConstruction.lean · lax-391470

proven

Loading review…

Sign in with ORCID

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    The scheduling instance built from an instance of AUX(p,q)\mathrm{AUX}(p, q), 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 00.

    Let w=qw = q and let ti=(p+q+w)it_i = -(p + q + w)\, i for i=1,,Ni = 1, \dots, N. For every connected pair ii the instance contains five jobs:

    • a separator with availability interval [ti+p+q,  ti+p+q+w][t_i + p + q,\; t_i + p + q + w] and length ww, which is thereby pinned in place;
    • an inner long job ([ti+q,  dp,i],p)([t_i + q,\; d'_{p,i}],\, p) and an outer long job ([ti,  dp,i],p)([t_i,\; d_{p,i}],\, p);
    • an inner short job ([ti+p,  dq,i],q)([t_i + p,\; d'_{q,i}],\, q) and an outer short job ([ti,  dq,i],q)([t_i,\; d_{q,i}],\, q).

    The ordinary jobs are kept unchanged. The separators cut the time before 00 into NN bins [ti,ti+p+q)[t_i,\, t_i + p + q), 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 00. 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 00 is an inner job and meets an early deadline — the condition on connected pairs.

    Concept map
    3 concepts; 2 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 3 statements. Each proof establishes one of them relative to its assumptions.

    Lean source view on GitHub

    1import Lax391470.AuxiliaryProblem
    2
    3/-!
    4---
    5title: The stacked scheduling instance
    6type: definition
    7---
    8The scheduling instance built from an instance of AUX(p,q)\mathrm{AUX}(p, q), in which the two
    9deadlines of a pending job are expressed by ordinary availability intervals. The
    10construction buys the second deadline with room on the time line before time 00.
    11
    12Let w=qw = q and let ti=(p+q+w)it_i = -(p + q + w)\, i for i=1,,Ni = 1, \dots, N. For every connected
    13pair ii the instance contains five jobs:
    14
    15- a *separator* with availability interval [ti+p+q,  ti+p+q+w][t_i + p + q,\; t_i + p + q + w] and length
    16 ww, which is thereby pinned in place;
    17- an *inner* long job ([ti+q,  dp,i],p)([t_i + q,\; d'_{p,i}],\, p) and an *outer* long job
    18 ([ti,  dp,i],p)([t_i,\; d_{p,i}],\, p);
    19- an *inner* short job ([ti+p,  dq,i],q)([t_i + p,\; d'_{q,i}],\, q) and an *outer* short job
    20 ([ti,  dq,i],q)([t_i,\; d_{q,i}],\, q).
    21
    22The ordinary jobs are kept unchanged. The separators cut the time before 00 into NN
    23*bins* [ti,ti+p+q)[t_i,\, t_i + p + q), each with room for exactly one long and one short job. The
    24availability intervals of the four jobs of a pair are nested, the inner ones carrying
    25the early deadlines. A feasible schedule parks two jobs of each pair in its bin and runs
    26the other two, one long and one short, after time 00. The inner long job and the inner
    27short job of a pair do not fit into its bin together, so one of the two jobs running
    28after 00 is an inner job and meets an early deadline — the condition on connected
    29pairs.
    30
    31# Formalization notes
    32
    33The source leaves the separator length w{p,q}w \in \{p, q\} free; it is fixed to qq here.
    34
    35Jobs are numbered: the ordinary jobs keep their numbers, and the five jobs of pair ii
    36(counted from 00) follow at positions n+5i,,n+5i+4n + 5i, \dots, n + 5i + 4 in the order
    37separator, inner long, outer long, inner short, outer short. With pairs counted from 00
    38the left end of bin ii is (p+2q)(i+1)-(p + 2q)(i + 1).
    39-/
    40
    41namespace Lax391470.StackedConstruction
    42
    43open Lax391470.Scheduling Lax391470.AuxiliaryProblem
    44
    45variable (p q : ℕ) (A : AuxiliaryProblem.Instance)
    46
    47/-- The left end `tᵢ` of the bin of pair `i`, pairs counted from `0`. -/
    48def binStart (i : ℕ) : ℤ := -(((p + 2 * q) * (i + 1) : ℕ) : ℤ)
    49
    50/-- The number of jobs: the ordinary ones and five for every connected pair. -/
    51def numJobs : ℕ := A.ordinary + 5 * A.pairs
    52
    53/-- The pair a job beyond the ordinary ones belongs to. -/
    54def 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
    57job, `2` the outer long job, `3` the inner short job, `4` the outer short job. -/
    58def partOf (j : ℕ) : ℕ := (j - A.ordinary) % 5
    59
    60/-- **The stacked instance** built from `A` at the lengths `p` and `q`. -/
    61def 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.longEarlypairOf A j, hi⟩
    83 | 2 => A.longDuepairOf A j, hi⟩
    84 | 3 => A.shortEarlypairOf A j, hi⟩
    85 | _ => A.shortDuepairOf 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}`. -/
    95axiom 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. -/
    99axiom 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
    103deadline of an ordered instance `A` is at most `T`, every release time and deadline of the
    104stacked instance lies within `T + (p + 2q)N` of `0`, where `N` is the number of pairs.
    105Together with `SatConstruction.times_le`, this bounds every number of the composed
    106reduction by a polynomial in the size of the formula. -/
    107axiom 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
    113end Lax391470.StackedConstruction
    114
    Show ProofShow ProofShow Proof
    Formalization notes

    The source leaves the separator length w{p,q}w \in \{p, q\} free; it is fixed to qq here.

    Jobs are numbered: the ordinary jobs keep their numbers, and the five jobs of pair ii (counted from 00) follow at positions n+5i,,n+5i+4n + 5i, \dots, n + 5i + 4 in the order separator, inner long, outer long, inner short, outer short. With pairs counted from 00 the left end of bin ii is (p+2q)(i+1)-(p + 2q)(i + 1).

    Builds on
    Used by
    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…