Lax Lean Archive

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

QPTAS for maximum-weight independent set

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

proven

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

    Theorem

    Let C\mathcal C be a hereditary graph class with strongly edge-sublinear separators. Then maximum-weight independent set admits a deterministic quasipolynomial-time approximation scheme on C\mathcal C.

    For every G∈CG\in\mathcal C and rational 0<ε<10<\varepsilon<1, it computes an independent set II with w(I)≥(1−ε)αw(G)w(I)\ge(1-\varepsilon)\alpha_w(G) in time

    exp⁡ ⁣((ε−1log⁡(n+2))OC(1))+(ℓ+1)OC(1).\exp\!\left((\varepsilon^{-1}\log(n+2))^{O_{\mathcal C}(1)}\right) +(\ell+1)^{O_{\mathcal C}(1)}.

    Here n=∣V(G)∣n=|V(G)|, αw(G)\alpha_w(G) is the maximum independent-set weight, and ℓ\ell is the binary encoding length of the rational weights and accuracy. No separator or algorithm for finding one is part of the input.

    Concept map
    7 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax263307.EdgeSublinearSeparators
    2import Lax263307.QPTAS
    3
    4/-!
    5---
    6title: QPTAS for maximum-weight independent set
    7type: theorem
    8---
    9Let C\mathcal C be a hereditary graph class with strongly edge-sublinear
    10separators. Then maximum-weight independent set admits a deterministic
    11quasipolynomial-time approximation scheme on C\mathcal C.
    12
    13For every G∈CG\in\mathcal C and rational 0<ε<10<\varepsilon<1, it computes
    14an independent set II with w(I)≥(1−ε)αw(G)w(I)\ge(1-\varepsilon)\alpha_w(G) in time
    15exp⁡ ⁣((ε−1log⁡(n+2))OC(1))+(ℓ+1)OC(1).\exp\!\left((\varepsilon^{-1}\log(n+2))^{O_{\mathcal C}(1)}\right) +(\ell+1)^{O_{\mathcal C}(1)}.
    16
    17Here n=∣V(G)∣n=|V(G)|, αw(G)\alpha_w(G) is the maximum independent-set weight,
    18and ℓ\ell is the binary encoding length of the rational weights and accuracy.
    19No separator or algorithm for finding one is part of the input.
    20
    21# Attribution
    22
    23Édouard Bonnet and Yeonsu Chang, *QPTAS for Max Weight Independent Set
    24in Graphs with Strongly Edge-Sublinear Separators*, Theorem 2.
    25
    26# Formalization notes
    27
    28This is the submission's headline theorem. The separator hypothesis
    29uses the harmless m+1m+1 normalization explained
    30in `EdgeSublinearSeparators`. The approximation scheme refers directly
    31to the registered RAM semantics through `QPTAS.HasQPTAS`.
    32-/
    33
    34namespace Lax263307.MainTheorem
    35
    36open GraphClasses EdgeSublinearSeparators QPTAS
    37
    38/-- Theorem 2: the deterministic weighted approximation scheme. -/
    39axiom exists_qptas (C : GraphClass) (hereditary : IsHereditary C)
    40 (separators : HasStronglyEdgeSublinearSeparators C) : HasQPTAS C
    41
    42end Lax263307.MainTheorem
    43
    Show Proof

    Attribution

    Édouard Bonnet and Yeonsu Chang, QPTAS for Max Weight Independent Set in Graphs with Strongly Edge-Sublinear Separators, Theorem 2.

    Formalization notes

    This is the submission's headline theorem. The separator hypothesis uses the harmless m+1m+1 normalization explained in EdgeSublinearSeparatorsEdgeSublinearSeparators. The approximation scheme refers directly to the registered RAM semantics through QPTAS.HasQPTASQPTAS.HasQPTAS.

    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…