Hamiltonian paths and cycles

A graph, given by a list of vertices and a list of edges, is read as a directed graph through its arcs (u, v) ∈ G.2, or as an undirected graph through Cslib.Complexity.Graph.toSimpleGraph restricted to the declared vertices (SimpleGraph.induce). In both readings the vertices are the declared ones: repeated vertex entries count once, and edges with an undeclared endpoint are never used.

• DirHamPath is the set of triples (G, s, t) such that the directed graph G has a Hamiltonian path from s to t Sipser, Section 7.3. Mathlib's Digraph has no walks, so the path is a list of vertices (Graph.IsDirHamPath).
• DirHamCycle is the set of directed graphs with a Hamiltonian cycle (Graph.IsDirHamCycle): a nonempty list of the vertices whose consecutive vertices, read cyclically (Cycle.Chain), are joined by arcs. A single vertex therefore needs a self-loop, and two vertices need arcs both ways.
• HamPath and HamCycle are the undirected versions, stated with Mathlib's SimpleGraph.Walk.IsHamiltonian and SimpleGraph.Walk.IsHamiltonianCycle. A Hamiltonian cycle is a cycle, so it has at least three vertices; unlike SimpleGraph.IsHamiltonian, no convention makes the one-vertex graph Hamiltonian. mem_HamPath_iff and mem_HamCycle_iff restate them with lists of vertices.

All four problems are in NP. A certificate names an ordering of the distinct declared vertices: for a vertex list of length m, it is read as one block of m bits for each distinct declared vertex, and each block names the entry of the vertex list whose position is its number of set bits (Graph.decodeVertexList). The verifiers check that the decoded list contains every declared vertex exactly once and nothing else (Graph.verifyOrdering), and then the endpoint, length and edge conditions. Every ordering has a certificate of length n ^ 2 for instances of encoded length n. Path instances (G, s, t) are encoded by encPair encGraph (encPair encNat encNat), cycle instances by encGraph.

Main definitions

• Cslib.Complexity.Graph.IsDirHamPath, Cslib.Complexity.DirHamPath.
• Cslib.Complexity.Graph.IsDirHamCycle, Cslib.Complexity.DirHamCycle.
• Cslib.Complexity.HamPath, Cslib.Complexity.HamCycle.
• Cslib.Complexity.Graph.arcBool, Cslib.Complexity.Graph.chainBool, Cslib.Complexity.Graph.cycleChainBool: executable tests on lists of vertices.
• Cslib.Complexity.DirHamPath.verifier, Cslib.Complexity.DirHamCycle.verifier, Cslib.Complexity.HamPath.verifier, Cslib.Complexity.HamCycle.verifier.

Main results

• Cslib.Complexity.mem_HamPath_iff: undirected Hamiltonian paths as lists of vertices.
• Cslib.Complexity.mem_HamCycle_iff: undirected Hamiltonian cycles as lists of vertices.
• Cslib.Complexity.Graph.mem_DirHamCycle_cons_iff: closing a Hamiltonian path with an arc back to its start gives a Hamiltonian cycle, when no other arc enters the start.
• Cslib.Complexity.DirHamPath.isVerifier, Cslib.Complexity.DirHamPath.mem_NP: DirHamPath ∈ NP (encPair encGraph (encPair encNat encNat)).
• Cslib.Complexity.DirHamCycle.isVerifier, Cslib.Complexity.DirHamCycle.mem_NP: DirHamCycle ∈ NP encGraph.
• Cslib.Complexity.HamPath.isVerifier, Cslib.Complexity.HamPath.mem_NP: HamPath ∈ NP (encPair encGraph (encPair encNat encNat)).
• Cslib.Complexity.HamCycle.isVerifier, Cslib.Complexity.HamCycle.mem_NP: HamCycle ∈ NP encGraph.

References

• M. R. Garey and D. S. Johnson, Computers and Intractability
• R. M. Karp, Reducibility among combinatorial problems
• M. Sipser, Introduction to the Theory of Computation

def Cslib.Complexity.Graph.IsDirHamPath (G : Graph) (s t : ℕ) (p : List ℕ) : Prop

p is a Hamiltonian path of the directed graph G from s to t: it lists every declared vertex exactly once, starts at s, ends at t, and consecutive vertices are joined by arcs.

def Cslib.Complexity.Graph.IsDirHamCycle (G : Graph) (p : List ℕ) : Prop

p is a Hamiltonian cycle of the directed graph G: a nonempty list of every declared vertex exactly once whose consecutive vertices, read cyclically, are joined by arcs.

def Cslib.Complexity.DirHamPath : Set (Graph × ℕ × ℕ)

The directed graphs with a Hamiltonian path from s to t Sipser, Section 7.3.

def Cslib.Complexity.DirHamCycle : Set Graph

