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

Unit Processing Times as a Bipartite Matching Problem

Lax117284.Theorem10 · concepts/Lax117284/Theorem10.lean · lax-117284

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

    Theorem

    Theorem 10. Let II be an instance all of whose processing times are 11 and let k≤mk \le m. Consider the bipartite graph whose one side holds a vertex vi,jv_{i,j} for every day ii and client jj, and whose other side holds a vertex ui,tu_{i,t} for every day ii and time tt together with m−km - k vertices w1,j,…,wm−k,jw_{1,j}, \ldots, w_{m-k,j} for every client jj; join vi,jv_{i,j} to ui,di,ju_{i,d_{i,j}} and to all m−km-k vertices w⋅,jw_{\cdot,j}. Then II admits a kk-fair schedule if and only if this graph has a matching saturating every vertex vi,jv_{i,j}.

    With unit processing times two jobs of a day conflict exactly when their due dates agree, so a day's machine may execute at most one job per due date; matching vi,jv_{i,j} to ui,di,ju_{i,d_{i,j}} records that client jj is served on day ii, and matching it to one of the m−km-k vertices w⋅,jw_{\cdot,j} records that it is not. A matching saturating the job side thus assigns every job either a slot of its day or one of the m−km-k rejections client jj is allowed.

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

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

    1 conflict_iff_d_eq_of_unitP proven

    2 hasKFairSchedule_iff_hasFullMatching proven

    In the paper

    • page 2 of this submission's paper

    Lean source view on GitHub

    1import Lax117284.Scheduling
    2
    3/-!
    4---
    5title: Unit Processing Times as a Bipartite Matching Problem
    6type: theorem
    7---
    8**Theorem 10.** Let II be an instance all of whose processing times are 11 and let
    9k≤mk \le m. Consider the bipartite graph whose one side holds a vertex vi,jv_{i,j} for every
    10day ii and client jj, and whose other side holds a vertex ui,tu_{i,t} for every day ii and
    11time tt together with m−km - k vertices w1,j,…,wm−k,jw_{1,j}, \ldots, w_{m-k,j} for every client jj;
    12join vi,jv_{i,j} to ui,di,ju_{i,d_{i,j}} and to all m−km-k vertices w⋅,jw_{\cdot,j}. Then II admits a
    13kk-fair schedule if and only if this graph has a matching saturating every vertex
    14vi,jv_{i,j}.
    15
    16With unit processing times two jobs of a day conflict exactly when their due dates agree,
    17so a day's machine may execute at most one job per due date; matching vi,jv_{i,j} to
    18ui,di,ju_{i,d_{i,j}} records that client jj is served on day ii, and matching it to one of the
    19m−km-k vertices w⋅,jw_{\cdot,j} records that it is not. A matching saturating the job side
    20thus assigns every job either a slot of its day or one of the m−km-k rejections client jj is
    21allowed.
    22
    23# Formalization Notes
    24
    25A matching saturating the nmn m vertices of the job side is an injective map from that side
    26whose values are neighbours of their arguments; stating it this way needs no cardinality
    27argument to see that the matching has nmnm edges.
    28
    29The far side is presented as a sum of the two families of vertices, and its time vertices
    30are indexed by a natural number, of which only the due dates occurring in the instance are
    31ever matched.
    32-/
    33
    34namespace Lax117284.Theorem10
    35
    36open Lax117284.Scheduling
    37
    38variable (I : Instance)
    39
    40/-- The far side of the bipartite graph: a slot vertex `u_{i,t}` for a day and a time, and
    41a rejection vertex `w_{l,j}` for a client. -/
    42def Target : Type := (Fin I.days × ℕ) ⊕ (ℕ × Fin I.clients)
    43
    44/-- The edges of the bipartite graph: the job vertex `v_{i,j}` is joined to the slot vertex
    45of its own day and due date, and to the `m - k` rejection vertices of its own client. -/
    46def Matchable (k : ℕ) (v : Fin I.days × Fin I.clients) (t : Target I) : Prop :=
    47 t = Sum.inl (v.1, I.d v.1 v.2) ∨ ∃ l < I.days - k, t = Sum.inr (l, v.2)
    48
    49/-- The bipartite graph has a matching saturating every job vertex. -/
    50def HasFullMatching (k : ℕ) : Prop :=
    51 ∃ f : Fin I.days × Fin I.clients → Target I,
    52 Function.Injective f ∧ ∀ v, Matchable I k v (f v)
    53
    54/-- **With unit processing times, two jobs of a day conflict exactly when their due dates
    55agree.** -/
    56axiom conflict_iff_d_eq_of_unitP {I : Instance} (h : I.UnitP) (i : Fin I.days)
    57 (j j' : Fin I.clients) : I.Conflict i j j' ↔ I.d i j = I.d i j'
    58
    59/-- **Theorem 10.** With unit processing times and `k ≤ m`, a `k`-fair schedule exists
    60exactly when the bipartite graph has a matching saturating every job vertex. -/
    61axiom hasKFairSchedule_iff_hasFullMatching {I : Instance} (h : I.UnitP) {k : ℕ}
    62 (hk : k ≤ I.days) : I.HasKFairSchedule k ↔ HasFullMatching I k
    63
    64end Lax117284.Theorem10
    65
    Show ProofShow Proof
    Formalization Notes

    A matching saturating the nmn m vertices of the job side is an injective map from that side whose values are neighbours of their arguments; stating it this way needs no cardinality argument to see that the matching has nmnm edges.

    The far side is presented as a sum of the two families of vertices, and its time vertices are indexed by a natural number, of which only the due dates occurring in the instance are ever matched.

    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…