[NOTE] High performance graph encoding
Record the signature of high-performance graph encoding1:
1. Compact representation
structure Edge (β : Type) where target : Nat weight : β structure Vertex (α : Type) (β : Type) where payload : α adjacencyList : Array (Edge β) := #[] structure Graph (α : Type) (β : Type) where vertices : Array (Graph.Vertex α β) := #[]
This is a very smart definition, ignore weight and payload.
- A
Vertexstores a list of adjacencies edge Edgestores the index of vertex in the big arrayvertices
It brings a very compact, low-memory layout.
2. Appendix: Algebraic Graph
Following the concept Algebraic Graph2, one can add three functions for this implementation:
2.1. vertex
Create a graph with only one vertex
def vertex (v : Vertex α β) : Graph α β := ⟨#[v]⟩
2.2. overlay
overlay two graph, but since the indicies of vertices are changed, implementation must rewrite them
def overlay (g₁ g₂ : Graph α β) : Graph α β := {
-- must rewrite all g₂ edge target, it will be shifted by g₁.vertices.size
vertices :=
g₁.vertices
++ g₂.vertices.map
(λ v => { v with
adjacencyList := v.adjacencyList.map (λ e => { e with target := e.target + g₁.vertices.size })})
}
2.3. connect
connect g₁ to g₂, except overlay indicies problem, implementation should also consider the new adjacencies:
Every vertices in
g₁should have a new adjacencies to each vertices ing₂
def connectW (g₁ g₂ : Graph α β) (w : β) : Graph α β := {
vertices :=
let shift := g₁.vertices.size
let connects : Array (Edge β) :=
g₂.vertices.size
|> List.range
|> List.map (λ i => { target := i + shift, weight := w })
|> List.toArray
let m := g₁.vertices.map (λ v => { v with
adjacencyList := v.adjacencyList.append connects
})
m
++ g₂.vertices.map
(λ v => { v with
adjacencyList := v.adjacencyList.map (λ e => { e with target := e.target + g₁.vertices.size })})
}
def connect [Inhabited β] (g₁ g₂ : Graph α β) : Graph α β := connectW g₁ g₂ default
Since this implementation requires weight, but we not always care about it, so I provide both:
connectWfor customizedweightconnectfor the people who just want default value (requiresInhabited β)