1 /**
2 @file
3
4 @ingroup cudd
5
6 @brief Reordering of DDs based on simulated annealing
7
8 @author Jae-Young Jang, Jorgen Sivesind
9
10 @copyright@parblock
11 Copyright (c) 1995-2015, Regents of the University of Colorado
12
13 All rights reserved.
14
15 Redistribution and use in source and binary forms, with or without
16 modification, are permitted provided that the following conditions
17 are met:
18
19 Redistributions of source code must retain the above copyright
20 notice, this list of conditions and the following disclaimer.
21
22 Redistributions in binary form must reproduce the above copyright
23 notice, this list of conditions and the following disclaimer in the
24 documentation and/or other materials provided with the distribution.
25
26 Neither the name of the University of Colorado nor the names of its
27 contributors may be used to endorse or promote products derived from
28 this software without specific prior written permission.
29
30 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
31 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
32 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
33 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
34 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
35 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
36 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
37 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
38 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
39 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
40 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
41 POSSIBILITY OF SUCH DAMAGE.
42 @endparblock
43
44 */
45
46 #include "util.h"
47 #include "cuddInt.h"
48
49 /*---------------------------------------------------------------------------*/
50 /* Constant declarations */
51 /*---------------------------------------------------------------------------*/
52
53 /* Annealing parameters */
54 #define BETA 0.6
55 #define ALPHA 0.90
56 #define EXC_PROB 0.4
57 #define JUMP_UP_PROB 0.36
58 #define MAXGEN_RATIO 15.0
59 #define STOP_TEMP 1.0
60
61 /*---------------------------------------------------------------------------*/
62 /* Stucture declarations */
63 /*---------------------------------------------------------------------------*/
64
65 /*---------------------------------------------------------------------------*/
66 /* Type declarations */
67 /*---------------------------------------------------------------------------*/
68
69 /*---------------------------------------------------------------------------*/
70 /* Variable declarations */
71 /*---------------------------------------------------------------------------*/
72
73 /*---------------------------------------------------------------------------*/
74 /* Macro declarations */
75 /*---------------------------------------------------------------------------*/
76
77 /** \cond */
78
79 /*---------------------------------------------------------------------------*/
80 /* Static function prototypes */
81 /*---------------------------------------------------------------------------*/
82
83 static int stopping_criterion (int c1, int c2, int c3, int c4, double temp);
84 static double random_generator (DdManager *dd);
85 static int ddExchange (DdManager *table, int x, int y, double temp);
86 static int ddJumpingAux (DdManager *table, int x, int x_low, int x_high, double temp);
87 static Move * ddJumpingUp (DdManager *table, int x, int x_low, int initial_size);
88 static Move * ddJumpingDown (DdManager *table, int x, int x_high, int initial_size);
89 static int siftBackwardProb (DdManager *table, Move *moves, int size, double temp);
90 static void copyOrder (DdManager *table, int *array, int lower, int upper);
91 static int restoreOrder (DdManager *table, int *array, int lower, int upper);
92
93 /** \endcond */
94
95 /*---------------------------------------------------------------------------*/
96 /* Definition of exported functions */
97 /*---------------------------------------------------------------------------*/
98
99 /*---------------------------------------------------------------------------*/
100 /* Definition of internal functions */
101 /*---------------------------------------------------------------------------*/
102
103
104 /**
105 @brief Get new variable-order by simulated annealing algorithm.
106
107 @details Get x, y by random selection. Choose either
108 exchange or jump randomly. In case of jump, choose between jump_up
109 and jump_down randomly. Do exchange or jump and get optimal case.
110 Loop until there is no improvement or temperature reaches
111 minimum.
112
113 @return 1 in case of success; 0 otherwise.
114
115 @sideeffect None
116
117 */
118 int
cuddAnnealing(DdManager * table,int lower,int upper)119 cuddAnnealing(
120 DdManager * table,
121 int lower,
122 int upper)
123 {
124 int nvars;
125 int size;
126 int x,y;
127 int result;
128 int c1, c2, c3, c4;
129 int BestCost;
130 int *BestOrder;
131 double NewTemp, temp;
132 double rand1;
133 int innerloop, maxGen;
134 int ecount, ucount, dcount;
135
136 nvars = upper - lower + 1;
137
138 result = cuddSifting(table,lower,upper);
139 #ifdef DD_STATS
140 (void) fprintf(table->out,"\n");
141 #endif
142 if (result == 0) return(0);
143
144 size = (int) (table->keys - table->isolated);
145
146 /* Keep track of the best order. */
147 BestCost = size;
148 BestOrder = ALLOC(int,nvars);
149 if (BestOrder == NULL) {
150 table->errorCode = CUDD_MEMORY_OUT;
151 return(0);
152 }
153 copyOrder(table,BestOrder,lower,upper);
154
155 temp = BETA * size;
156 maxGen = (int) (MAXGEN_RATIO * nvars);
157
158 c1 = size + 10;
159 c2 = c1 + 10;
160 c3 = size;
161 c4 = c2 + 10;
162 ecount = ucount = dcount = 0;
163
164 while (!stopping_criterion(c1, c2, c3, c4, temp)) {
165 #ifdef DD_STATS
166 (void) fprintf(table->out,"temp=%f\tsize=%d\tgen=%d\t",
167 temp,size,maxGen);
168 table->tosses = table->acceptances = 0;
169 #endif
170 for (innerloop = 0; innerloop < maxGen; innerloop++) {
171 /* Choose x, y randomly. */
172 x = (int) Cudd_Random(table) % nvars;
173 do {
174 y = (int) Cudd_Random(table) % nvars;
175 } while (x == y);
176 x += lower;
177 y += lower;
178 if (x > y) {
179 int tmp = x;
180 x = y;
181 y = tmp;
182 }
183
184 /* Choose move with roulette wheel. */
185 rand1 = random_generator(table);
186 if (rand1 < EXC_PROB) {
187 result = ddExchange(table,x,y,temp); /* exchange */
188 ecount++;
189 #if 0
190 (void) fprintf(table->out,
191 "Exchange of %d and %d: size = %d\n",
192 x,y,table->keys - table->isolated);
193 #endif
194 } else if (rand1 < EXC_PROB + JUMP_UP_PROB) {
195 result = ddJumpingAux(table,y,x,y,temp); /* jumping_up */
196 ucount++;
197 #if 0
198 (void) fprintf(table->out,
199 "Jump up of %d to %d: size = %d\n",
200 y,x,table->keys - table->isolated);
201 #endif
202 } else {
203 result = ddJumpingAux(table,x,x,y,temp); /* jumping_down */
204 dcount++;
205 #if 0
206 (void) fprintf(table->out,
207 "Jump down of %d to %d: size = %d\n",
208 x,y,table->keys - table->isolated);
209 #endif
210 }
211
212 if (!result) {
213 FREE(BestOrder);
214 return(0);
215 }
216
217 size = (int) (table->keys - table->isolated); /* keep current size */
218 if (size < BestCost) { /* update best order */
219 BestCost = size;
220 copyOrder(table,BestOrder,lower,upper);
221 }
222 }
223 c1 = c2;
224 c2 = c3;
225 c3 = c4;
226 c4 = size;
227 NewTemp = ALPHA * temp;
228 if (NewTemp >= 1.0) {
229 maxGen = (int)(log(NewTemp) / log(temp) * maxGen);
230 }
231 temp = NewTemp; /* control variable */
232 #ifdef DD_STATS
233 (void) fprintf(table->out,"uphill = %d\taccepted = %d\n",
234 table->tosses,table->acceptances);
235 fflush(table->out);
236 #endif
237 }
238
239 result = restoreOrder(table,BestOrder,lower,upper);
240 FREE(BestOrder);
241 if (!result) return(0);
242 #ifdef DD_STATS
243 fprintf(table->out,"#:N_EXCHANGE %8d : total exchanges\n",ecount);
244 fprintf(table->out,"#:N_JUMPUP %8d : total jumps up\n",ucount);
245 fprintf(table->out,"#:N_JUMPDOWN %8d : total jumps down",dcount);
246 #endif
247 return(1);
248
249 } /* end of cuddAnnealing */
250
251
252 /*---------------------------------------------------------------------------*/
253 /* Definition of static functions */
254 /*---------------------------------------------------------------------------*/
255
256 /**
257 @brief Checks termination condition.
258
259 @details If temperature is STOP_TEMP or there is no improvement
260 then terminates.
261
262 @return 1 if the termination criterion is met; 0 otherwise.
263
264 @sideeffect None
265
266 */
267 static int
stopping_criterion(int c1,int c2,int c3,int c4,double temp)268 stopping_criterion(
269 int c1,
270 int c2,
271 int c3,
272 int c4,
273 double temp)
274 {
275 if (STOP_TEMP < temp) {
276 return(0);
277 } else if ((c1 == c2) && (c1 == c3) && (c1 == c4)) {
278 return(1);
279 } else {
280 return(0);
281 }
282
283 } /* end of stopping_criterion */
284
285
286 /**
287 @brief Random number generator.
288
289 @return a double precision value between 0.0 and 1.0.
290
291 @sideeffect None
292
293 */
294 static double
random_generator(DdManager * dd)295 random_generator(DdManager * dd)
296 {
297 return((double)(Cudd_Random(dd) / 2147483561.0));
298
299 } /* end of random_generator */
300
301
302 /**
303 @brief Exchanges two variables, x and y.
304
305 @details This is the same funcion as ddSwapping except for the
306 comparison expression. Use probability function, exp(-size_change/temp).
307
308 @sideeffect None
309
310 */
311 static int
ddExchange(DdManager * table,int x,int y,double temp)312 ddExchange(
313 DdManager * table,
314 int x,
315 int y,
316 double temp)
317 {
318 Move *move,*moves;
319 int tmp;
320 int x_ref,y_ref;
321 int x_next,y_next;
322 int size, result;
323 int initial_size, limit_size;
324
325 x_ref = x;
326 y_ref = y;
327
328 x_next = cuddNextHigh(table,x);
329 y_next = cuddNextLow(table,y);
330 moves = NULL;
331 initial_size = limit_size = (int) (table->keys - table->isolated);
332
333 for (;;) {
334 if (x_next == y_next) {
335 size = cuddSwapInPlace(table,x,x_next);
336 if (size == 0) goto ddExchangeOutOfMem;
337 move = (Move *)cuddDynamicAllocNode(table);
338 if (move == NULL) goto ddExchangeOutOfMem;
339 move->x = x;
340 move->y = x_next;
341 move->size = size;
342 move->next = moves;
343 moves = move;
344 size = cuddSwapInPlace(table,y_next,y);
345 if (size == 0) goto ddExchangeOutOfMem;
346 move = (Move *)cuddDynamicAllocNode(table);
347 if (move == NULL) goto ddExchangeOutOfMem;
348 move->x = y_next;
349 move->y = y;
350 move->size = size;
351 move->next = moves;
352 moves = move;
353 size = cuddSwapInPlace(table,x,x_next);
354 if (size == 0) goto ddExchangeOutOfMem;
355 move = (Move *)cuddDynamicAllocNode(table);
356 if (move == NULL) goto ddExchangeOutOfMem;
357 move->x = x;
358 move->y = x_next;
359 move->size = size;
360 move->next = moves;
361 moves = move;
362
363 tmp = x;
364 x = y;
365 y = tmp;
366 } else if (x == y_next) {
367 size = cuddSwapInPlace(table,x,x_next);
368 if (size == 0) goto ddExchangeOutOfMem;
369 move = (Move *)cuddDynamicAllocNode(table);
370 if (move == NULL) goto ddExchangeOutOfMem;
371 move->x = x;
372 move->y = x_next;
373 move->size = size;
374 move->next = moves;
375 moves = move;
376 tmp = x;
377 x = y;
378 y = tmp;
379 } else {
380 size = cuddSwapInPlace(table,x,x_next);
381 if (size == 0) goto ddExchangeOutOfMem;
382 move = (Move *)cuddDynamicAllocNode(table);
383 if (move == NULL) goto ddExchangeOutOfMem;
384 move->x = x;
385 move->y = x_next;
386 move->size = size;
387 move->next = moves;
388 moves = move;
389 size = cuddSwapInPlace(table,y_next,y);
390 if (size == 0) goto ddExchangeOutOfMem;
391 move = (Move *)cuddDynamicAllocNode(table);
392 if (move == NULL) goto ddExchangeOutOfMem;
393 move->x = y_next;
394 move->y = y;
395 move->size = size;
396 move->next = moves;
397 moves = move;
398 x = x_next;
399 y = y_next;
400 }
401
402 x_next = cuddNextHigh(table,x);
403 y_next = cuddNextLow(table,y);
404 if (x_next > y_ref) break;
405
406 if ((double) size > DD_MAX_REORDER_GROWTH * (double) limit_size) {
407 break;
408 } else if (size < limit_size) {
409 limit_size = size;
410 }
411 }
412
413 if (y_next>=x_ref) {
414 size = cuddSwapInPlace(table,y_next,y);
415 if (size == 0) goto ddExchangeOutOfMem;
416 move = (Move *)cuddDynamicAllocNode(table);
417 if (move == NULL) goto ddExchangeOutOfMem;
418 move->x = y_next;
419 move->y = y;
420 move->size = size;
421 move->next = moves;
422 moves = move;
423 }
424
425 /* move backward and stop at best position or accept uphill move */
426 result = siftBackwardProb(table,moves,initial_size,temp);
427 if (!result) goto ddExchangeOutOfMem;
428
429 while (moves != NULL) {
430 move = moves->next;
431 cuddDeallocMove(table, moves);
432 moves = move;
433 }
434 return(1);
435
436 ddExchangeOutOfMem:
437 while (moves != NULL) {
438 move = moves->next;
439 cuddDeallocMove(table, moves);
440 moves = move;
441 }
442 return(0);
443
444 } /* end of ddExchange */
445
446
447 /**
448 @brief Moves a variable to a specified position.
449
450 @details If x==x_low, it executes jumping_down. If x==x_high, it
451 executes jumping_up. This funcion is similar to ddSiftingAux.
452
453 @return 1 in case of success; 0 otherwise.
454
455 @sideeffect None
456
457 */
458 static int
ddJumpingAux(DdManager * table,int x,int x_low,int x_high,double temp)459 ddJumpingAux(
460 DdManager * table,
461 int x,
462 int x_low,
463 int x_high,
464 double temp)
465 {
466 Move *move;
467 Move *moves; /* list of moves */
468 int initial_size;
469 int result;
470
471 initial_size = (int) (table->keys - table->isolated);
472
473 #ifdef DD_DEBUG
474 assert(table->subtables[x].keys > 0);
475 #endif
476
477 moves = NULL;
478
479 if (cuddNextLow(table,x) < x_low) {
480 if (cuddNextHigh(table,x) > x_high) return(1);
481 moves = ddJumpingDown(table,x,x_high,initial_size);
482 /* after that point x --> x_high unless early termination */
483 if (moves == NULL) goto ddJumpingAuxOutOfMem;
484 /* move backward and stop at best position or accept uphill move */
485 result = siftBackwardProb(table,moves,initial_size,temp);
486 if (!result) goto ddJumpingAuxOutOfMem;
487 } else if (cuddNextHigh(table,x) > x_high) {
488 moves = ddJumpingUp(table,x,x_low,initial_size);
489 /* after that point x --> x_low unless early termination */
490 if (moves == NULL) goto ddJumpingAuxOutOfMem;
491 /* move backward and stop at best position or accept uphill move */
492 result = siftBackwardProb(table,moves,initial_size,temp);
493 if (!result) goto ddJumpingAuxOutOfMem;
494 } else {
495 (void) fprintf(table->err,"Unexpected condition in ddJumping\n");
496 goto ddJumpingAuxOutOfMem;
497 }
498 while (moves != NULL) {
499 move = moves->next;
500 cuddDeallocMove(table, moves);
501 moves = move;
502 }
503 return(1);
504
505 ddJumpingAuxOutOfMem:
506 while (moves != NULL) {
507 move = moves->next;
508 cuddDeallocMove(table, moves);
509 moves = move;
510 }
511 return(0);
512
513 } /* end of ddJumpingAux */
514
515
516 /**
517 @brief This function is for jumping up.
518
519 @details This is a simplified version of ddSiftingUp. It does not
520 use lower bounding.
521
522 @return the set of moves in case of success; NULL if memory is full.
523
524 @sideeffect None
525
526 */
527 static Move *
ddJumpingUp(DdManager * table,int x,int x_low,int initial_size)528 ddJumpingUp(
529 DdManager * table,
530 int x,
531 int x_low,
532 int initial_size)
533 {
534 Move *moves;
535 Move *move;
536 int y;
537 int size;
538 int limit_size = initial_size;
539
540 moves = NULL;
541 y = cuddNextLow(table,x);
542 while (y >= x_low) {
543 size = cuddSwapInPlace(table,y,x);
544 if (size == 0) goto ddJumpingUpOutOfMem;
545 move = (Move *)cuddDynamicAllocNode(table);
546 if (move == NULL) goto ddJumpingUpOutOfMem;
547 move->x = y;
548 move->y = x;
549 move->size = size;
550 move->next = moves;
551 moves = move;
552 if ((double) size > table->maxGrowth * (double) limit_size) {
553 break;
554 } else if (size < limit_size) {
555 limit_size = size;
556 }
557 x = y;
558 y = cuddNextLow(table,x);
559 }
560 return(moves);
561
562 ddJumpingUpOutOfMem:
563 while (moves != NULL) {
564 move = moves->next;
565 cuddDeallocMove(table, moves);
566 moves = move;
567 }
568 return(NULL);
569
570 } /* end of ddJumpingUp */
571
572
573 /**
574 @brief This function is for jumping down.
575
576 @details This is a simplified version of ddSiftingDown. It does not
577 use lower bounding.
578
579 @return the set of moves in case of success; NULL if memory is full.
580
581 @sideeffect None
582
583 */
584 static Move *
ddJumpingDown(DdManager * table,int x,int x_high,int initial_size)585 ddJumpingDown(
586 DdManager * table,
587 int x,
588 int x_high,
589 int initial_size)
590 {
591 Move *moves;
592 Move *move;
593 int y;
594 int size;
595 int limit_size = initial_size;
596
597 moves = NULL;
598 y = cuddNextHigh(table,x);
599 while (y <= x_high) {
600 size = cuddSwapInPlace(table,x,y);
601 if (size == 0) goto ddJumpingDownOutOfMem;
602 move = (Move *)cuddDynamicAllocNode(table);
603 if (move == NULL) goto ddJumpingDownOutOfMem;
604 move->x = x;
605 move->y = y;
606 move->size = size;
607 move->next = moves;
608 moves = move;
609 if ((double) size > table->maxGrowth * (double) limit_size) {
610 break;
611 } else if (size < limit_size) {
612 limit_size = size;
613 }
614 x = y;
615 y = cuddNextHigh(table,x);
616 }
617 return(moves);
618
619 ddJumpingDownOutOfMem:
620 while (moves != NULL) {
621 move = moves->next;
622 cuddDeallocMove(table, moves);
623 moves = move;
624 }
625 return(NULL);
626
627 } /* end of ddJumpingDown */
628
629
630 /**
631 @brief Returns the %DD to the best position encountered during
632 sifting if there was improvement.
633
634 @details Otherwise, "tosses a coin" to decide whether to keep
635 the current configuration or return the %DD to the original
636 one.
637
638 @return 1 in case of success; 0 otherwise.
639
640 @sideeffect None
641
642 */
643 static int
siftBackwardProb(DdManager * table,Move * moves,int size,double temp)644 siftBackwardProb(
645 DdManager * table,
646 Move * moves,
647 int size,
648 double temp)
649 {
650 Move *move;
651 int res;
652 int best_size = size;
653 double coin, threshold;
654
655 /* Look for best size during the last sifting */
656 for (move = moves; move != NULL; move = move->next) {
657 if (move->size < best_size) {
658 best_size = move->size;
659 }
660 }
661
662 /* If best_size equals size, the last sifting did not produce any
663 ** improvement. We now toss a coin to decide whether to retain
664 ** this change or not.
665 */
666 if (best_size == size) {
667 coin = random_generator(table);
668 #ifdef DD_STATS
669 table->tosses++;
670 #endif
671 threshold = exp(-((double)(table->keys - table->isolated -
672 (unsigned int) size))/temp);
673 if (coin < threshold) {
674 #ifdef DD_STATS
675 table->acceptances++;
676 #endif
677 return(1);
678 }
679 }
680
681 /* Either there was improvement, or we have decided not to
682 ** accept the uphill move. Go to best position.
683 */
684 res = (int) (table->keys - table->isolated);
685 for (move = moves; move != NULL; move = move->next) {
686 if (res == best_size) return(1);
687 res = cuddSwapInPlace(table,(int)move->x,(int)move->y);
688 if (!res) return(0);
689 }
690
691 return(1);
692
693 } /* end of sift_backward_prob */
694
695
696 /**
697 @brief Copies the current variable order to array.
698
699 @details At the same time inverts the permutation.
700
701 @sideeffect None
702
703 */
704 static void
copyOrder(DdManager * table,int * array,int lower,int upper)705 copyOrder(
706 DdManager * table,
707 int * array,
708 int lower,
709 int upper)
710 {
711 int i;
712 int nvars;
713
714 nvars = upper - lower + 1;
715 for (i = 0; i < nvars; i++) {
716 array[i] = table->invperm[i+lower];
717 }
718
719 } /* end of copyOrder */
720
721
722 /**
723 @brief Restores the variable order in array by a series of sifts up.
724
725 @return 1 in case of success; 0 otherwise.
726
727 @sideeffect None
728
729 */
730 static int
restoreOrder(DdManager * table,int * array,int lower,int upper)731 restoreOrder(
732 DdManager * table,
733 int * array,
734 int lower,
735 int upper)
736 {
737 int i, x, y, size;
738 int nvars = upper - lower + 1;
739
740 for (i = 0; i < nvars; i++) {
741 x = table->perm[array[i]];
742 #ifdef DD_DEBUG
743 assert(x >= lower && x <= upper);
744 #endif
745 y = cuddNextLow(table,x);
746 while (y >= i + lower) {
747 size = cuddSwapInPlace(table,y,x);
748 if (size == 0) return(0);
749 x = y;
750 y = cuddNextLow(table,x);
751 }
752 }
753
754 return(1);
755
756 } /* end of restoreOrder */
757
758