Undirected Hamiltonian path

AbbreviationInstances of undirected Hamiltonian path#✓fully proved

An instance of undirected Hamiltonian path is a pair \((n, E)\) of a natural number \(n\), the number of vertices, and a finite list \(E\) of pairs of natural numbers, the edge list.

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

Used by 4

Used byGraph of an undirected Hamiltonian path instance · HAMILTONIAN PATH (UNDIRECTED) as a decision problem · Feasible undirected Hamiltonian path instances · Well-formed undirected Hamiltonian path instances

DefinitionGraph of an undirected Hamiltonian path instance#✓fully proved

For an instance \((n, E)\) of undirected Hamiltonian path, its graph is the simple graph on the vertex set \(\{0, \dots, n-1\}\) in which distinct vertices \(i\) and \(j\) are adjacent when \((i, j)\) or \((j, i)\) belongs to \(E\).

def Graph (i : HamiltonianPathUndirectedInstance) : SimpleGraph (Fin i.1) :=
  Cslib.Complexity.Karp.edgeGraph i.1 i.2

Uses 2 · Used by 1

Statement usesGraph of an edge list · Instances of undirected Hamiltonian path

Used byFeasible undirected Hamiltonian path instances

DefinitionWell-formed undirected Hamiltonian path instances#✓fully proved

An instance \((n, E)\) of undirected Hamiltonian path 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\), and the reversed pair \((v, u)\) does not belong to \(E\).

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

Uses 1 · Used by 1

Statement usesInstances of undirected Hamiltonian path

Used byHAMILTONIAN PATH (UNDIRECTED) as a decision problem

DefinitionFeasible undirected Hamiltonian path instances#✓fully proved

An instance \((n, E)\) of undirected Hamiltonian path is feasible when its graph has a Hamiltonian path: a list of length \(n\) of vertices of the graph, with no repeated entries and containing every vertex, in which any two consecutive entries are adjacent.

def HamiltonianPathUndirectedFeasible
    (i : HamiltonianPathUndirectedInstance) : Prop :=
  ∃ path : List (Fin i.1), path.Nodup ∧ path.length = i.1 ∧ (∀ v, v ∈ path) ∧
    ∀ j (h : j + 1 < path.length),
      (Graph i).Adj (path[j]'(by omega)) (path[j + 1]'h)

Uses 2 · Used by 1

Statement usesGraph of an undirected Hamiltonian path instance · Instances of undirected Hamiltonian path

Used byHAMILTONIAN PATH (UNDIRECTED) as a decision problem

DefinitionHAMILTONIAN PATH (UNDIRECTED) as a decision problem#✓fully proved

The decision problem HAMILTONIAN PATH (UNDIRECTED) accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to an instance \((n, E)\) of undirected Hamiltonian path that is well formed and feasible; bitstrings that do not decode to an instance are rejected.

noncomputable def hamiltonianPathUndirectedDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := HamiltonianPathUndirectedInstance) x with
  | some i => decide (WellFormed i ∧ HamiltonianPathUndirectedFeasible 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 undirected Hamiltonian path instances · Instances of undirected Hamiltonian path · Well-formed undirected Hamiltonian path instances · Decision problems

Used byHAMILTONIAN PATH (UNDIRECTED) is NP-complete

TheoremHAMILTONIAN PATH (UNDIRECTED) is NP-complete#●ready to prove

The decision problem HAMILTONIAN PATH (UNDIRECTED) belongs to NP, and every decision problem in NP reduces to it by a polynomial-time many-one reduction.

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), HAMILTONIAN PATH.

Uses 5

Statement usesPolynomial-time many-one reduction · HAMILTONIAN PATH (UNDIRECTED) 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.