Dominating Set: the problem

DOMINATING SET: is there a set of vertices, at most as large as the marked set, such that every vertex is in it or adjacent to it? The vocabulary is FirstOrder.Language.markedGraph, the one Vertex Cover and Clique already use: a graph together with a marked set whose cardinality is the threshold (DescriptiveComplexity.Numbers.Unary).

Domination differs from the covering properties of the clique family in one respect that matters for reductions: its condition ranges over every element of the universe, so a reduction into it cannot leave junk tuples behind – each of them has to be dominated too. The reduction of DescriptiveComplexity.Problems.DominatingSet.Reduction handles this by making the junk adjacent to the vertices that a solution always contains.

The generic property

def DescriptiveComplexity.DominatesOn {A : Type} (Adjp : A → A → Prop) (Kp : A → Prop) : Prop

Some set of vertices dominating the whole graph – every vertex belongs to it or has a neighbour in it – is at most as large as the number encoded by the Kp-marked elements.

Equations

• DescriptiveComplexity.DominatesOn Adjp Kp = ∃ (D : A → Prop), (∀ (v : A), D v ∨ ∃ (u : A), D u ∧ Adjp u v) ∧ {v : A | D v}.ncard ≤ {v : A | Kp v}.ncard

theorem DescriptiveComplexity.dominatesOn_iff_embedding {A : Type} [Finite A] (Adjp : A → A → Prop) (Kp : A → Prop) : DominatesOn Adjp Kp ↔ ∃ (D : A → Prop), (∀ (v : A), D v ∨ ∃ (u : A), D u ∧ Adjp u v) ∧ Nonempty ({ v : A // D v } ↪ { v : A // Kp v })

The domination property, with the threshold certified by an injection into the marked set – the shape the second-order definition guesses.

theorem DescriptiveComplexity.DominatesOn.of_equiv {A B : Type} (u : B ≃ A) {AdjB : B → B → Prop} {KB : B → Prop} {AdjA : A → A → Prop} {KA : A → Prop} (hadj : ∀ (b b' : B), AdjB b b' ↔ AdjA (u b) (u b')) (hK : ∀ (b : B), KB b ↔ KA (u b)) (h : DominatesOn AdjB KB) : DominatesOn AdjA KA

DominatesOn transports along an equivalence commuting with the two predicates.

theorem DescriptiveComplexity.DominatesOn.equiv_iff {A B : Type} (u : B ≃ A) {AdjB : B → B → Prop} {KB : B → Prop} {AdjA : A → A → Prop} {KA : A → Prop} (hadj : ∀ (b b' : B), AdjB b b' ↔ AdjA (u b) (u b')) (hK : ∀ (b : B), KB b ↔ KA (u b)) : DominatesOn AdjB KB ↔ DominatesOn AdjA KA

DominatesOn transports along an equivalence, iff version.

The problem

def DescriptiveComplexity.HasSmallDominatingSet (A : Type) [FirstOrder.Language.markedGraph.Structure A] : Prop

A marked graph has a dominating set at most as large as its marked set. (Finiteness of the universe is part of the property: cardinality thresholds are only meaningful on finite structures.)

Equations

• DescriptiveComplexity.HasSmallDominatingSet A = (Finite A ∧ DescriptiveComplexity.DominatesOn DescriptiveComplexity.MGAdj DescriptiveComplexity.MGMarked)

theorem DescriptiveComplexity.hasSmallDominatingSet_iso {A B : Type} [FirstOrder.Language.markedGraph.Structure A] [FirstOrder.Language.markedGraph.Structure B] (e : FirstOrder.Language.markedGraph.Equiv A B) : HasSmallDominatingSet A ↔ HasSmallDominatingSet B

The domination threshold property is isomorphism-invariant.

def DescriptiveComplexity.DominatingSet : DecisionProblem FirstOrder.Language.markedGraph

DOMINATING SET, as a problem on marked graphs: is there a set of vertices at most as large as the marked set that dominates every vertex?

Equations

• One or more equations did not get rendered due to their size.