Directed Hamiltonian paths and cycles are NP-hard

SAT.toDirHamPath is the diamond construction of Sipser, Theorem 7.46. Each variable occurrence of φ, in order of occurrence, gets a diamond: a top node, a bottom node (the top of the next diamond), and a row of 3 * φ.length + 3 nodes joined both ways in a line. The top has arcs to both ends of the row, and both ends have arcs to the bottom. Clause j owns the pair of row nodes 3 * j + 2 and 3 * j + 3, and the nodes 3 * j + 1 separate the pairs. A literal (x, b) of clause j adds a detour through the node of clause j across the pair of j in the diamond of the first occurrence of x: left to right when b is true, right to left when it is false. The instance asks for a Hamiltonian path from the first top to the last bottom.

A satisfying assignment gives a path that traverses each row rightwards or leftwards according to the value of its variable and visits each clause node by the detour of the first true literal of the clause. Conversely, in a Hamiltonian path every separator has its two row neighbours as predecessor and successor, a detour must return to the pair it left, so all separators of a row point the same way, and the node of a clause is entered from a pair whose row points the way of a true literal. Diamonds of repeated occurrences of a variable carry no detours and can be traversed either way. This argument is carried out for diamond graphs with any layout of the rows (Cslib.Complexity.Diamond.mem_DirHamPath_iff); the graph here has a slot for each clause in every row (SAT.toDirHamPath_eq). Clauses of every width, including the empty clause, are handled, so the reduction is from SAT; it also reduces ThreeSAT after rejecting clauses with more than three literals.

Graph.mem_DirHamCycle_cons_iff closes Hamiltonian paths into cycles with an arc back to a start vertex that no arc enters. The top of the first diamond is such a vertex (Diamond.mem_DirHamCycle_iff), which gives SAT.toDirHamCycle.

Main definitions

• Cslib.Complexity.SAT.diamondDetours, Cslib.Complexity.SAT.diamondGraph: the diamond graph, with the node labels of Cslib.Complexity.Diamond.graph.
• Cslib.Complexity.SAT.toDirHamPath, Cslib.Complexity.SAT.toDirHamCycle.

Main results

• Cslib.Complexity.SAT.toDirHamPath_eq: the graph as a diamond graph.
• Cslib.Complexity.SAT.toDirHamPath_mem_iff: toDirHamPath φ ∈ DirHamPath ↔ φ ∈ SAT.
• Cslib.Complexity.SAT.toDirHamCycle_mem_iff: toDirHamCycle φ ∈ DirHamCycle ↔ φ ∈ SAT.
• Cslib.Complexity.SAT.computableInPolyTime_toDirHamPath, Cslib.Complexity.SAT.computableInPolyTime_toDirHamCycle: the reductions are polynomial-time.
• Cslib.Complexity.polyTimeReducible_SAT_DirHamPath, Cslib.Complexity.polyTimeReducible_ThreeSAT_DirHamPath, Cslib.Complexity.DirHamPath_npHard, Cslib.Complexity.polyTimeReducible_SAT_DirHamCycle, Cslib.Complexity.DirHamCycle_npHard.
• Cslib.Complexity.DirHamPath_npComplete, Cslib.Complexity.DirHamCycle_npComplete: the directed problems are NP-complete.

References

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

The diamond graph

def Cslib.Complexity.SAT.diamondDetours (φ : Logic.PL.CNF ℕ) : List Diamond.Detour

The detours of the diamond graph: the literal l of clause j goes through the node of clause j across slot j of the row of the first occurrence of its variable, left to right when l is positive.

def Cslib.Complexity.SAT.diamondGraph (φ : Logic.PL.CNF ℕ) : Graph

The diamond graph of φ (Cslib.Complexity.Diamond.graph): a diamond for each variable occurrence, in order of occurrence, a slot for each clause in every row, and the detours of the literals.

def Cslib.Complexity.SAT.toDirHamPath (φ : Logic.PL.CNF ℕ) : PathInstance

The reduction from SAT to DirHamPath Sipser, Theorem 7.46: the diamond graph of φ, from the top of the first diamond to the bottom of the last.

