Lax Lean Archive

Maximum cuts

Lax222097.MaxCut · concepts/Lax222097/MaxCut.lean · lax-222097

definition

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

    For a graph FF on an ordered vertex set, each edge is represented once, by its endpoints u<vu<v. A cut is specified by a subset SS of vertices; its size is the number of edges with exactly one endpoint in SS. MaxCut⁡(F)\operatorname{MaxCut}(F) is the largest such size, with value zero for an edgeless graph.

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

    In the paper

    • page 3 of this submission's paper

    Lean source view on GitHub

    1import Lax222097.GraphEncoding
    2
    3/-!
    4---
    5title: Maximum cuts
    6type: definition
    7---
    8For a graph FF on an ordered vertex set, each edge is represented once, by
    9its endpoints u<vu<v. A cut is specified by a subset SS of vertices; its size
    10is the number of edges with exactly one endpoint in SS.
    11MaxCut⁡(F)\operatorname{MaxCut}(F) is the largest such size, with value zero for an
    12edgeless graph.
    13-/
    14
    15namespace Lax222097.MaxCut
    16
    17open scoped Classical
    18
    19open Finset
    20
    21/-- All edges, each listed once with its smaller endpoint first. -/
    22noncomputable def edges {n : ℕ} (F : SimpleGraph (Fin n)) :
    23 Finset (Fin n × Fin n) :=
    24 univ.filter fun e => e.1 < e.2 ∧ F.Adj e.1 e.2
    25
    26/-- The number of edges crossing between `S` and its complement. -/
    27noncomputable def cutSize {n : ℕ} (F : SimpleGraph (Fin n))
    28 (S : Finset (Fin n)) : ℕ :=
    29 ((edges F).filter fun e =>
    30 (e.1 ∈ S ∧ e.2 ∉ S) ∨ (e.1 ∉ S ∧ e.2 ∈ S)).card
    31
    32/-- The largest cut size over all subsets of vertices. -/
    33noncomputable def maxCut {n : ℕ} (F : SimpleGraph (Fin n)) : ℕ :=
    34 (univ : Finset (Fin n)).powerset.sup (cutSize F)
    35
    36end Lax222097.MaxCut
    37
    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…