An ADD-based algorithm for shortest path back-tracing of large graphs

Symbolic computation techniques play a fundamental role in logic synthesis and formal hardware verification algorithms. Recently, Algebraic Decision Diagrams, i.e., BDDs with a set of constant values different to the set {0,1}, have been used to solve general purpose problems, such as matrix multiplication, shortest path calculation, and solution of linear systems, as well as logic synthesis and formal verification problems, such as timing analysis, probabilistic analysis of finite state machines, and state space decomposition for approximate finite state machine traversal. ADD-based procedures for single-source and all-pairs shortest path weight calculation have appeared to be very effective for the manipulation of large graphs (over 1027 vertices and 1036 edges). However, for those procedures to be applicable to real problems, for example flow network problems, computing only shortest path weights is not enough; what it is needed is an algorithm that, given the weight of a shortest path between two vertices of a graph, actually determines the sequence of vertices belonging to the shortest path. This paper proposes a symbolic algorithm to execute shortest path back-tracing which exploits the compactness of the ADD data structure to handle large graphs.