Lax Lean Archive

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

Maximum-weight independent set as an optimization problem

Lax263307.MaxWeightIndependentSet · concepts/Lax263307/MaxWeightIndependentSet.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

    An instance is a finite simple graph with rational vertex weights. A feasible solution is an independent vertex set in that graph. Its objective is the nonnegative part of its total weight, as required by lax-213208. This does not change the optimum: the empty set is feasible and has weight zero. The approximation proof also ensures that the returned set has nonnegative weight.

    Membership in the input class means precisely that the instance graph belongs to C\mathcal C; all rational weight assignments are allowed. The separate IndependentSetEncodingIndependentSetEncoding concept fixes the standard representations used to measure running time. Feasibility, objective values, and class membership are defined directly on mathematical objects, without decoding machine words.

    Concept map
    9 concepts; 1 descendant hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Lax263307.GraphClasses
    2import Lax263307.IndependentSetEncoding
    3import Lax213208.OptimizationProblem
    4
    5/-!
    6---
    7title: Maximum-weight independent set as an optimization problem
    8type: definition
    9---
    10An instance is a finite simple graph with rational vertex weights. A feasible
    11solution is an independent vertex set in that graph. Its objective is the
    12nonnegative part of its total weight, as required by lax-213208. This does not
    13change the optimum: the empty set is feasible and has weight zero.
    14The approximation proof also ensures that the returned set has nonnegative
    15weight.
    16
    17Membership in the input class means precisely that the instance graph belongs
    18to C\mathcal C; all rational weight assignments are allowed. The separate
    19`IndependentSetEncoding` concept fixes the standard representations used to
    20measure running time. Feasibility, objective values, and class membership are
    21defined directly on mathematical objects, without decoding machine words.
    22-/
    23
    24namespace Lax263307
    25
    26open GraphClasses WeightedIndependentSet
    27open Lax213208.OptimizationProblem
    28
    29namespace MaxWeightIndependentSet
    30
    31/-- A feasible solution is an independent set of the instance graph. -/
    32def IsFeasible (x : Instance) (s : Solution) : Prop :=
    33 ∃ I : Finset (Fin x.order), s = ⟨x.order, I⟩ ∧
    34 x.graph.IsIndepSet (I : Set (Fin x.order))
    35
    36/-- Total weight, clipped at zero to meet the nonnegative-objective convention. -/
    37def objectiveValue (x : Instance) (s : Solution) : NNReal :=
    38 if h : s.1 = x.order then
    39 Real.toNNReal (weight x.weights (h ▸ s.2))
    40 else 0
    41
    42/-- Weighted graphs whose underlying graph belongs to the given class. -/
    43def instancesOn (C : GraphClass) : Set Instance :=
    44 {x | x.graph ∈ C x.order}
    45
    46end MaxWeightIndependentSet
    47
    48/-- The mathematical optimization problem with its fixed canonical representations. -/
    49noncomputable def MaxWeightIndependentSet : Problem Instance Solution where
    50 direction := .maximize
    51 feasible := MaxWeightIndependentSet.IsFeasible
    52 value := MaxWeightIndependentSet.objectiveValue
    53 input := IndependentSetEncoding.input
    54 output := IndependentSetEncoding.output
    55 input_faithful := IndependentSetEncoding.input_faithful
    56 output_injective := IndependentSetEncoding.output_injective
    57
    58end Lax263307
    59
    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…