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.

An ADD-based algorithm for shortest path back-tracing of large graphs / R. I., Bahar; G. D., Hachtel; Macii, Enrico; A., Pardo; Poncino, Massimo; F., Somenzi. - (1994), pp. 248-251. (Intervento presentato al convegno GLS-VLSI'94: 4th IEEE Great Lake Symposium on VLSI tenutosi a Notre Dame, IN (USA) nel 4-5 Mar 1994) [10.1109/GLSV.1994.289960].

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

#### Abstract

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.
##### Scheda breve Scheda completa Scheda completa (DC)
1994
0818656107
File in questo prodotto:
Non ci sono file associati a questo prodotto.
##### Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11583/1415626
##### Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo