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 : Array Bool
• id : Array ℕ

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

• lowlink : Array ℕ

  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 : Array Bool

  onStack[v] = true 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) : Array ℕ

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

Equations

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