Skip to content
  1. CLRS-Lean
  2. Chapters 1–35 · CLRS Fourth Edition
  3. Chapter 35. Approximation Algorithms
  4. 35.4. Randomization and Linear Programming
Browse chapters
Imports
import CLRSLean.FourthEdition.Chapter_35.Section_35_1_The_Vertex_Cover_Problem import CLRSLean.Probability.FiniteExpectation import Mathlib

35.4. Randomization and Linear Programming

The vertex-cover LP execution constructs the program, invokes SIMPLEX, and rounds its optimum.

This section formalizes the two approximation techniques of CLRS §35.4: randomization and linear programming. It covers (1) a randomized algorithm for MAX-3-CNF satisfiability that achieves a randomized 8/7-approximation (Theorem 35.5), and (2) an LP-rounding algorithm APPROX-MIN-WEIGHT-VC that achieves a factor-two approximation for the minimum-weight vertex-cover problem (Theorem 35.6).

Main results:

  • Definition Literal, ClauseSatisfied, Is3CNFClause: a MAX-3-CNF clause is a set of literals (variable/sign pairs), satisfied by an assignment when one of its literals holds.

  • Lemma unsatisfied_prob: a uniformly random assignment leaves a valid 3-CNF clause unsatisfied with probability 1/8 — its three literals are over distinct variables, so exactly 2^(n-3) of the 2^n assignments take the negated value at each of them (card_assignments_fixing_three).

  • Theorem max3cnf_clause_satisfied_prob (Theorem 35.5): the clause is satisfied with probability 7/8.

  • Theorem max3cnf_expect_satisfied (Theorem 35.5): the expected number of satisfied clauses over a family F is exactly 7/8 · |F|, by linearity of expectation.

  • Theorem max3cnf_approx (Theorem 35.5): MAX-3-CNF has a randomized 8/7-approximation — every assignment is matched in expectation to at least 7/8 of the clauses it satisfies.

  • Definition IsFractionalCover: the feasible region of the vertex-cover LP relaxation — a vector x : V → ℚ with 0 ≤ x v ≤ 1 and x(u) + x(v) ≥ 1 for every edge.

  • Definition roundCover: APPROX-MIN-WEIGHT-VC's rounding — the vertices with fractional value at least 1/2.

  • Theorem roundCover_isVertexCover (Theorem 35.6, correctness): the rounded vertices form a vertex cover.

  • Theorem approxMinWeightVC_two_approx (Theorem 35.6): the rounded cover's weight is at most twice the LP objective, hence at most twice the optimal cover's weight — a factor-two approximation.

The formula is an unweighted finite set of clauses: duplicates collapse and weighted or repeated-clause objectives are outside this model. Each admitted clause has three distinct variables. The rounding theorem below accepts a fractional solution and its objective-bound premise. The companion VertexCoverLP constructs a graph LP, calls initialized Chapter 29 SIMPLEX, and derives that bound for its returned optimum before rounding.

