Set Cover FO-reduces to Dominating Set

The classical reduction – ground elements and sets become vertices, the sets form a clique, and a set is joined to its elements – with the two degenerate cases that make it delicate handled by gates rather than by a canonical extra vertex. The reduction is therefore order-free, which a condition ranging over every vertex would not lead one to expect.

The two gates, both first-order:

• DescriptiveComplexity.DomRed.Uncoverable, “some ground element belongs to no set”: the input is then a no-instance, and the output is made edgeless with an empty threshold, hence a no-instance too;
• DescriptiveComplexity.DomRed.NoElem, “there is no ground element at all”: the input is then a yes-instance (the empty cover works), and the output is made edgeless with everything marked, hence a yes-instance too.

Outside those two cases every cover is nonempty – it has to cover something – which is exactly what the domination argument needs: a nonempty set of set-vertices dominates the whole clique, and with it every junk vertex, since the junk is made adjacent to all set-vertices. Junk cannot be ignored here: domination constrains every element of the universe, unlike the covering and packing conditions of the set family.

Formula builders over the vocabulary of set systems

def DescriptiveComplexity.DomRed.elemF {α : Type} (x : α) : FirstOrder.Language.setSystem.Formula α

x is a ground element, as a formula.

Equations

• DescriptiveComplexity.DomRed.elemF x = FirstOrder.Language.ssElem.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.DomRed.famF {α : Type} (f : α) : FirstOrder.Language.setSystem.Formula α

f is a set of the family, as a formula.

Equations

• DescriptiveComplexity.DomRed.famF f = FirstOrder.Language.ssFam.formula₁ (FirstOrder.Language.var f)

def DescriptiveComplexity.DomRed.memF {α : Type} (x f : α) : FirstOrder.Language.setSystem.Formula α

x belongs to f, as a formula.

Equations

• DescriptiveComplexity.DomRed.memF x f = FirstOrder.Language.ssMem.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var f)

def DescriptiveComplexity.DomRed.markF {α : Type} (x : α) : FirstOrder.Language.setSystem.Formula α

x is marked, as a formula.

Equations

• DescriptiveComplexity.DomRed.markF x = FirstOrder.Language.ssMarked.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.DomRed.eqF {α : Type} (x y : α) : FirstOrder.Language.setSystem.Formula α

x = y, as a formula.

Equations

• DescriptiveComplexity.DomRed.eqF x y = (FirstOrder.Language.var x).equal (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.DomRed.uncoverableF {α : Type} : FirstOrder.Language.setSystem.Formula α

Some ground element belongs to no set, as a formula.

Equations

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

noncomputable def DescriptiveComplexity.DomRed.noElemF {α : Type} : FirstOrder.Language.setSystem.Formula α

There is no ground element at all, as a formula.

Equations

• DescriptiveComplexity.DomRed.noElemF = FirstOrder.Language.Formula.iAlls Unit (FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.DomRed.elemF (Sum.inr ())))

noncomputable def DescriptiveComplexity.DomRed.gateF {α : Type} : FirstOrder.Language.setSystem.Formula α

The gate: either degenerate case.

Equations

• DescriptiveComplexity.DomRed.gateF = DescriptiveComplexity.DomRed.uncoverableF ⊔ DescriptiveComplexity.DomRed.noElemF

@[simp]

theorem DescriptiveComplexity.DomRed.realize_elemF {A : Type} [FirstOrder.Language.setSystem.Structure A] {α : Type} {v : α → A} {x : α} : (elemF x).Realize v ↔ SSElem (v x)

@[simp]

theorem DescriptiveComplexity.DomRed.realize_famF {A : Type} [FirstOrder.Language.setSystem.Structure A] {α : Type} {v : α → A} {f : α} : (famF f).Realize v ↔ SSFam (v f)

@[simp]

theorem DescriptiveComplexity.DomRed.realize_memF {A : Type} [FirstOrder.Language.setSystem.Structure A] {α : Type} {v : α → A} {x f : α} : (memF x f).Realize v ↔ SSMem (v x) (v f)

@[simp]

theorem DescriptiveComplexity.DomRed.realize_markF {A : Type} [FirstOrder.Language.setSystem.Structure A] {α : Type} {v : α → A} {x : α} : (markF x).Realize v ↔ SSMarked (v x)

@[simp]

theorem DescriptiveComplexity.DomRed.realize_eqF {A : Type} [FirstOrder.Language.setSystem.Structure A] {α : Type} {v : α → A} {x y : α} : (eqF x y).Realize v ↔ v x = v y

def DescriptiveComplexity.DomRed.Uncoverable (A : Type) [FirstOrder.Language.setSystem.Structure A] : Prop

Some ground element belongs to no set: the input is then a no-instance.

Equations

• DescriptiveComplexity.DomRed.Uncoverable A = ∃ (x : A), DescriptiveComplexity.SSElem x ∧ ∀ (f : A), ¬(DescriptiveComplexity.SSFam f ∧ DescriptiveComplexity.SSMem x f)