The directed graphs with a Hamiltonian cycle [Kar72].

def Cslib.Complexity.HamPath : Set (Graph × ℕ × ℕ)

The graphs with a Hamiltonian path from s to t through their declared vertices Sipser, Theorem 7.55.

def Cslib.Complexity.HamCycle : Set Graph

The graphs with a Hamiltonian cycle through their declared vertices [Kar72].

Lists of vertices

theorem Cycle.chain_coe_iff_isChain_append_take_one {α : Type u_1} {R : α → α → Prop} {p : List α} : Chain R ↑p ↔ List.IsChain R (p ++ List.take 1 p)

A list is a closed chain exactly when appending its first element gives a chain.

theorem Cslib.Complexity.mem_HamPath_iff {G : Graph} {s t : ℕ} : (G, s, t) ∈ HamPath ↔ ∃ (p : List ℕ), p.Nodup ∧ (∀ (v : ℕ), v ∈ p ↔ v ∈ G.1) ∧ p.head? = some s ∧ p.getLast? = some t ∧ List.IsChain G.toSimpleGraph.Adj p

Undirected Hamiltonian paths as lists of vertices.

theorem Cslib.Complexity.mem_HamCycle_iff {G : Graph} : G ∈ HamCycle ↔ ∃ (p : List ℕ), p.Nodup ∧ (∀ (v : ℕ), v ∈ p ↔ v ∈ G.1) ∧ 3 ≤ p.length ∧ Cycle.Chain G.toSimpleGraph.Adj ↑p

Undirected Hamiltonian cycles as lists of vertices.

Closing a path into a cycle

theorem Cslib.Complexity.Graph.mem_DirHamCycle_cons_iff {G : Graph} {s t : ℕ} (hs : s ∈ G.1) (hin : ∀ (u : ℕ), (u, s) ∉ G.2) : (G.1, (t, s) :: G.2) ∈ DirHamCycle ↔ (G, s, t) ∈ DirHamPath

Closing a Hamiltonian path with an arc back to its start. If no arc of G enters the declared vertex s, then adding the arc (t, s) creates a Hamiltonian cycle exactly when G has a Hamiltonian path from s to t.

Verifying lists of vertices

def Cslib.Complexity.Graph.arcBool (G : Graph) (u v : ℕ) : Bool

Executable arc test of a directed graph: (u, v) is an edge of G.

@[simp]

theorem Cslib.Complexity.Graph.arcBool_eq_true_iff (G : Graph) (u v : ℕ) : G.arcBool u v = true ↔ (u, v) ∈ G.2

arcBool decides whether (u, v) is an edge of the list.

theorem Cslib.Complexity.Graph.computableInPolyTime_arcBool : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (Graph × ℕ) × ℕ) => p.1.1.arcBool p.1.2 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair encGraph Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBool

Testing for an arc in an encoded graph is polynomial-time.

def Cslib.Complexity.Graph.chainBool (r : ℕ → ℕ → Bool) (p : List ℕ) : Bool

Executable test that r holds between all consecutive entries of p.

theorem Cslib.Complexity.Graph.chainBool_eq_true_iff {r : ℕ → ℕ → Bool} {R : ℕ → ℕ → Prop} (hr : ∀ (u v : ℕ), r u v = true ↔ R u v) {p : List ℕ} : chainBool r p = true ↔ List.IsChain R p

chainBool r decides List.IsChain R when r decides R.

def Cslib.Complexity.Graph.cycleChainBool (r : ℕ → ℕ → Bool) (p : List ℕ) : Bool

Executable test that r holds between all consecutive entries of p read cyclically: from each entry to the next one, and from the last entry to the first.

theorem Cslib.Complexity.Graph.cycleChainBool_eq_true_iff {r : ℕ → ℕ → Bool} {R : ℕ → ℕ → Prop} (hr : ∀ (u v : ℕ), r u v = true ↔ R u v) {p : List ℕ} : cycleChainBool r p = true ↔ Cycle.Chain R ↑p

cycleChainBool r decides Cycle.Chain R when r decides R: the empty list passes, and a one-entry list [a] passes exactly when R a a.

Polynomial-time verification

