distr/cudd/cuddAnneal.c

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