src/cuBdd/cuddGenetic.c File Reference

#include "util.h"
#include "cuddInt.h"
Include dependency graph for cuddGenetic.c:

Go to the source code of this file.

Defines

#define STOREDD(i, j)   storedd[(i)*(numvars+1)+(j)]

Functions

static int make_random (DdManager *table, int lower)
static int sift_up (DdManager *table, int x, int x_low)
static int build_dd (DdManager *table, int num, int lower, int upper)
static int largest (void)
static int rand_int (int a)
static int array_hash (char *array, int modulus)
static int array_compare (const char *array1, const char *array2)
static int find_best (void)
static int PMX (int maxvar)
static int roulette (int *p1, int *p2)
int cuddGa (DdManager *table, int lower, int upper)

Variables

static char rcsid[] DD_UNUSED = "$Id: cuddGenetic.c,v 1.28 2004/08/13 18:04:48 fabio Exp $"
static int popsize
static int numvars
static int * storedd
static st_tablecomputed
static int * repeat
static int large
static int result
static int cross

Define Documentation

#define STOREDD ( i,
 )     storedd[(i)*(numvars+1)+(j)]

Definition at line 131 of file cuddGenetic.c.


Function Documentation

static int array_compare ( const char *  array1,
const char *  array2 
) [static]

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

Synopsis [Comparison function for the computed table.]