theorem Cslib.Complexity.Graph.computableInPolyTime_chainBool {γ : Type} {encIn : γ ↪ List Bool} {r : γ → ℕ → ℕ → Bool} {p : γ → List ℕ} (hr : Turing.MultiTapeTM.ComputableInPolyTime (fun (q : (γ × ℕ) × ℕ) => r q.1.1 q.1.2 q.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair encIn Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBool) (hp : Turing.MultiTapeTM.ComputableInPolyTime p encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => chainBool (r x) (p x)) encIn Turing.MultiTapeTM.encBool

Testing whether r holds between consecutive entries of a computed list is polynomial-time, for an input-dependent polynomial-time test r.

theorem Cslib.Complexity.Graph.computableInPolyTime_cycleChainBool {γ : Type} {encIn : γ ↪ List Bool} {r : γ → ℕ → ℕ → Bool} {p : γ → List ℕ} (hr : Turing.MultiTapeTM.ComputableInPolyTime (fun (q : (γ × ℕ) × ℕ) => r q.1.1 q.1.2 q.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair encIn Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBool) (hp : Turing.MultiTapeTM.ComputableInPolyTime p encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => cycleChainBool (r x) (p x)) encIn Turing.MultiTapeTM.encBool

Testing whether r holds between cyclically consecutive entries of a computed list is polynomial-time, for an input-dependent polynomial-time test r.

Membership in NP

def Cslib.Complexity.DirHamPath.verifier : (Graph × ℕ × ℕ) × List Bool → Bool

The verifier for DirHamPath: decode a list of vertices from the certificate (Graph.decodeVertexList) and check that it lists every declared vertex exactly once, starts at s, ends at t, and that consecutive vertices are joined by arcs.

theorem Cslib.Complexity.DirHamPath.isVerifier : IsVerifier (Turing.MultiTapeTM.encPair encGraph (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat)) (Polynomial.X ^ 2) verifier DirHamPath

DirHamPath.verifier verifies DirHamPath with certificates of length n ^ 2 for instances of encoded length n.

theorem Cslib.Complexity.DirHamPath.computableInPolyTime_verifier : Turing.MultiTapeTM.ComputableInPolyTime verifier (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair encGraph (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat)) Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

The DirHamPath verifier is polynomial-time.

theorem Cslib.Complexity.DirHamPath.mem_NP : DirHamPath ∈ NP (Turing.MultiTapeTM.encPair encGraph (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat))

DirHamPath belongs to NP.

def Cslib.Complexity.DirHamCycle.verifier : Graph × List Bool → Bool

The verifier for DirHamCycle: decode a list of vertices from the certificate (Graph.decodeVertexList) and check that it is nonempty, lists every declared vertex exactly once, and that cyclically consecutive vertices are joined by arcs.

theorem Cslib.Complexity.DirHamCycle.isVerifier : IsVerifier encGraph (Polynomial.X ^ 2) verifier DirHamCycle

DirHamCycle.verifier verifies DirHamCycle with certificates of length n ^ 2 for graphs of encoded length n.

theorem Cslib.Complexity.DirHamCycle.computableInPolyTime_verifier : Turing.MultiTapeTM.ComputableInPolyTime verifier (Turing.MultiTapeTM.encPair encGraph Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

The DirHamCycle verifier is polynomial-time.

theorem Cslib.Complexity.DirHamCycle.mem_NP : DirHamCycle ∈ NP encGraph

DirHamCycle belongs to NP.

def Cslib.Complexity.HamPath.verifier : (Graph × ℕ × ℕ) × List Bool → Bool

The verifier for HamPath: decode a list of vertices from the certificate (Graph.decodeVertexList) and check that it lists every declared vertex exactly once, starts at s, ends at t, and that consecutive vertices are adjacent.

theorem Cslib.Complexity.HamPath.isVerifier : IsVerifier (Turing.MultiTapeTM.encPair encGraph (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat)) (Polynomial.X ^ 2) verifier HamPath

HamPath.verifier verifies HamPath with certificates of length n ^ 2 for instances of encoded length n.

theorem Cslib.Complexity.HamPath.computableInPolyTime_verifier : Turing.MultiTapeTM.ComputableInPolyTime verifier (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair encGraph (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat)) Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

The HamPath verifier is polynomial-time.

theorem Cslib.Complexity.HamPath.mem_NP : HamPath ∈ NP (Turing.MultiTapeTM.encPair encGraph (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat))

HamPath belongs to NP.

def Cslib.Complexity.HamCycle.verifier : Graph × List Bool → Bool

The verifier for HamCycle: decode a list of vertices from the certificate (Graph.decodeVertexList) and check that it has at least three vertices, lists every declared vertex exactly once, and that cyclically consecutive vertices are adjacent.

theorem Cslib.Complexity.HamCycle.isVerifier : IsVerifier encGraph (Polynomial.X ^ 2) verifier HamCycle

HamCycle.verifier verifies HamCycle with certificates of length n ^ 2 for graphs of encoded length n.

theorem Cslib.Complexity.HamCycle.computableInPolyTime_verifier : Turing.MultiTapeTM.ComputableInPolyTime verifier (Turing.MultiTapeTM.encPair encGraph Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

The HamCycle verifier is polynomial-time.

theorem Cslib.Complexity.HamCycle.mem_NP : HamCycle ∈ NP encGraph

HamCycle belongs to NP.