Maximum-weight independent set and its encoding
Lax263307.WeightedIndependentSet · concepts/Lax263307/WeightedIndependentSet.lean · lax-263307
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
Given a graph with rational vertex weights , maximum-weight independent set asks for an independent set of maximum total weight. An -approximation is an independent set with for every independent set .
The input consists of the number of vertices, the adjacency matrix, the vertex weights, and the requested rational accuracy. The output is the membership vector of the returned independent set.
Concept map
Lean source view on GitHub
| 1 | import Mathlib.Combinatorics.SimpleGraph.Clique |
| 2 | import Mathlib.Data.Rat.Floor |
| 3 | import Lax759944.BinaryWordEncoding |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: Maximum-weight independent set and its encoding |
| 8 | type: definition |
| 9 | --- |
| 10 | Given a graph with rational vertex weights , maximum-weight |
| 11 | independent set asks for an independent set of maximum total weight. |
| 12 | An -approximation is an independent set with |
| 13 | for every independent set . |
| 14 | |
| 15 | The input consists of the number of vertices, the adjacency matrix, |
| 16 | the vertex weights, and the requested rational accuracy. The output |
| 17 | is the membership vector of the returned independent set. |
| 18 | |
| 19 | # Formalization notes |
| 20 | |
| 21 | The comparison with every independent set avoids choosing an optimum. |
| 22 | Weights may be negative: such vertices can be discarded, as can zero-weight |
| 23 | vertices, so this includes the nonnegative case used in Section 6. |
| 24 | Each rational is encoded by the sign of its reduced numerator, its absolute |
| 25 | numerator, and its positive denominator. The sign is zero for nonnegative |
| 26 | numbers and one for negative numbers. All matrix and vector entries are in |
| 27 | vertex order. The rational encoding length includes the weights and |
| 28 | , and is measured by the registered binary word encoding. |
| 29 | -/ |
| 30 | |
| 31 | namespace Lax263307.WeightedIndependentSet |
| 32 | |
| 33 | /-- Total weight of a vertex set. -/ |
| 34 | def weight {n : ℕ} (w : Fin n → ℚ) (I : Finset (Fin n)) : ℚ := |
| 35 | ∑ v ∈ I, w v |
| 36 | |
| 37 | /-- An independent set that achieves the requested multiplicative guarantee. -/ |
| 38 | def IsApproximation {n : ℕ} (G : SimpleGraph (Fin n)) (w : Fin n → ℚ) |
| 39 | (ε : ℚ) (I : Finset (Fin n)) : Prop := |
| 40 | G.IsIndepSet (I : Set (Fin n)) ∧ |
| 41 | ∀ J : Finset (Fin n), G.IsIndepSet (J : Set (Fin n)) → |
| 42 | (1 - ε) * weight w J ≤ weight w I |
| 43 | |
| 44 | /-- Canonical sign, absolute numerator, and denominator of a rational. -/ |
| 45 | def encodeRational (q : ℚ) : List ℕ := |
| 46 | [if q.num < 0 then 1 else 0, q.num.natAbs, q.den] |
| 47 | |
| 48 | /-- The rational parameters in vertex order, followed by the accuracy. -/ |
| 49 | def encodeParameters {n : ℕ} (w : Fin n → ℚ) (ε : ℚ) : List ℕ := |
| 50 | (List.ofFn w).flatMap encodeRational ++ encodeRational ε |
| 51 | |
| 52 | /-- Total binary encoding length of the weights and the accuracy. -/ |
| 53 | def rationalBitSize {n : ℕ} (w : Fin n → ℚ) (ε : ℚ) : ℕ := |
| 54 | Lax759944.BinaryWordEncoding.bitSize (encodeParameters w ε) |
| 55 | |
| 56 | /-- The full input word, including the row-major adjacency matrix. -/ |
| 57 | def encodeInput {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] |
| 58 | (w : Fin n → ℚ) (ε : ℚ) : List ℕ := |
| 59 | [n] ++ (List.ofFn fun u => List.ofFn fun v => |
| 60 | if G.Adj u v then 1 else 0).flatten ++ encodeParameters w ε |
| 61 | |
| 62 | /-- The length-`n` membership vector of the selected independent set. -/ |
| 63 | def encodeOutput {n : ℕ} (I : Finset (Fin n)) : List ℕ := |
| 64 | List.ofFn fun v => if v ∈ I then 1 else 0 |
| 65 | |
| 66 | end Lax263307.WeightedIndependentSet |
| 67 |
Formalization notes
The comparison with every independent set avoids choosing an optimum. Weights may be negative: such vertices can be discarded, as can zero-weight vertices, so this includes the nonnegative case used in Section 6. Each rational is encoded by the sign of its reduced numerator, its absolute numerator, and its positive denominator. The sign is zero for nonnegative numbers and one for negative numbers. All matrix and vector entries are in vertex order. The rational encoding length includes the weights and , and is measured by the registered binary word encoding.
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments