3SAT is NP-complete

Umbrella file for the problem 3SAT (DescriptiveComplexity.ThreeSAT, defined in DescriptiveComplexity.Problems.ThreeSat.Defs), collecting its two first-order reductions –

• DescriptiveComplexity.threeSat_fo_reduction_sat : ThreeSAT ≤ᶠᵒ SAT (order-free, identity-like, gated on the first-order width check; DescriptiveComplexity.Problems.ThreeSat.ToSat), and
• DescriptiveComplexity.sat_ordered_fo_reduction_threeSat : SAT ≤ᶠᵒ[≤] ThreeSAT (ordered, clause splitting along the occurrence order; DescriptiveComplexity.Problems.ThreeSat.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 CNF structures only (ComplexityClass.mem_congr_finite/hard_congr_finite).

theorem DescriptiveComplexity.threeSat_mem_NP : NP.Mem ThreeSAT

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

theorem DescriptiveComplexity.threeSat_NP_hard : NP.Hard ThreeSAT

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

theorem DescriptiveComplexity.threeSat_NP_complete : NP.Complete ThreeSAT

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