Greedy set cover

DefinitionGreedy choice of a set#✓fully proved

Given a list \(F\) of finite sets and a finite set \(U\), the best set of \(F\) for \(U\) is the first set \(S\) in the list \(F\) that maximizes \(|S \cap U|\), or \(\emptyset\) when \(F\) is empty.

def bestSet (F : List (Finset α)) (U : Finset α) : Finset α :=
  (F.argmax fun S => (S ∩ U).card).getD ∅

Used by 6

Used byGreedy set cover · The greedy set cover is a cover · The greedy set cover has at most as many sets as elements · Potential bound for greedy set cover · The greedy set cover draws its sets from the family · Running time of greedy set cover

DefinitionGreedy set cover#✓fully proved

Let \(F = [S_1, \dots, S_n]\) be a list of finite sets and \(U\) a finite set. The greedy set cover of \(U\) from \(F\) is computed as follows. Let \(T\) be the first \(S_i\) in the list that maximizes \(|S_i \cap U|\), or \(T = \emptyset\) when \(n = 0\). If \(T \cap U = \emptyset\), the result is the empty list; otherwise it is \(T\) followed by the greedy set cover of \(U \setminus T\) from \(F\). Each step, including the last one, costs \(n + |S_1| + \dots + |S_n|\).

def greedySetCover (F : List (Finset α)) (U : Finset α) : TimeM ℕ (List (Finset α)) := do
  ✓[F.length + (F.map Finset.card).sum]
  let S := bestSet F U
  if _hS : (S ∩ U).card = 0 then pure []
  else do
    let C ← greedySetCover F (U \ S)
    pure (S :: C)
termination_by U.card
decreasing_by
  have h := Finset.card_sdiff_add_card_inter U (bestSet F U)
  have hS' : ¬ (bestSet F U ∩ U).card = 0 := _hS
  rw [Finset.inter_comm] at h
  omega

Uses 1 · Used by 8

Statement usesGreedy choice of a set

Used byHarmonic bound in the largest set size for greedy set cover · Harmonic bound in the universe size for greedy set cover · Greedy set cover is a logarithmic approximation · The greedy set cover is a cover · The greedy set cover has at most as many sets as elements · Potential bound for greedy set cover · The greedy set cover draws its sets from the family · Running time of greedy set cover

TheoremThe greedy set cover draws its sets from the family#✓fully proved

For every list \(F\) of finite sets and every finite set \(U\), every set in the list returned by the greedy set cover algorithm on \(F\) and \(U\) is a member of \(F\).

theorem greedySetCover_mem (F : List (Finset α)) (U : Finset α) :
    ∀ S ∈ (greedySetCover F U).ret, S ∈ F

Uses 2

Statement usesGreedy set cover

Proof usesGreedy choice of a set

TheoremThe greedy set cover is a cover#✓fully proved

Let \(F\) be a list of finite sets and \(U\) a finite set such that every element of \(U\) lies in some set of \(F\). Then every element of \(U\) lies in some set of the list returned by the greedy set cover algorithm on \(F\) and \(U\).

theorem greedySetCover_covers (F : List (Finset α)) (U : Finset α)
    (hU : ∀ x ∈ U, ∃ S ∈ F, x ∈ S) : ∀ x ∈ U, ∃ S ∈ (greedySetCover F U).ret, x ∈ S

Uses 2

Statement usesGreedy set cover

Proof usesGreedy choice of a set

TheoremThe greedy set cover has at most as many sets as elements#✓fully proved

For every list \(F\) of finite sets and every finite set \(U\), the list returned by the greedy set cover algorithm on \(F\) and \(U\) has length at most \(|U|\).

theorem greedySetCover_length_le (F : List (Finset α)) (U : Finset α) :
    (greedySetCover F U).ret.length ≤ U.card

Uses 2

Statement usesGreedy set cover

Proof usesGreedy choice of a set

TheoremRunning time of greedy set cover#✓fully proved

Let \(F\) be a list of finite sets and \(U\) a finite set. The running time of greedy set cover of \(U\) from \(F\) is at most \((|U| + 1)(|F| + \sum_{S \in F} |S|)\), where \(|F|\) is the length of the list and the sum runs over the entries of \(F\), counted with repetition.

There are at most \(|U| + 1\) searches for a best set, each costing \(|F| + \sum_{S \in F} |S|\).

theorem greedySetCover_time_le (F : List (Finset α)) (U : Finset α) :
    (greedySetCover F U).time ≤ (U.card + 1) * (F.length + (F.map Finset.card).sum)

Uses 2

Statement usesGreedy set cover

Proof usesGreedy choice of a set

TheoremLower bound for a difference of harmonic numbers#✓fully proved

Write \(H(n) = 1 + \frac12 + \dots + \frac1n\) for the \(n\)-th harmonic number, so \(H(0) = 0\). For natural numbers \(d \le a \le k\), we have \(\frac{d}{k} \le H(a) - H(a - d)\), where \(\frac{d}{k}\) is read as \(0\) when \(k = 0\).

Each of the \(d\) reciprocals \(\frac{1}{a - d + 1}, \dots, \frac{1}{a}\) is at least \(\frac1k\).

theorem div_le_harmonic_sub {a d k : ℕ} (hd : d ≤ a) (hak : a ≤ k) :
    (d : ℚ) / k ≤ harmonic a - harmonic (a - d)

Used by 2

Used byPotential bound for greedy set cover · Potential bound for weighted greedy set cover

TheoremCovering bound by intersections#✓fully proved

Let \(L\) be a list of finite sets and \(T\) a finite set such that every element of \(T\) lies in some member of \(L\). Then \(|T| \le \sum_{S \in L} |S \cap T|\), where the sum runs over the list \(L\) with repetitions.

theorem card_le_sum_card_inter (L : List (Finset α)) (T : Finset α)
    (hT : ∀ x ∈ T, ∃ S ∈ L, x ∈ S) : T.card ≤ (L.map fun S => (S ∩ T).card).sum

Used by 2

Used byPotential bound for greedy set cover · Potential bound for weighted greedy set cover

TheoremPotential bound for greedy set cover#✓fully proved

Let \(F\) be a list of finite sets, \(U\) a finite set, and \(H(n) = 1 + \frac12 + \dots + \frac1n\) the \(n\)-th harmonic number. For every list \(C^*\) of members of \(F\) that together cover \(U\), the list of sets returned by the greedy set cover algorithm on \(F\) and \(U\) has length at most \(\sum_{S \in C^*} H(|S \cap U|)\), where the sum runs over the list \(C^*\) with repetitions.

theorem greedySetCover_length_le_sum_harmonic (F : List (Finset α)) (U : Finset α)
    (Cstar : List (Finset α)) (hsub : ∀ S ∈ Cstar, S ∈ F)
    (hcov : ∀ x ∈ U, ∃ S ∈ Cstar, x ∈ S) :
    ((greedySetCover F U).ret.length : ℚ) ≤
      (Cstar.map fun S => harmonic (S ∩ U).card).sum

Uses 4 · Used by 2

Statement usesGreedy set cover

Proof usesGreedy choice of a set · Covering bound by intersections · Lower bound for a difference of harmonic numbers

Used byHarmonic bound in the largest set size for greedy set cover · Harmonic bound in the universe size for greedy set cover

TheoremHarmonic bound in the largest set size for greedy set cover#✓fully proved

Let \(F\) be a list of finite sets each with at most \(d\) elements, \(U\) a finite set, and \(H(n) = 1 + \frac12 + \dots + \frac1n\) the \(n\)-th harmonic number. For every list \(C^*\) of members of \(F\) that together cover \(U\), the list of sets returned by the greedy set cover algorithm on \(F\) and \(U\) has length at most \(|C^*| \cdot H(d)\), where \(|C^*|\) is the length of \(C^*\).

theorem greedySetCover_approx (F : List (Finset α)) (U : Finset α) {d : ℕ}
    (hd : ∀ S ∈ F, S.card ≤ d) (Cstar : List (Finset α)) (hsub : ∀ S ∈ Cstar, S ∈ F)
    (hcov : ∀ x ∈ U, ∃ S ∈ Cstar, x ∈ S) :
    ((greedySetCover F U).ret.length : ℚ) ≤ Cstar.length * harmonic d

Sources

• CLRS, third edition, Theorem 35.4.

Uses 2

Statement usesGreedy set cover

Proof usesPotential bound for greedy set cover

TheoremHarmonic bound in the universe size for greedy set cover#✓fully proved

Let \(F\) be a list of finite sets, \(U\) a finite set, and \(H(n) = 1 + \frac12 + \dots + \frac1n\) the \(n\)-th harmonic number. For every list \(C^*\) of members of \(F\) that together cover \(U\), the list of sets returned by the greedy set cover algorithm on \(F\) and \(U\) has length at most \(|C^*| \cdot H(|U|)\), where \(|C^*|\) is the length of \(C^*\).

theorem greedySetCover_approx_card (F : List (Finset α)) (U : Finset α)
    (Cstar : List (Finset α)) (hsub : ∀ S ∈ Cstar, S ∈ F)
    (hcov : ∀ x ∈ U, ∃ S ∈ Cstar, x ∈ S) :
    ((greedySetCover F U).ret.length : ℚ) ≤ Cstar.length * harmonic U.card

