2.7. The Catalogue🔗

Every other NP-completeness proof in the library starts from Cook–Levin and follows reductions. Here is the tree, with the reduction for each edge and the completeness theorem for each problem:

• SAT reduces to 3SAT (polyTimeReducible_SAT_ThreeSAT, ThreeSAT_npComplete), and 3SAT to exact 3SAT (polyTimeReducible_ThreeSAT_ExactThreeSAT, ExactThreeSAT_npComplete) and to subset sum (polyTimeReducible_ThreeSAT_SubsetSum, SubsetSum_npComplete).

• Subset sum reduces to partition (polyTimeReducible_SubsetSum_Partition, Partition_npComplete), knapsack (polyTimeReducible_SubsetSum_Knapsack, Knapsack_npComplete) and zero-one integer programming (polyTimeReducible_SubsetSum_ZeroOneIP, ZeroOneIP_npComplete).

• SAT reduces to independent set (polyTimeReducible_SAT_IndependentSet, IndependentSet_npComplete), which reduces to clique (polyTimeReducible_IndependentSet_Clique, Clique_npComplete) and vertex cover (polyTimeReducible_IndependentSet_VertexCover, VertexCover_npComplete).

• SAT reduces to three-colorability (polyTimeReducible_SAT_ThreeColoring, ThreeColoring_npComplete) and to k-colorability for every k ≥ 3 (polyTimeReducible_SAT_KColoring, KColoring_npComplete).

• SAT reduces to directed Hamiltonian paths and cycles (polyTimeReducible_SAT_DirHamPath, DirHamPath_npComplete, polyTimeReducible_SAT_DirHamCycle, DirHamCycle_npComplete), these reduce to their undirected versions (polyTimeReducible_DirHamPath_HamPath, HamPath_npComplete, polyTimeReducible_DirHamCycle_HamCycle, HamCycle_npComplete), and Hamiltonian cycles reduce to the traveling salesperson problem (polyTimeReducible_HamCycle_TSP, TSP_npComplete).

• SAT reduces to circuit satisfiability (SAT.polyTimeReducible_CircuitSAT, CircuitSAT_npComplete).

Chaining reductions with NPHard.trans gives the hardness of any problem in the tree directly from Cook–Levin:

The module documentation of Complexity.Computability.Complexity.Reduction indexes the same results by problem, with the module to import for each.