Undirected Hamiltonian cycle

DefinitionHamiltonian-cycle verifier#✓fully proved

Given bit strings \(x\) and \(y\), let \(m = \lfloor \sqrt{|x|} \rfloor\) and let \(w\) be the least natural number with \(m \le 2^w\). The verifier reads \(x\) as the adjacency matrix of a graph on the vertices \(0, \dots, m - 1\), stored row by row, and \(y\) as \(m\) words of \(w\) bits, the \(i\)-th word giving a number \(v_i\) in binary, least significant bit first. It accepts exactly when \(|x| = m^2\), every diagonal entry of the matrix is false, the matrix is symmetric, \(m \ge 3\), \(|y| = mw\), the numbers \(v_0, \dots, v_{m-1}\) are distinct and less than \(m\), and \(v_i\) is adjacent to \(v_{(i+1) \bmod m}\) for every \(i < m\). Along with the answer it returns a step count of the operations it performs: bit reads from \(x\) and \(y\), checks and updates.

Cslib.Algorithms.Lean.Graph.verifyHamiltonianCycle · 36 lines

public def verifyHamiltonianCycle (x y : Array Bool) : TimeM Nat Bool := do
  let m := Nat.sqrt x.size
  let valid ← validateGraph x m
  if !valid then return false
  TimeM.tick 1
  if m < 3 then return false
  let w := Nat.clog 2 m
  TimeM.tick 1
  if y.size != m * w then return false
  let mut seen : Vector Bool m := Vector.replicate m false
  let mut first : Option (Fin m) := none
  let mut previous : Option (Fin m) := none
  for i in Array.ofFn (fun i : Fin m => i) do
    let value ← countedBits y ((i.val + 1) * w) (i.val * w)
    TimeM.tick 1
    if h : value < m then
      let vertex : Fin m := ⟨value, h⟩
      TimeM.tick 1
      if seen[vertex] then return false
      TimeM.tick 1
      seen := seen.set value true h
      if let some p := previous then
        let present ← graphRead x (p.val * m + value)
        TimeM.tick 1
        if !present then return false
      else
        first := some vertex
      previous := some vertex
    else
      return false
  match first, previous with
  | some a, some b =>
    let present ← graphRead x (b.val * m + a.val)
    TimeM.tick 1
    pure present
  | _, _ => pure false

Used by 7

Used bySize of an accepted Hamiltonian-cycle certificate · Completeness of the Hamiltonian-cycle verifier · Acceptance condition of the Hamiltonian-cycle verifier · Certificates exist exactly for Hamiltonian graphs · Soundness of the Hamiltonian-cycle verifier · Quadratic step bound for the Hamiltonian-cycle verifier · Step bound for accepted Hamiltonian-cycle certificates

TheoremAcceptance condition of the Hamiltonian-cycle verifier#✓fully proved

Let \(x\) and \(y\) be bit strings, \(m = \lfloor \sqrt{|x|} \rfloor\), and \(w\) the least natural number with \(m \le 2^w\). For each \(i\) let \(d_i\) be the number whose binary digits, least significant first, are the bits of \(y\) at positions \(iw, \dots, iw + w - 1\) (counting from \(0\); positions past the end of \(y\) are omitted). The Hamiltonian-cycle verifier accepts \(x\) and \(y\) if and only if \(|x| = m^2\), \(m \ge 3\), \(|y| = mw\), and for all \(i, j < m\): entry \(im + i\) of \(x\) is false, entries \(im + j\) and \(jm + i\) of \(x\) are equal, \(d_i < m\), \(d_i = d_j\) implies \(i = j\), and entry \(d_i m + d_{(i+1) \bmod m}\) of \(x\) exists and is true.

public theorem verifyHamiltonianCycle_iff (x y : Array Bool) :
    let m := Nat.sqrt x.size
    let w := Nat.clog 2 m
    let decode := fun i : Nat => Nat.ofDigits 2
      ((y.toList.drop (i * w)).take w |>.map fun bit => if bit then 1 else 0)
    (verifyHamiltonianCycle x y).ret = true ↔
      m * m = x.size ∧ 3 ≤ m ∧ y.size = m * w ∧
      (∀ i < m, x[i * m + i]? = some false) ∧
      (∀ i < m, ∀ j < m, x[i * m + j]? = x[j * m + i]?) ∧
      (∀ i < m, decode i < m) ∧
      (∀ i < m, ∀ j < m, decode i = decode j → i = j) ∧
      (∀ i < m, x[decode i * m + decode ((i + 1) % m)]? = some true)

Uses 1 · Used by 1

Statement usesHamiltonian-cycle verifier

Used bySize of an accepted Hamiltonian-cycle certificate

TheoremSoundness of the Hamiltonian-cycle verifier#✓fully proved

If the Hamiltonian-cycle verifier accepts the bit strings \(x\) and \(y\), then, with \(m = \lfloor \sqrt{|x|} \rfloor\), we have \(|x| = m^2\) and \(m \ge 3\), and there is a simple graph \(G\) on the vertices \(0, \dots, m - 1\) in which \(i\) and \(j\) are adjacent exactly when entry \(im + j\) of \(x\) (counting from \(0\)) is true, and \(G\) has a Hamiltonian cycle.

public theorem verifyHamiltonianCycle_sound (x y : Array Bool)
    (h : (verifyHamiltonianCycle x y).ret = true) :
    let m := Nat.sqrt x.size
    m * m = x.size ∧ 3 ≤ m ∧
      ∃ G : SimpleGraph (Fin m),
        (∀ i j, G.Adj i j ↔ x[i.val * m + j.val]? = some true) ∧
        ∃ v : Fin m, ∃ p : G.Walk v v, p.IsHamiltonianCycle

Uses 1 · Used by 1

Statement usesHamiltonian-cycle verifier

Used byCertificates exist exactly for Hamiltonian graphs

TheoremCompleteness of the Hamiltonian-cycle verifier#✓fully proved

Let \(x\) be a bit string and \(m = \lfloor \sqrt{|x|} \rfloor\), suppose \(|x| = m^2\), and let \(G\) be a simple graph on the vertices \(0, \dots, m - 1\) in which \(i\) and \(j\) are adjacent exactly when entry \(im + j\) of \(x\) (counting from \(0\)) is true. If \(G\) has a Hamiltonian cycle, then there is a bit string \(y\) of length \(mw\), where \(w\) is the least natural number with \(m \le 2^w\), such that the Hamiltonian-cycle verifier accepts \(x\) and \(y\).

public theorem verifyHamiltonianCycle_complete (x : Array Bool) :
    let m := Nat.sqrt x.size
    ∀ G : SimpleGraph (Fin m), m * m = x.size →
      (∀ i j, G.Adj i j ↔ x[i.val * m + j.val]? = some true) →
      ∀ (v : Fin m) (p : G.Walk v v), p.IsHamiltonianCycle →
        ∃ y : Array Bool, y.size = m * Nat.clog 2 m ∧
          (verifyHamiltonianCycle x y).ret = true

Uses 1 · Used by 1

Statement usesHamiltonian-cycle verifier

Used byCertificates exist exactly for Hamiltonian graphs

TheoremCertificates exist exactly for Hamiltonian graphs#✓fully proved

For every bit string \(x\), with \(m = \lfloor \sqrt{|x|} \rfloor\), some bit string \(y\) makes the Hamiltonian-cycle verifier accept \(x\) and \(y\) if and only if \(|x| = m^2\), \(m \ge 3\), and there is a simple graph \(G\) on the vertices \(0, \dots, m - 1\) in which \(i\) and \(j\) are adjacent exactly when entry \(im + j\) of \(x\) (counting from \(0\)) is true, and \(G\) has a Hamiltonian cycle.

public theorem verifyHamiltonianCycle_language_iff (x : Array Bool) :
    (∃ y : Array Bool, (verifyHamiltonianCycle x y).ret = true) ↔
      let m := Nat.sqrt x.size
      m * m = x.size ∧ 3 ≤ m ∧
        ∃ G : SimpleGraph (Fin m),
          (∀ i j, G.Adj i j ↔ x[i.val * m + j.val]? = some true) ∧
          ∃ v : Fin m, ∃ p : G.Walk v v, p.IsHamiltonianCycle

Uses 3

Statement usesHamiltonian-cycle verifier

Proof usesCompleteness of the Hamiltonian-cycle verifier · Soundness of the Hamiltonian-cycle verifier

TheoremSize of an accepted Hamiltonian-cycle certificate#✓fully proved

If the Hamiltonian-cycle verifier accepts the bit strings \(x\) and \(y\), then \(|y| = mw\), where \(m = \lfloor \sqrt{|x|} \rfloor\) and \(w\) is the least natural number with \(m \le 2^w\), and moreover \(|y| \le |x|\).

