src/bdd/cudd/cuddAnneal.c File Reference

#include "util_hack.h"
#include "cuddInt.h"
Include dependency graph for cuddAnneal.c:

Go to the source code of this file.

Defines

#define BETA   0.6
#define ALPHA   0.90
#define EXC_PROB   0.4
#define JUMP_UP_PROB   0.36
#define MAXGEN_RATIO   15.0
#define STOP_TEMP   1.0

Functions

static int stopping_criterion ARGS ((int c1, int c2, int c3, int c4, double temp))
static double random_generator ARGS (())
static int ddExchange ARGS ((DdManager *table, int x, int y, double temp))
static int ddJumpingAux ARGS ((DdManager *table, int x, int x_low, int x_high, double temp))
static Move *ddJumpingUp ARGS ((DdManager *table, int x, int x_low, int initial_size))
static Move *ddJumpingDown ARGS ((DdManager *table, int x, int x_high, int initial_size))
static int siftBackwardProb ARGS ((DdManager *table, Move *moves, int size, double temp))
static void copyOrder ARGS ((DdManager *table, int *array, int lower, int upper))
int cuddAnnealing (DdManager *table, int lower, int upper)
static int stopping_criterion (int c1, int c2, int c3, int c4, double temp)
static double random_generator ()
static int ddExchange (DdManager *table, int x, int y, double temp)
static int ddJumpingAux (DdManager *table, int x, int x_low, int x_high, double temp)
static Move * ddJumpingUp (DdManager *table, int x, int x_low, int initial_size)
static Move * ddJumpingDown (DdManager *table, int x, int x_high, int initial_size)
static int siftBackwardProb (DdManager *table, Move *moves, int size, double temp)
static void copyOrder (DdManager *table, int *array, int lower, int upper)
static int restoreOrder (DdManager *table, int *array, int lower, int upper)

Variables

static char rcsid[] DD_UNUSED = "$Id: cuddAnneal.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $"

Define Documentation

#define ALPHA   0.90

Definition at line 47 of file cuddAnneal.c.

#define BETA   0.6

CFile***********************************************************************

FileName [cuddAnneal.c]

PackageName [cudd]

Synopsis [Reordering of DDs based on simulated annealing]

Description [Internal procedures included in this file:

Static procedures included in this file:

]

SeeAlso []

Author [Jae-Young Jang, Jorgen Sivesind]

Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]

Definition at line 46 of file cuddAnneal.c.

#define EXC_PROB   0.4

Definition at line 48 of file cuddAnneal.c.

#define JUMP_UP_PROB   0.36

Definition at line 49 of file cuddAnneal.c.

#define MAXGEN_RATIO   15.0

Definition at line 50 of file cuddAnneal.c.

#define STOP_TEMP   1.0

Definition at line 51 of file cuddAnneal.c.

Function Documentation

static int restoreOrder ARGS ( (DdManager *table, int *array, int lower, int upper)   )  [static]
static int siftBackwardProb ARGS ( (DdManager *table, Move *moves, int size, double temp)   )  [static]
static Move* ddJumpingDown ARGS ( (DdManager *table, int x, int x_high, int initial_size)   )  [static]
static Move* ddJumpingUp ARGS ( (DdManager *table, int x, int x_low, int initial_size)   )  [static]
static int ddJumpingAux ARGS ( (DdManager *table, int x, int x_low, int x_high, double temp)   )  [static]
static int ddExchange ARGS ( (DdManager *table, int x, int y, double temp)   )  [static]
static double random_generator ARGS ( ()   )  [static]
static int stopping_criterion ARGS ( (int c1, int c2, int c3, int c4, double temp)   )  [static]

AutomaticStart

static void copyOrder ( DdManager *  table,
int *  array,
int  lower,
int  upper 
) [static]

Function********************************************************************

Synopsis [Copies the current variable order to array.]

Description [Copies the current variable order to array. At the same time inverts the permutation.]

SideEffects [None]

SeeAlso []

Definition at line 732 of file cuddAnneal.c.