Notation conventions used in this section:

  • n : the number of Boolean variables

  • σ : an assignment Fin n → Bool (the sample space is uniform)

  • (i, b) : the literal "variable i is set to b"

  • c : a clause (a set of literals)

  • G : an undirected graph (edge-based Graph V E)

  • w : a positive vertex-weight function

  • x : a fractional vertex cover (the LP relaxation's solution)

  • C : a vertex cover

noncomputable sectionopen Finsetopen scoped BigOperatorsnamespace CLRSnamespace RandomizedLPopen CLRS.Probability

Randomization: MAX-3-CNF satisfiability (Theorem 35.5)

A literal is a pair (i, b): the assertion that variable i is set to b (true for a positive literal, false for a negative one). A clause is a set of literals, satisfied by an assignment when at least one of its literals holds. The randomized algorithm sets every variable independently to true with probability 1/2; a clause with three literals over three distinct variables is then satisfied with probability 7/8 (Theorem 35.5).

variable {n : ℕ}

A literal: the assertion that variable i (of n) is set to b.

abbrev Literal (n : ℕ) := Fin n × Bool

An assignment: a setting of every variable to true or false.

abbrev Assignment (n : ℕ) := Fin n → Bool

A literal (i, b) holds under σ when σ i = b.

def litHolds (σ : Assignment n) (l : Literal n) : Prop := σ l.1 = l.2

A clause is satisfied by σ when at least one of its literals holds.

def ClauseSatisfied (c : Finset (Literal n)) (σ : Assignment n) : Prop := ∃ l ∈ c, litHolds σ l

A clause is unsatisfied by σ when none of its literals holds.

def ClauseUnsatisfied (c : Finset (Literal n)) (σ : Assignment n) : Prop := ∀ l ∈ c, ¬ litHolds σ l

Satisfaction of a clause over a finite set of literals is decidable.

instance decClauseSatisfied (c : Finset (Literal n)) (σ : Assignment n) : Decidable (ClauseSatisfied c σ) := by unfold ClauseSatisfied litHolds infer_instance

Unsatisfaction of a clause over a finite set of literals is decidable.

instance decClauseUnsatisfied (c : Finset (Literal n)) (σ : Assignment n) : Decidable (ClauseUnsatisfied c σ) := by unfold ClauseUnsatisfied litHolds infer_instance

A valid MAX-3-CNF clause: exactly three literals, over three distinct variables (so no clause contains a variable and its negation).

def Is3CNFClause (c : Finset (Literal n)) : Prop := c.card = 3 ∧ ∀ ⦃l₁ l₂ : Literal n⦄, l₁ ∈ c → l₂ ∈ c → l₁ ≠ l₂ → l₁.1 ≠ l₂.1

A clause is satisfied iff it is not unsatisfied.

lemma clauseSatisfied_iff_not_unsatisfied (c : Finset (Literal n)) (σ : Assignment n) : ClauseSatisfied c σ ↔ ¬ ClauseUnsatisfied c σ := by unfold ClauseSatisfied ClauseUnsatisfied litHolds constructor · intro h hnone rcases h with ⟨l, hl, hlh⟩ exact hnone l hl hlh · intro h by_contra hnone apply h intro l hl exact fun hlt => hnone ⟨l, hl, hlt⟩

In Bool, x ≠ b holds exactly when x is the negation of b.

lemma bool_ne_iff_not (x b : Bool) : x ≠ b ↔ x = Bool.not b := by cases x <;> cases b <;> simp

The number of assignments that fix the value of three distinct variables is 2^(n-3): the remaining n-3 variables are free. This is the counting step of Theorem 35.5 — a uniformly random assignment hits a given triple of values with probability 2^(n-3) / 2^n = 1/8.

lemma card_assignments_fixing_three {i₁ i₂ i₃ : Fin n} (hi12 : i₁ ≠ i₂) (hi13 : i₁ ≠ i₃) (hi23 : i₂ ≠ i₃) {v₁ v₂ v₃ : Bool} : Fintype.card {σ : Assignment n // σ i₁ = v₁ ∧ σ i₂ = v₂ ∧ σ i₃ = v₃} = 2 ^ (n - 3) := by classical let C : Finset (Fin n) := {i₁, i₂, i₃} let Free : Type := {k : Fin n // k ∉ C} have hCcard : C.card = 3 := by dsimp [C] simp [hi12, hi13, hi23] have hfree : Fintype.card Free = n - 3 := by dsimp [Free, C] have hsub := Fintype.card_subtype_compl (fun k : Fin n => k ∈ C) rw [hsub] simp [hCcard, Fintype.card_fin] let e : {σ : Assignment n // σ i₁ = v₁ ∧ σ i₂ = v₂ ∧ σ i₃ = v₃} ≃ (Free → Bool) := { toFun := fun σ k => σ.1 k.1 invFun := fun τ => ⟨fun k => if h₁ : k = i₁ then v₁ else if h₂ : k = i₂ then v₂ else if h₃ : k = i₃ then v₃ else τ ⟨k, by intro hkC simp [C] at hkC rcases hkC with h | h | h · exact h₁ h · exact h₂ h · exact h₃ h⟩, by dsimp constructor · simp · constructor · simp [hi12.symm] · simp [hi13.symm, hi23.symm]⟩ left_inv := by intro σ apply Subtype.ext funext k dsimp by_cases h₁ : k = i₁ · subst k simp [σ.2.1] · by_cases h₂ : k = i₂ · subst k simp [σ.2.2.1, hi12.symm] · by_cases h₃ : k = i₃ · subst k simp [σ.2.2.2, hi13.symm, hi23.symm] · simp [h₁, h₂, h₃] right_inv := by intro τ funext k dsimp have hk1 : k.1 ≠ i₁ := by intro h apply k.2 simp [C, h] have hk2 : k.1 ≠ i₂ := by intro h apply k.2 simp [C, h] have hk3 : k.1 ≠ i₃ := by intro h apply k.2 simp [C, h] simp [hk1, hk2, hk3] } have hcard : Fintype.card {σ : Assignment n // σ i₁ = v₁ ∧ σ i₂ = v₂ ∧ σ i₃ = v₃} = 2 ^ (n - 3) := by rw [Fintype.card_congr e] calc Fintype.card (Free → Bool) = 2 ^ Fintype.card Free := by rw [Fintype.card_fun] simp [Fintype.card_bool] _ = 2 ^ (n - 3) := by rw [hfree] exact hcard

Linearity of fintypeExpect for c - X on a nonempty sample space: E[c - X] = c - E[X].

lemma fintypeExpect_sub_const {Ω : Type} [Fintype Ω] [DecidableEq Ω] (c : ℝ) (X : Ω → ℝ) (hΩ : Fintype.card Ω ≠ 0) : fintypeExpect (fun ω => c - X ω) = c - fintypeExpect X := by unfold fintypeExpect rw [Finset.sum_sub_distrib, Finset.sum_const, Finset.card_univ, nsmul_eq_mul] have hc : (Fintype.card Ω : ℝ) ≠ 0 := by exact_mod_cast hΩ field_simp [hc]

The sum of the indicator of a predicate over a finite type is the number of its elements satisfying the predicate.

lemma sum_indicator_card {Ω : Type} [Fintype Ω] (P : Ω → Prop) [DecidablePred P] : (∑ σ : Ω, if P σ then (1 : ℝ) else 0) = (Fintype.card {σ : Ω // P σ} : ℝ) := by calc (∑ σ : Ω, if P σ then (1 : ℝ) else 0) = (Finset.univ.filter P).card := by exact_mod_cast (Finset.sum_boole P Finset.univ) _ = (Fintype.card {σ : Ω // P σ} : ℝ) := by exact_mod_cast (Fintype.card_of_subtype (Finset.univ.filter P) (fun σ => by simp)).symm

A uniformly random assignment leaves a valid 3-CNF clause unsatisfied with probability exactly 1/8: its three literals are over distinct variables, so the assignment must take the negated value at each of the three variables, and exactly 2^(n-3) of the 2^n assignments do so (CLRS §35.4, Theorem 35.5).

try 'simp' instead of 'simpa' Note: This linter can be disabled with `set_option linter.unnecessarySimpa false` lemma unsatisfied_prob (c : Finset (Literal n)) (hc : Is3CNFClause c) : fintypeExpect (fun σ : Assignment n => indicator (ClauseUnsatisfied c σ)) = (1 : ℝ) / 8 := by classical rcases (Finset.card_eq_three.mp hc.1) with ⟨l₁, l₂, l₃, h12, h13, h23, hc_eq⟩ have hi12 : l₁.1 ≠ l₂.1 := hc.2 (by simp [hc_eq]) (by simp [hc_eq]) h12 have hi13 : l₁.1 ≠ l₃.1 := hc.2 (by simp [hc_eq]) (by simp [hc_eq]) h13 have hi23 : l₂.1 ≠ l₃.1 := hc.2 (by simp [hc_eq]) (by simp [hc_eq]) h23 have hun : ∀ σ : Assignment n, ClauseUnsatisfied c σ ↔ σ l₁.1 = Bool.not l₁.2 ∧ σ l₂.1 = Bool.not l₂.2 ∧ σ l₃.1 = Bool.not l₃.2 := by intro σ simp [ClauseUnsatisfied, litHolds, hc_eq, This simp argument is unused: h12 Hint: Omit it from the simp argument list. simp [ClauseUnsatisfied, litHolds, hc_eq, h12̵,̵ ̵h̵1̵3, h23, bool_ne_iff_not] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`h12, This simp argument is unused: h13 Hint: Omit it from the simp argument list. simp [ClauseUnsatisfied, litHolds, hc_eq, h12, h1̵3̵,̵ ̵h̵23, bool_ne_iff_not] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`h13, This simp argument is unused: h23 Hint: Omit it from the simp argument list. simp [ClauseUnsatisfied, litHolds, hc_eq, h12, h13, h̵2̵3̵,̵ ̵bool_ne_iff_not] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`h23, bool_ne_iff_not] have hcard : Fintype.card {σ : Assignment n // ClauseUnsatisfied c σ} = 2 ^ (n - 3) := by have hcard3 := card_assignments_fixing_three (i₁ := l₁.1) (i₂ := l₂.1) (i₃ := l₃.1) hi12 hi13 hi23 (v₁ := Bool.not l₁.2) (v₂ := Bool.not l₂.2) (v₃ := Bool.not l₃.2) have hcong : Fintype.card {σ : Assignment n // ClauseUnsatisfied c σ} = Fintype.card {σ : Assignment n // σ l₁.1 = Bool.not l₁.2 ∧ σ l₂.1 = Bool.not l₂.2 ∧ σ l₃.1 = Bool.not l₃.2} := by exact Fintype.card_congr (Equiv.subtypeEquivProp (funext fun σ => propext (hun σ))) rwa [hcong] unfold fintypeExpect indicator have hsum : (∑ σ : Assignment n, if ClauseUnsatisfied c σ then (1 : ℝ) else 0) = (2 ^ (n - 3) : ℝ) := by rw [sum_indicator_card] exact_mod_cast hcard have hcardA : (Fintype.card (Assignment n) : ℝ) = (2 ^ n : ℝ) := by have hnat : Fintype.card (Assignment n) = 2 ^ n := by rw [Fintype.card_fun] simp [Fintype.card_bool] exact_mod_cast hnat rw [hsum, hcardA] have hn : 3 ≤ n := by have hsub : ({l₁.1, l₂.1, l₃.1} : Finset (Fin n)) ⊆ Finset.univ := Finset.subset_univ _ have hthree : ({l₁.1, l₂.1, l₃.1} : Finset (Fin n)).card = 3 := by simp [hi12, hi13, hi23] have hle : 3 ≤ Finset.univ.card := le_trans (by try 'simp' instead of 'simpa' Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hthree]) (Finset.card_le_card hsub) simpa using hle have h2ne : (2 : ℝ) ≠ 0 := by norm_num have hpow : (2 ^ (n - 3) : ℝ) * 8 = (2 ^ n : ℝ) := by have hadd : (2 ^ (n - 3) : ℝ) * (2 ^ 3 : ℝ) = 2 ^ ((n - 3) + 3) := by rw [← pow_add] norm_num at hadd rwa [Nat.sub_add_cancel hn] at hadd calc (2 ^ (n - 3) : ℝ) / (2 ^ n : ℝ) = (2 ^ (n - 3) : ℝ) / ((2 ^ (n - 3) : ℝ) * 8) := by rw [hpow] _ = (1 : ℝ) / 8 := by field_simp [pow_ne_zero (n - 3) h2ne]

A uniformly random assignment satisfies a valid 3-CNF clause with probability exactly 7/8 (CLRS §35.4, Theorem 35.5).

theorem max3cnf_clause_satisfied_prob (c : Finset (Literal n)) (hc : Is3CNFClause c) : fintypeExpect (fun σ : Assignment n => indicator (ClauseSatisfied c σ)) = (7 : ℝ) / 8 := by classical have hU := unsatisfied_prob c hc have hfunc : ∀ σ : Assignment n, indicator (ClauseSatisfied c σ) = 1 - indicator (ClauseUnsatisfied c σ) := by intro σ have hiff := clauseSatisfied_iff_not_unsatisfied c σ unfold indicator by_cases h : ClauseSatisfied c σ · have hUσ : ¬ ClauseUnsatisfied c σ := hiff.mp h simp [h, hUσ] · have hUσ : ClauseUnsatisfied c σ := by by_contra hU' exact h (hiff.2 hU') simp [h, hUσ] calc fintypeExpect (fun σ : Assignment n => indicator (ClauseSatisfied c σ)) = fintypeExpect (fun σ : Assignment n => 1 - indicator (ClauseUnsatisfied c σ)) := by congr 1 funext σ exact hfunc σ _ = 1 - fintypeExpect (fun σ : Assignment n => indicator (ClauseUnsatisfied c σ)) := by have hne : Fintype.card (Assignment n) ≠ 0 := by have hpos : 0 < Fintype.card (Assignment n) := Fintype.card_pos_iff.mpr ⟨fun _ => true⟩ exact ne_of_gt hpos exact fintypeExpect_sub_const (1 : ℝ) (fun σ : Assignment n => indicator (ClauseUnsatisfied c σ)) hne _ = 1 - (1 : ℝ) / 8 := by rw [hU] _ = (7 : ℝ) / 8 := by norm_num

The number of clauses of F satisfied by the assignment σ.

def satisfiedCount (F : Finset (Finset (Literal n))) (σ : Assignment n) : ℕ := (F.filter (fun c => ClauseSatisfied c σ)).card

Theorem 35.5 (expectation). For a family F of valid 3-CNF clauses, the expected number of satisfied clauses under a uniformly random assignment is exactly 7/8 · |F|, by linearity of expectation over the per-clause probabilities (CLRS §35.4, Theorem 35.5).

theorem max3cnf_expect_satisfied (F : Finset (Finset (Literal n))) (hF : ∀ c ∈ F, Is3CNFClause c) : fintypeExpect (fun σ : Assignment n => (∑ c ∈ F, indicator (ClauseSatisfied c σ) : ℝ)) = (7 : ℝ) / 8 * (F.card : ℝ) := by rw [fintypeExpect_sum] have hper : ∀ c ∈ F, fintypeExpect (fun σ : Assignment n => indicator (ClauseSatisfied c σ)) = (7 : ℝ) / 8 := by intro c hc exact max3cnf_clause_satisfied_prob c (hF c hc) rw [Finset.sum_congr rfl hper] rw [Finset.sum_const, nsmul_eq_mul] ring

Theorem 35.5. MAX-3-CNF has a randomized 8/7-approximation algorithm: for any assignment σ₀ — in particular an optimal one — the expected number of clauses satisfied by a uniformly random assignment is at least 7/8 of the number that σ₀ satisfies (CLRS §35.4, Theorem 35.5).

theorem max3cnf_approx (F : Finset (Finset (Literal n))) (hF : ∀ c ∈ F, Is3CNFClause c) (σ₀ : Assignment n) : (7 : ℝ) / 8 * (satisfiedCount F σ₀ : ℝ) ≤ fintypeExpect (fun σ : Assignment n => (∑ c ∈ F, indicator (ClauseSatisfied c σ) : ℝ)) := by have hle : satisfiedCount F σ₀ ≤ F.card := by dsimp [satisfiedCount] exact Finset.card_le_card (Finset.filter_subset _ _) have hE := max3cnf_expect_satisfied F hF calc (7 : ℝ) / 8 * (satisfiedCount F σ₀ : ℝ) ≤ (7 : ℝ) / 8 * (F.card : ℝ) := by exact mul_le_mul_of_nonneg_left (by exact_mod_cast hle) (by norm_num) _ = fintypeExpect (fun σ : Assignment n => (∑ c ∈ F, indicator (ClauseSatisfied c σ) : ℝ)) := hE.symm

Linear programming: weighted vertex cover (Theorem 35.6)

The minimum-weight vertex-cover problem takes a graph with positive vertex weights w(v) and asks for a cover minimizing the total weight. The 0-1 integer program x(v) ∈ {0, 1} with x(u) + x(v) ≥ 1 on every edge is relaxed to the linear program 0 ≤ x(v) ≤ 1. Any feasible solution of the IP is feasible for the LP, so the LP optimum lower-bounds the IP optimum (the optimal cover's weight). APPROX-MIN-WEIGHT-VC solves the LP and rounds every vertex with x(v) ≥ 1/2 up to 1; the rounding is a vertex cover (for every edge at least one endpoint has x ≥ 1/2) and costs at most 2 times the LP objective (since each rounded vertex contributes w(v) ≤ 2·w(v)·x(v)).

variable {V E : Type} [DecidableEq V] [DecidableEq E] [Fintype V]

The weight of a set of vertices under the weight function w.

def vertexWeight (w : V → ℚ) (C : Finset V) : ℚ := ∑ v ∈ C, w v

A fractional vertex cover: a vector x : V → ℚ with 0 ≤ x v ≤ 1 satisfying x(u) + x(v) ≥ 1 for every edge of E₀. This is the feasible region of the linear-programming relaxation (CLRS §35.4, equations (35.15)-(35.18)).

def IsFractionalCover (G : ApproxVertexCover.Graph V E) (x : V → ℚ) (E₀ : Finset E) : Prop := (∀ v, 0 ≤ x v) ∧ (∀ v, x v ≤ 1) ∧ ∀ e ∈ E₀, x (G.src e) + x (G.dst e) ≥ 1

The LP rounding of a fractional cover: the vertices with fractional value at least 1/2. This is the rounding step of APPROX-MIN-WEIGHT-VC (CLRS §35.4, lines 3-5).

def roundCover (x : V → ℚ) : Finset V := Finset.univ.filter (fun v => (1 : ℚ) / 2 ≤ x v)

A vertex belongs to the rounding exactly when its fractional value is at least 1/2.

automatically included section variable(s) unused in theorem `CLRS.RandomizedLP.mem_roundCover`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.RandomizedLP.mem_roundCover`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` automatically included section variable(s) unused in theorem `CLRS.RandomizedLP.mem_roundCover`: [DecidableEq V] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq V] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`lemma mem_roundCover (x : V → ℚ) (v : V) : v ∈ roundCover x ↔ (1 : ℚ) / 2 ≤ x v := by simp [roundCover]

Theorem 35.6 (correctness). The rounding of a fractional cover is a vertex cover of the edge set: for every edge, at least one endpoint has fractional value at least 1/2 (because the two values sum to at least 1).

automatically included section variable(s) unused in theorem `CLRS.RandomizedLP.roundCover_isVertexCover`: [DecidableEq E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.RandomizedLP.roundCover_isVertexCover`: [DecidableEq E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.RandomizedLP.roundCover_isVertexCover`: [DecidableEq E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.RandomizedLP.roundCover_isVertexCover`: [DecidableEq E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.RandomizedLP.roundCover_isVertexCover`: [DecidableEq E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.RandomizedLP.roundCover_isVertexCover`: [DecidableEq E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.RandomizedLP.roundCover_isVertexCover`: [DecidableEq E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.RandomizedLP.roundCover_isVertexCover`: [DecidableEq E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.RandomizedLP.roundCover_isVertexCover`: [DecidableEq E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.RandomizedLP.roundCover_isVertexCover`: [DecidableEq E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.RandomizedLP.roundCover_isVertexCover`: [DecidableEq E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.RandomizedLP.roundCover_isVertexCover`: [DecidableEq E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.RandomizedLP.roundCover_isVertexCover`: [DecidableEq E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.RandomizedLP.roundCover_isVertexCover`: [DecidableEq E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` automatically included section variable(s) unused in theorem `CLRS.RandomizedLP.roundCover_isVertexCover`: [DecidableEq E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`lemma roundCover_isVertexCover (G : ApproxVertexCover.Graph V E) {x : V → ℚ} {E₀ : Finset E} (hx : IsFractionalCover G x E₀) : G.IsVertexCoverOn E₀ (roundCover x) := by intro e he have hineq : x (G.src e) + x (G.dst e) ≥ 1 := hx.2.2 e he by_cases hsrc : (1 : ℚ) / 2 ≤ x (G.src e) · left exact (mem_roundCover x (G.src e)).mpr hsrc · right have hsrc' : x (G.src e) < (1 : ℚ) / 2 := lt_of_not_ge hsrc have hdst : (1 : ℚ) / 2 ≤ x (G.dst e) := by nlinarith exact (mem_roundCover x (G.dst e)).mpr hdst

The weight of the rounded cover is at most twice the LP objective Σ v, w(v)·x(v): each rounded vertex v has x(v) ≥ 1/2, so its weight w(v) ≤ 2·w(v)·x(v).

automatically included section variable(s) unused in theorem `CLRS.RandomizedLP.roundCover_weight_le`: [DecidableEq E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.RandomizedLP.roundCover_weight_le`: [DecidableEq E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.RandomizedLP.roundCover_weight_le`: [DecidableEq E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.RandomizedLP.roundCover_weight_le`: [DecidableEq E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.RandomizedLP.roundCover_weight_le`: [DecidableEq E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.RandomizedLP.roundCover_weight_le`: [DecidableEq E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.RandomizedLP.roundCover_weight_le`: [DecidableEq E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.RandomizedLP.roundCover_weight_le`: [DecidableEq E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.RandomizedLP.roundCover_weight_le`: [DecidableEq E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.RandomizedLP.roundCover_weight_le`: [DecidableEq E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.RandomizedLP.roundCover_weight_le`: [DecidableEq E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.RandomizedLP.roundCover_weight_le`: [DecidableEq E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.RandomizedLP.roundCover_weight_le`: [DecidableEq E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.RandomizedLP.roundCover_weight_le`: [DecidableEq E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.RandomizedLP.roundCover_weight_le`: [DecidableEq E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`automatically included section variable(s) unused in theorem `CLRS.RandomizedLP.roundCover_weight_le`: [DecidableEq E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` automatically included section variable(s) unused in theorem `CLRS.RandomizedLP.roundCover_weight_le`: [DecidableEq E] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq E] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`lemma roundCover_weight_le (G : ApproxVertexCover.Graph V E) {w : V → ℚ} {x : V → ℚ} {E₀ : Finset E} (hw : ∀ v, 0 < w v) (hx : IsFractionalCover G x E₀) : vertexWeight w (roundCover x) ≤ 2 * (∑ v : V, w v * x v) := by have hstep : ∀ v, v ∈ roundCover x → w v ≤ 2 * (w v * x v) := by intro v hv have hx5 : (1 : ℚ) / 2 ≤ x v := (mem_roundCover x v).mp hv have hwpos : 0 < w v := hw v nlinarith have hsum1 : vertexWeight w (roundCover x) ≤ ∑ v ∈ roundCover x, 2 * (w v * x v) := by exact Finset.sum_le_sum hstep have hsum2 : (∑ v ∈ roundCover x, 2 * (w v * x v)) ≤ ∑ v : V, 2 * (w v * x v) := by refine Finset.sum_le_sum_of_subset_of_nonneg (Finset.subset_univ _) ?_ intro v _ hvnot exact mul_nonneg (by norm_num) (mul_nonneg (le_of_lt (hw v)) (hx.1 v)) calc vertexWeight w (roundCover x) = ∑ v ∈ roundCover x, w v := rfl _ ≤ ∑ v ∈ roundCover x, 2 * (w v * x v) := hsum1 _ ≤ ∑ v : V, 2 * (w v * x v) := hsum2 _ = 2 * (∑ v : V, w v * x v) := by rw [Finset.mul_sum]

Theorem 35.6. APPROX-MIN-WEIGHT-VC is a 2-approximation algorithm for the minimum-weight vertex-cover problem: for any positive weights w, any fractional cover x whose LP objective is at most the weight of a vertex cover C* (in particular the LP optimum, which lower-bounds the IP optimum), the rounded cover has weight at most 2 · w(C*) (CLRS §35.4, Theorem 35.6).

theorem approxMinWeightVC_two_approx (G : ApproxVertexCover.Graph V E) {w : V → ℚ} {x : V → ℚ} {E₀ : Finset E} (hw : ∀ v, 0 < w v) (hx : IsFractionalCover G x E₀) (Cstar : Finset V) (Variable name `hCstar` is not explicitly referenced. The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false`hCstar : G.IsVertexCoverOn E₀ Cstar) (hLP : (∑ v : V, w v * x v) ≤ vertexWeight w Cstar) : vertexWeight w (roundCover x) ≤ 2 * vertexWeight w Cstar := by have h1 := roundCover_weight_le (G := G) hw hx calc vertexWeight w (roundCover x) ≤ 2 * (∑ v : V, w v * x v) := h1 _ ≤ 2 * vertexWeight w Cstar := by exact mul_le_mul_of_nonneg_left hLP (by norm_num)
end RandomizedLPend CLRS

Definitions and proofs

CLRSLean.FourthEdition.Chapter_35.Section_35_4_Randomization_And_Linear_Programming.VertexCoverLP

Vertex-cover LP construction and initialized-solver composition

The graph supplies all constraints. The initialized Chapter 29 solver produces a fractional optimum; feasibility and boundedness discharge its other outcomes. Rounding that returned vector gives a cover within twice every comparator cover. The new solver bridge uses real fractional vectors and rational input weights; the older rational-vector rounding interface is retained. This is a classical exact-real construction, without a polynomial SIMPLEX runtime claim.

noncomputable sectionnamespace CLRS.RandomizedLP.VertexCoverLPopen Finset Matrixvariable {n m : Nat} (G : ApproxVertexCover.Graph (Fin n) (Fin m)) (edges : Finset (Fin m)) (w : Fin n → ℚ)

Maximize the negated cover weight under edge and upper-bound constraints.

def program : Chapter29.StandardLP (m+n) n where A := Fin.addCases (fun e j => if e ∈ edges then -(if j = G.src e then 1 else 0) - (if j = G.dst e then 1 else 0) else 0) (fun v j => if j = v then 1 else 0) b := Fin.addCases (fun e => if e ∈ edges then -1 else 0) (fun _ => 1) c := fun v => -(w v : ℝ)
@[simp] theorem edge_row (x : Fin n → ℝ) (e : Fin m) : ((program G edges w).A *ᵥ x) (Fin.castAdd n e) = if e ∈ edges then -(x (G.src e) + x (G.dst e)) else 0 := by by_cases he : e ∈ edges <;> simp [program, Matrix.mulVec, dotProduct, he, sub_mul, Finset.sum_sub_distrib] ring@[simp] theorem upper_row (x : Fin n → ℝ) (v : Fin n) : ((program G edges w).A *ᵥ x) (Fin.natAdd m v) = x v := by simp [program, Matrix.mulVec, dotProduct]

Exact LP encoding of fractional cover constraints.

theorem feasible_iff (x : Fin n → ℝ) : (program G edges w).IsFeasible x ↔ (∀ v, 0 ≤ x v) ∧ (∀ v, x v ≤ 1) ∧ ∀ e ∈ edges, 1 ≤ x (G.src e)+x (G.dst e) := by constructor · intro h refine ⟨h.1,?_,?_⟩ · intro v have hb := h.2 (Fin.natAdd m v) rw [upper_row] at hb simpa [program] using hb · intro e he have heq := edge_row G edges w x e have hb := h.2 (Fin.castAdd n e) rw [heq] at hb simpa [program,he] using hb · rintro ⟨hzero,hupper,hedge⟩ refine ⟨hzero,?_⟩ intro i refine Fin.addCases (fun e => ?_) (fun v => ?_) i · rw [edge_row] by_cases he : e ∈ edges · simpa [program,he] using neg_le_neg (hedge e he) · simp [program,he] · rw [upper_row] simpa [program] using hupper v
@[simp] theorem objective_eq (x : Fin n → ℝ) : (program G edges w).objective x = -(∑ v, (w v : ℝ)*x v) := by simp [Chapter29.StandardLP.objective, program, dotProduct, Finset.sum_neg_distrib] theorem feasible_one : (program G edges w).IsFeasible (fun _ => 1) := by rw [feasible_iff] norm_num theorem objective_nonpos (hw : ∀ v, 0 ≤ w v) {x : Fin n → ℝ} (hx : (program G edges w).IsFeasible x) : (program G edges w).objective x ≤ 0 := by rw [objective_eq] have hs : 0 ≤ ∑ v, (w v : ℝ)*x v := by apply Finset.sum_nonneg intro v _ exact mul_nonneg (by exact_mod_cast hw v) (hx.1 v) linarith

Invoke initialized SIMPLEX and retain its returned optimal vector.

def solve (hw : ∀ v, 0 ≤ w v) : {x : Fin n → ℝ // (program G edges w).IsOptimal x} := match (program G edges w).initializedSimplex with | .infeasible h => False.elim (h ⟨_,feasible_one G edges w⟩) | .optimal x hx => ⟨x,hx⟩ | .unbounded h => False.elim (by obtain ⟨x,hx,hpos⟩ := h 0 exact (not_lt_of_ge (objective_nonpos G edges w hw hx)) hpos)

Round the actual returned vector at one half.

def execute (hw : ∀ v, 0 ≤ w v) : Finset (Fin n) := let x := solve G edges w hw Finset.univ.filter (fun v => (1:ℝ)/2 ≤ x.val v)
theorem execute_isVertexCover (hw : ∀ v, 0 ≤ w v) : G.IsVertexCoverOn edges (execute G edges w hw) := by intro e he have hx := (feasible_iff G edges w _).mp (solve G edges w hw).property.1 have hedge := hx.2.2 e he simp only [execute, Finset.mem_filter, Finset.mem_univ, true_and] by_cases h : (1:ℝ)/2 ≤ (solve G edges w hw).val (G.src e) · exact Or.inl h · right push Not at h linarith

Every integral comparator cover gives a feasible LP vector.

theorem indicator_feasible (C : Finset (Fin n)) (hC : G.IsVertexCoverOn edges C) : (program G edges w).IsFeasible (fun v => if v ∈ C then 1 else 0) := by rw [feasible_iff] refine ⟨?_,?_,?_⟩ · intro v; split_ifs <;> norm_num · intro v; split_ifs <;> norm_num · intro e he rcases hC e he with hs | hd · simp only [hs, if_true]; split_ifs <;> norm_num · simp only [hd, if_true]; split_ifs <;> norm_num

The bound against every integral cover follows from the returned optimum.

theorem solve_weight_le (hw : ∀ v, 0 ≤ w v) (C : Finset (Fin n)) (hC : G.IsVertexCoverOn edges C) : (∑ v, (w v : ℝ)*(solve G edges w hw).val v) ≤ ∑ v ∈ C, (w v : ℝ) := by have h := (solve G edges w hw).property.2 _ (indicator_feasible G edges w C hC) simp only [objective_eq] at h have hi : (∑ v, (w v : ℝ)*(if v ∈ C then 1 else 0)) = ∑ v ∈ C, (w v : ℝ) := by simp [mul_ite, Finset.sum_ite_mem] rw [hi] at h linarith

Threshold rounding costs at most twice the returned fractional objective.

theorem execute_weight_le_fractional (hw : ∀ v, 0 ≤ w v) : (∑ v ∈ execute G edges w hw, (w v : ℝ)) ≤ 2 * ∑ v, (w v : ℝ)*(solve G edges w hw).val v := by have hx := (solve G edges w hw).property.1.1 have hstep : ∀ v ∈ execute G edges w hw, (w v : ℝ) ≤ 2*((w v : ℝ)*(solve G edges w hw).val v) := by intro v hv have hv' : (1:ℝ)/2 ≤ (solve G edges w hw).val v := by simpa [execute] using hv have hw' : (0:ℝ) ≤ w v := by exact_mod_cast hw v nlinarith calc _ ≤ ∑ v ∈ execute G edges w hw, 2*((w v : ℝ)*(solve G edges w hw).val v) := Finset.sum_le_sum hstep _ ≤ ∑ v, 2*((w v : ℝ)*(solve G edges w hw).val v) := by apply Finset.sum_le_sum_of_subset_of_nonneg (Finset.subset_univ _) intro v _ _ exact mul_nonneg (by norm_num) (mul_nonneg (by exact_mod_cast hw v) (hx v)) _ = _ := by rw [Finset.mul_sum]

Graph-to-solver-to-rounded-cover factor two, without a supplied LP bound.

theorem execute_two_approx (hw : ∀ v, 0 ≤ w v) (C : Finset (Fin n)) (hC : G.IsVertexCoverOn edges C) : vertexWeight w (execute G edges w hw) ≤ 2 * vertexWeight w C := by have hr := execute_weight_le_fractional G edges w hw have ho := solve_weight_le G edges w hw C hC have h : (∑ v ∈ execute G edges w hw, (w v : ℝ)) ≤ 2*∑ v ∈ C, (w v : ℝ) := by linarith unfold vertexWeight exact_mod_cast h

The same returned set satisfies feasibility and the approximation guarantee.

theorem execute_correct (hw : ∀ v, 0 ≤ w v) (C : Finset (Fin n)) (hC : G.IsVertexCoverOn edges C) : G.IsVertexCoverOn edges (execute G edges w hw) ∧ vertexWeight w (execute G edges w hw) ≤ 2*vertexWeight w C := ⟨execute_isVertexCover G edges w hw,execute_two_approx G edges w hw C hC⟩
end CLRS.RandomizedLP.VertexCoverLP