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.edges, 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 instances ⟨G, s, t⟩ (Cslib.Complexity.PathInstance) 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 Cslib.Complexity.encPathInstance, the graph followed by the two endpoints in binary, and cycle instances by encGraph.

Main definitions

• Cslib.Complexity.PathInstance: instances ⟨G, source, target⟩ for DirHamPath and HamPath.
• Cslib.Complexity.Graph.IsDirHamPath, Cslib.Complexity.DirHamPath.
• Cslib.Complexity.Graph.IsDirHamCycle, Cslib.Complexity.DirHamCycle.
• Cslib.Complexity.HamPath, Cslib.Complexity.HamCycle.
• Cslib.Complexity.encPathInstance: the encoding of PathInstance.
• 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 encPathInstance.
• Cslib.Complexity.DirHamCycle.isVerifier, Cslib.Complexity.DirHamCycle.mem_NP: DirHamCycle ∈ NP encGraph.
• Cslib.Complexity.HamPath.isVerifier, Cslib.Complexity.HamPath.mem_NP: HamPath ∈ NP encPathInstance.
• 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.

structure Cslib.Complexity.PathInstance : Type

An instance ⟨G, source, target⟩ of the Hamiltonian path problems Cslib.Complexity.DirHamPath and Cslib.Complexity.HamPath.

• graph : Graph

  The graph in which to find a Hamiltonian path.

• source : ℕ

  The start vertex of the path.

• target : ℕ

  The end vertex of the path.

theorem Cslib.Complexity.PathInstance.ext_iff {x y : PathInstance} : x = y ↔ x.graph = y.graph ∧ x.source = y.source ∧ x.target = y.target

theorem Cslib.Complexity.PathInstance.ext {x y : PathInstance} (graph : x.graph = y.graph) (source : x.source = y.source) (target : x.target = y.target) : x = y

def Cslib.Complexity.instDecidableEqPathInstance.decEq (x✝ x✝¹ : PathInstance) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Complexity.instDecidableEqPathInstance : DecidableEq PathInstance

@[instance_reducible]

instance Cslib.Complexity.instReprPathInstance : Repr PathInstance

def Cslib.Complexity.instReprPathInstance.repr : PathInstance → ℕ → Std.Format

@[instance_reducible]

instance Cslib.Complexity.instInhabitedPathInstance : Inhabited PathInstance

theorem Cslib.Complexity.encPathInstance_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → Graph} {x1 x2 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInPolyTime x0 encIn encGraph) (h1 : Turing.MultiTapeTM.ComputableInPolyTime x1 encIn Turing.MultiTapeTM.encNat) (h2 : Turing.MultiTapeTM.ComputableInPolyTime x2 encIn Turing.MultiTapeTM.encNat) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { graph := x0 x, source := x1 x, target := x2 x }) encIn encPathInstance

theorem Cslib.Complexity.encPathInstance_target_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → PathInstance} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encPathInstance → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).target) encIn✝ Turing.MultiTapeTM.encNat

theorem Cslib.Complexity.encPathInstance_source_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → PathInstance} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encPathInstance S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).source) encIn✝ Turing.MultiTapeTM.encNat S✝

theorem Cslib.Complexity.encPathInstance_target_deg : Turing.MultiTapeTM.ComputableInDegree PathInstance.target encPathInstance Turing.MultiTapeTM.encNat 1 1

theorem Cslib.Complexity.encPathInstance_source_deg : Turing.MultiTapeTM.ComputableInDegree PathInstance.source encPathInstance Turing.MultiTapeTM.encNat 1 1

theorem Cslib.Complexity.encPathInstance_graph_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → PathInstance} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encPathInstance → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).graph) encIn✝ encGraph

theorem Cslib.Complexity.encPathInstance_graph_deg : Turing.MultiTapeTM.ComputableInDegree PathInstance.graph encPathInstance encGraph 1 1

theorem Cslib.Complexity.encPathInstance_target_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → PathInstance} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encPathInstance S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).target) encIn✝ Turing.MultiTapeTM.encNat S✝

@[reducible, inline]

abbrev Cslib.Complexity.encPathInstanceFields : Graph × ℕ × ℕ ↪ List Bool

The tuple of the fields of encPathInstance.

