Unit Processing Times as a Bipartite Matching Problem
Lax117284.Theorem10 · concepts/Lax117284/Theorem10.lean · lax-117284
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Theorem 10. Let be an instance all of whose processing times are and let . Consider the bipartite graph whose one side holds a vertex for every day and client , and whose other side holds a vertex for every day and time together with vertices for every client ; join to and to all vertices . Then admits a -fair schedule if and only if this graph has a matching saturating every vertex .
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 to records that client is served on day , and matching it to one of the vertices 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 rejections client is allowed.
Concept map
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
| 1 | import Lax117284.Scheduling |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Unit Processing Times as a Bipartite Matching Problem |
| 6 | type: theorem |
| 7 | --- |
| 8 | **Theorem 10.** Let be an instance all of whose processing times are and let |
| 9 | . Consider the bipartite graph whose one side holds a vertex for every |
| 10 | day and client , and whose other side holds a vertex for every day and |
| 11 | time together with vertices for every client ; |
| 12 | join to and to all vertices . Then admits a |
| 13 | -fair schedule if and only if this graph has a matching saturating every vertex |
| 14 | . |
| 15 | |
| 16 | With unit processing times two jobs of a day conflict exactly when their due dates agree, |
| 17 | so a day's machine may execute at most one job per due date; matching to |
| 18 | records that client is served on day , and matching it to one of the |
| 19 | vertices records that it is not. A matching saturating the job side |
| 20 | thus assigns every job either a slot of its day or one of the rejections client is |
| 21 | allowed. |
| 22 | |
| 23 | # Formalization Notes |
| 24 | |
| 25 | A matching saturating the vertices of the job side is an injective map from that side |
| 26 | whose values are neighbours of their arguments; stating it this way needs no cardinality |
| 27 | argument to see that the matching has edges. |
| 28 | |
| 29 | The far side is presented as a sum of the two families of vertices, and its time vertices |
| 30 | are indexed by a natural number, of which only the due dates occurring in the instance are |
| 31 | ever matched. |
| 32 | -/ |
| 33 | |
| 34 | namespace Lax117284.Theorem10 |
| 35 | |
| 36 | open Lax117284.Scheduling |
| 37 | |
| 38 | variable (I : Instance) |
| 39 | |
| 40 | /-- The far side of the bipartite graph: a slot vertex `u_{i,t}` for a day and a time, and |
| 41 | a rejection vertex `w_{l,j}` for a client. -/ |
| 42 | def 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 |
| 45 | of its own day and due date, and to the `m - k` rejection vertices of its own client. -/ |
| 46 | def 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. -/ |
| 50 | def 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 |
| 55 | agree.** -/ |
| 56 | axiom 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 |
| 60 | exactly when the bipartite graph has a matching saturating every job vertex. -/ |
| 61 | axiom hasKFairSchedule_iff_hasFullMatching {I : Instance} (h : I.UnitP) {k : ℕ} |
| 62 | (hk : k ≤ I.days) : I.HasKFairSchedule k ↔ HasFullMatching I k |
| 63 | |
| 64 | end Lax117284.Theorem10 |
| 65 |
Formalization Notes
A matching saturating the 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 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.
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments