1 /**CFile***********************************************************************
7 Synopsis [Symbolic shortest paths algorithms.]
9 Description [This file contains the functions that implement the
10 symbolic version of several shortest path algorithms described in the
13 Author [Fabio Somenzi, Iris Bahar]
15 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
19 Redistribution and use in source and binary forms, with or without
20 modification, are permitted provided that the following conditions
23 Redistributions of source code must retain the above copyright
24 notice, this list of conditions and the following disclaimer.
26 Redistributions in binary form must reproduce the above copyright
27 notice, this list of conditions and the following disclaimer in the
28 documentation and/or other materials provided with the distribution.
30 Neither the name of the University of Colorado nor the names of its
31 contributors may be used to endorse or promote products derived from
32 this software without specific prior written permission.
34 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
35 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
36 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
37 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
38 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
39 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
40 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
41 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
42 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
43 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
44 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
45 POSSIBILITY OF SUCH DAMAGE.]
47 ******************************************************************************/
52 /*---------------------------------------------------------------------------*/
53 /* Constant declarations */
54 /*---------------------------------------------------------------------------*/
56 /*---------------------------------------------------------------------------*/
57 /* Stucture declarations */
58 /*---------------------------------------------------------------------------*/
60 /*---------------------------------------------------------------------------*/
61 /* Type declarations */
62 /*---------------------------------------------------------------------------*/
64 /*---------------------------------------------------------------------------*/
65 /* Variable declarations */
66 /*---------------------------------------------------------------------------*/
69 static char rcsid
[] UTIL_UNUSED
= "$Id: ntrShort.c,v 1.4 2004/08/13 18:28:28 fabio Exp fabio $";
72 /*---------------------------------------------------------------------------*/
73 /* Macro declarations */
74 /*---------------------------------------------------------------------------*/
76 /**AutomaticStart*************************************************************/
78 /*---------------------------------------------------------------------------*/
79 /* Static function prototypes */
80 /*---------------------------------------------------------------------------*/
82 static DdNode
* ntrBellman (DdManager
*dd
, DdNode
*D
, DdNode
*source
, DdNode
**x
, DdNode
**y
, int vars
, int pr
);
83 static DdNode
* ntrWarshall (DdManager
*dd
, DdNode
*D
, DdNode
**x
, DdNode
**y
, int vars
, int pr
);
84 static DdNode
* ntrSquare (DdManager
*dd
, DdNode
*D
, DdNode
**x
, DdNode
**y
, DdNode
**z
, int vars
, int pr
, int st
);
86 /**AutomaticEnd***************************************************************/
88 /*---------------------------------------------------------------------------*/
89 /* Definition of exported functions */
90 /*---------------------------------------------------------------------------*/
92 /**Function********************************************************************
94 Synopsis [Computes shortest paths in a state graph.]
96 Description [Computes shortest paths in the state transition graph of
97 a network. Three methods are availabe:
99 <li> Bellman-Ford algorithm for single-source shortest paths; the
100 algorithm computes the distance (number of transitions) from the initial
101 states to all states.
102 <li> Floyd-Warshall algorithm for all-pair shortest paths.
103 <li> Repeated squaring algorithm for all-pair shortest paths.
105 The function returns 1 in case of success; 0 otherwise.
108 SideEffects [ADD variables are created in the manager.]
112 ******************************************************************************/
120 DdNode
*edges
, *source
, *res
, *r
, *q
, *bddSource
;
121 DdNode
**xadd
, **yadd
, **zadd
;
123 int pr
= option
->verb
;
124 int algorithm
= option
->shortPath
;
125 int selectiveTrace
= option
->selectiveTrace
;
126 int nvars
= net
->nlatches
;
128 /* Set background to infinity for shortest paths. */
129 Cudd_SetBackground(dd
,Cudd_ReadPlusInfinity(dd
));
131 /* Build the monolithic TR. */
132 TR
= Ntr_buildTR(dd
,net
,option
,NTR_IMAGE_MONO
);
134 /* Build the ADD variable vectors for x and y. */
135 xadd
= ALLOC(DdNode
*, nvars
);
136 yadd
= ALLOC(DdNode
*, nvars
);
137 for(i
= 0; i
< nvars
; i
++) {
138 q
= Cudd_addIthVar(dd
,TR
->x
[i
]->index
);
141 q
= Cudd_addIthVar(dd
,TR
->y
[i
]->index
);
146 /* Convert the transition relation BDD into an ADD... */
147 q
= Cudd_BddToAdd(dd
,TR
->part
[0]);
149 /* ...replacing zeroes with infinities... */
150 r
= Cudd_addIte(dd
,q
,Cudd_ReadOne(dd
),Cudd_ReadPlusInfinity(dd
));
152 Cudd_RecursiveDeref(dd
,q
);
153 /* ...and zeroing the diagonal. */
154 q
= Cudd_addXeqy(dd
,nvars
,xadd
,yadd
);
156 edges
= Cudd_addIte(dd
,q
,Cudd_ReadZero(dd
),r
);
158 Cudd_RecursiveDeref(dd
,r
);
159 Cudd_RecursiveDeref(dd
,q
);
162 case NTR_SHORT_BELLMAN
:
163 bddSource
= Ntr_initState(dd
,net
,option
);
164 source
= Cudd_BddToAdd(dd
,bddSource
);
166 res
= ntrBellman(dd
,edges
,source
,xadd
,yadd
,nvars
,pr
);
167 if (res
== NULL
) return(0);
169 Cudd_RecursiveDeref(dd
,source
);
170 Cudd_RecursiveDeref(dd
,bddSource
);
172 (void) fprintf(stdout
,"Distance Matrix");
173 Cudd_PrintDebug(dd
,res
,nvars
,pr
);
176 case NTR_SHORT_FLOYD
:
177 res
= ntrWarshall(dd
,edges
,xadd
,yadd
,nvars
,pr
);
178 if (res
== NULL
) return(0);
181 (void) fprintf(stdout
,"Distance Matrix");
182 Cudd_PrintDebug(dd
,res
,2*nvars
,pr
);
185 case NTR_SHORT_SQUARE
:
186 /* Create a third set of ADD variables. */
187 zadd
= ALLOC(DdNode
*, nvars
);
188 for(i
= 0; i
< nvars
; i
++) {
190 level
= Cudd_ReadIndex(dd
,TR
->x
[i
]->index
);
191 q
= Cudd_addNewVarAtLevel(dd
,level
);
195 /* Compute the shortest paths. */
196 res
= ntrSquare(dd
,edges
,zadd
,yadd
,xadd
,nvars
,pr
,selectiveTrace
);
197 if (res
== NULL
) return(0);
199 /* Dispose of the extra variables. */
200 for(i
= 0; i
< nvars
; i
++) {
201 Cudd_RecursiveDeref(dd
,zadd
[i
]);
205 (void) fprintf(stdout
,"Distance Matrix");
206 Cudd_PrintDebug(dd
,res
,2*nvars
,pr
);
210 (void) printf("Unrecognized method. Try again.\n");
214 /* Here we should compute the paths. */
218 Cudd_RecursiveDeref(dd
,edges
);
219 Cudd_RecursiveDeref(dd
,res
);
220 for(i
= 0; i
< nvars
; i
++) {
221 Cudd_RecursiveDeref(dd
,xadd
[i
]);
222 Cudd_RecursiveDeref(dd
,yadd
[i
]);
227 if (option
->autoDyn
& 1) {
228 (void) printf("Order after short path computation\n");
229 if (!Bnet_PrintOrder(net
,dd
)) return(0);
234 } /* end of Ntr_ShortestPaths */
237 /*---------------------------------------------------------------------------*/
238 /* Definition of internal functions */
239 /*---------------------------------------------------------------------------*/
241 /*---------------------------------------------------------------------------*/
242 /* Definition of static functions */
243 /*---------------------------------------------------------------------------*/
246 /**Function********************************************************************
248 Synopsis [Bellman-Ford algorithm for single-source shortest paths.]
250 Description [Bellman-Ford algorithm for single-source shortest
251 paths. Returns the vector of the distances of all states from the
252 initial states. In case of multiple initial states the distance for
253 each state is from the nearest initial state. Negative-weight
254 cycles are detected, though only in the naive way. (Lack of
255 convergence after nodes-1 iterations.) In such a case, a constant
256 ADD with value minus infinity is returned. Bellman-Ford is based on
257 matrix-vector multiplication. The matrix is the distance matrix
258 D(x,y), such that D(a,b) is the length of the arc connecting state a
259 to state b. The vector V(x) stores the distances of all states from
260 the initial states. The actual vector used in the matrix-vector
261 multiplication is diff(x), that holds those distances that have
262 changed during the last update.]
266 SeeAlso [ntrWarshall ntrSquare]
268 ******************************************************************************/
279 DdNode
*u
, *w
, *V
, *min
, *diff
;
280 DdApaNumber i
, nodes
, one
;
281 int digits
= vars
+ 1;
283 /* To avoid overflow when there are many variables, use APA. */
284 nodes
= Cudd_NewApaNumber(digits
);
285 Cudd_ApaPowerOfTwo(digits
,nodes
,vars
);
286 i
= Cudd_NewApaNumber(digits
);
287 one
= Cudd_NewApaNumber(digits
);
288 Cudd_ApaSetToLiteral(digits
,one
,1);
291 /* Find the distances from the initial state along paths using one
293 w
= Cudd_Cofactor(dd
,D
,source
); /* works only if source is a cube */
295 V
= Cudd_addSwapVariables(dd
,w
,x
,y
,vars
);
297 Cudd_RecursiveDeref(dd
,w
);
300 /* The initial states are at distance 0. The other states are
301 ** initially at infinite distance. */
302 V
= Cudd_addIte(dd
,source
,Cudd_ReadZero(dd
),Cudd_ReadPlusInfinity(dd
));
305 /* Selective trace algorithm. For the next update, only consider the
306 ** nodes whose distance has changed in the last update. */
310 for (Cudd_ApaSetToLiteral(digits
,i
,1);
311 Cudd_ApaCompare(digits
,i
,digits
,nodes
) < 0;
312 Cudd_ApaAdd(digits
,i
,one
,i
)) {
313 if (pr
>2) {(void) printf("V"); Cudd_PrintDebug(dd
,V
,vars
,pr
);}
314 /* Compute the distances via triangulation as a function of x. */
315 w
= Cudd_addTriangle(dd
,diff
,D
,x
,vars
);
317 Cudd_RecursiveDeref(dd
,diff
);
318 u
= Cudd_addSwapVariables(dd
,w
,x
,y
,vars
);
320 Cudd_RecursiveDeref(dd
,w
);
321 if (pr
>2) {(void) printf("u"); Cudd_PrintDebug(dd
,u
,vars
,pr
);}
323 /* Take the minimum of the previous distances and those just
325 min
= Cudd_addApply(dd
,Cudd_addMinimum
,V
,u
);
327 Cudd_RecursiveDeref(dd
,u
);
328 if (pr
>2) {(void) printf("min"); Cudd_PrintDebug(dd
,min
,vars
,pr
);}
330 if (V
== min
) { /* convergence */
331 Cudd_RecursiveDeref(dd
,min
);
333 (void) printf("Terminating after ");
334 Cudd_ApaPrintDecimal(stdout
,digits
,i
);
335 (void) printf(" iterations\n");
339 /* Find the distances that decreased. */
340 diff
= Cudd_addApply(dd
,Cudd_addDiff
,V
,min
);
342 if (pr
>2) {(void) printf("diff"); Cudd_PrintDebug(dd
,diff
,vars
,pr
);}
343 Cudd_RecursiveDeref(dd
,V
);
346 /* Negative cycle detection. */
347 if (Cudd_ApaCompare(digits
,i
,digits
,nodes
) == 0 &&
348 diff
!= Cudd_ReadPlusInfinity(dd
)) {
349 (void) printf("Negative cycle\n");
350 Cudd_RecursiveDeref(dd
,diff
);
351 Cudd_RecursiveDeref(dd
,V
);
352 V
= Cudd_ReadMinusInfinity(dd
);
362 } /* end of ntrBellman */
365 /**Function********************************************************************
367 Synopsis [Floyd-Warshall algorithm for all-pair shortest paths.]
375 ******************************************************************************/
386 DdNode
*xminterm
, *w
, *V
, *V2
;
399 Cudd_Ref(R
= D
); /* make copy of original matrix */
401 /* Extract pivot row and column from D */
402 start_time
= util_cpu_time();
403 for (k
= 0; k
< nodes
; k
++) {
404 if (k
% 10000 == 0) {
405 (void) printf("Starting iteration %d at time %s\n",
406 k
,util_print_time(util_cpu_time() - start_time
));
408 Cudd_Ref(xminterm
= one
);
410 for (i
= vars
-1; i
>= 0; i
--) {
412 Cudd_Ref(w
= Cudd_addIte(dd
,x
[i
],xminterm
,zero
));
414 Cudd_Ref(w
= Cudd_addIte(dd
,x
[i
],zero
,xminterm
));
416 Cudd_RecursiveDeref(dd
,xminterm
);
421 Cudd_Ref(V
= Cudd_Cofactor(dd
,R
,xminterm
));
422 Cudd_RecursiveDeref(dd
,xminterm
);
423 if (pr
>2) {(void) printf("V"); Cudd_PrintDebug(dd
,V
,vars
,pr
);}
426 Cudd_Ref(xminterm
= one
);
428 for (i
= vars
-1; i
>= 0; i
--) {
430 Cudd_Ref(w
= Cudd_addIte(dd
,y
[i
],xminterm
,zero
));
432 Cudd_Ref(w
= Cudd_addIte(dd
,y
[i
],zero
,xminterm
));
434 Cudd_RecursiveDeref(dd
,xminterm
);
439 Cudd_Ref(V2
= Cudd_Cofactor(dd
,R
,xminterm
));
440 Cudd_RecursiveDeref(dd
,xminterm
);
441 if (pr
>2) {(void) printf("V2"); Cudd_PrintDebug(dd
,V2
,vars
,pr
);}
443 Cudd_Ref(P
= Cudd_addOuterSum(dd
,R
,V
,V2
));
445 Cudd_RecursiveDeref(dd
,V
);
446 Cudd_RecursiveDeref(dd
,V2
);
447 Cudd_RecursiveDeref(dd
,R
);
449 if (pr
>2) {(void) printf("R"); Cudd_PrintDebug(dd
,R
,vars
,pr
);}
455 } /* end of ntrWarshall */
458 /**Function********************************************************************
460 Synopsis [Repeated squaring algorithm for all-pairs shortest paths.]
468 ******************************************************************************/
471 DdManager
*dd
/* manager */,
472 DdNode
*D
/* D(z,y): distance matrix */,
473 DdNode
**x
/* array of x variables */,
474 DdNode
**y
/* array of y variables */,
475 DdNode
**z
/* array of z variables */,
476 int vars
/* number of variables in each of the three arrays */,
477 int pr
/* verbosity level */,
478 int st
/* use the selective trace algorithm */)
481 DdNode
*I
; /* identity matirix */
482 DdNode
*w
, *V
, *P
, *M
, *R
, *RT
;
483 DdNode
*diff
, *min
, *minDiag
;
488 zero
= Cudd_ReadZero(dd
);
489 /* Make a working copy of the original matrix. */
492 I
= Cudd_addXeqy(dd
,vars
,z
,y
); /* identity matrix */
495 /* Make a copy of the matrix for the selective trace algorithm. */
499 start_time
= util_cpu_time();
500 for (n
= vars
; n
>= 0; n
--) {
501 printf("Starting iteration %d at time %s\n",vars
-n
,
502 util_print_time(util_cpu_time() - start_time
));
504 /* Check for negative cycles: They are identified by negative
505 ** elements on the diagonal.
508 /* Extract values from the diagonal. */
509 Cudd_Ref(w
= Cudd_addIte(dd
,I
,R
,zero
));
510 minDiag
= Cudd_addFindMin(dd
,w
); /* no need to ref */
511 neg
= Cudd_V(minDiag
) < 0;
512 Cudd_RecursiveDeref(dd
,w
);
514 Cudd_RecursiveDeref(dd
,diff
);
515 (void) printf("Negative cycle after %d iterations!\n",vars
-n
);
519 /* Prepare the first operand of matrix multiplication:
520 ** diff(z,y) -> RT(x,y) -> V(x,z)
524 Cudd_Ref(RT
= Cudd_addSwapVariables(dd
,diff
,x
,z
,vars
));
525 Cudd_RecursiveDeref(dd
,diff
);
527 Cudd_Ref(V
= Cudd_addSwapVariables(dd
,RT
,y
,z
,vars
));
528 Cudd_RecursiveDeref(dd
,RT
);
531 (void) printf("V"); Cudd_PrintDebug(dd
,V
,2*vars
,pr
);
532 pathcount
= Cudd_CountPath(V
);
533 (void) printf("Path count = %g\n", pathcount
);
536 /* V(x,z) * R(z,y) -> P(x,y) */
537 Cudd_Ref(P
= Cudd_addTriangle(dd
,V
,R
,z
,vars
));
538 Cudd_RecursiveDeref(dd
,V
);
539 /* P(x,y) => M(z,y) */
540 Cudd_Ref(M
= Cudd_addSwapVariables(dd
,P
,x
,z
,vars
));
541 Cudd_RecursiveDeref(dd
,P
);
542 if (pr
>0) {(void) printf("M"); Cudd_PrintDebug(dd
,M
,2*vars
,pr
);}
545 Cudd_Ref(min
= Cudd_addApply(dd
,Cudd_addMinimum
,R
,M
));
546 Cudd_RecursiveDeref(dd
,M
);
549 Cudd_RecursiveDeref(dd
,min
);
550 if (pr
>0) {printf("Done after %d iterations\n",vars
-n
+1); }
555 Cudd_Ref(diff
= Cudd_addApply(dd
,Cudd_addDiff
,min
,R
));
557 Cudd_Ref(diff
= min
);
559 Cudd_RecursiveDeref(dd
,R
);
560 R
= min
; /* keep a copy of matrix at current iter. */
563 (void) printf("R"); Cudd_PrintDebug(dd
,R
,2*vars
,pr
);
564 pathcount
= Cudd_CountPath(R
);
565 (void) printf("Path count = %g\n", pathcount
);
569 (void) printf("Negative cycle!\n");
574 Cudd_RecursiveDeref(dd
,I
);
578 } /* end of ntrSquare */