Set Cover and Hitting Set are transposes of each other

The inter-reduction inside the set family, the counterpart of the complementation reductions of DescriptiveComplexity.Problems.CliqueFamily.Reductions: the two problems are the same condition read in the two directions of the incidence relation, so a single interpretation of tag Unit and dimension 1 (DescriptiveComplexity.transposeInterp) – exchange the two unary marks, transpose the incidence relation, keep the threshold – reduces each of them to the other (DescriptiveComplexity.setCover_fo_reduction_hittingSet and DescriptiveComplexity.hittingSet_fo_reduction_setCover), quantifier-free.

Set Packing has no such partner: its condition is not the transpose of another problem of the family, and its hardness comes from graphs directly (DescriptiveComplexity.Problems.SetFamily.FromGraphs).

Set Cover and Hitting Set are transposes of each other

def DescriptiveComplexity.transposeInterp : FOInterpretation FirstOrder.Language.setSystem FirstOrder.Language.setSystem Unit 1

The transposing interpretation: ground elements and sets of the family exchange their marks, incidence is read backwards, the threshold is kept.

Equations

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

theorem DescriptiveComplexity.transposeInterp_isQuantifierFree : transposeInterp.IsQuantifierFree

The transposing interpretation is quantifier-free.

@[simp]

theorem DescriptiveComplexity.transpose_elem {A : Type} [FirstOrder.Language.setSystem.Structure A] (w : Fin 1 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.ssElem ![((), w)] ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.ssFam ![w 0]

@[simp]

theorem DescriptiveComplexity.transpose_fam {A : Type} [FirstOrder.Language.setSystem.Structure A] (w : Fin 1 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.ssFam ![((), w)] ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.ssElem ![w 0]

@[simp]

theorem DescriptiveComplexity.transpose_mem {A : Type} [FirstOrder.Language.setSystem.Structure A] (w₁ w₂ : Fin 1 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.ssMem ![((), w₁), ((), w₂)] ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.ssMem ![w₂ 0, w₁ 0]

@[simp]

theorem DescriptiveComplexity.transpose_marked {A : Type} [FirstOrder.Language.setSystem.Structure A] (w : Fin 1 → A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.ssMarked ![((), w)] ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.ssMarked ![w 0]

theorem DescriptiveComplexity.hasSmallHittingSet_iff_map (A : Type) [FirstOrder.Language.setSystem.Structure A] : HasSmallHittingSet A ↔ HasSmallSetCover (transposeInterp.Map A)

Correctness of the transposition, hitting-set-to-set-cover direction: a hitting set of a set system is a cover of its transpose.

theorem DescriptiveComplexity.hasSmallSetCover_iff_map (A : Type) [FirstOrder.Language.setSystem.Structure A] : HasSmallSetCover A ↔ HasSmallHittingSet (transposeInterp.Map A)

Correctness of the transposition, set-cover-to-hitting-set direction: a cover of a set system is a hitting set of its transpose.

def DescriptiveComplexity.setCover_fo_reduction_hittingSet : FOReduction SetCover HittingSet

Set Cover FO-reduces to Hitting Set, by transposing the incidence relation.

Equations

• DescriptiveComplexity.setCover_fo_reduction_hittingSet = { Tag := Unit, tagFinite := ⋯, tagNonempty := ⋯, dim := 1, toInterpretation := DescriptiveComplexity.transposeInterp, correct := ⋯ }

def DescriptiveComplexity.hittingSet_fo_reduction_setCover : FOReduction HittingSet SetCover

Hitting Set FO-reduces to Set Cover, by transposing the incidence relation.

Equations

• DescriptiveComplexity.hittingSet_fo_reduction_setCover = { Tag := Unit, tagFinite := ⋯, tagNonempty := ⋯, dim := 1, toInterpretation := DescriptiveComplexity.transposeInterp, correct := ⋯ }