Tarjan's Algorithm

This file implements Tarjan's algorithm for finding the strongly connected components (SCCs) of a graph.

structure Mathlib.Tactic.Order.Graph.TarjanStateextends Mathlib.Tactic.Order.Graph.DFSState : Type

State for Tarjan's algorithm.

• visited : Std.HashSet ℕ
• id : Std.HashMap ℕ ℕ

  id[v] is the index of the vertex v in the DFS traversal.

• lowlink : Std.HashMap ℕ ℕ

  lowlink[v] is the smallest index of any node on the stack that is reachable from v through v's DFS subtree.

• stack : Array ℕ

  The stack of visited vertices used in Tarjan's algorithm.

• onStack : Std.HashSet ℕ

  onStack.contains v iff v is in stack. The structure is used to check it efficiently.

• time : ℕ

  A time counter that increments each time the algorithm visits an unvisited vertex.

partial def Mathlib.Tactic.Order.Graph.tarjanDFS (g : Graph) (v : ℕ) : StateM TarjanState Unit

The Tarjan's algorithm. See Wikipedia.

def Mathlib.Tactic.Order.Graph.findSCCsImp (g : Graph) : StateM TarjanState Unit

Implementation of findSCCs in the StateM TarjanState monad.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Order.Graph.findSCCs (g : Graph) : Std.HashMap ℕ ℕ

Finds the strongly connected components of the graph g. Returns a hashmap where the value at key v represents the SCC number containing vertex v. The numbering of SCCs is arbitrary.

Equations

• g.findSCCs = (StateT.run g.findSCCsImp { visited := ∅, id := ∅, lowlink := ∅, stack := #[], onStack := ∅, time := 0 }).snd.lowlink