def Cslib.Complexity.SAT.toDirHamCycle (φ : Logic.PL.CNF ℕ) : Graph

The reduction from SAT to DirHamCycle: the diamond graph of φ with an arc from the bottom of the last diamond back to the top of the first.

theorem Cslib.Complexity.SAT.toDirHamPath_eq (φ : Logic.PL.CNF ℕ) : toDirHamPath φ = { graph := Diamond.graph φ.vars.length (fun (x : ℕ) => List.length φ) (List.length φ) (diamondDetours φ), source := Diamond.topNode 0, target := Diamond.topNode φ.vars.length }

The diamond graph of φ as a diamond graph with a slot for each clause in every row.

Correctness

theorem Cslib.Complexity.SAT.satisfiable_diamondDetours_iff (φ : Logic.PL.CNF ℕ) : Diamond.Satisfiable (List.length φ) (diamondDetours φ) ↔ φ ∈ SAT

Directions of the rows satisfying every clause are satisfying assignments.

theorem Cslib.Complexity.SAT.toDirHamPath_mem_iff (φ : Logic.PL.CNF ℕ) : toDirHamPath φ ∈ DirHamPath ↔ φ ∈ SAT

Correctness of the diamond construction. A formula is satisfiable exactly when its diamond graph has a Hamiltonian path from the top of the first diamond to the bottom of the last.

theorem Cslib.Complexity.SAT.mem_SAT_of_toDirHamPath_mem {φ : Logic.PL.CNF ℕ} (h : toDirHamPath φ ∈ DirHamPath) : φ ∈ SAT

A Hamiltonian path of the diamond graph yields a satisfying assignment.

Polynomial-time reductions

theorem Cslib.Complexity.SAT.computableInPolyTime_diamondGraph : Turing.MultiTapeTM.ComputableInPolyTime diamondGraph encCNF encGraph

The diamond graph is computable in polynomial time: node labels are computed in unary from diamond, row, clause and first-occurrence indices, then converted to binary.

theorem Cslib.Complexity.SAT.computableInPolyTime_toDirHamPath : Turing.MultiTapeTM.ComputableInPolyTime toDirHamPath encCNF encPathInstance

The reduction toDirHamPath is computable in polynomial time.

theorem Cslib.Complexity.SAT.toDirHamCycle_mem_iff (φ : Logic.PL.CNF ℕ) : toDirHamCycle φ ∈ DirHamCycle ↔ φ ∈ SAT

Correctness of the cycle construction. A formula is satisfiable exactly when its closed diamond graph has a Hamiltonian cycle.

theorem Cslib.Complexity.SAT.computableInPolyTime_toDirHamCycle : Turing.MultiTapeTM.ComputableInPolyTime toDirHamCycle encCNF encGraph

The closed diamond graph is computable in polynomial time.

theorem Cslib.Complexity.polyTimeReducible_SAT_DirHamPath : PolyTimeReducible encCNF encPathInstance SAT DirHamPath

SAT reduces to DirHamPath in polynomial time via SAT.toDirHamPath.

theorem Cslib.Complexity.polyTimeReducible_ThreeSAT_DirHamPath : PolyTimeReducible encCNF encPathInstance ThreeSAT DirHamPath

ThreeSAT reduces to DirHamPath in polynomial time: a formula with a clause of more than three literals is mapped to the diamond graph of the empty clause, which has no Hamiltonian path.

theorem Cslib.Complexity.DirHamPath_npHard : NPHard encPathInstance DirHamPath

DirHamPath is NP-hard.

theorem Cslib.Complexity.polyTimeReducible_SAT_DirHamCycle : PolyTimeReducible encCNF encGraph SAT DirHamCycle

SAT reduces to DirHamCycle in polynomial time via SAT.toDirHamCycle.

theorem Cslib.Complexity.DirHamCycle_npHard : NPHard encGraph DirHamCycle

DirHamCycle is NP-hard.

theorem Cslib.Complexity.DirHamPath_npComplete : NPComplete encPathInstance DirHamPath

DirHamPath is NP-complete.

theorem Cslib.Complexity.DirHamCycle_npComplete : NPComplete encGraph DirHamCycle

DirHamCycle is NP-complete.