cuddAnneal.c

Go to the documentation of this file.

#include "CUDD/util.h"
#include "CUDD/cuddInt.h"

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

/* Annealing parameters */
#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

/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

#ifndef lint
static char rcsid[] DD_UNUSED = "$Id: cuddAnneal.c,v 1.15 2012/02/05 01:07:18 fabio Exp $";
#endif

#ifdef DD_STATS
extern  int ddTotalNumberSwapping;
extern  int ddTotalNISwaps;
static  int tosses;
static  int acceptances;
#endif

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

static int stopping_criterion (int c1, int c2, int c3, int c4, double temp);
static double random_generator (void);
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);

/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/


int
cuddAnnealing(
  DdManager * table,
  int  lower,
  int  upper)
{
    int         nvars;
    int         size;
    int         x,y;
    int         result;
    int     c1, c2, c3, c4;
    int     BestCost;
    int     *BestOrder;
    double  NewTemp, temp;
    double  rand1;
    int         innerloop, maxGen;
    int         ecount, ucount, dcount;
   
    nvars = upper - lower + 1;

    result = cuddSifting(table,lower,upper);
#ifdef DD_STATS
    (void) fprintf(table->out,"\n");
#endif
    if (result == 0) return(0);

    size = table->keys - table->isolated;

    /* Keep track of the best order. */
    BestCost = size;
    BestOrder = ALLOC(int,nvars);
    if (BestOrder == NULL) {
    table->errorCode = CUDD_MEMORY_OUT;
    return(0);
    }
    copyOrder(table,BestOrder,lower,upper);

    temp = BETA * size;
    maxGen = (int) (MAXGEN_RATIO * nvars);

    c1 = size + 10;
    c2 = c1 + 10;
    c3 = size;
    c4 = c2 + 10;
    ecount = ucount = dcount = 0;
 
    while (!stopping_criterion(c1, c2, c3, c4, temp)) {
#ifdef DD_STATS
    (void) fprintf(table->out,"temp=%f\tsize=%d\tgen=%d\t",
               temp,size,maxGen);
    tosses = acceptances = 0;
#endif
    for (innerloop = 0; innerloop < maxGen; innerloop++) {
        /* Choose x, y  randomly. */
        x = (int) Cudd_Random() % nvars;
        do {
        y = (int) Cudd_Random() % nvars;
        } while (x == y);
        x += lower;
        y += lower;
        if (x > y) {
        int tmp = x;
        x = y;
        y = tmp;
        }

        /* Choose move with roulette wheel. */
        rand1 = random_generator();
        if (rand1 < EXC_PROB) {
        result = ddExchange(table,x,y,temp);       /* exchange */
        ecount++;
#if 0
        (void) fprintf(table->out,
                   "Exchange of %d and %d: size = %d\n",
                   x,y,table->keys - table->isolated);
#endif
        } else if (rand1 < EXC_PROB + JUMP_UP_PROB) {
        result = ddJumpingAux(table,y,x,y,temp); /* jumping_up */
        ucount++;
#if 0
        (void) fprintf(table->out,
                   "Jump up of %d to %d: size = %d\n",
                   y,x,table->keys - table->isolated);
#endif
        } else {
        result = ddJumpingAux(table,x,x,y,temp); /* jumping_down */
        dcount++;
#if 0
        (void) fprintf(table->out,
                   "Jump down of %d to %d: size = %d\n",
                   x,y,table->keys - table->isolated);
#endif
        }

        if (!result) {
        FREE(BestOrder);
        return(0);
        }

        size = table->keys - table->isolated;   /* keep current size */
        if (size < BestCost) {          /* update best order */
        BestCost = size;
        copyOrder(table,BestOrder,lower,upper);
        }
    }
    c1 = c2;
    c2 = c3;
    c3 = c4;
    c4 = size;
    NewTemp = ALPHA * temp;
    if (NewTemp >= 1.0) {
        maxGen = (int)(log(NewTemp) / log(temp) * maxGen);
    }
    temp = NewTemp;                 /* control variable */
#ifdef DD_STATS
    (void) fprintf(table->out,"uphill = %d\taccepted = %d\n",
               tosses,acceptances);
    fflush(table->out);
#endif
    }

    result = restoreOrder(table,BestOrder,lower,upper);
    FREE(BestOrder);
    if (!result) return(0);
#ifdef DD_STATS
    fprintf(table->out,"#:N_EXCHANGE %8d : total exchanges\n",ecount);
    fprintf(table->out,"#:N_JUMPUP   %8d : total jumps up\n",ucount);
    fprintf(table->out,"#:N_JUMPDOWN %8d : total jumps down",dcount);
#endif
    return(1);

} /* end of cuddAnnealing */


/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/

static int
stopping_criterion(
  int  c1,
  int  c2,
  int  c3,
  int  c4,
  double  temp)
{
    if (STOP_TEMP < temp) {
    return(0);
    } else if ((c1 == c2) && (c1 == c3) && (c1 == c4)) {
    return(1);
    } else {
    return(0);
    }

} /* end of stopping_criterion */


static double
random_generator(void)
{
    return((double)(Cudd_Random() / 2147483561.0));

} /* end of random_generator */


static int
ddExchange(
  DdManager * table,
  int  x,
  int  y,
  double  temp)
{
    Move       *move,*moves;
    int        tmp;
    int        x_ref,y_ref;
    int        x_next,y_next;
    int        size, result;
    int        initial_size, limit_size;

    x_ref = x;
    y_ref = y;

    x_next = cuddNextHigh(table,x);
    y_next = cuddNextLow(table,y);
    moves = NULL;
    initial_size = limit_size = table->keys - table->isolated;

    for (;;) {
    if (x_next == y_next) {
        size = cuddSwapInPlace(table,x,x_next);
        if (size == 0) goto ddExchangeOutOfMem;
        move = (Move *)cuddDynamicAllocNode(table);
        if (move == NULL) goto ddExchangeOutOfMem;
        move->x = x;
        move->y = x_next;
        move->size = size;
        move->next = moves;
        moves = move;
        size = cuddSwapInPlace(table,y_next,y);
        if (size == 0) goto ddExchangeOutOfMem;
        move = (Move *)cuddDynamicAllocNode(table);
        if (move == NULL) goto ddExchangeOutOfMem;
        move->x = y_next;
        move->y = y;
        move->size = size;
        move->next = moves;
        moves = move;
        size = cuddSwapInPlace(table,x,x_next);
        if (size == 0) goto ddExchangeOutOfMem;
        move = (Move *)cuddDynamicAllocNode(table);
        if (move == NULL) goto ddExchangeOutOfMem;
        move->x = x;
        move->y = x_next;
        move->size = size;
        move->next = moves;
        moves = move;

        tmp = x;
        x = y;
        y = tmp;
    } else if (x == y_next) {
        size = cuddSwapInPlace(table,x,x_next);
        if (size == 0) goto ddExchangeOutOfMem;
        move = (Move *)cuddDynamicAllocNode(table);
        if (move == NULL) goto ddExchangeOutOfMem;
        move->x = x;
        move->y = x_next;
        move->size = size;
        move->next = moves;
        moves = move;
        tmp = x;
        x = y;
        y = tmp;
    } else {
        size = cuddSwapInPlace(table,x,x_next);
        if (size == 0) goto ddExchangeOutOfMem;
        move = (Move *)cuddDynamicAllocNode(table);
        if (move == NULL) goto ddExchangeOutOfMem;
        move->x = x;
        move->y = x_next;
        move->size = size;
        move->next = moves;
        moves = move;
        size = cuddSwapInPlace(table,y_next,y);
        if (size == 0) goto ddExchangeOutOfMem;
        move = (Move *)cuddDynamicAllocNode(table);
        if (move == NULL) goto ddExchangeOutOfMem;
        move->x = y_next;
        move->y = y;
        move->size = size;
        move->next = moves;
        moves = move;
        x = x_next;
        y = y_next;
    }

    x_next = cuddNextHigh(table,x);
    y_next = cuddNextLow(table,y);
    if (x_next > y_ref) break;

    if ((double) size > DD_MAX_REORDER_GROWTH * (double) limit_size) {
        break;
    } else if (size < limit_size) {
        limit_size = size;
    }
    }

    if (y_next>=x_ref) {
        size = cuddSwapInPlace(table,y_next,y);
        if (size == 0) goto ddExchangeOutOfMem;
        move = (Move *)cuddDynamicAllocNode(table);
        if (move == NULL) goto ddExchangeOutOfMem;
        move->x = y_next;
        move->y = y;
        move->size = size;
        move->next = moves;
        moves = move;
    }

    /* move backward and stop at best position or accept uphill move */
    result = siftBackwardProb(table,moves,initial_size,temp);
    if (!result) goto ddExchangeOutOfMem;

    while (moves != NULL) {
    move = moves->next;
    cuddDeallocMove(table, moves);
    moves = move;
    }
    return(1);

ddExchangeOutOfMem:
    while (moves != NULL) {
        move = moves->next;
        cuddDeallocMove(table, moves);
        moves = move;
    }
    return(0);

} /* end of ddExchange */


static int
ddJumpingAux(
  DdManager * table,
  int  x,
  int  x_low,
  int  x_high,
  double  temp)
{
    Move       *move;
    Move       *moves;        /* list of moves */
    int        initial_size;
    int        result;

    initial_size = table->keys - table->isolated;

#ifdef DD_DEBUG
    assert(table->subtables[x].keys > 0);
#endif

    moves = NULL;

    if (cuddNextLow(table,x) < x_low) {
    if (cuddNextHigh(table,x) > x_high) return(1);
    moves = ddJumpingDown(table,x,x_high,initial_size);
    /* after that point x --> x_high unless early termination */
    if (moves == NULL) goto ddJumpingAuxOutOfMem;
    /* move backward and stop at best position or accept uphill move */
    result = siftBackwardProb(table,moves,initial_size,temp);
    if (!result) goto ddJumpingAuxOutOfMem;
    } else if (cuddNextHigh(table,x) > x_high) {
    moves = ddJumpingUp(table,x,x_low,initial_size);
    /* after that point x --> x_low unless early termination */
    if (moves == NULL) goto ddJumpingAuxOutOfMem;
    /* move backward and stop at best position or accept uphill move */
    result = siftBackwardProb(table,moves,initial_size,temp);
    if (!result) goto ddJumpingAuxOutOfMem;
    } else {
    (void) fprintf(table->err,"Unexpected condition in ddJumping\n");
    goto ddJumpingAuxOutOfMem;
    }
    while (moves != NULL) {
    move = moves->next;
    cuddDeallocMove(table, moves);
    moves = move;
    }
    return(1);

ddJumpingAuxOutOfMem:
    while (moves != NULL) {
    move = moves->next;
    cuddDeallocMove(table, moves);
    moves = move;
    }
    return(0);

} /* end of ddJumpingAux */


