#Set Cover and #Hitting Set

The counting versions of DescriptiveComplexity.SetCover and DescriptiveComplexity.HittingSet, each counting the solutions of exactly the threshold size:

• DescriptiveComplexity.SharpSetCover: the covering subfamilies with as many sets as the marked set;
• DescriptiveComplexity.SharpHittingSet: the hitting sets with as many elements as the marked set.

Both are parsimoniously #P-complete (DescriptiveComplexity.sharpSetCover_sharpP_parsimoniousComplete, DescriptiveComplexity.sharpHittingSet_sharpP_parsimoniousComplete). Membership of #Set Cover is the generic argument for a solution of the threshold size (DescriptiveComplexity.sharpPDefinable_of_sized_set); its hardness is the edge-incidence interpretation unchanged, from #Vertex Cover, the sets of the interpreted system being the vertices, one each (DescriptiveComplexity.coverEquiv). #Hitting Set is #Set Cover transposed, in both directions.

The support is not the decision problem. A cover smaller than the threshold extends to one of exactly that size only while unused sets remain: with a threshold above the size of the family, Set Cover may hold and the count be 0. The support of these counts is “some cover has exactly the threshold size” (DescriptiveComplexity.sharpSetCover_support_iff), which implies Set Cover (DescriptiveComplexity.setCover_of_sharpSetCover_support) and is not implied by it. This is unlike #Vertex Cover, where the family is the whole universe.

The generic property

def DescriptiveComplexity.CoverFamOfSizeOn {A : Type} (Ep Fp : A → Prop) (Mp : A → A → Prop) (Kp G : A → Prop) : Prop

The subfamily G of the Fp-sets covers every Ep-element and has exactly as many members as the Kp-marked set.

Equations

• DescriptiveComplexity.CoverFamOfSizeOn Ep Fp Mp Kp G = ((∀ (s : A), G s → Fp s) ∧ (∀ (x : A), Ep x → ∃ (s : A), G s ∧ Mp x s) ∧ {s : A | G s}.ncard = {x : A | Kp x}.ncard)

def DescriptiveComplexity.coverFamOfSizeEquiv {A B : Type} (u : B ≃ A) {EB FB KB : B → Prop} {MB : B → B → Prop} {EA FA KA : A → Prop} {MA : A → A → Prop} (hE : ∀ (b : B), EB b ↔ EA (u b)) (hF : ∀ (b : B), FB b ↔ FA (u b)) (hM : ∀ (b b' : B), MB b b' ↔ MA (u b) (u b')) (hK : ∀ (b : B), KB b ↔ KA (u b)) : { G : B → Prop // Finite B ∧ CoverFamOfSizeOn EB FB MB KB G } ≃ { G : A → Prop // Finite A ∧ CoverFamOfSizeOn EA FA MA KA G }

The covers of the threshold size transport along an equivalence commuting with the four predicates.

Equations

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

The two counting problems

def DescriptiveComplexity.SetCoverOfSize (A : Type) [FirstOrder.Language.setSystem.Structure A] (G : A → Prop) : Prop

The subfamily G is a cover with exactly as many sets as the marked set, in a finite set system.

Equations

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

def DescriptiveComplexity.HittingSetOfSize (A : Type) [FirstOrder.Language.setSystem.Structure A] (H : A → Prop) : Prop

The set H of ground elements is a hitting set with exactly as many elements as the marked set, in a finite set system.

Equations

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

noncomputable def DescriptiveComplexity.SharpSetCover : CountingProblem FirstOrder.Language.setSystem

#Set Cover: the number of covering subfamilies with exactly as many sets as the marked set.

Equations

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

noncomputable def DescriptiveComplexity.SharpHittingSet : CountingProblem FirstOrder.Language.setSystem

#Hitting Set: the number of hitting sets with exactly as many elements as the marked set.

Equations

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

theorem DescriptiveComplexity.sharpSetCover_support_iff (A : Type) [FirstOrder.Language.setSystem.Structure A] [Finite A] : SharpSetCover.support.Holds A ↔ ∃ (G : A → Prop), SetCoverOfSize A G

The support of #Set Cover: some cover has exactly the threshold size. Registered in the Lax archive as Lax280166.SetCoverComplete.sharpSetCover_support_iff.

theorem DescriptiveComplexity.sharpHittingSet_support_iff (A : Type) [FirstOrder.Language.setSystem.Structure A] [Finite A] : SharpHittingSet.support.Holds A ↔ ∃ (H : A → Prop), HittingSetOfSize A H

The support of #Hitting Set: some hitting set has exactly the threshold size. Registered in the Lax archive as Lax280166.HittingSetComplete.sharpHittingSet_support_iff.

theorem DescriptiveComplexity.setCover_of_sharpSetCover_support (A : Type) [FirstOrder.Language.setSystem.Structure A] [Finite A] (h : SharpSetCover.support.Holds A) : SetCover.Holds A

The support of #Set Cover implies Set Cover; the converse fails when the threshold exceeds the size of the family. Registered in the Lax archive as Lax280166.SetCoverComplete.setCover_of_sharpSetCover_support.

theorem DescriptiveComplexity.hittingSet_of_sharpHittingSet_support (A : Type) [FirstOrder.Language.setSystem.Structure A] [Finite A] (h : SharpHittingSet.support.Holds A) : HittingSet.Holds A

The support of #Hitting Set implies Hitting Set. Registered in the Lax archive as Lax280166.HittingSetComplete.hittingSet_of_sharpHittingSet_support.

Transposition, for counting

theorem DescriptiveComplexity.sharpHittingSet_transpose_map (A : Type) [FirstOrder.Language.setSystem.Structure A] : SharpHittingSet.Count (transposeInterp.Map A) = SharpSetCover.Count A

The hitting sets of the transposed system are the covers.

Membership

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqCoverSelBlockIx : DecidableEq CoverSelBlockIx

Equations

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

@[instance_reducible]

instance DescriptiveComplexity.instFintypeCoverSelBlockIx : Fintype CoverSelBlockIx

Equations

• DescriptiveComplexity.instFintypeCoverSelBlockIx = { elems := [DescriptiveComplexity.CoverSelBlockIx.sel].toFinset, complete := DescriptiveComplexity.instFintypeCoverSelBlockIx._proof_1 }

def DescriptiveComplexity.cvSelRel : coverSelBlock.lang.Relations 1

The sel relation variable.

Equations

• DescriptiveComplexity.cvSelRel = ⟨DescriptiveComplexity.CoverSelBlockIx.sel, DescriptiveComplexity.cvSelRel._proof_1⟩

def DescriptiveComplexity.coverSelBlock : SOBlock

The block of the counting definition of Set Cover: the cover itself.

Equations

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

inductive DescriptiveComplexity.CoverSelBlockIx : Type

The relation variables of the block.

• sel : CoverSelBlockIx

  The cover.

@[reducible, inline]

abbrev DescriptiveComplexity.cvMarkedSym : coverSelLang.Relations 1

The marked symbol over the sum.

Equations

• DescriptiveComplexity.cvMarkedSym = Sum.inl FirstOrder.Language.ssMarked

@[reducible, inline]

abbrev DescriptiveComplexity.cvFamSym : coverSelLang.Relations 1

The fam symbol over the sum.

Equations

• DescriptiveComplexity.cvFamSym = Sum.inl FirstOrder.Language.ssFam

@[reducible, inline]

abbrev DescriptiveComplexity.coverSelLang : FirstOrder.Language

The vocabulary of the kernel: the instance expanded by the block.

Equations

• DescriptiveComplexity.coverSelLang = FirstOrder.Language.setSystem.sum DescriptiveComplexity.coverSelBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.cvElemSym : coverSelLang.Relations 1

The elem symbol over the sum.

Equations

• DescriptiveComplexity.cvElemSym = Sum.inl FirstOrder.Language.ssElem

@[reducible, inline]

abbrev DescriptiveComplexity.cvMemSym : coverSelLang.Relations 2

The mem symbol over the sum.

Equations

• DescriptiveComplexity.cvMemSym = Sum.inl FirstOrder.Language.ssMem

@[reducible, inline]

abbrev DescriptiveComplexity.cvSelSym : coverSelLang.Relations 1

The sel symbol over the sum.

Equations

• DescriptiveComplexity.cvSelSym = Sum.inr DescriptiveComplexity.cvSelRel

instance DescriptiveComplexity.instSubsingletonιCoverSelBlock : Subsingleton coverSelBlock.ι

Hardness of #Set Cover

theorem DescriptiveComplexity.setCoverOfSize_vertexFamily {A : Type} [FirstOrder.Language.markedGraph.Structure A] {C : A → Prop} (h : CoverOfSize A C) : SetCoverOfSize (edgeIncidenceInterp.Map A) (vertexFamily C)

The vertex-sets of a vertex cover of the threshold size are a cover of the threshold size.

theorem DescriptiveComplexity.setCover_diag {A : Type} [FirstOrder.Language.markedGraph.Structure A] {G : edgeIncidenceInterp.Map A → Prop} (h : SetCoverOfSize (edgeIncidenceInterp.Map A) G) (p : edgeIncidenceInterp.Map A) : G p → ∃ (v : A), p = diagPt v

A cover of the interpreted system consists of vertex-sets.

theorem DescriptiveComplexity.coverOfSize_of_setCover {A : Type} [FirstOrder.Language.markedGraph.Structure A] {G : edgeIncidenceInterp.Map A → Prop} (h : SetCoverOfSize (edgeIncidenceInterp.Map A) G) : CoverOfSize A fun (v : A) => G (diagPt v)

The vertices of a cover of the threshold size are a vertex cover of the threshold size.

def DescriptiveComplexity.coverEquiv (A : Type) [FirstOrder.Language.markedGraph.Structure A] : { C : A → Prop // CoverOfSize A C } ≃ { G : edgeIncidenceInterp.Map A → Prop // SetCoverOfSize (edgeIncidenceInterp.Map A) G }

The covers of the threshold size of the edge-incidence system are the vertex covers of the threshold size, bijectively.

Equations

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

The reductions and the completeness theorems

noncomputable def DescriptiveComplexity.sharpVertexCover_parsimonious_sharpSetCover : ParsimoniousReduction SharpVertexCover SharpSetCover

#Vertex Cover reduces parsimoniously to #Set Cover, by the edge-incidence interpretation.

Equations

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

noncomputable def DescriptiveComplexity.sharpSetCover_parsimonious_sharpHittingSet : ParsimoniousReduction SharpSetCover SharpHittingSet

#Set Cover reduces parsimoniously to #Hitting Set, by transposition.

Equations

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

theorem DescriptiveComplexity.sharpSetCover_sharpP_parsimoniousHard : SharpP.ParsimoniousHard SharpSetCover

#Set Cover is parsimoniously #P-hard.

theorem DescriptiveComplexity.sharpSetCover_sharpP_parsimoniousComplete : SharpP.ParsimoniousComplete SharpSetCover

#Set Cover is parsimoniously #P-complete, counting the covers of exactly the threshold size. Registered in the Lax archive as Lax280166.SetCoverComplete.sharpSetCover_sharpP_parsimoniousComplete.

theorem DescriptiveComplexity.sharpSetCover_sharpP_complete : SharpP.Complete SharpSetCover

SharpSetCover is #P-complete: parsimoniously, hence under subtractive reductions.

theorem DescriptiveComplexity.sharpHittingSet_sharpP_parsimoniousHard : SharpP.ParsimoniousHard SharpHittingSet

#Hitting Set is parsimoniously #P-hard.

theorem DescriptiveComplexity.sharpHittingSet_sharpP_parsimoniousComplete : SharpP.ParsimoniousComplete SharpHittingSet

#Hitting Set is parsimoniously #P-complete, counting the hitting sets of exactly the threshold size. Registered in the Lax archive as Lax280166.HittingSetComplete.sharpHittingSet_sharpP_parsimoniousComplete.

theorem DescriptiveComplexity.sharpHittingSet_sharpP_complete : SharpP.Complete SharpHittingSet

SharpHittingSet is #P-complete: parsimoniously, hence under subtractive reductions.