Set Cover, Hitting Set and Set Packing: definitions

The three classical problems on set systems (Karp 1972), as decision problems on FirstOrder.Language.setSystem-structures: a universe carrying two unary marks separating the ground elements from the sets of a family, a binary incidence relation between them, and a third unary mark carrying the numeric threshold k in the unary representation of DescriptiveComplexity.Numbers.Unary (the threshold is the cardinality Set.ncard of the marked set, order-free and isomorphism-invariant for free).

• DescriptiveComplexity.SetCover: some subfamily of at most k sets covers every element;
• DescriptiveComplexity.HittingSet: some set of at most k elements meets every set of the family;
• DescriptiveComplexity.SetPacking: some subfamily of at least k pairwise disjoint sets exists.

They are the set-system counterparts of the clique family (DescriptiveComplexity.Problems.CliqueFamily), and are organized the same way: the semantics is carried by generic properties of predicates on a type – DescriptiveComplexity.CoversOn, its transpose DescriptiveComplexity.HitsOn (elements and sets exchanged, incidence read backwards) and DescriptiveComplexity.PacksOn – which the isomorphism-invariance proofs and the reductions share. Set Cover and Hitting Set being literally one property read in two directions is what makes them inter-reducible by a single interpretation (DescriptiveComplexity.Problems.SetFamily.Reductions), just as complementation relates Clique and Independent Set.

Two conventions worth stating once:

• Nothing forces an element of the universe to be an element or a set, or forbids it to be both: elements outside both marks are junk that no condition mentions, which is what lets a first-order interpretation build a set system inside a tagged power of its input universe without a definable-subset mechanism. Junk marked elements would change the threshold, so interpretations remain responsible for the mark they define.
• Disjointness in DescriptiveComplexity.PacksOn is required of the ground elements only. This is not cosmetic: the interpretation of DescriptiveComplexity.Problems.SetFamily.FromGraphs produces junk tuples incident to two sets each, and those must not count as witnesses of an intersection.

As with the clique family, cardinality thresholds are only meaningful on finite structures, so finiteness of the universe is part of the yes-instances; by DescriptiveComplexity.ComplexityClass.mem_congr_finite this does not affect any complexity-theoretic statement.

inductive FirstOrder.Language.setSystemRel : ℕ → Type

Relation symbols of the language of set systems.

• elem : setSystemRel 1

  elem a: the element a belongs to the ground set.

• fam : setSystemRel 1

  fam a: the element a is one of the sets of the family.

• mem : setSystemRel 2

  mem a b: the ground element a belongs to the set b.

• marked : setSystemRel 1

  marked a: the element a belongs to the marked set.

@[instance_reducible]

instance FirstOrder.Language.instDecidableEqSetSystemRel {a✝ : ℕ} : DecidableEq (setSystemRel a✝)

Equations

• FirstOrder.Language.instDecidableEqSetSystemRel = FirstOrder.Language.instDecidableEqSetSystemRel.decEq

def FirstOrder.Language.instDecidableEqSetSystemRel.decEq {a✝ : ℕ} (x✝ x✝¹ : setSystemRel a✝) : Decidable (x✝ = x✝¹)

Equations

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

def FirstOrder.Language.setSystem : Language

The relational language of set systems: a bipartite incidence structure between ground elements and sets of a family, together with a marked subset of the universe whose cardinality serves as threshold.

Equations

• FirstOrder.Language.setSystem = { Functions := fun (x : ℕ) => Empty, Relations := FirstOrder.Language.setSystemRel }

instance FirstOrder.Language.instIsRelationalSetSystem : Language.setSystem.IsRelational

@[reducible, inline]

abbrev FirstOrder.Language.ssElem : Language.setSystem.Relations 1

The ground-element symbol of set systems.

Equations

• FirstOrder.Language.ssElem = FirstOrder.Language.setSystemRel.elem

@[reducible, inline]

abbrev FirstOrder.Language.ssFam : Language.setSystem.Relations 1

The family symbol of set systems.

Equations

• FirstOrder.Language.ssFam = FirstOrder.Language.setSystemRel.fam

@[reducible, inline]

abbrev FirstOrder.Language.ssMem : Language.setSystem.Relations 2

The incidence symbol of set systems.

Equations

• FirstOrder.Language.ssMem = FirstOrder.Language.setSystemRel.mem

@[reducible, inline]

abbrev FirstOrder.Language.ssMarked : Language.setSystem.Relations 1

The mark symbol of set systems.

Equations

• FirstOrder.Language.ssMarked = FirstOrder.Language.setSystemRel.marked

The generic covering property

The property underlying both problems, for arbitrary unary predicates Ep (ground elements), Fp (sets of the family) and Kp (marks), and an arbitrary binary predicate Mp (incidence) on a type.

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

Some subfamily of the Fp-sets covers every Ep-element and is at most as large as the number encoded by the Kp-marked elements: “some cover is at most as large as the marked set”.

Equations

• DescriptiveComplexity.CoversOn Ep Fp Mp Kp = ∃ (G : A → Prop), (∀ (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.HitsOn {A : Type} (Ep Fp : A → Prop) (Mp : A → A → Prop) (Kp : A → Prop) : Prop

Some set of Ep-elements meets every Fp-set and is at most as large as the number encoded by the Kp-marked elements: “some hitting set is at most as large as the marked set”. This is DescriptiveComplexity.CoversOn with the roles of elements and sets exchanged and the incidence relation transposed.

Equations

• DescriptiveComplexity.HitsOn Ep Fp Mp Kp = DescriptiveComplexity.CoversOn Fp Ep (fun (s x : A) => Mp x s) Kp

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

Some subfamily of the Fp-sets is pairwise disjoint – no Ep-element belongs to two distinct members – and is at least as large as the number encoded by the Kp-marked elements: “some packing is at least as large as the marked set”.

Equations

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

def DescriptiveComplexity.ExactlyCoversOn {A : Type} (Ep Fp : A → Prop) (Mp : A → A → Prop) : Prop

Some subfamily of the Fp-sets covers every Ep-element exactly once: it covers, and no element belongs to two distinct members. Unlike the three properties above this one carries no threshold – exactness is the whole constraint.

Equations

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

theorem DescriptiveComplexity.exactlyCoversOn_iff_unique {A : Type} (Ep Fp : A → Prop) (Mp : A → A → Prop) : ExactlyCoversOn Ep Fp Mp ↔ ∃ (G : A → Prop), (∀ (s : A), G s → Fp s) ∧ ∀ (x : A), Ep x → ∃! s : A, G s ∧ Mp x s

Exactness in the “exactly one” form: covering plus disjointness is one covering set per element.

def DescriptiveComplexity.SplitsOn {A : Type} (Ep Fp : A → Prop) (Mp : A → A → Prop) : Prop

Some two-colouring of the ground elements splits every set of the family: no set is monochromatic. Like DescriptiveComplexity.ExactlyCoversOn this property carries no threshold.

Equations

• DescriptiveComplexity.SplitsOn Ep Fp Mp = ∃ (S : A → Prop), ∀ (f : A), Fp f → (∃ (x : A), Ep x ∧ Mp x f ∧ S x) ∧ ∃ (x : A), Ep x ∧ Mp x f ∧ ¬S x

The threshold as an injection

On a finite universe, comparing the decoded numbers is comparing sizes, so the threshold condition can equivalently be read as the existence of an injection. This is the form the second-order definitions guess.

theorem DescriptiveComplexity.coversOn_iff_embedding {A : Type} [Finite A] (Ep Fp : A → Prop) (Mp : A → A → Prop) (Kp : A → Prop) : CoversOn Ep Fp Mp Kp ↔ ∃ (G : A → Prop), (∀ (s : A), G s → Fp s) ∧ (∀ (x : A), Ep x → ∃ (s : A), G s ∧ Mp x s) ∧ Nonempty ({ s : A // G s } ↪ { x : A // Kp x })

The cover threshold as an injection of the cover into the marked set.

theorem DescriptiveComplexity.hitsOn_iff_embedding {A : Type} [Finite A] (Ep Fp : A → Prop) (Mp : A → A → Prop) (Kp : A → Prop) : HitsOn Ep Fp Mp Kp ↔ ∃ (H : A → Prop), (∀ (x : A), H x → Ep x) ∧ (∀ (s : A), Fp s → ∃ (x : A), H x ∧ Mp x s) ∧ Nonempty ({ x : A // H x } ↪ { x : A // Kp x })

The hitting-set threshold as an injection of the hitting set into the marked set.

theorem DescriptiveComplexity.packsOn_iff_embedding {A : Type} [Finite A] (Ep Fp : A → Prop) (Mp : A → A → Prop) (Kp : A → Prop) : PacksOn Ep Fp Mp Kp ↔ ∃ (G : A → Prop), (∀ (s : A), G s → Fp s) ∧ (∀ (s s' : A), G s → G s' → s ≠ s' → ∀ (x : A), Ep x → ¬(Mp x s ∧ Mp x s')) ∧ Nonempty ({ x : A // Kp x } ↪ { s : A // G s })

The packing threshold as an injection of the marked set into the packing: a lower bound, so the injection runs the other way round.

theorem DescriptiveComplexity.CoversOn.of_equiv {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)) (h : CoversOn EB FB MB KB) : CoversOn EA FA MA KA

CoversOn transports along an equivalence commuting with the four predicates.

theorem DescriptiveComplexity.CoversOn.equiv_iff {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)) : CoversOn EB FB MB KB ↔ CoversOn EA FA MA KA

CoversOn transports along an equivalence, iff version.

theorem DescriptiveComplexity.HitsOn.equiv_iff {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)) : HitsOn EB FB MB KB ↔ HitsOn EA FA MA KA

HitsOn transports along an equivalence, iff version.

theorem DescriptiveComplexity.PacksOn.of_equiv {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)) (h : PacksOn EB FB MB KB) : PacksOn EA FA MA KA

PacksOn transports along an equivalence commuting with the four predicates.

theorem DescriptiveComplexity.ExactlyCoversOn.of_equiv {A B : Type} (u : B ≃ A) {EB FB : B → Prop} {MB : B → B → Prop} {EA FA : 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')) (h : ExactlyCoversOn EB FB MB) : ExactlyCoversOn EA FA MA

ExactlyCoversOn transports along an equivalence commuting with the three predicates.

theorem DescriptiveComplexity.SplitsOn.of_equiv {A B : Type} (u : B ≃ A) {EB FB : B → Prop} {MB : B → B → Prop} {EA FA : 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')) (h : SplitsOn EB FB MB) : SplitsOn EA FA MA

SplitsOn transports along an equivalence commuting with the three predicates.

theorem DescriptiveComplexity.SplitsOn.equiv_iff {A B : Type} (u : B ≃ A) {EB FB : B → Prop} {MB : B → B → Prop} {EA FA : 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')) : SplitsOn EB FB MB ↔ SplitsOn EA FA MA

SplitsOn transports along an equivalence, iff version.

theorem DescriptiveComplexity.ExactlyCoversOn.equiv_iff {A B : Type} (u : B ≃ A) {EB FB : B → Prop} {MB : B → B → Prop} {EA FA : 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')) : ExactlyCoversOn EB FB MB ↔ ExactlyCoversOn EA FA MA

ExactlyCoversOn transports along an equivalence, iff version.

theorem DescriptiveComplexity.PacksOn.equiv_iff {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)) : PacksOn EB FB MB KB ↔ PacksOn EA FA MA KA

PacksOn transports along an equivalence, iff version.

The two problems

def DescriptiveComplexity.SSElem {A : Type} [FirstOrder.Language.setSystem.Structure A] (a : A) : Prop

Being a ground element in a set system.

Equations

• DescriptiveComplexity.SSElem a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.ssElem ![a]

def DescriptiveComplexity.SSFam {A : Type} [FirstOrder.Language.setSystem.Structure A] (a : A) : Prop

Being a set of the family in a set system.

Equations

• DescriptiveComplexity.SSFam a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.ssFam ![a]

def DescriptiveComplexity.SSMem {A : Type} [FirstOrder.Language.setSystem.Structure A] (a b : A) : Prop

Incidence in a set system.

Equations

• DescriptiveComplexity.SSMem a b = FirstOrder.Language.Structure.RelMap FirstOrder.Language.ssMem ![a, b]

def DescriptiveComplexity.SSMarked {A : Type} [FirstOrder.Language.setSystem.Structure A] (a : A) : Prop

Markedness in a set system.

Equations

• DescriptiveComplexity.SSMarked a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.ssMarked ![a]

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

A set system admits a cover 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

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

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

A set system admits a hitting set at most as large as its marked set.

Equations

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

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

A set system admits a packing at least as large as its marked set.

Equations

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

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

A set system admits an exact cover: a subfamily covering every ground element exactly once. There is no threshold here, so no finiteness assumption either.

Equations

• DescriptiveComplexity.HasExactCover A = DescriptiveComplexity.ExactlyCoversOn DescriptiveComplexity.SSElem DescriptiveComplexity.SSFam DescriptiveComplexity.SSMem

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

A set system admits a splitting two-colouring: no set of the family is monochromatic.

Equations

• DescriptiveComplexity.HasSetSplitting A = DescriptiveComplexity.SplitsOn DescriptiveComplexity.SSElem DescriptiveComplexity.SSFam DescriptiveComplexity.SSMem

Isomorphism-invariance and the bundled problems

theorem DescriptiveComplexity.hasSmallSetCover_iso {A B : Type} [FirstOrder.Language.setSystem.Structure A] [FirstOrder.Language.setSystem.Structure B] (e : FirstOrder.Language.setSystem.Equiv A B) : HasSmallSetCover A ↔ HasSmallSetCover B

The set-cover threshold property is isomorphism-invariant.

theorem DescriptiveComplexity.hasSmallHittingSet_iso {A B : Type} [FirstOrder.Language.setSystem.Structure A] [FirstOrder.Language.setSystem.Structure B] (e : FirstOrder.Language.setSystem.Equiv A B) : HasSmallHittingSet A ↔ HasSmallHittingSet B

The hitting-set threshold property is isomorphism-invariant.

theorem DescriptiveComplexity.hasLargeSetPacking_iso {A B : Type} [FirstOrder.Language.setSystem.Structure A] [FirstOrder.Language.setSystem.Structure B] (e : FirstOrder.Language.setSystem.Equiv A B) : HasLargeSetPacking A ↔ HasLargeSetPacking B

The set-packing threshold property is isomorphism-invariant.

theorem DescriptiveComplexity.hasExactCover_iso {A B : Type} [FirstOrder.Language.setSystem.Structure A] [FirstOrder.Language.setSystem.Structure B] (e : FirstOrder.Language.setSystem.Equiv A B) : HasExactCover A ↔ HasExactCover B

The exact-cover property is isomorphism-invariant.

theorem DescriptiveComplexity.hasSetSplitting_iso {A B : Type} [FirstOrder.Language.setSystem.Structure A] [FirstOrder.Language.setSystem.Structure B] (e : FirstOrder.Language.setSystem.Equiv A B) : HasSetSplitting A ↔ HasSetSplitting B

The set-splitting property is isomorphism-invariant.

def DescriptiveComplexity.SetCover : DecisionProblem FirstOrder.Language.setSystem

SET COVER, as a problem on set systems: is there a subfamily covering every ground element, at most as large as the marked set?

Equations

• DescriptiveComplexity.SetCover = { Holds := fun (A : Type) (inst : FirstOrder.Language.setSystem.Structure A) => DescriptiveComplexity.HasSmallSetCover A, iso_invariant := ⋯ }

def DescriptiveComplexity.HittingSet : DecisionProblem FirstOrder.Language.setSystem

HITTING SET, as a problem on set systems: is there a set of ground elements meeting every set of the family, at most as large as the marked set?

Equations

• DescriptiveComplexity.HittingSet = { Holds := fun (A : Type) (inst : FirstOrder.Language.setSystem.Structure A) => DescriptiveComplexity.HasSmallHittingSet A, iso_invariant := ⋯ }

def DescriptiveComplexity.SetPacking : DecisionProblem FirstOrder.Language.setSystem

SET PACKING, as a problem on set systems: is there a pairwise disjoint subfamily at least as large as the marked set?

Equations

• DescriptiveComplexity.SetPacking = { Holds := fun (A : Type) (inst : FirstOrder.Language.setSystem.Structure A) => DescriptiveComplexity.HasLargeSetPacking A, iso_invariant := ⋯ }

def DescriptiveComplexity.ExactCover : DecisionProblem FirstOrder.Language.setSystem

EXACT COVER, as a problem on set systems: is there a subfamily covering every ground element exactly once? The marked set plays no role – exactness replaces the threshold.

Equations

• DescriptiveComplexity.ExactCover = { Holds := fun (A : Type) (inst : FirstOrder.Language.setSystem.Structure A) => DescriptiveComplexity.HasExactCover A, iso_invariant := ⋯ }

def DescriptiveComplexity.SetSplitting : DecisionProblem FirstOrder.Language.setSystem

SET SPLITTING, as a problem on set systems: is there a two-colouring of the ground elements leaving no set of the family monochromatic? (Also known as hypergraph 2-colourability.)

Equations

• DescriptiveComplexity.SetSplitting = { Holds := fun (A : Type) (inst : FirstOrder.Language.setSystem.Structure A) => DescriptiveComplexity.HasSetSplitting A, iso_invariant := ⋯ }