3-colorability is NP-complete

Umbrella file for the problem 3COL (DescriptiveComplexity.ThreeCol, defined in DescriptiveComplexity.Problems.ThreeColorability.Defs), collecting its two first-order reductions –

• DescriptiveComplexity.threeCol_fo_reduction_sat : ThreeCol ≤ᶠᵒ SAT (order-free, quantifier-free; DescriptiveComplexity.Problems.ThreeColorability.ToSat), and
• DescriptiveComplexity.sat_ordered_fo_reduction_threeCol : SAT ≤ᶠᵒ[≤] ThreeCol (ordered; DescriptiveComplexity.Problems.ThreeColorability.FromSat) –

and deriving its NP-completeness from the Cook–Levin theorem (Cook 1971; Levin 1973; DescriptiveComplexity.SAT_NP_complete), with no machine model anywhere. As with any complexity-theoretic statement, these results are about finite graphs only (ComplexityClass.mem_congr_finite/hard_congr_finite).

theorem DescriptiveComplexity.threeCol_mem_NP : NP.Mem ThreeCol

3-colorability is in NP: it FO-reduces to SAT, which is in NP.

theorem DescriptiveComplexity.threeCol_NP_hard : NP.Hard ThreeCol

3-colorability is NP-hard: SAT, which is NP-hard, reduces to it by an ordered FO reduction.

theorem DescriptiveComplexity.threeCol_NP_complete : NP.Complete ThreeCol

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