Description [Comparison function for the computed table. Returns 0 if the two arrays are equal; 1 otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 702 of file cuddGenetic.c.

00705 {
00706     int i;
00707     int *intarray1, *intarray2;
00708 
00709     intarray1 = (int *) array1;
00710     intarray2 = (int *) array2;
00711 
00712     for (i = 0; i < numvars; i++) {
00713         if (intarray1[i] != intarray2[i]) return(1);
00714     }
00715     return(0);
00716 
00717 } /* end of array_compare */

static int array_hash ( char *  array,
int  modulus 
) [static]

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

Synopsis [Hash function for the computed table.]

Description [Hash function for the computed table. Returns the bucket number.]

SideEffects [None]

SeeAlso []

Definition at line 670 of file cuddGenetic.c.

00673 {
00674     int val = 0;
00675     int i;
00676     int *intarray;
00677 
00678     intarray = (int *) array;
00679 
00680     for (i = 0; i < numvars; i++) {
00681         val = val * 997 + intarray[i];
00682     }
00683 
00684     return ((val < 0) ? -val : val) % modulus;
00685 
00686 } /* end of array_hash */

static int build_dd ( DdManager table,
int  num,
int  lower,
int  upper 
) [static]

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

Synopsis [Builds a DD from a given order.]

Description [Builds a DD from a given order. This procedure also sifts the final order and inserts into the array the size in nodes of the result. Returns 1 if successful; 0 otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 549 of file cuddGenetic.c.

00554 {
00555     int         i,j;            /* loop vars */
00556     int         position;
00557     int         index;
00558     int         limit;          /* how large the DD for this order can grow */
00559     int         size;
00560 
00561     /* Check the computed table. If the order already exists, it
00562     ** suffices to copy the size from the existing entry.
00563     */
00564     if (computed && st_lookup_int(computed,(char *)&STOREDD(num,0),&index)) {
00565         STOREDD(num,numvars) = STOREDD(index,numvars);
00566 #ifdef DD_STATS
00567         (void) fprintf(table->out,"\nCache hit for index %d", index);
00568 #endif
00569         return(1);
00570     }
00571 
00572     /* Stop if the DD grows 20 times larges than the reference size. */
00573     limit = 20 * STOREDD(0,numvars);
00574 
00575     /* Sift up the variables so as to build the desired permutation.
00576     ** First the variable that has to be on top is sifted to the top.
00577     ** Then the variable that has to occupy the secon position is sifted
00578     ** up to the second position, and so on.
00579     */
00580     for (j = 0; j < numvars; j++) {
00581         i = STOREDD(num,j);
00582         position = table->perm[i];
00583         result = sift_up(table,position,j+lower);
00584         if (!result) return(0);
00585         size = table->keys - table->isolated;
00586         if (size > limit) break;
00587     }
00588 
00589     /* Sift the DD just built. */
00590 #ifdef DD_STATS
00591     (void) fprintf(table->out,"\n");
00592 #endif
00593     result = cuddSifting(table,lower,upper);
00594     if (!result) return(0);
00595 
00596     /* Copy order and size to table. */
00597     for (j = 0; j < numvars; j++) {
00598         STOREDD(num,j) = table->invperm[lower+j];
00599     }
00600     STOREDD(num,numvars) = table->keys - table->isolated; /* size of new DD */
00601     return(1);
00602 
00603 } /* end of build_dd */

int cuddGa ( DdManager table,
int  lower,
int  upper 
)

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

Synopsis [Genetic algorithm for DD reordering.]

Description [Genetic algorithm for DD reordering. The two children of a crossover will be stored in storedd[popsize] and storedd[popsize+1] --- the last two slots in the storedd array. (This will make comparisons and replacement easy.) Returns 1 in case of success; 0 otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 188 of file cuddGenetic.c.

00192 {
00193     int         i,n,m;          /* dummy/loop vars */
00194     int         index;
00195 #ifdef DD_STATS
00196     double      average_fitness;
00197 #endif
00198     int         small;          /* index of smallest DD in population */
00199 
00200     /* Do an initial sifting to produce at least one reasonable individual. */
00201     if (!cuddSifting(table,lower,upper)) return(0);
00202 
00203     /* Get the initial values. */
00204     numvars = upper - lower + 1; /* number of variables to be reordered */
00205     if (table->populationSize == 0) {
00206         popsize = 3 * numvars;  /* population size is 3 times # of vars */
00207         if (popsize > 120) {
00208             popsize = 120;      /* Maximum population size is 120 */
00209         }
00210     } else {
00211         popsize = table->populationSize;  /* user specified value */
00212     }
00213     if (popsize < 4) popsize = 4;       /* enforce minimum population size */
00214 
00215     /* Allocate population table. */
00216     storedd = ALLOC(int,(popsize+2)*(numvars+1));
00217     if (storedd == NULL) {
00218         table->errorCode = CUDD_MEMORY_OUT;
00219         return(0);
00220     }
00221 
00222     /* Initialize the computed table. This table is made up of two data
00223     ** structures: A hash table with the key given by the order, which says
00224     ** if a given order is present in the population; and the repeat
00225     ** vector, which says how many copies of a given order are stored in
00226     ** the population table. If there are multiple copies of an order, only
00227     ** one has a repeat count greater than 1. This copy is the one pointed
00228     ** by the computed table.
00229     */
00230     repeat = ALLOC(int,popsize);
00231     if (repeat == NULL) {
00232         table->errorCode = CUDD_MEMORY_OUT;
00233         FREE(storedd);
00234         return(0);
00235     }
00236     for (i = 0; i < popsize; i++) {
00237         repeat[i] = 0;
00238     }
00239     computed = st_init_table(array_compare,array_hash);
00240     if (computed == NULL) {
00241         table->errorCode = CUDD_MEMORY_OUT;
00242         FREE(storedd);
00243         FREE(repeat);
00244         return(0);
00245     }
00246 
00247     /* Copy the current DD and its size to the population table. */
00248     for (i = 0; i < numvars; i++) {
00249         STOREDD(0,i) = table->invperm[i+lower]; /* order of initial DD */
00250     }
00251     STOREDD(0,numvars) = table->keys - table->isolated; /* size of initial DD */
00252 
00253     /* Store the initial order in the computed table. */
00254     if (st_insert(computed,(char *)storedd,(char *) 0) == ST_OUT_OF_MEM) {
00255         FREE(storedd);
00256         FREE(repeat);
00257         st_free_table(computed);
00258         return(0);
00259     }
00260     repeat[0]++;
00261 
00262     /* Insert the reverse order as second element of the population. */
00263     for (i = 0; i < numvars; i++) {
00264         STOREDD(1,numvars-1-i) = table->invperm[i+lower]; /* reverse order */
00265     }
00266 
00267     /* Now create the random orders. make_random fills the population
00268     ** table with random permutations. The successive loop builds and sifts
00269     ** the DDs for the reverse order and each random permutation, and stores
00270     ** the results in the computed table.
00271     */
00272     if (!make_random(table,lower)) {
00273         table->errorCode = CUDD_MEMORY_OUT;
00274         FREE(storedd);
00275         FREE(repeat);
00276         st_free_table(computed);
00277         return(0);
00278     }
00279     for (i = 1; i < popsize; i++) {
00280         result = build_dd(table,i,lower,upper); /* build and sift order */
00281         if (!result) {
00282             FREE(storedd);
00283             FREE(repeat);
00284             st_free_table(computed);
00285             return(0);
00286         }
00287         if (st_lookup_int(computed,(char *)&STOREDD(i,0),&index)) {
00288             repeat[index]++;
00289         } else {
00290             if (st_insert(computed,(char *)&STOREDD(i,0),(char *)(long)i) ==
00291             ST_OUT_OF_MEM) {
00292                 FREE(storedd);
00293                 FREE(repeat);
00294                 st_free_table(computed);
00295                 return(0);
00296             }
00297             repeat[i]++;
00298         }
00299     }
00300 
00301 #if 0
00302 #ifdef DD_STATS
00303     /* Print the initial population. */
00304     (void) fprintf(table->out,"Initial population after sifting\n");
00305     for (m = 0; m < popsize; m++) {
00306         for (i = 0; i < numvars; i++) {
00307             (void) fprintf(table->out," %2d",STOREDD(m,i));
00308         }
00309         (void) fprintf(table->out," : %3d (%d)\n",
00310                        STOREDD(m,numvars),repeat[m]);
00311     }
00312 #endif
00313 #endif
00314 
00315     small = find_best();
00316 #ifdef DD_STATS
00317     average_fitness = find_average_fitness();
00318     (void) fprintf(table->out,"\nInitial population: best fitness = %d, average fitness %8.3f",STOREDD(small,numvars),average_fitness);
00319 #endif
00320 
00321     /* Decide how many crossovers should be tried. */
00322     if (table->numberXovers == 0) {
00323         cross = 3*numvars;
00324         if (cross > 60) {       /* do a maximum of 50 crossovers */
00325             cross = 60;
00326         }
00327     } else {
00328         cross = table->numberXovers;      /* use user specified value */
00329     }
00330 
00331     /* Perform the crossovers to get the best order. */
00332     for (m = 0; m < cross; m++) {
00333         if (!PMX(table->size)) {        /* perform one crossover */
00334             table->errorCode = CUDD_MEMORY_OUT;
00335             FREE(storedd);
00336             FREE(repeat);
00337             st_free_table(computed);
00338             return(0);
00339         }
00340         /* The offsprings are left in the last two entries of the
00341         ** population table. These are now considered in turn.
00342         */
00343         for (i = popsize; i <= popsize+1; i++) {
00344             result = build_dd(table,i,lower,upper); /* build and sift child */
00345             if (!result) {
00346                 FREE(storedd);
00347                 FREE(repeat);
00348                 st_free_table(computed);
00349                 return(0);
00350             }
00351             large = largest();  /* find the largest DD in population */
00352 
00353             /* If the new child is smaller than the largest DD in the current
00354             ** population, enter it into the population in place of the
00355             ** largest DD.
00356             */
00357             if (STOREDD(i,numvars) < STOREDD(large,numvars)) {
00358                 /* Look up the largest DD in the computed table.
00359                 ** Decrease its repetition count. If the repetition count
00360                 ** goes to 0, remove the largest DD from the computed table.
00361                 */
00362                 result = st_lookup_int(computed,(char *)&STOREDD(large,0),
00363                                        &index);
00364                 if (!result) {
00365                     FREE(storedd);
00366                     FREE(repeat);
00367                     st_free_table(computed);
00368                     return(0);
00369                 }
00370                 repeat[index]--;
00371                 if (repeat[index] == 0) {
00372                     int *pointer = &STOREDD(index,0);
00373                     result = st_delete(computed, &pointer, NULL);
00374                     if (!result) {
00375                         FREE(storedd);
00376                         FREE(repeat);
00377                         st_free_table(computed);
00378                         return(0);
00379                     }
00380                 }
00381                 /* Copy the new individual to the entry of the
00382                 ** population table just made available and update the
00383                 ** computed table.
00384                 */
00385                 for (n = 0; n <= numvars; n++) {
00386                     STOREDD(large,n) = STOREDD(i,n);
00387                 }
00388                 if (st_lookup_int(computed,(char *)&STOREDD(large,0),
00389                                   &index)) {
00390                     repeat[index]++;
00391                 } else {
00392                     if (st_insert(computed,(char *)&STOREDD(large,0),
00393                     (char *)(long)large) == ST_OUT_OF_MEM) {
00394                         FREE(storedd);
00395                         FREE(repeat);
00396                         st_free_table(computed);
00397                         return(0);
00398                     }
00399                     repeat[large]++;
00400                 }
00401             }
00402         }
00403     }
00404 
00405     /* Find the smallest DD in the population and build it;
00406     ** that will be the result.
00407     */
00408     small = find_best();
00409 
00410     /* Print stats on the final population. */
00411 #ifdef DD_STATS
00412     average_fitness = find_average_fitness();
00413     (void) fprintf(table->out,"\nFinal population: best fitness = %d, average fitness %8.3f",STOREDD(small,numvars),average_fitness);
00414 #endif
00415 
00416     /* Clean up, build the result DD, and return. */
00417     st_free_table(computed);
00418     computed = NULL;
00419     result = build_dd(table,small,lower,upper);
00420     FREE(storedd);
00421     FREE(repeat);
00422     return(result);
00423 
00424 } /* end of cuddGa */

static int find_best ( void   )  [static]

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

Synopsis [Returns the index of the fittest individual.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 732 of file cuddGenetic.c.

00733 {
00734     int i,small;
00735 
00736     small = 0;
00737     for (i = 1; i < popsize; i++) {
00738         if (STOREDD(i,numvars) < STOREDD(small,numvars)) {
00739             small = i;
00740         }
00741     }
00742     return(small);
00743 
00744 } /* end of find_best */

static int largest ( void   )  [static]

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

Synopsis [Finds the largest DD in the population.]

Description [Finds the largest DD in the population. If an order is repeated, it avoids choosing the copy that is in the computed table (it has repeat[i] > 1).]

SideEffects [None]

SeeAlso []

Definition at line 620 of file cuddGenetic.c.

00621 {
00622     int i;      /* loop var */
00623     int big;    /* temporary holder to return result */
00624 
00625     big = 0;
00626     while (repeat[big] > 1) big++;
00627     for (i = big + 1; i < popsize; i++) {
00628         if (STOREDD(i,numvars) >= STOREDD(big,numvars) && repeat[i] <= 1) {
00629             big = i;
00630         }
00631     }
00632     return(big);
00633 
00634 } /* end of largest */

static int make_random ( DdManager table,
int  lower 
) [static]

AutomaticStart

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

Synopsis [Generates the random sequences for the initial population.]

Description [Generates the random sequences for the initial population. The sequences are permutations of the indices between lower and upper in the current order.]

SideEffects [None]

SeeAlso []

Definition at line 445 of file cuddGenetic.c.

00448 {
00449     int i,j;            /* loop variables */
00450     int *used;          /* is a number already in a permutation */
00451     int next;           /* next random number without repetitions */
00452 
00453     used = ALLOC(int,numvars);
00454     if (used == NULL) {
00455         table->errorCode = CUDD_MEMORY_OUT;
00456         return(0);
00457     }
00458 #if 0
00459 #ifdef DD_STATS
00460     (void) fprintf(table->out,"Initial population before sifting\n");
00461     for (i = 0; i < 2; i++) {
00462         for (j = 0; j < numvars; j++) {
00463             (void) fprintf(table->out," %2d",STOREDD(i,j));
00464         }
00465         (void) fprintf(table->out,"\n");
00466     }
00467 #endif
00468 #endif
00469     for (i = 2; i < popsize; i++) {
00470         for (j = 0; j < numvars; j++) {
00471             used[j] = 0;
00472         }
00473         /* Generate a permutation of {0...numvars-1} and use it to
00474         ** permute the variables in the layesr from lower to upper.
00475         */
00476         for (j = 0; j < numvars; j++) {
00477             do {
00478                 next = rand_int(numvars-1);
00479             } while (used[next] != 0);
00480             used[next] = 1;
00481             STOREDD(i,j) = table->invperm[next+lower];
00482         }
00483 #if 0
00484 #ifdef DD_STATS
00485         /* Print the order just generated. */
00486         for (j = 0; j < numvars; j++) {
00487             (void) fprintf(table->out," %2d",STOREDD(i,j));
00488         }
00489         (void) fprintf(table->out,"\n");
00490 #endif
00491 #endif
00492     }
00493     FREE(used);
00494     return(1);
00495 
00496 } /* end of make_random */

static int PMX ( int  maxvar  )  [static]

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

Synopsis [Returns the average fitness of the population.]

Description []

SideEffects [None]

SeeAlso []Function********************************************************************

Synopsis [Performs the crossover between two parents.]

Description [Performs the crossover between two randomly chosen parents, and creates two children, x1 and x2. Uses the Partially Matched Crossover operator.]

SideEffects [None]

SeeAlso []

Definition at line 790 of file cuddGenetic.c.

00792 {
00793     int         cut1,cut2;      /* the two cut positions (random) */
00794     int         mom,dad;        /* the two randomly chosen parents */
00795     int         *inv1;          /* inverse permutations for repair algo */
00796     int         *inv2;
00797     int         i;              /* loop vars */
00798     int         u,v;            /* aux vars */
00799 
00800     inv1 = ALLOC(int,maxvar);
00801     if (inv1 == NULL) {
00802         return(0);
00803     }
00804     inv2 = ALLOC(int,maxvar);
00805     if (inv2 == NULL) {
00806         FREE(inv1);
00807         return(0);
00808     }
00809 
00810     /* Choose two orders from the population using roulette wheel. */
00811     if (!roulette(&mom,&dad)) {
00812         FREE(inv1);
00813         FREE(inv2);
00814         return(0);
00815     }
00816 
00817     /* Choose two random cut positions. A cut in position i means that
00818     ** the cut immediately precedes position i.  If cut1 < cut2, we
00819     ** exchange the middle of the two orderings; otherwise, we
00820     ** exchange the beginnings and the ends.
00821     */
00822     cut1 = rand_int(numvars-1);
00823     do {
00824         cut2 = rand_int(numvars-1);
00825     } while (cut1 == cut2);
00826 
00827 #if 0
00828     /* Print out the parents. */
00829     (void) fprintf(table->out,
00830                    "Crossover of %d (mom) and %d (dad) between %d and %d\n",
00831                    mom,dad,cut1,cut2);
00832     for (i = 0; i < numvars; i++) {
00833         if (i == cut1 || i == cut2) (void) fprintf(table->out,"|");
00834         (void) fprintf(table->out,"%2d ",STOREDD(mom,i));
00835     }
00836     (void) fprintf(table->out,"\n");
00837     for (i = 0; i < numvars; i++) {
00838         if (i == cut1 || i == cut2) (void) fprintf(table->out,"|");
00839         (void) fprintf(table->out,"%2d ",STOREDD(dad,i));
00840     }
00841     (void) fprintf(table->out,"\n");
00842 #endif
00843 
00844     /* Initialize the inverse permutations: -1 means yet undetermined. */
00845     for (i = 0; i < maxvar; i++) {
00846         inv1[i] = -1;
00847         inv2[i] = -1;
00848     }
00849 
00850     /* Copy the portions whithin the cuts. */
00851     for (i = cut1; i != cut2; i = (i == numvars-1) ? 0 : i+1) {
00852         STOREDD(popsize,i) = STOREDD(dad,i);
00853         inv1[STOREDD(popsize,i)] = i;
00854         STOREDD(popsize+1,i) = STOREDD(mom,i);
00855         inv2[STOREDD(popsize+1,i)] = i;
00856     }
00857 
00858     /* Now apply the repair algorithm outside the cuts. */
00859     for (i = cut2; i != cut1; i = (i == numvars-1 ) ? 0 : i+1) {
00860         v = i;
00861         do {
00862             u = STOREDD(mom,v);
00863             v = inv1[u];
00864         } while (v != -1);
00865         STOREDD(popsize,i) = u;
00866         inv1[u] = i;
00867         v = i;
00868         do {
00869             u = STOREDD(dad,v);
00870             v = inv2[u];
00871         } while (v != -1);
00872         STOREDD(popsize+1,i) = u;
00873         inv2[u] = i;
00874     }
00875 
00876 #if 0
00877     /* Print the results of crossover. */
00878     for (i = 0; i < numvars; i++) {
00879         if (i == cut1 || i == cut2) (void) fprintf(table->out,"|");
00880         (void) fprintf(table->out,"%2d ",STOREDD(popsize,i));
00881     }
00882     (void) fprintf(table->out,"\n");
00883     for (i = 0; i < numvars; i++) {
00884         if (i == cut1 || i == cut2) (void) fprintf(table->out,"|");
00885         (void) fprintf(table->out,"%2d ",STOREDD(popsize+1,i));
00886     }
00887     (void) fprintf(table->out,"\n");
00888 #endif
00889 
00890     FREE(inv1);
00891     FREE(inv2);
00892     return(1);
00893 
00894 } /* end of PMX */

static int rand_int ( int  a  )  [static]

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

Synopsis [Generates a random number between 0 and the integer a.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 649 of file cuddGenetic.c.

00651 {
00652     return(Cudd_Random() % (a+1));
00653 
00654 } /* end of rand_int */

static int roulette ( int *  p1,
int *  p2 
) [static]

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

Synopsis [Selects two parents with the roulette wheel method.]

Description [Selects two distinct parents with the roulette wheel method.]

SideEffects [The indices of the selected parents are returned as side effects.]

SeeAlso []

Definition at line 910 of file cuddGenetic.c.

00913 {
00914     double *wheel;
00915     double spin;
00916     int i;
00917 
00918     wheel = ALLOC(double,popsize);
00919     if (wheel == NULL) {
00920         return(0);
00921     }
00922 
00923     /* The fitness of an individual is the reciprocal of its size. */
00924     wheel[0] = 1.0 / (double) STOREDD(0,numvars);
00925 
00926     for (i = 1; i < popsize; i++) {
00927         wheel[i] = wheel[i-1] + 1.0 / (double) STOREDD(i,numvars);
00928     }
00929 
00930     /* Get a random number between 0 and wheel[popsize-1] (that is,
00931     ** the sum of all fitness values. 2147483561 is the largest number
00932     ** returned by Cudd_Random.
00933     */
00934     spin = wheel[numvars-1] * (double) Cudd_Random() / 2147483561.0;
00935 
00936     /* Find the lucky element by scanning the wheel. */
00937     for (i = 0; i < popsize; i++) {
00938         if (spin <= wheel[i]) break;
00939     }
00940     *p1 = i;
00941 
00942     /* Repeat the process for the second parent, making sure it is
00943     ** distinct from the first.
00944     */
00945     do {
00946         spin = wheel[popsize-1] * (double) Cudd_Random() / 2147483561.0;
00947         for (i = 0; i < popsize; i++) {
00948             if (spin <= wheel[i]) break;
00949         }
00950     } while (i == *p1);
00951     *p2 = i;
00952 
00953     FREE(wheel);
00954     return(1);
00955 
00956 } /* end of roulette */

static int sift_up ( DdManager table,
int  x,
int  x_low 
) [static]

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

Synopsis [Moves one variable up.]

Description [Takes a variable from position x and sifts it up to position x_low; x_low should be less than x. Returns 1 if successful; 0 otherwise]

SideEffects [None]

SeeAlso []

Definition at line 513 of file cuddGenetic.c.

00517 {
00518     int        y;
00519     int        size;
00520 
00521     y = cuddNextLow(table,x);
00522     while (y >= x_low) {
00523         size = cuddSwapInPlace(table,y,x);
00524         if (size == 0) {
00525             return(0);
00526         }
00527         x = y;
00528         y = cuddNextLow(table,x);
00529     }
00530     return(1);
00531 
00532 } /* end of sift_up */


Variable Documentation

st_table* computed [static]

Definition at line 117 of file cuddGenetic.c.

int cross [static]

Definition at line 122 of file cuddGenetic.c.

char rcsid [] DD_UNUSED = "$Id: cuddGenetic.c,v 1.28 2004/08/13 18:04:48 fabio Exp $" [static]

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

FileName [cuddGenetic.c]

PackageName [cudd]

Synopsis [Genetic algorithm for variable reordering.]

Description [Internal procedures included in this file:

Static procedures included in this module:

The genetic algorithm implemented here is as follows. We start with the current DD order. We sift this order and use this as the reference DD. We only keep 1 DD around for the entire process and simply rearrange the order of this DD, storing the various orders and their corresponding DD sizes. We generate more random orders to build an initial population. This initial population is 3 times the number of variables, with a maximum of 120. Each random order is built (from the reference DD) and its size stored. Each random order is also sifted to keep the DD sizes fairly small. Then a crossover is performed between two orders (picked randomly) and the two resulting DDs are built and sifted. For each new order, if its size is smaller than any DD in the population, it is inserted into the population and the DD with the largest number of nodes is thrown out. The crossover process happens up to 50 times, and at this point the DD in the population with the smallest size is chosen as the result. This DD must then be built from the reference DD.]

SeeAlso []

Author [Curt Musfeldt, Alan Shuler, Fabio Somenzi]

Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado

All rights reserved.

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]

Definition at line 103 of file cuddGenetic.c.

int large [static]

Definition at line 119 of file cuddGenetic.c.

int numvars [static]

Definition at line 107 of file cuddGenetic.c.

int popsize [static]

Definition at line 106 of file cuddGenetic.c.

int* repeat [static]

Definition at line 118 of file cuddGenetic.c.

int result [static]

Definition at line 121 of file cuddGenetic.c.

int* storedd [static]

Definition at line 116 of file cuddGenetic.c.


Generated on Tue Jan 12 13:57:19 2010 for glu-2.2 by  doxygen 1.6.1