Hamilton circuits are NP-complete

Umbrella file for Karp's DIRECTED HAMILTON CIRCUIT (DescriptiveComplexity.DirHamCircuit) and HAMILTON CIRCUIT (DescriptiveComplexity.HamCircuit), both on the vocabulary FirstOrder.Language.digraph – a single binary relation, read as it stands by the first problem and symmetrically by the second.

A circuit visiting every vertex exactly once is a linear order of the universe whose consecutive elements are adjacent and whose last element is adjacent to its first (DescriptiveComplexity.TourOn). That reading is what puts both problems in NP without any path machinery (DescriptiveComplexity.dirHamCircuit_mem_NP, DescriptiveComplexity.hamCircuit_mem_NP): a linear order is a relation, so an existential second-order block can guess it, and the four order axioms, “is the immediate successor” and the two adjacency demands are first-order. It is the device the job-sequencing certificate uses for its schedule, closed into a cycle, and DescriptiveComplexity.tourOn_iff_enum checks that it is the intended reading: a tour is exactly a cyclic enumeration of the universe along which consecutive elements are adjacent.

The undirected problem reduces to the directed one by replacing each edge with its two arcs (DescriptiveComplexity.hamCircuit_fo_reduction_dirHamCircuit), so hardness only has to be proved on the undirected side. There it is Karp's twelve-vertex cover-testing gadget, as the relativized ordered reduction DescriptiveComplexity.vertexCover_rel_ordered_fo_reduction_hamCircuit from Vertex Cover (DescriptiveComplexity.Problems.Hamilton.Gadget for the interpretation, Forward and Reverse for the two directions of correctness, Hardness for the assembly). Both problems are NP-complete – the last of Karp's 21.

theorem DescriptiveComplexity.dirHamCircuit_mem_NP : NP.Mem DirHamCircuit

Directed Hamilton Circuit is in NP: it is Σ₁-definable, the certificate being the circuit, guessed as a linear order of the universe.

theorem DescriptiveComplexity.hamCircuit_mem_NP : NP.Mem HamCircuit

Hamilton Circuit is in NP, by the same certificate read on the symmetrized arc relation.

theorem DescriptiveComplexity.hamCircuit_NP_hard : NP.Hard HamCircuit

Hamilton Circuit is NP-hard: Vertex Cover, which is NP-hard, relativized- ordered-FO-reduces to it by the cover-testing gadget interpretation DescriptiveComplexity.hamInterp.

theorem DescriptiveComplexity.dirHamCircuit_NP_hard : NP.Hard DirHamCircuit

Directed Hamilton Circuit is NP-hard: the undirected problem, now NP-hard, FO-reduces to it by doubling each edge.

theorem DescriptiveComplexity.hamCircuit_NP_complete : NP.Complete HamCircuit

Hamilton Circuit is NP-complete, derived from the first-order reductions of this library and the Cook–Levin theorem.

theorem DescriptiveComplexity.dirHamCircuit_NP_complete : NP.Complete DirHamCircuit

Directed Hamilton Circuit is NP-complete – closing Karp's 21.