Directed Hamiltonian cycle

AbbreviationInstances of HAMILTONIAN CYCLE (DIRECTED)#✓fully proved

An instance of HAMILTONIAN CYCLE (DIRECTED) is a pair \((n, E)\) of a natural number \(n\), the number of vertices, and a finite list \(E\) of ordered pairs of natural numbers, the arcs.

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

Used by 3

Used byThe directed Hamiltonian cycle decision problem · Directed Hamiltonian cycles of an instance · Well-formed instances of HAMILTONIAN CYCLE (DIRECTED)

DefinitionDirected adjacency for HAMILTONIAN CYCLE (DIRECTED)#✓fully proved

For a finite list \(E\) of ordered pairs of natural numbers and natural numbers \(u\) and \(v\), the directed adjacency of \(u\) to \(v\) in \(E\) is the boolean value that is true exactly when the pair \((u, v)\) occurs in \(E\).

def DAdj (edges : List (ℕ × ℕ)) (u v : ℕ) : Bool :=
  edges.contains (u, v)

Used by 1

Used byDirected Hamiltonian cycles of an instance

DefinitionWell-formed instances of HAMILTONIAN CYCLE (DIRECTED)#✓fully proved

An instance \((n, E)\) of HAMILTONIAN CYCLE (DIRECTED), with \(n\) a natural number and \(E\) a finite list of ordered pairs of natural numbers, is well formed when \(n > 0\), the list \(E\) has no repeated entries, and every pair \((u, v)\) in \(E\) satisfies \(u < n\), \(v < n\) and \(u \ne v\).

def WellFormed (i : HamiltonianCycleDirectedInstance) : Prop :=
  0 < i.1 ∧ i.2.Nodup ∧ ∀ e ∈ i.2, e.1 < i.1 ∧ e.2 < i.1 ∧ e.1 ≠ e.2

Uses 1 · Used by 1

Statement usesInstances of HAMILTONIAN CYCLE (DIRECTED)

Used byThe directed Hamiltonian cycle decision problem

DefinitionDirected Hamiltonian cycles of an instance#✓fully proved

An instance \((n, E)\) of HAMILTONIAN CYCLE (DIRECTED), with \(n\) a natural number and \(E\) a finite list of ordered pairs of natural numbers, has a directed Hamiltonian cycle when there is a list \((v_0, \dots, v_{n-1})\) of \(n\) distinct natural numbers containing every natural number below \(n\) such that the pair \((v_j, v_{(j+1) \bmod n})\) occurs in \(E\) for every \(j < n\).

def HamiltonianCycleDirectedFeasible
    (i : HamiltonianCycleDirectedInstance) : Prop :=
  ∃ cycle : List ℕ, cycle.Nodup ∧ cycle.length = i.1 ∧ (∀ v < i.1, v ∈ cycle) ∧
    ∀ j < i.1, DAdj i.2 (cycle.getD j 0) (cycle.getD ((j + 1) % i.1) 0)

Uses 2 · Used by 1

Statement usesDirected adjacency for HAMILTONIAN CYCLE (DIRECTED) · Instances of HAMILTONIAN CYCLE (DIRECTED)

Used byThe directed Hamiltonian cycle decision problem

DefinitionThe directed Hamiltonian cycle decision problem#✓fully proved

The decision problem HAMILTONIAN CYCLE (DIRECTED) accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to an instance \((n, E)\), consisting of a natural number \(n\) and a finite list \(E\) of ordered pairs of natural numbers, such that \((n, E)\) is well formed (\(n > 0\), \(E\) has no repeated entries, and every pair \((u, v)\) in \(E\) satisfies \(u < n\), \(v < n\) and \(u \ne v\)) and has a directed Hamiltonian cycle (a list \((v_0, \dots, v_{n-1})\) of \(n\) distinct natural numbers containing every natural number below \(n\) such that \((v_j, v_{(j+1) \bmod n})\) occurs in \(E\) for every \(j < n\)). It rejects every bitstring that does not decode to an instance.

noncomputable def hamiltonianCycleDirectedDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := HamiltonianCycleDirectedInstance) x with
  | some i => decide (WellFormed i ∧ HamiltonianCycleDirectedFeasible 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 · Directed Hamiltonian cycles of an instance · Instances of HAMILTONIAN CYCLE (DIRECTED) · Well-formed instances of HAMILTONIAN CYCLE (DIRECTED) · Decision problems

Used byHAMILTONIAN CYCLE (DIRECTED) is NP-complete

TheoremHAMILTONIAN CYCLE (DIRECTED) is NP-complete#●ready to prove

The decision problem HAMILTONIAN CYCLE (DIRECTED) belongs to NP, and every decision problem \(L\) in NP has a polynomial-time many-one reduction to it.

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), HAMILTONIAN CIRCUIT (directed); R. M. Karp, "Reducibility among combinatorial problems" (1972).

Uses 5

Statement usesPolynomial-time many-one reduction · The directed Hamiltonian cycle 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.