Lax Lean Archive

Maximum cuts

Lax762056.MaxCut · concepts/Lax762056/MaxCut.lean · lax-762056

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 Lax762056.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 Lax762056.MaxCut
    16
    17open Finset
    18
    19noncomputable def edges {n : ℕ} (F : SimpleGraph (Fin n)) :
    20 Finset (Fin n × Fin n) := by
    21 classical
    22 exact univ.filter fun e => e.1 < e.2 ∧ F.Adj e.1 e.2
    23
    24noncomputable def cutSize {n : ℕ} (F : SimpleGraph (Fin n))
    25 (S : Finset (Fin n)) : ℕ := by
    26 classical
    27 exact ((edges F).filter fun e =>
    28 (e.1 ∈ S ∧ e.2 ∉ S) ∨ (e.1 ∉ S ∧ e.2 ∈ S)).card
    29
    30noncomputable def maxCut {n : ℕ} (F : SimpleGraph (Fin n)) : ℕ :=
    31 (univ : Finset (Fin n)).powerset.sup (cutSize F)
    32
    33end Lax762056.MaxCut
    34
    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…