Lax Lean Archive

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

The Conflict Graphs of an Instance

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

proven

Loading review…

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

    Let II be an instance with nn clients and mm days. The day ii conflict graph of II is the graph on the nn clients in which two clients are adjacent if their jobs of day ii conflict. The overall conflict graph of II is the graph on the nn clients in which two clients are adjacent if their jobs conflict on at least one day; its edge set is the union of the edge sets of the mm daily graphs.

    A day's conflict graph is the intersection graph of that day's nn intervals, so it is an interval graph. The observation the results of the source rest on is that a set of clients can be served on day ii exactly when it is an independent set of the day ii conflict graph: a schedule is feasible if and only if each of its days is independent in that day's graph.

    The treewidth τ\tau of the overall conflict graph is the structural parameter measured in the last section of the source, and it is the archive's treewidth.

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

    Each proof establishes this claim relative to its assumptions.

    In the paper

    • page 1 of this submission's paper

    Lean source view on GitHub

    1import Lax117284.Scheduling
    2import Lax228581.Treewidth
    3import Mathlib.Combinatorics.SimpleGraph.Clique
    4
    5/-!
    6---
    7title: The Conflict Graphs of an Instance
    8type: definition
    9---
    10Let II be an instance with nn clients and mm days. The *day ii conflict graph* of II
    11is the graph on the nn clients in which two clients are adjacent if their jobs of day ii
    12conflict. The *overall conflict graph* of II is the graph on the nn clients in which two
    13clients are adjacent if their jobs conflict on at least one day; its edge set is the union
    14of the edge sets of the mm daily graphs.
    15
    16A day's conflict graph is the intersection graph of that day's nn intervals, so it is an
    17interval graph. The observation the results of the source rest on is that a set of clients
    18can be served on day ii exactly when it is an independent set of the day ii conflict
    19graph: a schedule is feasible if and only if each of its days is independent in that day's
    20graph.
    21
    22The treewidth τ\tau of the overall conflict graph is the structural parameter measured in
    23the last section of the source, and it is the archive's treewidth.
    24
    25# Formalization Notes
    26
    27Both graphs are irreflexive by construction, the adjacency conjoining distinctness of the
    28two clients: a job always conflicts with itself, which carries no information about the
    29instance.
    30
    31Interval graphs are not defined here. A day's conflict graph is an interval graph by
    32construction, and the only property of interval graphs that is used is that such a graph
    33can be coloured with as many colours as its largest clique has vertices, which is a
    34statement about these graphs and is proved as one.
    35-/
    36
    37namespace Lax117284.ConflictGraph
    38
    39open Lax117284.Scheduling
    40
    41/-- Conflict is a symmetric relation: the two jobs share a time point either way. -/
    42theorem conflict_symm {I : Instance} {i : Fin I.days} {j j' : Fin I.clients}
    43 (h : I.Conflict i j j') : I.Conflict i j' j :=
    44 let ⟨t, ht⟩ := h; ⟨t, ht.2, ht.1⟩
    45
    46variable (I : Instance)
    47
    48/-- **The day `i` conflict graph** of `I`: two distinct clients are adjacent when their
    49jobs of day `i` conflict. -/
    50def dayGraph (i : Fin I.days) : SimpleGraph (Fin I.clients) where
    51 Adj j j' := j ≠ j' ∧ I.Conflict i j j'
    52 symm := ⟨fun _ _ h => ⟨h.1.symm, conflict_symm h.2⟩⟩
    53 loopless := ⟨fun _ h => h.1 rfl⟩
    54
    55/-- **The overall conflict graph** of `I`: two distinct clients are adjacent when their
    56jobs conflict on some day. -/
    57def overallGraph : SimpleGraph (Fin I.clients) where
    58 Adj j j' := j ≠ j' ∧ ∃ i, I.Conflict i j j'
    59 symm := ⟨fun _ _ h => ⟨h.1.symm, h.2.imp fun _ => conflict_symm⟩⟩
    60 loopless := ⟨fun _ h => h.1 rfl⟩
    61
    62/-- The treewidth `τ` of the overall conflict graph of `I`. -/
    63noncomputable def treewidth : ℕ := Lax228581.Treewidth.treewidth (overallGraph I)
    64
    65/-- **A schedule is feasible exactly when every day's set of clients is an independent set
    66of that day's conflict graph.** -/
    67axiom feasible_iff_isIndepSet {I : Instance} (σ : I.Schedule) :
    68 Instance.Feasible σ ↔ ∀ i, (dayGraph I i).IsIndepSet (σ i : Set (Fin I.clients))
    69
    70end Lax117284.ConflictGraph
    71
    Show Proof
    Formalization Notes

    Both graphs are irreflexive by construction, the adjacency conjoining distinctness of the two clients: a job always conflicts with itself, which carries no information about the instance.

    Interval graphs are not defined here. A day's conflict graph is an interval graph by construction, and the only property of interval graphs that is used is that such a graph can be coloured with as many colours as its largest clique has vertices, which is a statement about these graphs and is proved as one.

    Builds on
    Used by
    From Mathlib

    Discussion

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

    Loading discussion…