static Move *
ddJumpingUp(
  DdManager * table,
  int  x,
  int  x_low,
  int  initial_size)
{
    Move       *moves;
    Move       *move;
    int        y;
    int        size;
    int        limit_size = initial_size;

    moves = NULL;
    y = cuddNextLow(table,x);
    while (y >= x_low) {
    size = cuddSwapInPlace(table,y,x);
    if (size == 0) goto ddJumpingUpOutOfMem;
    move = (Move *)cuddDynamicAllocNode(table);
    if (move == NULL) goto ddJumpingUpOutOfMem;
    move->x = y;
    move->y = x;
    move->size = size;
    move->next = moves;
    moves = move;
    if ((double) size > table->maxGrowth * (double) limit_size) {
        break;
    } else if (size < limit_size) {
        limit_size = size;
    }
    x = y;
    y = cuddNextLow(table,x);
    }
    return(moves);

ddJumpingUpOutOfMem:
    while (moves != NULL) {
    move = moves->next;
    cuddDeallocMove(table, moves);
    moves = move;
    }
    return(NULL);

} /* end of ddJumpingUp */


static Move *
ddJumpingDown(
  DdManager * table,
  int  x,
  int  x_high,
  int  initial_size)
{
    Move       *moves;
    Move       *move;
    int        y;
    int        size;
    int        limit_size = initial_size;

    moves = NULL;
    y = cuddNextHigh(table,x);
    while (y <= x_high) {
    size = cuddSwapInPlace(table,x,y);
    if (size == 0) goto ddJumpingDownOutOfMem;
    move = (Move *)cuddDynamicAllocNode(table);
    if (move == NULL) goto ddJumpingDownOutOfMem;
    move->x = x;
    move->y = y;
    move->size = size;
    move->next = moves;
    moves = move;
    if ((double) size > table->maxGrowth * (double) limit_size) {
        break;
    } else if (size < limit_size) {
        limit_size = size;
    }
    x = y;
    y = cuddNextHigh(table,x);
    }
    return(moves);

ddJumpingDownOutOfMem:
    while (moves != NULL) {
    move = moves->next;
    cuddDeallocMove(table, moves);
    moves = move;
    }
    return(NULL);

} /* end of ddJumpingDown */


static int
siftBackwardProb(
  DdManager * table,
  Move * moves,
  int  size,
  double  temp)
{
    Move   *move;
    int    res;
    int    best_size = size;
    double coin, threshold;

    /* Look for best size during the last sifting */
    for (move = moves; move != NULL; move = move->next) {
    if (move->size < best_size) {
        best_size = move->size;
    }
    }
    
    /* If best_size equals size, the last sifting did not produce any
    ** improvement. We now toss a coin to decide whether to retain
    ** this change or not.
    */
    if (best_size == size) {
    coin = random_generator();
#ifdef DD_STATS
    tosses++;
#endif
    threshold = exp(-((double)(table->keys - table->isolated - size))/temp);
    if (coin < threshold) {
#ifdef DD_STATS
        acceptances++;
#endif
        return(1);
    }
    }

    /* Either there was improvement, or we have decided not to
    ** accept the uphill move. Go to best position.
    */
    res = table->keys - table->isolated;
    for (move = moves; move != NULL; move = move->next) {
    if (res == best_size) return(1);
    res = cuddSwapInPlace(table,(int)move->x,(int)move->y);
    if (!res) return(0);
    }

    return(1);

} /* end of sift_backward_prob */


static void
copyOrder(
  DdManager * table,
  int * array,
  int  lower,
  int  upper)
{
    int i;
    int nvars;

    nvars = upper - lower + 1;
    for (i = 0; i < nvars; i++) {
    array[i] = table->invperm[i+lower];
    }

} /* end of copyOrder */


static int
restoreOrder(
  DdManager * table,
  int * array,
  int  lower,
  int  upper)
{
    int i, x, y, size;
    int nvars = upper - lower + 1;

    for (i = 0; i < nvars; i++) {
    x = table->perm[array[i]];
#ifdef DD_DEBUG
    assert(x >= lower && x <= upper);
#endif
    y = cuddNextLow(table,x);
    while (y >= i + lower) {
        size = cuddSwapInPlace(table,y,x);
        if (size == 0) return(0);
        x = y;
        y = cuddNextLow(table,x);
    }
    }

    return(1);

} /* end of restoreOrder */