Weighted vertex cover by the pricing method

DefinitionPricing scan#✓fully proved

Given rational residual weights \(r\) on the vertices, a rational total price \(P\) and a list of edges (ordered pairs of vertices), the pricing scan processes the edges in order: an edge \((u, v)\) has price \(\delta = \min(r(u), r(v))\), which is subtracted from the residual weight of \(u\) and of \(v\) (once if \(u = v\)) and added to the total price. The result is the final pair of residual weights and total price, and the scan costs one time unit per edge.

def pricingScan : (V → ℚ) → ℚ → List (V × V) → TimeM ℕ ((V → ℚ) × ℚ)
  | r, P, [] => pure (r, P)
  | r, P, (u, v) :: es => do
      ✓
      let δ := min (r u) (r v)
      pricingScan (fun x => if x = u ∨ x = v then r x - δ else r x) (P + δ) es

Used by 8

Used byPricing scan: the total price is at most what a cover pays · Pricing scan: every edge has an exhausted endpoint · Pricing scan: residual weights stay between \(0\) and their start · Pricing method for weighted vertex cover · The pricing method covers every listed edge · Running time of the pricing method · The pricing method weighs at most twice any cover of the listed edges · Pricing scan: the vertices pay at most twice the price

DefinitionPricing method for weighted vertex cover#✓fully proved

Given rational weights \(w\) on a finite vertex set \(V\) and a list of edges (ordered pairs of vertices), run the pricing scan on the list starting from residual weights \(w\) and total price \(0\), then return the set of vertices whose final residual weight is \(0\). On top of the cost of the scan, the selection costs \(|V|\) time units.

def pricingVertexCover [Fintype V] (w : V → ℚ) (edges : List (V × V)) : TimeM ℕ (Finset V) := do
  let res ← pricingScan w 0 edges
  ✓[Fintype.card V]
  pure (Finset.univ.filter fun v => res.1 v = 0)

Uses 1 · Used by 4

Statement usesPricing scan

Used byThe pricing method covers every listed edge · The pricing method returns a vertex cover · Running time of the pricing method · The pricing method weighs at most twice any cover of the listed edges

10 fully proved

The scan

TheoremPricing scan: residual weights stay between \(0\) and their start#✓fully proved

Let \(r\) be rational residual weights with \(r(v) \ge 0\) for every vertex \(v\), let \(P\) be a rational number and let \(L\) be a list of edges. If the pricing scan of \(L\) from residual weights \(r\) and total price \(P\) ends with residual weights \(r'\), then \(0 \le r'(v) \le r(v)\) for every vertex \(v\).

theorem pricingScan_residual : ∀ (es : List (V × V)) (r : V → ℚ) (P : ℚ), (∀ v, 0 ≤ r v) →
    ∀ v, 0 ≤ (pricingScan r P es).ret.1 v ∧ (pricingScan r P es).ret.1 v ≤ r v

Uses 1 · Used by 2

Statement usesPricing scan

Used byPricing scan: every edge has an exhausted endpoint · The pricing method weighs at most twice any cover of the listed edges

TheoremPricing scan: every edge has an exhausted endpoint#✓fully proved

Let \(r\) be rational residual weights with \(r(v) \ge 0\) for every vertex \(v\), let \(P\) be a rational number and let \(L\) be a list of edges (ordered pairs of vertices). If the pricing scan of \(L\) from residual weights \(r\) and total price \(P\) ends with residual weights \(r'\), then every pair \((u, v)\) in \(L\) has \(r'(u) = 0\) or \(r'(v) = 0\).

theorem pricingScan_covers : ∀ (es : List (V × V)) (r : V → ℚ) (P : ℚ), (∀ v, 0 ≤ r v) →
    ∀ e ∈ es, (pricingScan r P es).ret.1 e.1 = 0 ∨ (pricingScan r P es).ret.1 e.2 = 0

Uses 2 · Used by 1

Statement usesPricing scan

Proof usesPricing scan: residual weights stay between \(0\) and their start

Used byThe pricing method covers every listed edge

TheoremPricing scan: the vertices pay at most twice the price#✓fully proved

Let \(V\) be a finite vertex set, let \(r\) be rational residual weights with \(r(v) \ge 0\) for every vertex \(v\), let \(P\) be a rational number and let \(L\) be a list of edges. If the pricing scan of \(L\) from residual weights \(r\) and total price \(P\) ends with residual weights \(r'\) and total price \(P'\), then \(\sum_{v \in V} (r(v) - r'(v)) \le 2 (P' - P)\).

Each edge's price is paid by its two endpoints.

theorem sum_drop_le_two_mul_price [Fintype V] : ∀ (es : List (V × V)) (r : V → ℚ) (P : ℚ),
    (∀ v, 0 ≤ r v) →
    ∑ v, (r v - (pricingScan r P es).ret.1 v) ≤ 2 * ((pricingScan r P es).ret.2 - P)

Uses 1 · Used by 1

Statement usesPricing scan

Used byThe pricing method weighs at most twice any cover of the listed edges

TheoremPricing scan: the total price is at most what a cover pays#✓fully proved

Let \(C\) be a finite set of vertices, let \(r\) be rational residual weights with \(r(v) \ge 0\) for every vertex \(v\), let \(P\) be a rational number, and let \(L\) be a list of edges (ordered pairs of vertices) such that every pair \((u, v)\) in \(L\) has \(u \in C\) or \(v \in C\). If the pricing scan of \(L\) from residual weights \(r\) and total price \(P\) ends with residual weights \(r'\) and total price \(P'\), then \(P' - P \le \sum_{v \in C} (r(v) - r'(v))\).

Every edge has an endpoint in \(C\), which pays that edge's price.

theorem price_le_sum_drop (C : Finset V) : ∀ (es : List (V × V)) (r : V → ℚ) (P : ℚ),
    (∀ v, 0 ≤ r v) → (∀ e ∈ es, e.1 ∈ C ∨ e.2 ∈ C) →
    (pricingScan r P es).ret.2 - P ≤ ∑ v ∈ C, (r v - (pricingScan r P es).ret.1 v)

Uses 1 · Used by 1

Statement usesPricing scan

Used byThe pricing method weighs at most twice any cover of the listed edges

The pricing method

TheoremThe pricing method covers every listed edge#✓fully proved

Let \(w\) be rational weights on a finite vertex set with \(w(v) \ge 0\) for every vertex \(v\), and let \(L\) be a list of edges (ordered pairs of vertices). For every pair \((u, v)\) in \(L\), \(u\) or \(v\) belongs to the set returned by the pricing method on \(w\) and \(L\).

theorem pricingVertexCover_covers (w : V → ℚ) (hw : ∀ v, 0 ≤ w v) (edges : List (V × V)) :
    ∀ e ∈ edges,
      e.1 ∈ (pricingVertexCover w edges).ret ∨ e.2 ∈ (pricingVertexCover w edges).ret

Uses 3 · Used by 1

Statement usesPricing method for weighted vertex cover

Proof usesPricing scan · Pricing scan: every edge has an exhausted endpoint

Used byThe pricing method returns a vertex cover

TheoremThe pricing method returns a vertex cover#✓fully proved

Let \(G\) be a simple graph on a finite vertex set, let \(w\) be rational vertex weights with \(w(v) \ge 0\) for every vertex \(v\), and let \(L\) be a list of ordered pairs of vertices such that for every edge \(uv\) of \(G\), the pair \((u, v)\) or the pair \((v, u)\) is in \(L\). Then the set returned by the pricing method on \(w\) and \(L\) is a vertex cover of \(G\).

theorem pricingVertexCover_isVertexCover (G : SimpleGraph V) (w : V → ℚ) (hw : ∀ v, 0 ≤ w v)
    (edges : List (V × V)) (hG : ∀ u v, G.Adj u v → (u, v) ∈ edges ∨ (v, u) ∈ edges) :
    G.IsVertexCover ↑(pricingVertexCover w edges).ret

Uses 2

Statement usesPricing method for weighted vertex cover

Proof usesThe pricing method covers every listed edge

TheoremThe pricing method weighs at most twice any cover of the listed edges#✓fully proved

Let \(w\) be rational weights on a finite vertex set with \(w(v) \ge 0\) for every vertex \(v\), let \(L\) be a list of edges (ordered pairs of vertices), and let \(C\) be a set of vertices such that every pair \((u, v)\) in \(L\) has \(u \in C\) or \(v \in C\). Then the total weight of the set returned by the pricing method on \(w\) and \(L\) is at most \(2 \sum_{v \in C} w(v)\).

theorem pricingVertexCover_weight_le (w : V → ℚ) (hw : ∀ v, 0 ≤ w v) (edges : List (V × V))
    (C : Finset V) (hC : ∀ e ∈ edges, e.1 ∈ C ∨ e.2 ∈ C) :
    ∑ v ∈ (pricingVertexCover w edges).ret, w v ≤ 2 * ∑ v ∈ C, w v

Uses 5

Statement usesPricing method for weighted vertex cover

Proof usesPricing scan: the total price is at most what a cover pays · Pricing scan · Pricing scan: residual weights stay between \(0\) and their start · Pricing scan: the vertices pay at most twice the price

TheoremRunning time of the pricing method#✓fully proved

For all rational vertex weights \(w\) on a finite vertex set \(V\) and every list \(L\) of edges, the pricing method on \(w\) and \(L\) takes exactly \(|L| + |V|\) time units, where \(|L|\) is the length of the list: one unit per listed edge and one per vertex.

theorem pricingVertexCover_time (w : V → ℚ) (edges : List (V × V)) :
    (pricingVertexCover w edges).time = edges.length + Fintype.card V

Uses 2

Statement usesPricing method for weighted vertex cover

Proof usesPricing scan

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.