Densest k-subgraph

AbbreviationInstances of DENSEST k-SUBGRAPH#✓fully proved

An instance of DENSEST k-SUBGRAPH is a quadruple \((n, E, k, m)\) consisting of a natural number \(n\) (the number of vertices), a list \(E\) of pairs of natural numbers (the edges), a natural number \(k\) (the size of the vertex set sought) and a natural number \(m\) (the edge threshold).

abbrev DensestKSubgraphInstance := ℕ × List (ℕ × ℕ) × ℕ × ℕ

Used by 3

Used byDENSEST k-SUBGRAPH as a decision problem · Feasibility for DENSEST k-SUBGRAPH · Well-formed DENSEST k-SUBGRAPH instances

DefinitionWell-formed DENSEST k-SUBGRAPH instances#✓fully proved

An instance \((n, E, k, m)\) of DENSEST k-SUBGRAPH is well formed when the list \(E\) has no repeated entries and every pair \((u, v)\) in \(E\) satisfies \(u < n\), \(v < n\) and \(u \ne v\), with the reversed pair \((v, u)\) not in \(E\).

def WellFormed (i : DensestKSubgraphInstance) : Prop :=
  i.2.1.Nodup ∧ (∀ e ∈ i.2.1, e.1 < i.1 ∧ e.2 < i.1 ∧ e.1 ≠ e.2 ∧ (e.2, e.1) ∉ i.2.1)

Uses 1 · Used by 1

Statement usesInstances of DENSEST k-SUBGRAPH

Used byDENSEST k-SUBGRAPH as a decision problem

DefinitionFeasibility for DENSEST k-SUBGRAPH#✓fully proved

An instance \((n, E, k, m)\) of DENSEST k-SUBGRAPH is feasible when there are a finite set \(S\) of exactly \(k\) natural numbers, each less than \(n\), and a sublist \(E'\) of \(E\) (obtained by deleting entries and keeping the order) with at least \(m\) entries such that both components of every pair in \(E'\) lie in \(S\).

For a well-formed instance this says that some \(k\) vertices of the graph of \(E\) on \(n\) vertices induce at least \(m\) edges.

def DensestKSubgraphFeasible
    (i : DensestKSubgraphInstance) : Prop :=
  ∃ S : Finset ℕ, (∀ v ∈ S, v < i.1) ∧ S.card = i.2.2.1 ∧
    ∃ E' : List (ℕ × ℕ), E'.Sublist i.2.1 ∧ i.2.2.2 ≤ E'.length ∧
      ∀ e ∈ E', e.1 ∈ S ∧ e.2 ∈ S

Uses 1 · Used by 1

Statement usesInstances of DENSEST k-SUBGRAPH

Used byDENSEST k-SUBGRAPH as a decision problem

DefinitionDENSEST k-SUBGRAPH as a decision problem#✓fully proved

The decision problem DENSEST k-SUBGRAPH accepts a bitstring \(x\) exactly when bitstring decoding of \(x\) as a quadruple \((n, E, k, m)\) succeeds and returns an instance of DENSEST k-SUBGRAPH that is both well formed and feasible; every bitstring that does not decode is rejected.

noncomputable def densestKSubgraphDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := DensestKSubgraphInstance) x with
  | some i => decide (WellFormed i ∧ DensestKSubgraphFeasible i)
  | none => false

Uses 12 · Used by 1

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Feasibility for DENSEST k-SUBGRAPH · Instances of DENSEST k-SUBGRAPH · Well-formed DENSEST k-SUBGRAPH instances · Decision problems

Used byDENSEST k-SUBGRAPH is NP-complete

TheoremDENSEST k-SUBGRAPH is NP-complete#●ready to prove

The decision problem DENSEST k-SUBGRAPH belongs to the class NP, and every decision problem in NP has a polynomial-time many-one reduction to it.

public theorem_wanted densestKSubgraph_npComplete :
    densestKSubgraphDec ∈ MetaMathlibExt.ComplexityTheory.NP ∧
      ∀ L : MetaMathlibExt.ComplexityTheory.DecisionProblem,
        L ∈ MetaMathlibExt.ComplexityTheory.NP →
          Cslib.CookLevin.PolyManyOneRed L densestKSubgraphDec

Sources

• U. Feige, G. Kortsarz, and D. Peleg, "The dense k-subgraph problem" (2001); M. R. Garey and D. S. Johnson, Computers and Intractability (1979), DENSEST k-SUBGRAPH.

Uses 5

Statement usesPolynomial-time many-one reduction · DENSEST k-SUBGRAPH as a decision problem · Complexity classes · Decision problems · The complexity class NP

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.