Feedback vertex set

AbbreviationInstances of FEEDBACK VERTEX SET#✓fully proved

An instance of FEEDBACK VERTEX SET is a triple \((n, es, K)\) of a natural number \(n\) (the number of vertices), a list \(es\) of pairs of natural numbers (the edges) and a natural number \(K\) (the bound).

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

Used by 4

Used byFEEDBACK VERTEX SET as a decision problem · Feedback vertex sets within the bound · Graph of a FEEDBACK VERTEX SET instance · Well-formed FEEDBACK VERTEX SET instances

DefinitionGraph of a FEEDBACK VERTEX SET instance#✓fully proved

For an instance \((n, es, K)\) of FEEDBACK VERTEX SET, its graph is the simple graph on \(\{0, \dots, n-1\}\) in which distinct vertices \(i\) and \(j\) are adjacent when \((i, j)\) or \((j, i)\) belongs to \(es\).

def Graph (i : FeedbackVertexSetInstance) : SimpleGraph (Fin i.1) :=
  Cslib.Complexity.Karp.edgeGraph i.1 i.2.1

Uses 2 · Used by 1

Statement usesGraph of an edge list · Instances of FEEDBACK VERTEX SET

Used byFeedback vertex sets within the bound

DefinitionWell-formed FEEDBACK VERTEX SET instances#✓fully proved

An instance \((n, es, K)\) of FEEDBACK VERTEX SET is well formed when the list \(es\) has no repeated entries and every pair \((u, v)\) in \(es\) satisfies \(u < n\), \(v < n\) and \(u \ne v\), and \((v, u)\) does not belong to \(es\).

def WellFormed (i : FeedbackVertexSetInstance) : 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 FEEDBACK VERTEX SET

Used byFEEDBACK VERTEX SET as a decision problem

DefinitionFeedback vertex sets within the bound#✓fully proved

An instance \((n, es, K)\) of FEEDBACK VERTEX SET is feasible when there is a set \(S\) of at most \(K\) vertices of its graph such that the subgraph of its graph induced on the vertices outside \(S\) is acyclic.

def FeedbackVertexSetFeasible
    (i : FeedbackVertexSetInstance) : Prop :=
  ∃ S : Finset (Fin i.1), S.card ≤ i.2.2 ∧
    ((Graph i).induce (↑Sᶜ : Set (Fin i.1))).IsAcyclic

Uses 2 · Used by 1

Statement usesInstances of FEEDBACK VERTEX SET · Graph of a FEEDBACK VERTEX SET instance

Used byFEEDBACK VERTEX SET as a decision problem

DefinitionFEEDBACK VERTEX SET as a decision problem#✓fully proved

The decision problem FEEDBACK VERTEX SET accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding of instances, to an instance of FEEDBACK VERTEX SET that is well formed and feasible. Bitstrings that do not decode to an instance are rejected.

noncomputable def feedbackVertexSetDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := FeedbackVertexSetInstance) x with
  | some i => decide (WellFormed i ∧ FeedbackVertexSetFeasible 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 · Feedback vertex sets within the bound · Instances of FEEDBACK VERTEX SET · Well-formed FEEDBACK VERTEX SET instances · Decision problems

Used byFEEDBACK VERTEX SET is NP-complete

TheoremFEEDBACK VERTEX SET is NP-complete#●ready to prove

The decision problem FEEDBACK VERTEX SET belongs to NP, and every decision problem in NP reduces to FEEDBACK VERTEX SET by a polynomial-time many-one reduction.

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), FEEDBACK VERTEX SET.

Uses 5

Statement usesPolynomial-time many-one reduction · FEEDBACK VERTEX SET as a decision problem · Complexity classes · Decision problems · The complexity class NP

5 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.