Documentation

Complexity.Computability.Circuit.BipartiteMatching

Bipartite perfect matching #

A bipartite graph with n left and n right vertices is a subgraph of the complete bipartite graph K_{n,n}, given by the indicator of its edges, one bit for each pair (i, j) of a left vertex i and a right vertex j (Cslib.Circuits.BipartiteMatching.graph, numbering the pairs by finProdFinEquiv). It has a perfect matching when some bijection σ from the left to the right vertices uses only edges, (i, σ i) for every i (BipartiteMatching.HasPerfectMatching). The bipartite perfect matching function Cslib.Circuits.bipartitePerfectMatching n of the n * n possible edges says whether the graph has a perfect matching. It is monotone (monotone_bipartitePerfectMatching): adding edges keeps a perfect matching.

Relabelling the left and the right vertices along bijections preserves perfect matchings (BipartiteMatching.hasPerfectMatching_comp_iff). A graph has no perfect matching when a set of left vertices has fewer neighbours (BipartiteMatching.not_hasPerfectMatching_of_card_lt), the easy direction of Hall's theorem; Hall's theorem itself, from Mathlib's Finset.all_card_le_biUnion_card_iff_existsInjective', says that a perfect matching exists exactly when every set of left vertices has at least as many neighbours (BipartiteMatching.hasPerfectMatching_iff_forall_card_le).

Main definitions #

Main results #

References #

source
def Cslib.Circuits.BipartiteMatching.HasPerfectMatching {V : Type u_1} (G : V × V → Bool) :
Prop

A bipartite graph whose left and right vertices are both indexed by V, given by the indicator of its edges (left, right), has a perfect matching: a bijection σ from the left to the right vertices with (v, σ v) an edge for every v.

Instances For
    source
    @[instance_reducible]
    instance Cslib.Circuits.BipartiteMatching.instDecidableHasPerfectMatchingOfFintypeOfDecidableEq {V : Type u_1} [Fintype V] [DecidableEq V] (G : V × V → Bool) :
    Decidable (HasPerfectMatching G)
    source
    theorem Cslib.Circuits.BipartiteMatching.hasPerfectMatching_comp_iff {V : Type u_1} {W : Type u_2} (hL hR : W ≃ V) (G : V × V → Bool) :
    (HasPerfectMatching fun (e : W × W) => G (hL e.1, hR e.2)) ↔ HasPerfectMatching G

    Relabelling the left vertices along hL and the right vertices along hR preserves perfect matchings.

    source
    theorem Cslib.Circuits.BipartiteMatching.not_hasPerfectMatching_of_card_lt {V : Type u_1} {G : V × V → Bool} {S T : Finset V} (hST : ∀ v ∈ S, ∀ (w : V), G (v, w) = true → w ∈ T) (hcard : T.card < S.card) :
    ¬HasPerfectMatching G

    Hall's condition is necessary: if the edges from a set S of left vertices all end in a set T of fewer right vertices, the graph has no perfect matching.

    source
    theorem Cslib.Circuits.BipartiteMatching.hasPerfectMatching_iff_forall_card_le {V : Type u_1} [Fintype V] [DecidableEq V] (G : V × V → Bool) :
    HasPerfectMatching G ↔ ∀ (S : Finset V), S.card ≤ (S.biUnion fun (v : V) => {w : V | G (v, w) = true}).card

    Hall's theorem for bipartite graphs on V × V: a perfect matching exists exactly when every set of left vertices has at least as many neighbours.

    source
    theorem Cslib.Circuits.BipartiteMatching.HasPerfectMatching.mono {V : Type u_1} {G H : V × V → Bool} (hG : HasPerfectMatching G) (h : G ≤ H) :
    HasPerfectMatching H

    Adding edges keeps a perfect matching.

    source
    def Cslib.Circuits.BipartiteMatching.graph {n : ℕ} (x : BitString (n * n)) :
    Fin n × Fin n → Bool

    The bipartite graph of an input: the left vertex i and the right vertex j are adjacent when the bit numbered finProdFinEquiv (i, j) is one.

    Instances For
      source
      def Cslib.Circuits.bipartitePerfectMatching (n : ℕ) :
      BooleanFunction (n * n)

      The bipartite perfect matching function of the n * n possible edges of the complete bipartite graph K_{n,n}: whether the graph of the input (BipartiteMatching.graph) has a perfect matching.

      Instances For
        source
        theorem Cslib.Circuits.bipartitePerfectMatching_eq_true_iff {n : ℕ} {x : BitString (n * n)} :
        bipartitePerfectMatching n x = true ↔ BipartiteMatching.HasPerfectMatching (BipartiteMatching.graph x)

        The bipartite perfect matching function is true exactly on graphs with a perfect matching.

        source
        theorem Cslib.Circuits.monotone_bipartitePerfectMatching {n : ℕ} :
        Monotone (bipartitePerfectMatching n)

        The bipartite perfect matching function is monotone: adding edges keeps a perfect matching.