Lax Lean Archive

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

The independent-set relaxation and its exact hull

Lax263307.LinearRelaxation · concepts/Lax263307/LinearRelaxation.lean · lax-263307

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 an nn-vertex graph GG, target kk, and level rr, the relaxation Rr(G,k)R_r(G,k) has coordinates yAy_A for vertex sets ∣A∣≤r+2|A|\le r+2 and constraints

    y∅=1,0≤yA≤1,y_\varnothing=1,\qquad 0\le y_A\le1,yA∪{v}≤yA(∣A∣≤r+1),y_{A\cup\{v\}}\le y_A\quad (|A|\le r+1),yA=0if A is not independent,y_A=0\quad\text{if }A\text{ is not independent},∑vyA∪{v}=kyA(∣A∣≤r+1).\sum_v y_{A\cup\{v\}}=k y_A\quad (|A|\le r+1).

    The exact hull Pr(G,k)P_r(G,k) is the convex hull of the vectors yA=1[A⊆I]y_A=\mathbf1[A\subseteq I] over independent sets II of size kk. For yA>0y_A>0, conditioning on AA gives costs xv=yA∪{v}/yAx_v=y_{A\cup\{v\}}/y_A.

    Concept map
    1 concept
    100%
    DefinitionThis conceptDescendants are omitted for concepts with more than 10 descendants.

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Clique
    2import Mathlib.Analysis.Convex.Hull
    3import Mathlib.Data.Real.Basic
    4
    5/-!
    6---
    7title: The independent-set relaxation and its exact hull
    8type: definition
    9---
    10For an nn-vertex graph GG, target kk, and level rr, the relaxation
    11Rr(G,k)R_r(G,k) has coordinates yAy_A for vertex sets ∣A∣≤r+2|A|\le r+2 and constraints
    12y∅=1,0≤yA≤1,y_\varnothing=1,\qquad 0\le y_A\le1,
    13yA∪{v}≤yA(∣A∣≤r+1),y_{A\cup\{v\}}\le y_A\quad (|A|\le r+1),
    14yA=0if A is not independent,y_A=0\quad\text{if }A\text{ is not independent},
    15∑vyA∪{v}=kyA(∣A∣≤r+1).\sum_v y_{A\cup\{v\}}=k y_A\quad (|A|\le r+1).
    16The exact hull Pr(G,k)P_r(G,k) is the convex hull of the vectors
    17yA=1[A⊆I]y_A=\mathbf1[A\subseteq I] over independent sets II of size kk.
    18For yA>0y_A>0, conditioning on AA gives costs xv=yA∪{v}/yAx_v=y_{A\cup\{v\}}/y_A.
    19
    20# Formalization notes
    21
    22The coordinate type contains exactly the sets of size at most r+2r+2;
    23there are no coordinates for larger sets. The accessor is extended by zero
    24outside this domain, solely to simplify notation. Every constraint that
    25uses it supplies a size bound ensuring that it reads an actual coordinate.
    26The vector space and convex hull are over the reals, as in the paper;
    27the algorithms will use rational points in this space.
    28-/
    29
    30namespace Lax263307.LinearRelaxation
    31
    32/-- The coordinate sets of the level-`r` relaxation. -/
    33abbrev Coordinate (n r : ℕ) := {A : Finset (Fin n) // A.card ≤ r + 2}
    34
    35/-- A vector with precisely the coordinates used by the relaxation. -/
    36abbrev MomentVector (n r : ℕ) := Coordinate n r → ℝ
    37
    38/-- Read a coordinate, returning zero outside the truncated coordinate domain. -/
    39def value {n r : ℕ} (y : MomentVector n r) (A : Finset (Fin n)) : ℝ :=
    40 if h : A.card ≤ r + 2 then y ⟨A, h⟩ else 0
    41
    42/-- The indicator encoding of a vertex set. -/
    43def indicator {n : ℕ} (r : ℕ) (I : Finset (Fin n)) : MomentVector n r :=
    44 fun A => if A.val ⊆ I then 1 else 0
    45
    46/-- The five families of linear constraints defining `R_r(G,k)`. -/
    47structure IsFeasible {n : ℕ} (G : SimpleGraph (Fin n)) (k r : ℕ)
    48 (y : MomentVector n r) : Prop where
    49 /-- The empty moment is normalized. -/
    50 normalized : value y ∅ = 1
    51 /-- Each moment lies in the unit interval. -/
    52 bounds : ∀ A, 0 ≤ y A ∧ y A ≤ 1
    53 /-- Adding a vertex cannot increase a moment. -/
    54 monotone : ∀ A : Finset (Fin n), A.card ≤ r + 1 →
    55 ∀ v, value y (insert v A) ≤ value y A
    56 /-- Nonindependent sets have zero moment. -/
    57 vanishes : ∀ A : Coordinate n r, ¬G.IsIndepSet (A.val : Set (Fin n)) → y A = 0
    58 /-- The cardinality constraint remains valid after conditioning. -/
    59 mass : ∀ A : Finset (Fin n), A.card ≤ r + 1 →
    60 ∑ v : Fin n, value y (insert v A) = (k : ℝ) * value y A
    61
    62/-- The convex hull of encodings of size-`k` independent sets. -/
    63def independentSetHull {n : ℕ} (G : SimpleGraph (Fin n)) (k r : ℕ) :
    64 Set (MomentVector n r) :=
    65 convexHull ℝ {y | ∃ I : Finset (Fin n),
    66 G.IsIndepSet (I : Set (Fin n)) ∧ I.card = k ∧ y = indicator r I}
    67
    68/-- Vertex costs after conditioning on inclusion of `A`. -/
    69noncomputable def conditioned {n r : ℕ} (y : MomentVector n r)
    70 (A : Finset (Fin n)) (v : Fin n) : ℝ :=
    71 value y (insert v A) / value y A
    72
    73/-- A certified upper bound on independent sets contained in a vertex set. -/
    74def IsIndependenceBound {n : ℕ} (G : SimpleGraph (Fin n))
    75 (C : Finset (Fin n)) (u : ℕ) : Prop :=
    76 ∀ J : Finset (Fin n), J ⊆ C → G.IsIndepSet (J : Set (Fin n)) → J.card ≤ u
    77
    78end Lax263307.LinearRelaxation
    79
    Formalization notes

    The coordinate type contains exactly the sets of size at most r+2r+2; there are no coordinates for larger sets. The accessor is extended by zero outside this domain, solely to simplify notation. Every constraint that uses it supplies a size bound ensuring that it reads an actual coordinate. The vector space and convex hull are over the reals, as in the paper; the algorithms will use rational points in this space.

    Builds on

    none

    Used by
    From Mathlib

    Discussion

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

    Loading discussion…