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).

• 3SAT reduces to maximum 2-satisfiability (polyTimeReducible_ThreeSAT_MaxTwoSAT, MaxTwoSAT_npComplete): given clauses of at most two literals and a binary target K, can some assignment satisfy K of them? Each clause of three literals becomes the ten-clause gadget of Garey, Johnson and Stockmeyer (MaxTwoSAT.gadget) with a fresh variable, whose satisfied clauses depend only on four truth values (MaxTwoSAT.countP_gadget). An assignment satisfies at most seven of them (MaxTwoSAT.gadgetScore_le), seven when the source clause holds and the fresh variable is the majority of its literals (MaxTwoSAT.gadgetScore_majority), and at most six when it fails (MaxTwoSAT.gadgetScore_false_le). Short clauses are first padded by repetition through toExactThreeSAT. Plain 2-satisfiability, by contrast, is in NL (TwoSAT.mem_NL).

• 3SAT reduces to ThreeSATThree via toThreeSATThree (ThreeSATThree_npComplete). Its clauses have at most three literals, including binary clauses, and every variable has at most three literal occurrences. Repetitions within a clause count separately. Cslib.Logic.PL.CNF.toThreeOccurrence gives each occurrence a fresh copy and connects copies by binary implication cycles. For m clauses and ℓ literal occurrences it produces exactly m + ℓ clauses, 3ℓ literal occurrences, and ℓ distinct variables. The implication cycles force each copy's value, so the reduction also preserves the exact number of satisfying assignments (modelCount_toThreeSATThree). No planarity condition is imposed.

• Ordinary SAT with exactly three distinct variables per clause is NP-complete (EUThreeSAT_npComplete). This strengthens the repeated-literal convention of ExactThreeSAT. There is no occurrence bound: exact-three distinct-variable formulas with at most three occurrences per variable are always satisfiable by Hall's matching argument (Cslib.Logic.PL.CNF.satisfiable_of_exactThreeDistinct_of_count_le_three). Accordingly, EUThreeSATThree.mem_P decides this language by checking its syntax alone.

• Not-all-equal SAT requires both a true and a false literal in every clause (Cslib.Logic.PL.CNF.evalNAE). NAE3SAT, with width at most three, is NP-complete (NAEThreeSAT_npComplete). NAE EU3SAT, with exactly three distinct variables per clause, is NP-complete (NAEEUThreeSAT_npComplete). NAE3SAT-3, with width at most three and at most three occurrences per variable, is NP-complete (NAEThreeSATThree_npComplete). The last reduction reuses toThreeSATThree and permits binary clauses. It does not establish hardness with both exact-three clauses and occurrence bound three.

• Orthogonal planar 3SAT-3 is NP-hard, both when a drawing must exist (PlanarThreeSATThree_npHard) and when it is supplied (DrawnPlanarThreeSATThree_npHard). Clauses have width at most three, binary clauses are allowed, and each variable has at most three literal occurrences. Routes are simple integer orthogonal paths whose full real supports meet only at common graph endpoints. The native polynomial-time compiler toDrawnPlanarThreeSAT starts from ordinary 3SAT. Its paired implications and local templates have unique extensions, preserving the exact model count (modelCount_toPlanarThreeSAT); only occurring variables are counted. For original size S = clauses + literal occurrences + 1, its grid sides are at most 13440*S; formula size, route count, segment count and Manhattan wire length are quadratic in S (toDrawnPlanarThreeSAT_fits, toDrawnPlanarThreeSAT_costs).

• Positive 1-in-3SAT and positive 1-in-E3SAT are NP-complete, with or without the restriction that each variable occurs at most three times (PositiveOneInThreeSAT_npComplete, PositiveOneInExactThreeSAT_npComplete, PositiveOneInThreeSATThree_npComplete, PositiveOneInExactThreeSATThree_npComplete). Positive means no negated literals; exactly one literal occurrence must be true in each clause. E3 requires exactly three distinct variables per clause. The same compiler toPositiveOneInExactThreeSATThree produces this strongest syntax and, on valid 3SAT inputs, preserves counts on occurring variables (oneModelCount_toPositiveOneInExactThreeSATThree). For m source clauses and ℓ literal occurrences, it produces at most 169*(m + ℓ) clauses and 507*(m + ℓ) occurrences (size_toPositiveOneInExactThreeSATThree).

• Planar positive 1-in-E3SAT-3 is NP-hard both with an existential drawing (PlanarPositiveOneInExactThreeSATThree_npHard) and with its actual drawing supplied (DrawnPlanarPositiveOneInExactThreeSATThree_npHard). The width-at-most-three planar variant is also NP-hard (PlanarPositiveOneInThreeSATThree_npHard). These endpoints assert NP-hardness; the NP membership proofs above concern the nonplanar languages. The local positive replacement scales supplied grid sides from W,H to at most 1080000*(W + 1),1080000*(H + 1) (SAT.ExactOne.positiveDrawing_fits), with constant-factor formula and drawing costs (SAT.ExactOne.positiveDrawing_costs). Composed with ordinary 3SAT planarization, grid sides remain linear and formula size, vertices, routes, segments and Manhattan wire length remain quadratic in S = clauses + literal occurrences + 1 (toDrawnPlanarPositiveOneInExactThreeSATThree_fits, toDrawnPlanarPositiveOneInExactThreeSATThree_costs). The full compiler toDrawnPlanarPositiveOneInExactThreeSATThree computes the actual formula, binary coordinates and route lists in native polynomial time (computableInPolyTime_toDrawnPlanarPositiveOneInExactThreeSATThree). On valid 3SAT inputs it preserves the exact model count (oneModelCount_toPlanarPositiveOneInExactThreeSATThree). The positive gadgets follow Hunt et al., Theorem 3.8, Figures 3.4–3.5; their satisfying extensions are unique.

• Subset sum reduces to partition (polyTimeReducible_SubsetSum_Partition, Partition_npComplete), knapsack (polyTimeReducible_SubsetSum_Knapsack, Knapsack_npComplete), zero-one integer programming (polyTimeReducible_SubsetSum_ZeroOneIP, ZeroOneIP_npComplete) and sequencing with deadlines and penalties (polyTimeReducible_SubsetSum_JobSequencing, JobSequencing_npComplete). Partition reduces to weighted maximum cut through Karp's complete graph weighted by products (polyTimeReducible_Partition_MaxCut, MaxCut_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).

• Vertex cover reduces to directed feedback vertex set by replacing every edge with two opposite arcs (polyTimeReducible_VertexCover_FeedbackVertexSet, FeedbackVertexSet_npComplete), which reduces to feedback arc set by splitting every vertex into an arc (polyTimeReducible_FeedbackVertexSet_FeedbackArcSet, FeedbackArcSet_npComplete).

• Vertex cover reduces to dominating set through a hub adjacent to a copy of every vertex, a pendant on the hub, and a vertex for every edge adjacent to the copies of its endpoints (polyTimeReducible_VertexCover_DominatingSet, DominatingSet_npComplete).

• SAT reduces to three-colorability (polyTimeReducible_SAT_ThreeColoring, ThreeColoring_npComplete) and to k-colorability for every k ≥ 3 (polyTimeReducible_SAT_KColoring, KColoring_npComplete). Fixed colorability reduces to chromatic number, with the number of colors in the input (polyTimeReducible_KColoring_ChromaticNumber, ChromaticNumber_npComplete), which reduces to clique cover by complementing the graph (polyTimeReducible_ChromaticNumber_CliqueCover, CliqueCover_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 CslibFrontier.Computability.Complexity.Reduction indexes the same results by problem, with the module to import for each.