theorem Cslib.Complexity.encPathInstance_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget : γ → ℕ} {x0 : γ → Graph} {x1 x2 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInSpace x0 encIn encGraph budget) (h1 : Turing.MultiTapeTM.ComputableInSpace x1 encIn Turing.MultiTapeTM.encNat budget) (h2 : Turing.MultiTapeTM.ComputableInSpace x2 encIn Turing.MultiTapeTM.encNat budget) : Turing.MultiTapeTM.ComputableInSpace (fun (x : γ) => { graph := x0 x, source := x1 x, target := x2 x }) encIn encPathInstance budget

theorem Cslib.Complexity.encPathInstance_source_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → PathInstance} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encPathInstance → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).source) encIn✝ Turing.MultiTapeTM.encNat

theorem Cslib.Complexity.encPathInstance_target_inO : Turing.MultiTapeTM.ComputableInO PathInstance.target encPathInstance Turing.MultiTapeTM.encNat (fun (a : PathInstance) => (encPathInstance a).length) fun (a : PathInstance) => (encPathInstance a).length

theorem Cslib.Complexity.encPathInstance_graph_inO : Turing.MultiTapeTM.ComputableInO PathInstance.graph encPathInstance encGraph (fun (a : PathInstance) => (encPathInstance a).length) fun (a : PathInstance) => (encPathInstance a).length

theorem Cslib.Complexity.encPathInstance_graph_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → PathInstance} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encPathInstance S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).graph) encIn✝ encGraph S✝

@[simp]

theorem Cslib.Complexity.encPathInstance_apply (a : PathInstance) : encPathInstance a = encPathInstanceFields (a.graph, a.source, a.target)

theorem Cslib.Complexity.encPathInstance_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : PathInstance) => (a.graph, a.source, a.target)) encPathInstance encPathInstanceFields 1 1

def Cslib.Complexity.encPathInstance : PathInstance ↪ List Bool

Encoding of PathInstance as (graph, (source, target)) with both endpoints in binary.

theorem Cslib.Complexity.encPathInstance_source_inO : Turing.MultiTapeTM.ComputableInO PathInstance.source encPathInstance Turing.MultiTapeTM.encNat (fun (a : PathInstance) => (encPathInstance a).length) fun (a : PathInstance) => (encPathInstance a).length

theorem Cslib.Complexity.encPathInstance_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → Graph} {T0 S0 x1 T1 S1 x2 T2 S2 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInO x0 encIn encGraph T0 S0) (h1 : Turing.MultiTapeTM.ComputableInO x1 encIn Turing.MultiTapeTM.encNat T1 S1) (h2 : Turing.MultiTapeTM.ComputableInO x2 encIn Turing.MultiTapeTM.encNat T2 S2) : Turing.MultiTapeTM.ComputableInO (fun (x : γ) => { graph := x0 x, source := x1 x, target := x2 x }) encIn encPathInstance (fun (x : γ) => T0 x + (T1 x + T2 x)) fun (x : γ) => S0 x + (S1 x + S2 x)

theorem Cslib.Complexity.encPathInstance_mk_deg : Turing.MultiTapeTM.ComputableInDegree (fun (p : Graph × ℕ × ℕ) => { graph := p.1, source := p.2.1, target := p.2.2 }) encPathInstanceFields encPathInstance 1 1

def Cslib.Complexity.DirHamPath : Set PathInstance

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 PathInstance

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 : ℕ} : { graph := G, source := s, target := t } ∈ HamPath ↔ ∃ (p : List ℕ), p.Nodup ∧ (∀ (v : ℕ), v ∈ p ↔ v ∈ G.vertices) ∧ 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.vertices) ∧ 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.vertices) (hin : ∀ (u : ℕ), (u, s) ∉ G.edges) : { vertices := G.vertices, edges := (t, s) :: G.edges } ∈ DirHamCycle ↔ { graph := G, source := s, target := 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.edges

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 : PathInstance × 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 encPathInstance (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 encPathInstance Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

The DirHamPath verifier is polynomial-time.

theorem Cslib.Complexity.DirHamPath.mem_NP : DirHamPath ∈ NP encPathInstance

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 : PathInstance × 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 encPathInstance (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 encPathInstance Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

The HamPath verifier is polynomial-time.

theorem Cslib.Complexity.HamPath.mem_NP : HamPath ∈ NP encPathInstance

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.