Odd cycle transversal

AbbreviationOdd cycle transversal instances#✓fully proved

An odd cycle transversal instance 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 on the number of removed vertices).

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

Used by 4

Used byGraph of an odd cycle transversal instance · ODD CYCLE TRANSVERSAL as a decision problem · Feasible odd cycle transversal instances · Well-formed odd cycle transversal instances

DefinitionGraph of an odd cycle transversal instance#✓fully proved

For an odd cycle transversal instance \((n, es, K)\), its graph is the graph of the edge list \(es\) on \(n\) vertices: 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 : OddCycleTransversalInstance) : SimpleGraph (Fin i.1) :=
  Cslib.Complexity.Karp.edgeGraph i.1 i.2.1

Uses 2 · Used by 1

Statement usesGraph of an edge list · Odd cycle transversal instances

Used byFeasible odd cycle transversal instances

DefinitionWell-formed odd cycle transversal instances#✓fully proved

An odd cycle transversal instance \((n, es, K)\) 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 : OddCycleTransversalInstance) : 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 usesOdd cycle transversal instances

Used byODD CYCLE TRANSVERSAL as a decision problem

DefinitionFeasible odd cycle transversal instances#✓fully proved

An odd cycle transversal instance \((n, es, K)\) is feasible when there is a set \(S\) of at most \(K\) vertices of its graph such that the subgraph induced on the vertices outside \(S\) is bipartite.

def OddCycleTransversalFeasible
    (i : OddCycleTransversalInstance) : Prop :=
  ∃ S : Finset (Fin i.1), S.card ≤ i.2.2 ∧
    ((Graph i).induce (↑Sᶜ : Set (Fin i.1))).IsBipartite

Uses 2 · Used by 1

Statement usesGraph of an odd cycle transversal instance · Odd cycle transversal instances

Used byODD CYCLE TRANSVERSAL as a decision problem

DefinitionODD CYCLE TRANSVERSAL as a decision problem#✓fully proved

The decision problem ODD CYCLE TRANSVERSAL accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to an odd cycle transversal instance \((n, es, K)\) that is well formed and feasible. Well formed means that \(es\) has no repeated entries and every pair \((u, v)\) in \(es\) satisfies \(u < n\), \(v < n\), \(u \ne v\) and \((v, u) \notin es\); feasible means that some set of at most \(K\) vertices can be removed from the graph of the instance so that the remaining induced subgraph is bipartite. Bitstrings that do not decode to an instance are rejected.

noncomputable def oddCycleTransversalDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := OddCycleTransversalInstance) x with
  | some i => decide (WellFormed i ∧ OddCycleTransversalFeasible 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 · Feasible odd cycle transversal instances · Odd cycle transversal instances · Well-formed odd cycle transversal instances · Decision problems

Used byODD CYCLE TRANSVERSAL is NP-complete

TheoremODD CYCLE TRANSVERSAL is NP-complete#●ready to prove

The decision problem ODD CYCLE TRANSVERSAL, which accepts a bitstring exactly when it decodes to a well-formed instance \((n, es, K)\) whose graph becomes bipartite after removing some set of at most \(K\) vertices, belongs to NP, and every decision problem in NP has a polynomial-time many-one reduction to it.

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), ODD CYCLE TRANSVERSAL (vertex deletion to a bipartite graph).

Uses 5

Statement usesPolynomial-time many-one reduction · ODD CYCLE TRANSVERSAL 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.