Lax Lean Archive

Graph decision problems and NP-hardness

Lax762056.GraphProblems · concepts/Lax762056/GraphProblems.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

    Independent Set asks whether a graph has an independent set of size at least kk. Max Cut asks whether it has a cut with at least kk crossing edges.

    A graph problem is NP-hard on a class C\mathcal C if every language in NP has a polynomial-time many-one reduction to the problem whose output graph always belongs to C\mathcal C. Instances use the adjacency-matrix encoding.

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

    Lean source view on GitHub

    1import Lax762056.MaxCut
    2import Lax434930.NondeterministicPolynomialTime
    3
    4/-!
    5---
    6title: Graph decision problems and NP-hardness
    7type: definition
    8---
    9Independent Set asks whether a graph has an independent set of size at least
    10kk. Max Cut asks whether it has a cut with at least kk crossing edges.
    11
    12A graph problem is NP-hard on a class C\mathcal C if every language in NP
    13has a polynomial-time many-one reduction to the problem whose output graph
    14always belongs to C\mathcal C. Instances use the adjacency-matrix encoding.
    15-/
    16
    17namespace Lax762056.GraphProblems
    18
    19open GraphEncoding MaxCut Turing
    20open Lax434930.PolynomialTime Lax434930.NondeterministicPolynomialTime
    21
    22abbrev GraphClass := ∀ {n : ℕ}, SimpleGraph (Fin n) → Prop
    23abbrev DecisionProblem := Instance → Prop
    24
    25def IndependentSet (I : Instance) : Prop := I.threshold ≤ I.graph.indepNum
    26
    27def MaxCut (I : Instance) : Prop := I.threshold ≤ maxCut I.graph
    28
    29def NPHard (problem : DecisionProblem) : Prop :=
    30 ∀ A : Language, A ∈ NP →
    31 ∃ f : Word → Instance,
    32 Nonempty (TM2ComputableInPolyTime id encode f) ∧
    33 ∀ x, x ∈ A ↔ problem (f x)
    34
    35def NPHardOn (problem : DecisionProblem) (graphs : GraphClass) : Prop :=
    36 ∀ A : Language, A ∈ NP →
    37 ∃ f : Word → Instance,
    38 Nonempty (TM2ComputableInPolyTime id encode f) ∧
    39 ∀ x, graphs (f x).graph ∧ (x ∈ A ↔ problem (f x))
    40
    41end Lax762056.GraphProblems
    42
    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…