Longest cycle

AbbreviationInstances of LONGEST CYCLE#✓fully proved

An instance of LONGEST CYCLE is a triple \((n, E, K)\) of a natural number \(n\) (the number of vertices), a list \(E\) of pairs of natural numbers (the edges), and a natural number \(K\) (the bound).

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

Used by 4

Used byGraph of a LONGEST CYCLE instance · The decision problem LONGEST CYCLE · Feasible LONGEST CYCLE instances · Well-formed LONGEST CYCLE instances

DefinitionGraph of a LONGEST CYCLE instance#✓fully proved

For an instance \((n, E, K)\) of LONGEST CYCLE, 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 \(E\). Loops are dropped, and pairs with an endpoint at least \(n\) contribute no edge.

def Graph (i : LongestCycleInstance) : 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 LONGEST CYCLE

Used byFeasible LONGEST CYCLE instances

DefinitionWell-formed LONGEST CYCLE instances#✓fully proved

An instance \((n, E, K)\) of LONGEST CYCLE is well formed when the list \(E\) has no repeated entries and every pair \((u, v)\) in \(E\) satisfies \(u < n\), \(v < n\), \(u \ne v\) and \((v, u) \notin E\).

def WellFormed (i : LongestCycleInstance) : 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 LONGEST CYCLE

Used byThe decision problem LONGEST CYCLE

DefinitionFeasible LONGEST CYCLE instances#✓fully proved

An instance \((n, E, K)\) of LONGEST CYCLE is feasible when there are pairwise distinct vertices \(v_1, \dots, v_m\) of the graph of the instance, with \(m \ge K\) and \(m \ge 3\), such that \(v_j\) is adjacent to \(v_{j+1}\) for every \(1 \le j < m\) and \(v_m\) is adjacent to \(v_1\). That is, the graph has a simple cycle with at least \(K\) edges and at least three vertices.

def LongestCycleFeasible
    (i : LongestCycleInstance) : Prop :=
  ∃ cycle : List (Fin i.1), cycle.Nodup ∧ i.2.2 ≤ cycle.length ∧ 3 ≤ cycle.length ∧
    (∀ j (h : j + 1 < cycle.length),
      (Graph i).Adj (cycle[j]'(by omega)) (cycle[j + 1]'h)) ∧
    ∀ h : cycle ≠ [], (Graph i).Adj (cycle.getLast h) (cycle.head h)

Uses 2 · Used by 1

Statement usesGraph of a LONGEST CYCLE instance · Instances of LONGEST CYCLE

Used byThe decision problem LONGEST CYCLE

DefinitionThe decision problem LONGEST CYCLE#✓fully proved

LONGEST CYCLE accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding of instances, to an instance of LONGEST CYCLE that is well formed and feasible. Bitstrings that do not decode, and bitstrings that decode to instances that are not well formed, are rejected.

noncomputable def longestCycleDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := LongestCycleInstance) x with
  | some i => decide (WellFormed i ∧ LongestCycleFeasible 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 LONGEST CYCLE instances · Instances of LONGEST CYCLE · Well-formed LONGEST CYCLE instances · Decision problems

Used byLONGEST CYCLE is NP-complete

TheoremLONGEST CYCLE is NP-complete#●ready to prove

The decision problem LONGEST CYCLE belongs to NP, and every decision problem in NP has a polynomial-time many-one reduction to LONGEST CYCLE.

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), LONGEST CYCLE.

Uses 5

Statement usesPolynomial-time many-one reduction · The decision problem LONGEST CYCLE · 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.