public theorem verifyHamiltonianCycle_certificate_size (x y : Array Bool)
    (h : (verifyHamiltonianCycle x y).ret = true) :
    y.size = Nat.sqrt x.size * Nat.clog 2 (Nat.sqrt x.size) ∧ y.size ≤ x.size

Uses 2

Statement usesHamiltonian-cycle verifier

Proof usesAcceptance condition of the Hamiltonian-cycle verifier

TheoremQuadratic step bound for the Hamiltonian-cycle verifier#✓fully proved

There is a constant \(c > 0\) such that for all bit strings \(x\) and \(y\), the step count of the Hamiltonian-cycle verifier on \(x\) and \(y\) is at most \(c\,(|x| + |y| + 1)^2\).

public theorem verifyHamiltonianCycle_time_le :
    ∃ c : Nat, 0 < c ∧ ∀ x y : Array Bool,
      (verifyHamiltonianCycle x y).time ≤ c * (x.size + y.size + 1) ^ 2

Uses 1

Statement usesHamiltonian-cycle verifier

TheoremStep bound for accepted Hamiltonian-cycle certificates#✓fully proved

There is a constant \(c > 0\) such that for all bit strings \(x\) and \(y\) that the Hamiltonian-cycle verifier accepts, its step count on \(x\) and \(y\) is at most \(c\,(|x| + 1)^2\).

public theorem verifyHamiltonianCycle_time_le_of_accept :
    ∃ c : Nat, 0 < c ∧ ∀ x y : Array Bool,
      (verifyHamiltonianCycle x y).ret = true →
        (verifyHamiltonianCycle x y).time ≤ c * (x.size + 1) ^ 2

Uses 1

Statement usesHamiltonian-cycle verifier

AbbreviationInstances of HAMILTONIAN CYCLE (UNDIRECTED)#✓fully proved

An instance of HAMILTONIAN CYCLE (UNDIRECTED) 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 edges.

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

Used by 4

Used byGraph of a HAMILTONIAN CYCLE (UNDIRECTED) instance · HAMILTONIAN CYCLE (UNDIRECTED) as a decision problem · Feasible HAMILTONIAN CYCLE (UNDIRECTED) instances · Well-formed HAMILTONIAN CYCLE (UNDIRECTED) instances

DefinitionGraph of a HAMILTONIAN CYCLE (UNDIRECTED) instance#✓fully proved

For an instance \((n, E)\), its graph is the simple graph on the vertices \(\{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 : HamiltonianCycleUndirectedInstance) : 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 HAMILTONIAN CYCLE (UNDIRECTED)

Used byFeasible HAMILTONIAN CYCLE (UNDIRECTED) instances

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

An instance \((n, E)\) is well formed when \(0 < n\), the list \(E\) has no repeated entries, and every pair \((u, v)\) in \(E\) satisfies \(u < n\), \(v < n\) and \(u \ne v\), and its reversal \((v, u)\) does not belong to \(E\).

def WellFormed (i : HamiltonianCycleUndirectedInstance) : 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 HAMILTONIAN CYCLE (UNDIRECTED)

Used byHAMILTONIAN CYCLE (UNDIRECTED) as a decision problem

DefinitionFeasible HAMILTONIAN CYCLE (UNDIRECTED) instances#✓fully proved

An instance \((n, E)\) is feasible when \(n \ge 3\) and its graph has a Hamiltonian cycle, that is, a cycle that visits every vertex exactly once.

def HamiltonianCycleUndirectedFeasible
    (i : HamiltonianCycleUndirectedInstance) : Prop :=
  3 ≤ i.1 ∧ (Graph i).IsHamiltonian

Uses 2 · Used by 1

Statement usesGraph of a HAMILTONIAN CYCLE (UNDIRECTED) instance · Instances of HAMILTONIAN CYCLE (UNDIRECTED)

Used byHAMILTONIAN CYCLE (UNDIRECTED) as a decision problem

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

The decision problem HAMILTONIAN CYCLE (UNDIRECTED) accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to a well-formed instance \((n, E)\) with \(n \ge 3\) whose graph has a Hamiltonian cycle. It rejects every bitstring that does not decode to an instance.

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

Used byHAMILTONIAN CYCLE (UNDIRECTED) is NP-complete

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

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

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

Sources

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

Uses 5

Statement usesPolynomial-time many-one reduction · HAMILTONIAN CYCLE (UNDIRECTED) as a decision problem · Complexity classes · Decision problems · The complexity class NP

13 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.