From directed to undirected Hamiltonian paths and cycles

Splitting every vertex of a directed graph into three reduces directed Hamiltonian cycles and paths to undirected ones: for cycles this is Karp's reduction [Kar72], for paths a variant of Sipser, Theorem 7.55. In Graph.split G, every declared vertex v of G becomes a path in(v) - mid(v) - out(v) (Graph.splitVertex G v r for r = 0, 1, 2), and every arc (u, v) of G becomes an edge out(u) - in(v). A middle vertex is adjacent only to the two other vertices of its gadget, so an undirected Hamiltonian path from in(s) to out(t) traverses every gadget from its entry to its exit, and the order of the gadgets is a directed Hamiltonian path from s to t; an undirected Hamiltonian cycle, read in a suitable direction, likewise traverses every gadget from its entry to its exit. Unlike Sipser's construction, the gadgets of s and t keep all three vertices, which treats the endpoints uniformly and covers s = t.

Vertices of the split graph are numbered by first occurrence in the vertex list, so repeated vertex entries share one gadget. An undeclared vertex gets labels that no declared vertex has: arcs with an undeclared endpoint become edges with an undeclared endpoint, which the undirected problems ignore, and an undeclared s or t makes both path instances negative. A self-loop (v, v) becomes the edge out(v) - in(v), so a single vertex with a self-loop, which is a directed Hamiltonian cycle, becomes a triangle.

Main definitions

• Cslib.Complexity.Graph.splitVertex, Cslib.Complexity.Graph.split.
• Cslib.Complexity.DirHamPath.toHamPath.

Main results

• Cslib.Complexity.Graph.split_mem_HamPath_iff, Cslib.Complexity.DirHamPath.toHamPath_mem_iff: ⟨G.split, G.splitVertex s 0, G.splitVertex t 2⟩ ∈ HamPath ↔ ⟨G, s, t⟩ ∈ DirHamPath.
• Cslib.Complexity.Graph.split_mem_HamCycle_iff: G.split ∈ HamCycle ↔ G ∈ DirHamCycle.
• Cslib.Complexity.Graph.computableInPolyTime_split, Cslib.Complexity.DirHamPath.computableInPolyTime_toHamPath: both reductions are polynomial-time.
• Cslib.Complexity.polyTimeReducible_DirHamPath_HamPath, Cslib.Complexity.polyTimeReducible_DirHamCycle_HamCycle.
• Cslib.Complexity.HamPath_npHard, Cslib.Complexity.HamPath_npComplete, Cslib.Complexity.HamCycle_npHard, Cslib.Complexity.HamCycle_npComplete: the undirected problems are NP-complete.

References

• R. M. Karp, Reducibility among combinatorial problems
• M. Sipser, Introduction to the Theory of Computation

def Cslib.Complexity.Graph.splitVertex (G : Graph) (v r : ℕ) : ℕ

Vertex r of the gadget of v in Graph.split G: r = 0 is in(v), r = 1 is mid(v) and r = 2 is out(v). Vertices are numbered by their first occurrence in G.1, so an undeclared vertex gets the number G.1.length, which no declared vertex has.

def Cslib.Complexity.Graph.split (G : Graph) : Graph

The vertex-splitting graph of a directed graph G: every declared vertex v becomes a path in(v) - mid(v) - out(v), and every arc (u, v) becomes an edge out(u) - in(v).

theorem Cslib.Complexity.Graph.splitVertex_eq_splitVertex_iff {G : Graph} {u v r r' : ℕ} : G.splitVertex u r = G.splitVertex v r' ↔ List.idxOf u G.vertices = List.idxOf v G.vertices ∧ r = r'

Gadget vertices are equal exactly when their vertices have the same first occurrence and their positions in the gadget agree.

theorem Cslib.Complexity.Graph.splitVertex_eq_splitVertex_iff_of_mem {G : Graph} {u v r r' : ℕ} (hv : v ∈ G.vertices) : G.splitVertex u r = G.splitVertex v r' ↔ u = v ∧ r = r'

Gadget vertices of a declared vertex determine the vertex and the position in the gadget.

theorem Cslib.Complexity.Graph.length_split_fst (G : Graph) : G.split.vertices.length = 3 * G.vertices.length

The split graph lists three vertices for each declared vertex.

theorem Cslib.Complexity.Graph.length_split_snd (G : Graph) : G.split.edges.length = 2 * G.vertices.length + G.edges.length

The split graph lists two edges for each declared vertex and one for each arc.

theorem Cslib.Complexity.Graph.mem_split_fst_iff {G : Graph} {x : ℕ} : x ∈ G.split.vertices ↔ ∃ v ∈ G.vertices, ∃ r < 3, x = G.splitVertex v r

The declared vertices of the split graph are the gadget vertices of declared vertices.

theorem Cslib.Complexity.Graph.splitVertex_mem_split_fst_iff {G : Graph} {v r : ℕ} : G.splitVertex v r ∈ G.split.vertices ↔ v ∈ G.vertices ∧ r < 3

A gadget vertex is a declared vertex of the split graph exactly when its vertex is declared and its position is 0, 1 or 2.

Adjacency in the split graph

Sequences of gadgets

Correctness of the reductions

theorem Cslib.Complexity.Graph.split_mem_HamPath_iff (G : Graph) (s t : ℕ) : { graph := G.split, source := G.splitVertex s 0, target := G.splitVertex t 2 } ∈ HamPath ↔ { graph := G, source := s, target := t } ∈ DirHamPath

Vertex splitting preserves Hamiltonian paths. A directed graph has a Hamiltonian path from s to t exactly when its split graph has an undirected Hamiltonian path from in(s) to out(t).

theorem Cslib.Complexity.Graph.split_mem_HamCycle_iff (G : Graph) : G.split ∈ HamCycle ↔ G ∈ DirHamCycle

Vertex splitting preserves Hamiltonian cycles [Kar72]. A directed graph has a Hamiltonian cycle exactly when its split graph has an undirected Hamiltonian cycle.

Polynomial-time reductions

theorem Cslib.Complexity.Graph.computableInPolyTime_split : Turing.MultiTapeTM.ComputableInPolyTime split encGraph encGraph

Splitting the vertices of a graph is polynomial-time.

def Cslib.Complexity.DirHamPath.toHamPath (x : PathInstance) : PathInstance

The reduction from DirHamPath to HamPath: split the vertices of the graph, and ask for a path from the entry of s to the exit of t.

theorem Cslib.Complexity.DirHamPath.toHamPath_mem_iff (x : PathInstance) : toHamPath x ∈ HamPath ↔ x ∈ DirHamPath

Correctness of DirHamPath.toHamPath.

theorem Cslib.Complexity.DirHamPath.computableInPolyTime_toHamPath : Turing.MultiTapeTM.ComputableInPolyTime toHamPath encPathInstance encPathInstance

The reduction DirHamPath.toHamPath is polynomial-time.

theorem Cslib.Complexity.polyTimeReducible_DirHamPath_HamPath : PolyTimeReducible encPathInstance encPathInstance DirHamPath HamPath

DirHamPath reduces to HamPath in polynomial time via DirHamPath.toHamPath.

theorem Cslib.Complexity.polyTimeReducible_DirHamCycle_HamCycle : PolyTimeReducible encGraph encGraph DirHamCycle HamCycle

DirHamCycle reduces to HamCycle in polynomial time via Graph.split.

theorem Cslib.Complexity.HamPath_npHard : NPHard encPathInstance HamPath

HamPath is NP-hard.

theorem Cslib.Complexity.HamPath_npComplete : NPComplete encPathInstance HamPath

HamPath is NP-complete Sipser, Theorem 7.55.

theorem Cslib.Complexity.HamCycle_npHard : NPHard encGraph HamCycle

HamCycle is NP-hard.

theorem Cslib.Complexity.HamCycle_npComplete : NPComplete encGraph HamCycle

HamCycle is NP-complete [Kar72].