Sources

• CLRS, third edition, Corollary 35.5, in the stronger harmonic form.

Uses 2 · Used by 1

Statement usesGreedy set cover

Proof usesPotential bound for greedy set cover

Used byGreedy set cover is a logarithmic approximation

TheoremGreedy set cover is a logarithmic approximation#✓fully proved

Let \(F\) be a list of finite sets and \(U\) a finite set. For every list \(C^*\) of members of \(F\) that together cover \(U\), the list of sets returned by the greedy set cover algorithm on \(F\) and \(U\) has length at most \(|C^*| \cdot (\ln |U| + 1)\), where \(|C^*|\) is the length of \(C^*\) and \(\ln 0 = 0\).

theorem greedySetCover_approx_log (F : List (Finset α)) (U : Finset α)
    (Cstar : List (Finset α)) (hsub : ∀ S ∈ Cstar, S ∈ F)
    (hcov : ∀ x ∈ U, ∃ S ∈ Cstar, x ∈ S) :
    ((greedySetCover F U).ret.length : ℝ) ≤ Cstar.length * (Real.log U.card + 1)

Sources

• CLRS, third edition, Corollary 35.5, via Mathlib's harmonic_le_one_add_log.

Uses 2

Statement usesGreedy set cover

Proof usesHarmonic bound in the universe size for greedy set cover

DefinitionSet with the least cost per new element#✓fully proved

Given a list \(F\) of finite sets, a finite set \(U\) and a rational cost \(w(S)\) for each finite set \(S\), this is the first set \(S\) in \(F\) with \(S \cap U \ne \emptyset\) that minimizes the ratio \(w(S) / |S \cap U|\) among the sets of \(F\) meeting \(U\), or nothing when no set of \(F\) meets \(U\).

def bestRatioSet (w : Finset α → ℚ) (F : List (Finset α)) (U : Finset α) : Option (Finset α) :=
  (F.filter fun S => (S ∩ U).card ≠ 0).argmax fun S => -(w S / (S ∩ U).card)

Used by 5

Used byWeighted greedy set cover · Potential bound for weighted greedy set cover · The weighted greedy set cover is a cover · The weighted greedy set cover uses sets of the family · Running time of weighted greedy set cover

DefinitionWeighted greedy set cover#✓fully proved

Let \(F = [S_1, \dots, S_n]\) be a list of finite sets, \(U\) a finite set and \(w\) a function giving each finite set \(S\) a rational cost \(w(S)\). The weighted greedy set cover of \(U\) from \(F\) with costs \(w\) is computed as follows. If no \(S_i\) meets \(U\), the result is the empty list. Otherwise let \(T\) be the first \(S_i\) in the list with \(S_i \cap U \ne \emptyset\) that minimizes \(w(S_i) / |S_i \cap U|\) among the sets of \(F\) meeting \(U\); the result is \(T\) followed by the weighted greedy set cover of \(U \setminus T\) from \(F\) with costs \(w\). Each step, including the last one, costs \(n + |S_1| + \dots + |S_n|\).

def weightedGreedySetCover (w : Finset α → ℚ) (F : List (Finset α)) (U : Finset α) :
    TimeM ℕ (List (Finset α)) := do
  ✓[F.length + (F.map Finset.card).sum]
  match _h : bestRatioSet w F U with
  | none => pure []
  | some S => do
      let C ← weightedGreedySetCover w F (U \ S)
      pure (S :: C)
termination_by U.card
decreasing_by exact card_sdiff_lt (bestRatioSet_spec _h).2.1

Uses 1 · Used by 5

Statement usesSet with the least cost per new element

Used byChvátal's bound · Potential bound for weighted greedy set cover · The weighted greedy set cover is a cover · The weighted greedy set cover uses sets of the family · Running time of weighted greedy set cover

TheoremThe weighted greedy set cover uses sets of the family#✓fully proved

For every list \(F\) of finite sets, finite set \(U\) and rational cost function \(w\) on finite sets, every set chosen by the weighted greedy set cover of \(U\) from \(F\) with costs \(w\) belongs to \(F\).

theorem weightedGreedySetCover_mem (w : Finset α → ℚ) (F : List (Finset α)) (U : Finset α) :
    ∀ S ∈ (weightedGreedySetCover w F U).ret, S ∈ F

Uses 2

Statement usesWeighted greedy set cover

Proof usesSet with the least cost per new element

TheoremThe weighted greedy set cover is a cover#✓fully proved

Let \(F\) be a list of finite sets, \(U\) a finite set and \(w\) any rational cost function on finite sets. If every element of \(U\) lies in some set of \(F\), then every element of \(U\) lies in some set chosen by the weighted greedy set cover of \(U\) from \(F\) with costs \(w\).

theorem weightedGreedySetCover_covers (w : Finset α → ℚ) (F : List (Finset α)) (U : Finset α)
    (hU : ∀ x ∈ U, ∃ S ∈ F, x ∈ S) :
    ∀ x ∈ U, ∃ S ∈ (weightedGreedySetCover w F U).ret, x ∈ S

Uses 2

Statement usesWeighted greedy set cover

Proof usesSet with the least cost per new element

TheoremRunning time of weighted greedy set cover#✓fully proved

Let \(F = [S_1, \dots, S_m]\) be a list of finite sets, \(U\) a finite set and \(w\) a rational cost function on finite sets. The weighted greedy set cover of \(U\) from \(F\) with costs \(w\) runs in time at most \((|U| + 1)\,(m + |S_1| + \dots + |S_m|)\): at most \(|U| + 1\) searches for a best set, each costing \(m\) plus the total size of the sets of \(F\).

theorem weightedGreedySetCover_time_le (w : Finset α → ℚ) (F : List (Finset α)) (U : Finset α) :
    (weightedGreedySetCover w F U).time ≤
      (U.card + 1) * (F.length + (F.map Finset.card).sum)

Uses 2

Statement usesWeighted greedy set cover

Proof usesSet with the least cost per new element

DefinitionTotal cost of a list of sets#✓fully proved

For a function \(w\) assigning a rational cost to each finite set, the total cost of a list \(C = [S_1, \dots, S_m]\) of finite sets is \(w(S_1) + \dots + w(S_m)\), a set that occurs several times in \(C\) being counted each time.

def totalCost (w : Finset α → ℚ) (C : List (Finset α)) : ℚ := (C.map w).sum

Used by 2

Used byChvátal's bound · Potential bound for weighted greedy set cover

TheoremPotential bound for weighted greedy set cover#✓fully proved

Let \(F\) be a list of finite sets, \(U\) a finite set and \(w\) a rational cost function on finite sets with \(w(S) \ge 0\) for every \(S\) in \(F\). If \(C^*\) is a list of sets from \(F\) whose union contains \(U\), then the weighted greedy set cover of \(U\) from \(F\) with costs \(w\) has total cost at most \(\sum_{S \in C^*} w(S)\, H(|S \cap U|)\), the sum running over the entries of \(C^*\) with repetition, where \(H(n) = 1 + \frac{1}{2} + \dots + \frac{1}{n}\) is the \(n\)-th harmonic number.

theorem weightedGreedySetCover_cost_le_sum_harmonic (w : Finset α → ℚ) (F : List (Finset α))
    (U : Finset α) (hw : ∀ S ∈ F, 0 ≤ w S) (Cstar : List (Finset α))
    (hsub : ∀ S ∈ Cstar, S ∈ F) (hcov : ∀ x ∈ U, ∃ S ∈ Cstar, x ∈ S) :
    totalCost w (weightedGreedySetCover w F U).ret ≤
      (Cstar.map fun S => w S * harmonic (S ∩ U).card).sum

Uses 5 · Used by 1

Statement usesTotal cost of a list of sets · Weighted greedy set cover

Proof usesSet with the least cost per new element · Covering bound by intersections · Lower bound for a difference of harmonic numbers

Used byChvátal's bound

TheoremChvátal's bound#✓fully proved

Let \(F\) be a list of finite sets, \(U\) a finite set, \(w\) a rational cost function on finite sets with \(w(S) \ge 0\) for every \(S\) in \(F\), and \(d\) a natural number such that every set in \(F\) has at most \(d\) elements. If \(C^*\) is a list of sets from \(F\) whose union contains \(U\), then the weighted greedy set cover of \(U\) from \(F\) with costs \(w\) has total cost at most \(H(d)\) times the total cost of \(C^*\), where \(H(d) = 1 + \frac{1}{2} + \dots + \frac{1}{d}\) is the \(d\)-th harmonic number.

theorem weightedGreedySetCover_approx (w : Finset α → ℚ) (F : List (Finset α)) (U : Finset α)
    (hw : ∀ S ∈ F, 0 ≤ w S) {d : ℕ} (hd : ∀ S ∈ F, S.card ≤ d) (Cstar : List (Finset α))
    (hsub : ∀ S ∈ Cstar, S ∈ F) (hcov : ∀ x ∈ U, ∃ S ∈ Cstar, x ∈ S) :
    totalCost w (weightedGreedySetCover w F U).ret ≤ harmonic d * totalCost w Cstar

Uses 3

Statement usesTotal cost of a list of sets · Weighted greedy set cover

Proof usesPotential bound for weighted greedy set cover

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.