00737 {
00738     int i;
00739     int nvars;
00740 
00741     nvars = upper - lower + 1;
00742     for (i = 0; i < nvars; i++) {
00743         array[i] = table->invperm[i+lower];
00744     }
00745 
00746 } /* end of copyOrder */

int cuddAnnealing ( DdManager *  table,
int  lower,
int  upper 
)

AutomaticEnd Function********************************************************************

Synopsis [Get new variable-order by simulated annealing algorithm.]

Description [Get x, y by random selection. Choose either exchange or jump randomly. In case of jump, choose between jump_up and jump_down randomly. Do exchange or jump and get optimal case. Loop until there is no improvement or temperature reaches minimum. Returns 1 in case of success; 0 otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 127 of file cuddAnneal.c.

00131 {
00132     int         nvars;
00133     int         size;
00134     int         x,y;
00135     int         result;
00136     int         c1, c2, c3, c4;
00137     int         BestCost;
00138     int         *BestOrder;
00139     double      NewTemp, temp;
00140     double      rand1;
00141     int         innerloop, maxGen;
00142     int         ecount, ucount, dcount;
00143    
00144     nvars = upper - lower + 1;
00145 
00146     result = cuddSifting(table,lower,upper);
00147 #ifdef DD_STATS
00148     (void) fprintf(table->out,"\n");
00149 #endif
00150     if (result == 0) return(0);
00151 
00152     size = table->keys - table->isolated;
00153 
00154     /* Keep track of the best order. */
00155     BestCost = size;
00156     BestOrder = ALLOC(int,nvars);
00157     if (BestOrder == NULL) {
00158         table->errorCode = CUDD_MEMORY_OUT;
00159         return(0);
00160     }
00161     copyOrder(table,BestOrder,lower,upper);
00162 
00163     temp = BETA * size;
00164     maxGen = (int) (MAXGEN_RATIO * nvars);
00165 
00166     c1 = size + 10;
00167     c2 = c1 + 10;
00168     c3 = size;
00169     c4 = c2 + 10;
00170     ecount = ucount = dcount = 0;
00171  
00172     while (!stopping_criterion(c1, c2, c3, c4, temp)) {
00173 #ifdef DD_STATS
00174         (void) fprintf(table->out,"temp=%f\tsize=%d\tgen=%d\t",
00175                        temp,size,maxGen);
00176         tosses = acceptances = 0;
00177 #endif
00178         for (innerloop = 0; innerloop < maxGen; innerloop++) {
00179             /* Choose x, y  randomly. */
00180             x = (int) Cudd_Random() % nvars;
00181             do {
00182                 y = (int) Cudd_Random() % nvars;
00183             } while (x == y);
00184             x += lower;
00185             y += lower;
00186             if (x > y) {
00187                 int tmp = x;
00188                 x = y;
00189                 y = tmp;
00190             }
00191 
00192             /* Choose move with roulette wheel. */
00193             rand1 = random_generator();
00194             if (rand1 < EXC_PROB) {
00195                 result = ddExchange(table,x,y,temp);       /* exchange */
00196                 ecount++;
00197 #if 0
00198                 (void) fprintf(table->out,
00199                                "Exchange of %d and %d: size = %d\n",
00200                                x,y,table->keys - table->isolated);
00201 #endif
00202             } else if (rand1 < EXC_PROB + JUMP_UP_PROB) {
00203                 result = ddJumpingAux(table,y,x,y,temp); /* jumping_up */
00204                 ucount++;
00205 #if 0
00206                 (void) fprintf(table->out,
00207                                "Jump up of %d to %d: size = %d\n",
00208                                y,x,table->keys - table->isolated);
00209 #endif
00210             } else {
00211                 result = ddJumpingAux(table,x,x,y,temp); /* jumping_down */
00212                 dcount++;
00213 #if 0
00214                 (void) fprintf(table->out,
00215                                "Jump down of %d to %d: size = %d\n",
00216                                x,y,table->keys - table->isolated);
00217 #endif
00218             }
00219 
00220             if (!result) {
00221                 FREE(BestOrder);
00222                 return(0);
00223             }
00224 
00225             size = table->keys - table->isolated;       /* keep current size */
00226             if (size < BestCost) {                      /* update best order */
00227                 BestCost = size;
00228                 copyOrder(table,BestOrder,lower,upper);
00229             }
00230         }
00231         c1 = c2;
00232         c2 = c3;
00233         c3 = c4;
00234         c4 = size;
00235         NewTemp = ALPHA * temp;
00236         if (NewTemp >= 1.0) {
00237             maxGen = (int)(log(NewTemp) / log(temp) * maxGen);
00238         }
00239         temp = NewTemp;                 /* control variable */
00240 #ifdef DD_STATS
00241         (void) fprintf(table->out,"uphill = %d\taccepted = %d\n",
00242                        tosses,acceptances);
00243         fflush(table->out);
00244 #endif
00245     }
00246 
00247     result = restoreOrder(table,BestOrder,lower,upper);
00248     FREE(BestOrder);
00249     if (!result) return(0);
00250 #ifdef DD_STATS
00251     fprintf(table->out,"#:N_EXCHANGE %8d : total exchanges\n",ecount);
00252     fprintf(table->out,"#:N_JUMPUP   %8d : total jumps up\n",ucount);
00253     fprintf(table->out,"#:N_JUMPDOWN %8d : total jumps down",dcount);
00254 #endif
00255     return(1);
00256 
00257 } /* end of cuddAnnealing */

static int ddExchange ( DdManager *  table,
int  x,
int  y,
double  temp 
) [static]

Function********************************************************************

Synopsis [This function is for exchanging two variables, x and y.]

Description [This is the same funcion as ddSwapping except for comparison expression. Use probability function, exp(-size_change/temp).]

SideEffects [None]

SeeAlso []

Definition at line 329 of file cuddAnneal.c.

00334 {
00335     Move       *move,*moves;
00336     int        tmp;
00337     int        x_ref,y_ref;
00338     int        x_next,y_next;
00339     int        size, result;
00340     int        initial_size, limit_size;
00341 
00342     x_ref = x;
00343     y_ref = y;
00344 
00345     x_next = cuddNextHigh(table,x);
00346     y_next = cuddNextLow(table,y);
00347     moves = NULL;
00348     initial_size = limit_size = table->keys - table->isolated;
00349 
00350     for (;;) {
00351         if (x_next == y_next) {
00352             size = cuddSwapInPlace(table,x,x_next);
00353             if (size == 0) goto ddExchangeOutOfMem;
00354             move = (Move *)cuddDynamicAllocNode(table);
00355             if (move == NULL) goto ddExchangeOutOfMem;
00356             move->x = x;
00357             move->y = x_next;
00358             move->size = size;
00359             move->next = moves;
00360             moves = move;
00361             size = cuddSwapInPlace(table,y_next,y);
00362             if (size == 0) goto ddExchangeOutOfMem;
00363             move = (Move *)cuddDynamicAllocNode(table);
00364             if (move == NULL) goto ddExchangeOutOfMem;
00365             move->x = y_next;
00366             move->y = y;
00367             move->size = size;
00368             move->next = moves;
00369             moves = move;
00370             size = cuddSwapInPlace(table,x,x_next);
00371             if (size == 0) goto ddExchangeOutOfMem;
00372             move = (Move *)cuddDynamicAllocNode(table);
00373             if (move == NULL) goto ddExchangeOutOfMem;
00374             move->x = x;
00375             move->y = x_next;
00376             move->size = size;
00377             move->next = moves;
00378             moves = move;
00379 
00380             tmp = x;
00381             x = y;
00382             y = tmp;
00383         } else if (x == y_next) {
00384             size = cuddSwapInPlace(table,x,x_next);
00385             if (size == 0) goto ddExchangeOutOfMem;
00386             move = (Move *)cuddDynamicAllocNode(table);
00387             if (move == NULL) goto ddExchangeOutOfMem;
00388             move->x = x;
00389             move->y = x_next;
00390             move->size = size;
00391             move->next = moves;
00392             moves = move;
00393             tmp = x;
00394             x = y;
00395             y = tmp;
00396         } else {
00397             size = cuddSwapInPlace(table,x,x_next);
00398             if (size == 0) goto ddExchangeOutOfMem;
00399             move = (Move *)cuddDynamicAllocNode(table);
00400             if (move == NULL) goto ddExchangeOutOfMem;
00401             move->x = x;
00402             move->y = x_next;
00403             move->size = size;
00404             move->next = moves;
00405             moves = move;
00406             size = cuddSwapInPlace(table,y_next,y);
00407             if (size == 0) goto ddExchangeOutOfMem;
00408             move = (Move *)cuddDynamicAllocNode(table);
00409             if (move == NULL) goto ddExchangeOutOfMem;
00410             move->x = y_next;
00411             move->y = y;
00412             move->size = size;
00413             move->next = moves;
00414             moves = move;
00415             x = x_next;
00416             y = y_next;
00417         }
00418 
00419         x_next = cuddNextHigh(table,x);
00420         y_next = cuddNextLow(table,y);
00421         if (x_next > y_ref) break;
00422 
00423         if ((double) size > DD_MAX_REORDER_GROWTH * (double) limit_size) {
00424             break;
00425         } else if (size < limit_size) {
00426             limit_size = size;
00427         }
00428     }
00429 
00430     if (y_next>=x_ref) {
00431         size = cuddSwapInPlace(table,y_next,y);
00432         if (size == 0) goto ddExchangeOutOfMem;
00433         move = (Move *)cuddDynamicAllocNode(table);
00434         if (move == NULL) goto ddExchangeOutOfMem;
00435         move->x = y_next;
00436         move->y = y;
00437         move->size = size;
00438         move->next = moves;
00439         moves = move;
00440     }
00441 
00442     /* move backward and stop at best position or accept uphill move */
00443     result = siftBackwardProb(table,moves,initial_size,temp);
00444     if (!result) goto ddExchangeOutOfMem;
00445 
00446     while (moves != NULL) {
00447         move = moves->next;
00448         cuddDeallocNode(table, (DdNode *) moves);
00449         moves = move;
00450     }
00451     return(1);
00452 
00453 ddExchangeOutOfMem:
00454     while (moves != NULL) {
00455         move = moves->next;
00456         cuddDeallocNode(table,(DdNode *) moves);
00457         moves = move;
00458     }
00459     return(0);
00460 
00461 } /* end of ddExchange */

static int ddJumpingAux ( DdManager *  table,
int  x,
int  x_low,
int  x_high,
double  temp 
) [static]

Function********************************************************************

Synopsis [Moves a variable to a specified position.]

Description [If x==x_low, it executes jumping_down. If x==x_high, it executes jumping_up. This funcion is similar to ddSiftingAux. Returns 1 in case of success; 0 otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 478 of file cuddAnneal.c.

00484 {
00485     Move       *move;
00486     Move       *moves;        /* list of moves */
00487     int        initial_size;
00488     int        result;
00489 
00490     initial_size = table->keys - table->isolated;
00491 
00492 #ifdef DD_DEBUG
00493     assert(table->subtables[x].keys > 0);
00494 #endif
00495 
00496     moves = NULL;
00497 
00498     if (cuddNextLow(table,x) < x_low) {
00499         if (cuddNextHigh(table,x) > x_high) return(1);
00500         moves = ddJumpingDown(table,x,x_high,initial_size);
00501         /* after that point x --> x_high unless early termination */
00502         if (moves == NULL) goto ddJumpingAuxOutOfMem;
00503         /* move backward and stop at best position or accept uphill move */
00504         result = siftBackwardProb(table,moves,initial_size,temp);
00505         if (!result) goto ddJumpingAuxOutOfMem;
00506     } else if (cuddNextHigh(table,x) > x_high) {
00507         moves = ddJumpingUp(table,x,x_low,initial_size);
00508         /* after that point x --> x_low unless early termination */
00509         if (moves == NULL) goto ddJumpingAuxOutOfMem;
00510         /* move backward and stop at best position or accept uphill move */
00511         result = siftBackwardProb(table,moves,initial_size,temp);
00512         if (!result) goto ddJumpingAuxOutOfMem;
00513     } else {
00514         (void) fprintf(table->err,"Unexpected condition in ddJumping\n");
00515         goto ddJumpingAuxOutOfMem;
00516     }
00517     while (moves != NULL) {
00518         move = moves->next;
00519         cuddDeallocNode(table, (DdNode *) moves);
00520         moves = move;
00521     }
00522     return(1);
00523 
00524 ddJumpingAuxOutOfMem:
00525     while (moves != NULL) {
00526         move = moves->next;
00527         cuddDeallocNode(table, (DdNode *) moves);
00528         moves = move;
00529     }
00530     return(0);
00531 
00532 } /* end of ddJumpingAux */

static Move* ddJumpingDown ( DdManager *  table,
int  x,
int  x_high,
int  initial_size 
) [static]

Function********************************************************************

Synopsis [This function is for jumping down.]

Description [This is a simplified version of ddSiftingDown. It does not use lower bounding. Returns the set of moves in case of success; NULL if memory is full.]

SideEffects [None]

SeeAlso []

Definition at line 608 of file cuddAnneal.c.

00613 {
00614     Move       *moves;
00615     Move       *move;
00616     int        y;
00617     int        size;
00618     int        limit_size = initial_size;
00619 
00620     moves = NULL;
00621     y = cuddNextHigh(table,x);
00622     while (y <= x_high) {
00623         size = cuddSwapInPlace(table,x,y);
00624         if (size == 0) goto ddJumpingDownOutOfMem;
00625         move = (Move *)cuddDynamicAllocNode(table);
00626         if (move == NULL) goto ddJumpingDownOutOfMem;
00627         move->x = x;
00628         move->y = y;
00629         move->size = size;
00630         move->next = moves;
00631         moves = move;
00632         if ((double) size > table->maxGrowth * (double) limit_size) {
00633             break;
00634         } else if (size < limit_size) {
00635             limit_size = size;
00636         }
00637         x = y;
00638         y = cuddNextHigh(table,x);
00639     }
00640     return(moves);
00641 
00642 ddJumpingDownOutOfMem:
00643     while (moves != NULL) {
00644         move = moves->next;
00645         cuddDeallocNode(table, (DdNode *) moves);
00646         moves = move;
00647     }
00648     return(NULL);
00649 
00650 } /* end of ddJumpingDown */

static Move* ddJumpingUp ( DdManager *  table,
int  x,
int  x_low,
int  initial_size 
) [static]

Function********************************************************************

Synopsis [This function is for jumping up.]

Description [This is a simplified version of ddSiftingUp. It does not use lower bounding. Returns the set of moves in case of success; NULL if memory is full.]

SideEffects [None]

SeeAlso []

Definition at line 549 of file cuddAnneal.c.

00554 {
00555     Move       *moves;
00556     Move       *move;
00557     int        y;
00558     int        size;
00559     int        limit_size = initial_size;
00560 
00561     moves = NULL;
00562     y = cuddNextLow(table,x);
00563     while (y >= x_low) {
00564         size = cuddSwapInPlace(table,y,x);
00565         if (size == 0) goto ddJumpingUpOutOfMem;
00566         move = (Move *)cuddDynamicAllocNode(table);
00567         if (move == NULL) goto ddJumpingUpOutOfMem;
00568         move->x = y;
00569         move->y = x;
00570         move->size = size;
00571         move->next = moves;
00572         moves = move;
00573         if ((double) size > table->maxGrowth * (double) limit_size) {
00574             break;
00575         } else if (size < limit_size) {
00576             limit_size = size;
00577         }
00578         x = y;
00579         y = cuddNextLow(table,x);
00580     }
00581     return(moves);
00582 
00583 ddJumpingUpOutOfMem:
00584     while (moves != NULL) {
00585         move = moves->next;
00586         cuddDeallocNode(table, (DdNode *) moves);
00587         moves = move;
00588     }
00589     return(NULL);
00590 
00591 } /* end of ddJumpingUp */

static double random_generator (  )  [static]

Function********************************************************************

Synopsis [Random number generator.]

Description [Returns a double precision value between 0.0 and 1.0.]

SideEffects [None]

SeeAlso []

Definition at line 308 of file cuddAnneal.c.

00310 {
00311     return((double)(Cudd_Random() / 2147483561.0));
00312 
00313 } /* end of random_generator */

static int restoreOrder ( DdManager *  table,
int *  array,
int  lower,
int  upper 
) [static]

Function********************************************************************

Synopsis [Restores the variable order in array by a series of sifts up.]

Description [Restores the variable order in array by a series of sifts up. Returns 1 in case of success; 0 otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 762 of file cuddAnneal.c.

00767 {
00768     int i, x, y, size;
00769     int nvars = upper - lower + 1;
00770 
00771     for (i = 0; i < nvars; i++) {
00772         x = table->perm[array[i]];
00773 #ifdef DD_DEBUG
00774     assert(x >= lower && x <= upper);
00775 #endif
00776         y = cuddNextLow(table,x);
00777         while (y >= i + lower) {
00778             size = cuddSwapInPlace(table,y,x);
00779             if (size == 0) return(0);
00780             x = y;
00781             y = cuddNextLow(table,x);
00782         }
00783     }
00784 
00785     return(1);
00786 
00787 } /* end of restoreOrder */

static int siftBackwardProb ( DdManager *  table,
Move *  moves,
int  size,
double  temp 
) [static]

Function********************************************************************

Synopsis [Returns the DD to the best position encountered during sifting if there was improvement.]

Description [Otherwise, "tosses a coin" to decide whether to keep the current configuration or return the DD to the original one. Returns 1 in case of success; 0 otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 668 of file cuddAnneal.c.

00673 {
00674     Move   *move;
00675     int    res;
00676     int    best_size = size;
00677     double coin, threshold;
00678 
00679     /* Look for best size during the last sifting */
00680     for (move = moves; move != NULL; move = move->next) {
00681         if (move->size < best_size) {
00682             best_size = move->size;
00683         }
00684     }
00685     
00686     /* If best_size equals size, the last sifting did not produce any
00687     ** improvement. We now toss a coin to decide whether to retain
00688     ** this change or not.
00689     */
00690     if (best_size == size) {
00691         coin = random_generator();
00692 #ifdef DD_STATS
00693         tosses++;
00694 #endif
00695         threshold = exp(-((double)(table->keys - table->isolated - size))/temp);
00696         if (coin < threshold) {
00697 #ifdef DD_STATS
00698             acceptances++;
00699 #endif
00700             return(1);
00701         }
00702     }
00703 
00704     /* Either there was improvement, or we have decided not to
00705     ** accept the uphill move. Go to best position.
00706     */
00707     res = table->keys - table->isolated;
00708     for (move = moves; move != NULL; move = move->next) {
00709         if (res == best_size) return(1);
00710         res = cuddSwapInPlace(table,(int)move->x,(int)move->y);
00711         if (!res) return(0);
00712     }
00713 
00714     return(1);
00715 
00716 } /* end of sift_backward_prob */

static int stopping_criterion ( int  c1,
int  c2,
int  c3,
int  c4,
double  temp 
) [static]

Function********************************************************************

Synopsis [Checks termination condition.]

Description [If temperature is STOP_TEMP or there is no improvement then terminates. Returns 1 if the termination criterion is met; 0 otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 278 of file cuddAnneal.c.

00284 {
00285     if (STOP_TEMP < temp) {
00286         return(0);
00287     } else if ((c1 == c2) && (c1 == c3) && (c1 == c4)) {
00288         return(1);
00289     } else {
00290         return(0);
00291     }
00292 
00293 } /* end of stopping_criterion */

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddAnneal.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $" [static]

Definition at line 68 of file cuddAnneal.c.

Generated on Tue Jan 5 12:18:52 2010 for abc70930 by  doxygen 1.6.1