Dominating Set is NP-complete

Umbrella file for DescriptiveComplexity.DominatingSet, deriving NP-completeness from

• DescriptiveComplexity.dominatingSet_sigmaSODefinable (DescriptiveComplexity.Problems.DominatingSet.Membership): membership, by guessing the dominating set and an injection of it into the marked set;
• DescriptiveComplexity.DomRed.setCover_fo_reduction_dominatingSet (DescriptiveComplexity.Problems.DominatingSet.Reduction): hardness, from the NP-hardness of Set Cover, and so ultimately from the Cook–Levin theorem.

The reduction is order-free, which is worth recording: domination constrains every element of the universe, junk tuples included, and the two degenerate cases (an element in no set, and no element at all) look at first sight as if they needed a canonical extra vertex – i.e. an order. They do not: both are first-order conditions, so gating on them is enough.

theorem DescriptiveComplexity.dominatingSet_mem_NP : NP.Mem DominatingSet

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

theorem DescriptiveComplexity.dominatingSet_NP_hard : NP.Hard DominatingSet

Dominating Set is NP-hard: Set Cover, which is NP-hard, FO-reduces to it by the incidence graph of the set system.

theorem DescriptiveComplexity.dominatingSet_NP_complete : NP.Complete DominatingSet

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