findSCCs

Mathlib.Tactic.Order.Graph.Tarjan

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Order.Graph.findSCCs

Lean4

/-- 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. -/
def findSCCs (g : Graph) : Array Nat :=
  let s : TarjanState :=
    { visited := .replicate g.size false
      id := .replicate g.size 0
      lowlink := .replicate g.size 0
      stack := #[]
      onStack := .replicate g.size false
      time := 0 }
  (findSCCsImp g).run s |>.snd.lowlink

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru