Computing strongly connected components in a linear number of symbolic steps

Abstract

We present an algorithm that computes in a linear number of symbolic steps (O(vVv)) the strongly connected components (sccs) of a graph G = 〈V, E〉 represented by an Ordered Binary Decision Diagram (OBDD). This result matches the complexity of the (celebrated) Tarjan's algorithm operating on explicit data structures. To date, the best algorithm for the above problem works in Θ(vVvlogvVv) symbolic steps ([BGS00]).