Vertex cover 2-approximation

DefinitionVertex cover scan#✓fully proved

Given a finite set \(C\) of vertices and a list of pairs of vertices, the scan processes the pairs in order, starting from the cover \(C\) and charging one time unit per pair. A pair \((u, v)\) is covered when \(u\) or \(v\) is already in the current cover; a covered pair is skipped, and an uncovered pair adds both \(u\) and \(v\) to the cover. The scan returns the cover reached after the last pair.

def vertexCoverScan (cover : Finset V) : List (V × V) → TimeM ℕ (Finset V)
  | [] => pure cover
  | (u, v) :: es => do
      ✓
      if u ∈ cover ∨ v ∈ cover then vertexCoverScan cover es
      else vertexCoverScan (insert u (insert v cover)) es

Used by 8

Used byAPPROX-VERTEX-COVER · APPROX-VERTEX-COVER covers every listed pair · The edges APPROX-VERTEX-COVER takes form a maximal matching of the listed pairs · APPROX-VERTEX-COVER is at most twice any vertex cover · Counting invariant of the vertex cover scan · Matching invariant of the vertex cover scan · The vertex cover scan only adds vertices · Running time of the vertex cover scan

DefinitionAPPROX-VERTEX-COVER#✓fully proved

Given a list \(L\) of ordered pairs of vertices, APPROX-VERTEX-COVER starts from the empty cover and goes through \(L\) in order: a pair \((u, v)\) with \(u\) or \(v\) already in the cover is skipped, and otherwise both \(u\) and \(v\) are added to the cover. It returns the final cover, a finite set of vertices, at a cost of one unit per pair of \(L\).

CLRS (third edition, Section 35.1) takes an arbitrary uncovered edge at each step; here it is the first uncovered pair in list order.

def approxVertexCover (edges : List (V × V)) : TimeM ℕ (Finset V) :=
  vertexCoverScan ∅ edges

def vertexCoverScan (cover : Finset V) : List (V × V) → TimeM ℕ (Finset V)
  | [] => pure cover
  | (u, v) :: es => do
      ✓
      if u ∈ cover ∨ v ∈ cover then vertexCoverScan cover es
      else vertexCoverScan (insert u (insert v cover)) es

CSLibExt/Algorithms/Lean/Approximation/VertexCover.lean:53

Uses 1 · Used by 6

Statement usesVertex cover scan

Used byAPPROX-VERTEX-COVER covers every listed pair · APPROX-VERTEX-COVER returns a vertex cover · The edges APPROX-VERTEX-COVER takes form a maximal matching of the listed pairs · Running time of APPROX-VERTEX-COVER · APPROX-VERTEX-COVER is a 2-approximation · APPROX-VERTEX-COVER is at most twice any vertex cover

13 fully proved

Cost

TheoremRunning time of the vertex cover scan#✓fully proved

For every finite set \(C\) of vertices and every list \(L\) of pairs of vertices, the running time of the vertex cover scan starting from \(C\) on \(L\) is the length of \(L\).

@[simp]
theorem vertexCoverScan_time (cover : Finset V) (edges : List (V × V)) :
    (vertexCoverScan cover edges).time = edges.length

def vertexCoverScan (cover : Finset V) : List (V × V) → TimeM ℕ (Finset V)
  | [] => pure cover
  | (u, v) :: es => do
      ✓
      if u ∈ cover ∨ v ∈ cover then vertexCoverScan cover es
      else vertexCoverScan (insert u (insert v cover)) es

CSLibExt/Algorithms/Lean/Approximation/VertexCover.lean:53

Uses 1 · Used by 1

Statement usesVertex cover scan

Used byRunning time of APPROX-VERTEX-COVER

TheoremRunning time of APPROX-VERTEX-COVER#✓fully proved

For every list \(L\) of ordered pairs of vertices, the cost of APPROX-VERTEX-COVER on \(L\) is the length of \(L\): one unit per listed pair.

@[simp]
theorem approxVertexCover_time (edges : List (V × V)) :
    (approxVertexCover edges).time = edges.length

Uses 2

Statement usesAPPROX-VERTEX-COVER

Proof usesRunning time of the vertex cover scan

The result is a vertex cover

TheoremThe vertex cover scan only adds vertices#✓fully proved

For every finite set \(C\) of vertices and every list of pairs of vertices, the cover returned by the vertex cover scan starting from \(C\) on that list contains \(C\).

theorem subset_vertexCoverScan (cover : Finset V) (edges : List (V × V)) :
    cover ⊆ (vertexCoverScan cover edges).ret

def vertexCoverScan (cover : Finset V) : List (V × V) → TimeM ℕ (Finset V)
  | [] => pure cover
  | (u, v) :: es => do
      ✓
      if u ∈ cover ∨ v ∈ cover then vertexCoverScan cover es
      else vertexCoverScan (insert u (insert v cover)) es

CSLibExt/Algorithms/Lean/Approximation/VertexCover.lean:53

Uses 1 · Used by 1

Statement usesVertex cover scan

Used byAPPROX-VERTEX-COVER covers every listed pair

TheoremAPPROX-VERTEX-COVER covers every listed pair#✓fully proved

For every list \(L\) of ordered pairs of vertices and every pair \((u, v)\) in \(L\), the cover that APPROX-VERTEX-COVER returns on \(L\) contains \(u\) or \(v\).

theorem approxVertexCover_covers (edges : List (V × V)) :
    ∀ e ∈ edges, e.1 ∈ (approxVertexCover edges).ret ∨ e.2 ∈ (approxVertexCover edges).ret

Uses 3 · Used by 2

Statement usesAPPROX-VERTEX-COVER

Proof usesThe vertex cover scan only adds vertices · Vertex cover scan

Used byAPPROX-VERTEX-COVER returns a vertex cover · The edges APPROX-VERTEX-COVER takes form a maximal matching of the listed pairs

TheoremAPPROX-VERTEX-COVER returns a vertex cover#✓fully proved

Let \(G\) be a simple graph and \(L\) a list of ordered pairs of vertices such that for every edge \(uv\) of \(G\), \((u, v)\) or \((v, u)\) is in \(L\). Then the cover that APPROX-VERTEX-COVER returns on \(L\) is a vertex cover of \(G\).

theorem approxVertexCover_isVertexCover (G : SimpleGraph V) (edges : List (V × V))
    (hcomplete : ∀ ⦃u v⦄, G.Adj u v → (u, v) ∈ edges ∨ (v, u) ∈ edges) :
    G.IsVertexCover ↑(approxVertexCover edges).ret

Uses 2 · Used by 1

Statement usesAPPROX-VERTEX-COVER

Proof usesAPPROX-VERTEX-COVER covers every listed pair

Used byAPPROX-VERTEX-COVER is a 2-approximation

The factor-two bound

TheoremCounting invariant of the vertex cover scan#✓fully proved

Let \(G\) be a simple graph, \(S\) a vertex cover of \(G\), \(C_0\) a finite set of vertices with \(|C_0| \le 2|C_0 \cap S|\), and \(L\) a list of ordered pairs of vertices such that \(u\) and \(v\) are adjacent in \(G\) for every \((u, v)\) in \(L\). Then the cover \(C\) that the vertex cover scan returns on \(L\) starting from \(C_0\) satisfies \(|C| \le 2|C \cap S|\).

The invariant holds because each taken edge adds two new vertices, at least one of them in \(S\).

theorem card_vertexCoverScan_le (G : SimpleGraph V) (S : Set V) (hS : G.IsVertexCover S)
    [DecidablePred (· ∈ S)] (cover : Finset V) (edges : List (V × V))
    (hsound : ∀ e ∈ edges, G.Adj e.1 e.2)
    (hcover : cover.card ≤ 2 * (cover.filter (· ∈ S)).card) :
    (vertexCoverScan cover edges).ret.card ≤
      2 * ((vertexCoverScan cover edges).ret.filter (· ∈ S)).card

def vertexCoverScan (cover : Finset V) : List (V × V) → TimeM ℕ (Finset V)
  | [] => pure cover
  | (u, v) :: es => do
      ✓
      if u ∈ cover ∨ v ∈ cover then vertexCoverScan cover es
      else vertexCoverScan (insert u (insert v cover)) es

CSLibExt/Algorithms/Lean/Approximation/VertexCover.lean:53

Uses 1 · Used by 1

Statement usesVertex cover scan

Used byAPPROX-VERTEX-COVER is at most twice any vertex cover

TheoremAPPROX-VERTEX-COVER is at most twice any vertex cover#✓fully proved

Let \(G\) be a simple graph and \(L\) a list of ordered pairs of vertices such that \(u\) and \(v\) are adjacent in \(G\) for every \((u, v)\) in \(L\). Then for every vertex cover \(S\) of \(G\), finite or infinite, the cover \(C\) that APPROX-VERTEX-COVER returns on \(L\) satisfies \(|C| \le 2|S|\), with sizes in \(\mathbb{N} \cup \{\infty\}\).

theorem card_approxVertexCover_le_two_mul (G : SimpleGraph V) (edges : List (V × V))
    (hsound : ∀ e ∈ edges, G.Adj e.1 e.2) (S : Set V) (hS : G.IsVertexCover S) :
    ((approxVertexCover edges).ret.card : ℕ∞) ≤ 2 * S.encard

Uses 3 · Used by 1

Statement usesAPPROX-VERTEX-COVER

Proof usesCounting invariant of the vertex cover scan · Vertex cover scan

Used byAPPROX-VERTEX-COVER is a 2-approximation

TheoremAPPROX-VERTEX-COVER is a 2-approximation#✓fully proved

Let \(G\) be a simple graph and \(L\) a list of ordered pairs of vertices that lists exactly the edges of \(G\), each in at least one orientation: \(u\) and \(v\) are adjacent in \(G\) for every \((u, v)\) in \(L\), and for every edge \(uv\) of \(G\), \((u, v)\) or \((v, u)\) is in \(L\). Then the cover \(C\) that APPROX-VERTEX-COVER returns on \(L\) is a vertex cover of \(G\) and \(|C| \le 2\tau(G)\), where \(\tau(G) \in \mathbb{N} \cup \{\infty\}\) is the vertex cover number of \(G\), the minimum size of a vertex cover of \(G\).

theorem approxVertexCover_two_approximation (G : SimpleGraph V) (edges : List (V × V))
    (hsound : ∀ e ∈ edges, G.Adj e.1 e.2)
    (hcomplete : ∀ ⦃u v⦄, G.Adj u v → (u, v) ∈ edges ∨ (v, u) ∈ edges) :
    G.IsVertexCover ↑(approxVertexCover edges).ret ∧
      ((approxVertexCover edges).ret.card : ℕ∞) ≤ 2 * G.vertexCoverNum

Sources

CLRS, third edition, Theorem 35.1.

Uses 3

Statement usesAPPROX-VERTEX-COVER

Proof usesAPPROX-VERTEX-COVER returns a vertex cover · APPROX-VERTEX-COVER is at most twice any vertex cover

The edges taken form a maximal matching

DefinitionVertex-disjoint pairs#✓fully proved

Two pairs \((a, b)\) and \((c, d)\) of vertices are vertex-disjoint when they share no endpoint: \(a \ne c\), \(a \ne d\), \(b \ne c\) and \(b \ne d\).

def VertexDisjoint (e f : V × V) : Prop :=
  e.1 ≠ f.1 ∧ e.1 ≠ f.2 ∧ e.2 ≠ f.1 ∧ e.2 ≠ f.2

Used by 2

Used byThe edges APPROX-VERTEX-COVER takes form a maximal matching of the listed pairs · Matching invariant of the vertex cover scan

TheoremMatching invariant of the vertex cover scan#✓fully proved

Let \(G\) be a simple graph, \(C_0\) a finite set of vertices, and \(L\) a list of ordered pairs of vertices such that \(u\) and \(v\) are adjacent in \(G\) for every \((u, v)\) in \(L\), and let \(C\) be the cover that the vertex cover scan returns on \(L\) starting from \(C_0\). Then there is a sublist \(A\) of \(L\) such that neither endpoint of any pair in \(A\) lies in \(C_0\), pairs at different positions of \(A\) are vertex-disjoint, a vertex lies in \(C\) exactly when it lies in \(C_0\) or is an endpoint of some pair in \(A\), and \(|C| = |C_0| + 2|A|\), where \(|A|\) is the length of \(A\).

theorem exists_matching_vertexCoverScan (G : SimpleGraph V) (cover : Finset V)
    (edges : List (V × V)) (hsound : ∀ e ∈ edges, G.Adj e.1 e.2) :
    ∃ A : List (V × V), A.Sublist edges ∧ (∀ e ∈ A, e.1 ∉ cover ∧ e.2 ∉ cover) ∧
      A.Pairwise VertexDisjoint ∧
      (∀ x, x ∈ (vertexCoverScan cover edges).ret ↔ x ∈ cover ∨ ∃ e ∈ A, x = e.1 ∨ x = e.2) ∧
      (vertexCoverScan cover edges).ret.card = cover.card + 2 * A.length

def VertexDisjoint (e f : V × V) : Prop :=
  e.1 ≠ f.1 ∧ e.1 ≠ f.2 ∧ e.2 ≠ f.1 ∧ e.2 ≠ f.2

CSLibExt/Algorithms/Lean/Approximation/VertexCover.lean:203

def vertexCoverScan (cover : Finset V) : List (V × V) → TimeM ℕ (Finset V)
  | [] => pure cover
  | (u, v) :: es => do
      ✓
      if u ∈ cover ∨ v ∈ cover then vertexCoverScan cover es
      else vertexCoverScan (insert u (insert v cover)) es

CSLibExt/Algorithms/Lean/Approximation/VertexCover.lean:53

Uses 2 · Used by 1

Statement usesVertex-disjoint pairs · Vertex cover scan

Used byThe edges APPROX-VERTEX-COVER takes form a maximal matching of the listed pairs

TheoremThe edges APPROX-VERTEX-COVER takes form a maximal matching of the listed pairs#✓fully proved

Let \(G\) be a simple graph and \(L\) a list of ordered pairs of vertices such that \(u\) and \(v\) are adjacent in \(G\) for every \((u, v)\) in \(L\), and let \(C\) be the cover that APPROX-VERTEX-COVER returns on \(L\). Then there is a sublist \(A\) of \(L\) such that pairs at different positions of \(A\) are vertex-disjoint, every pair in \(L\) shares an endpoint with some pair in \(A\), a vertex lies in \(C\) exactly when it is an endpoint of some pair in \(A\), and \(|C| = 2|A|\), where \(|A|\) is the length of \(A\).

theorem approxVertexCover_matching (G : SimpleGraph V) (edges : List (V × V))
    (hsound : ∀ e ∈ edges, G.Adj e.1 e.2) :
    ∃ A : List (V × V), A.Sublist edges ∧ A.Pairwise VertexDisjoint ∧
      (∀ e ∈ edges, ∃ f ∈ A, e.1 = f.1 ∨ e.1 = f.2 ∨ e.2 = f.1 ∨ e.2 = f.2) ∧
      (∀ x, x ∈ (approxVertexCover edges).ret ↔ ∃ e ∈ A, x = e.1 ∨ x = e.2) ∧
      (approxVertexCover edges).ret.card = 2 * A.length

def VertexDisjoint (e f : V × V) : Prop :=
  e.1 ≠ f.1 ∧ e.1 ≠ f.2 ∧ e.2 ≠ f.1 ∧ e.2 ≠ f.2

CSLibExt/Algorithms/Lean/Approximation/VertexCover.lean:203

def approxVertexCover (edges : List (V × V)) : TimeM ℕ (Finset V) :=
  vertexCoverScan ∅ edges

CSLibExt/Algorithms/Lean/Approximation/VertexCover.lean:61

Uses 5

Statement usesVertex-disjoint pairs · APPROX-VERTEX-COVER

Proof usesAPPROX-VERTEX-COVER covers every listed pair · Matching invariant of the vertex cover scan · Vertex cover scan

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.