The set family is NP-complete

Umbrella file for the three problems on set systems – Set Cover, Hitting Set and Set Packing (DescriptiveComplexity.SetCover, DescriptiveComplexity.HittingSet, DescriptiveComplexity.SetPacking, defined in DescriptiveComplexity.Problems.SetFamily.Defs) – collecting the quantifier-free reductions of DescriptiveComplexity.Problems.SetFamily.Reductions (the transposition relating Set Cover and Hitting Set) and DescriptiveComplexity.Problems.SetFamily.FromGraphs (the edge-incidence reading of a marked graph), and deriving NP-completeness from

• DescriptiveComplexity.setCover_sigmaSODefinable and DescriptiveComplexity.setPacking_sigmaSODefinable (DescriptiveComplexity.Problems.SetFamily.Membership): membership, by guessing the subfamily and the injection witnessing the threshold;
• DescriptiveComplexity.vertexCover_fo_reduction_setCover and DescriptiveComplexity.indSet_fo_reduction_setPacking: hardness, from the NP-hardness of Vertex Cover and Independent Set (DescriptiveComplexity.Problems.CliqueFamily), and so ultimately from the Cook–Levin theorem, with no machine model anywhere.

Membership then travels backward and hardness forward along the transposition, which relates Set Cover and Hitting Set in both directions, giving DescriptiveComplexity.hittingSet_NP_complete. This is the set-system mirror of the clique family: there, complementation relates the three graph problems and one Σ₁ definition serves them all; here the transposition relates two of them, while Set Packing – whose threshold is a lower bound, like Clique's – carries its own definition. As with any complexity-theoretic statement, these results are about finite set systems only (DescriptiveComplexity.ComplexityClass.mem_congr_finite/hard_congr_finite).

NP-completeness

theorem DescriptiveComplexity.setCover_mem_NP : NP.Mem SetCover

Set Cover is in NP: it is Σ₁-definable.

theorem DescriptiveComplexity.setCover_NP_hard : NP.Hard SetCover

Set Cover is NP-hard: Vertex Cover, which is NP-hard, reduces to it by the edge-incidence interpretation.

theorem DescriptiveComplexity.setCover_NP_complete : NP.Complete SetCover

Set Cover is NP-complete, derived from the first-order reductions of this library and the Cook–Levin theorem. Registered in the Lax archive as Lax799700.SetFamily.setCover_NP_complete.

theorem DescriptiveComplexity.hittingSet_mem_NP : NP.Mem HittingSet

Hitting Set is in NP: it FO-reduces to Set Cover, which is in NP.

theorem DescriptiveComplexity.hittingSet_NP_hard : NP.Hard HittingSet

Hitting Set is NP-hard: Set Cover, which is NP-hard, reduces to it by transposing the incidence relation.

theorem DescriptiveComplexity.hittingSet_NP_complete : NP.Complete HittingSet

Hitting Set is NP-complete. Registered in the Lax archive as Lax799700.SetFamily.hittingSet_NP_complete.

theorem DescriptiveComplexity.setPacking_mem_NP : NP.Mem SetPacking

Set Packing is in NP: it is Σ₁-definable.

theorem DescriptiveComplexity.setPacking_NP_hard : NP.Hard SetPacking

Set Packing is NP-hard: Independent Set, which is NP-hard, reduces to it by the edge-incidence interpretation.

theorem DescriptiveComplexity.setPacking_NP_complete : NP.Complete SetPacking

Set Packing is NP-complete. Registered in the Lax archive as Lax799700.SetFamily.setPacking_NP_complete.

theorem DescriptiveComplexity.exactCover_mem_NP : NP.Mem ExactCover

Exact Cover is in NP: it is Σ₁-definable – guess the subfamily, then check covering and disjointness first-order. Its NP-hardness, from exactly-one satisfiability, is in DescriptiveComplexity.Problems.ExactCover.