def DescriptiveComplexity.DomRed.NoElem (A : Type) [FirstOrder.Language.setSystem.Structure A] : Prop

There is no ground element at all: the empty cover then works.

Equations

• DescriptiveComplexity.DomRed.NoElem A = ∀ (x : A), ¬DescriptiveComplexity.SSElem x

@[simp]

theorem DescriptiveComplexity.DomRed.realize_uncoverableF {A : Type} [FirstOrder.Language.setSystem.Structure A] {α : Type} {v : α → A} : uncoverableF.Realize v ↔ Uncoverable A

@[simp]

theorem DescriptiveComplexity.DomRed.realize_noElemF {A : Type} [FirstOrder.Language.setSystem.Structure A] {α : Type} {v : α → A} : noElemF.Realize v ↔ NoElem A

@[simp]

theorem DescriptiveComplexity.DomRed.realize_gateF {A : Type} [FirstOrder.Language.setSystem.Structure A] {α : Type} {v : α → A} : gateF.Realize v ↔ Uncoverable A ∨ NoElem A

The interpretation

inductive DescriptiveComplexity.DomRed.DSTag : Type

Tags of the reduction: the vertex of a ground element and the vertex of a set.

• elt : DSTag

  The vertex of a ground element.

• set : DSTag

  The vertex of a set of the family.

@[instance_reducible]

instance DescriptiveComplexity.DomRed.instDecidableEqDSTag : DecidableEq DSTag

Equations

• DescriptiveComplexity.DomRed.instDecidableEqDSTag x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DescriptiveComplexity.DomRed.instFintypeDSTag : Fintype DSTag

Equations

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

instance DescriptiveComplexity.DomRed.instNonemptyDSTag : Nonempty DSTag

noncomputable def DescriptiveComplexity.DomRed.adjF : DSTag → DSTag → FirstOrder.Language.setSystem.Formula (Fin 2 × Fin 1)

Defining formula for adjacency, before the gate: the sets form a clique, and a set is joined to its elements – and to every junk vertex.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.DomRed.adjF DescriptiveComplexity.DomRed.DSTag.elt DescriptiveComplexity.DomRed.DSTag.elt = ⊥

noncomputable def DescriptiveComplexity.DomRed.dsInterp : FOInterpretation FirstOrder.Language.setSystem FirstOrder.Language.markedGraph DSTag 1

The interpretation of Dominating Set instances in set systems.

Equations

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

The points

def DescriptiveComplexity.DomRed.dsPt {A : Type} (t : DSTag) (x : A) : dsInterp.Map A

The vertex of tag t over the element x.

Equations

• DescriptiveComplexity.DomRed.dsPt t x = (t, fun (x_1 : Fin 1) => x)

theorem DescriptiveComplexity.DomRed.dsPt_eq_iff {A : Type} {t t' : DSTag} {x x' : A} : dsPt t x = dsPt t' x' ↔ t = t' ∧ x = x'

theorem DescriptiveComplexity.DomRed.dsPt_injective {A : Type} (t : DSTag) : Function.Injective (dsPt t)

theorem DescriptiveComplexity.DomRed.dsPt_surj {A : Type} (q : dsInterp.Map A) : ∃ (t : DSTag) (x : A), q = dsPt t x

Characterization of the two relations

theorem DescriptiveComplexity.DomRed.mgAdj_pt {A : Type} [FirstOrder.Language.setSystem.Structure A] (t₁ t₂ : DSTag) (x y : A) : MGAdj (dsPt t₁ x) (dsPt t₂ y) ↔ ¬(Uncoverable A ∨ NoElem A) ∧ (t₁ = DSTag.set ∧ t₂ = DSTag.set ∧ x ≠ y ∨ t₁ = DSTag.set ∧ t₂ = DSTag.elt ∧ (SSFam x ∧ SSElem y ∧ SSMem y x ∨ ¬SSElem y) ∨ t₁ = DSTag.elt ∧ t₂ = DSTag.set ∧ (SSFam y ∧ SSElem x ∧ SSMem x y ∨ ¬SSElem x))

theorem DescriptiveComplexity.DomRed.mgMarked_pt {A : Type} [FirstOrder.Language.setSystem.Structure A] (t : DSTag) (x : A) : MGMarked (dsPt t x) ↔ t = DSTag.set ∧ SSMarked x ∧ ¬(Uncoverable A ∨ NoElem A) ∨ NoElem A

Correctness

theorem DescriptiveComplexity.DomRed.hasSmallSetCover_iff_hasSmallDominatingSet (A : Type) [FirstOrder.Language.setSystem.Structure A] : HasSmallSetCover A ↔ HasSmallDominatingSet (dsInterp.Map A)

Correctness of the reduction: a set system has a small cover iff its incidence graph has a small dominating set.

noncomputable def DescriptiveComplexity.DomRed.setCover_fo_reduction_dominatingSet : FOReduction SetCover DominatingSet

Set Cover FO-reduces to Dominating Set: elements and sets become vertices, the sets form a clique, and each set is joined to its elements – and to the junk, which domination cannot ignore.

Equations

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