abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
cuddGenetic.c File Reference
#include "misc/util/util_hack.h"
#include "cuddInt.h"

Go to the source code of this file.

Macros

#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 (const 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
ABC_NAMESPACE_IMPL_START 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
 

Macro Definition Documentation

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

Definition at line 135 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 706 of file cuddGenetic.c.

709 {
710  int i;
711  int *intarray1, *intarray2;
712 
713  intarray1 = (int *) array1;
714  intarray2 = (int *) array2;
715 
716  for (i = 0; i < numvars; i++) {
717  if (intarray1[i] != intarray2[i]) return(1);
718  }
719  return(0);
720 
721 } /* end of array_compare */
static int numvars
Definition: cuddGenetic.c:111
static int array_hash ( const 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 674 of file cuddGenetic.c.

677 {
678  int val = 0;
679  int i;
680  int *intarray;
681 
682  intarray = (int *) array;
683 
684  for (i = 0; i < numvars; i++) {
685  val = val * 997 + intarray[i];
686  }
687 
688  return ((val < 0) ? -val : val) % modulus;
689 
690 } /* end of array_hash */
static int numvars
Definition: cuddGenetic.c:111
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 553 of file cuddGenetic.c.

558 {
559  int i,j; /* loop vars */
560  int position;
561  int index;
562  int limit; /* how large the DD for this order can grow */
563  int size;
564 
565  /* Check the computed table. If the order already exists, it
566  ** suffices to copy the size from the existing entry.
567  */
568  if (computed && st__lookup_int(computed,(char *)&STOREDD(num,0),&index)) {
569  STOREDD(num,numvars) = STOREDD(index,numvars);
570 #ifdef DD_STATS
571  (void) fprintf(table->out,"\nCache hit for index %d", index);
572 #endif
573  return(1);
574  }
575 
576  /* Stop if the DD grows 20 times larges than the reference size. */
577  limit = 20 * STOREDD(0,numvars);
578 
579  /* Sift up the variables so as to build the desired permutation.
580  ** First the variable that has to be on top is sifted to the top.
581  ** Then the variable that has to occupy the secon position is sifted
582  ** up to the second position, and so on.
583  */
584  for (j = 0; j < numvars; j++) {
585  i = STOREDD(num,j);
586  position = table->perm[i];
587  result = sift_up(table,position,j+lower);
588  if (!result) return(0);
589  size = table->keys - table->isolated;
590  if (size > limit) break;
591  }
592 
593  /* Sift the DD just built. */
594 #ifdef DD_STATS
595  (void) fprintf(table->out,"\n");
596 #endif
597  result = cuddSifting(table,lower,upper);
598  if (!result) return(0);
599 
600  /* Copy order and size to table. */
601  for (j = 0; j < numvars; j++) {
602  STOREDD(num,j) = table->invperm[lower+j];
603  }
604  STOREDD(num,numvars) = table->keys - table->isolated; /* size of new DD */
605  return(1);
606 
607 } /* end of build_dd */
static int sift_up(DdManager *table, int x, int x_low)
Definition: cuddGenetic.c:517
int cuddSifting(DdManager *table, int lower, int upper)
Definition: cuddReorder.c:508
int st__lookup_int(st__table *table, char *key, int *value)
Definition: st.c:134
static st__table * computed
Definition: cuddGenetic.c:121
unsigned int keys
Definition: cuddInt.h:369
FILE * out
Definition: cuddInt.h:441
static int numvars
Definition: cuddGenetic.c:111
static int size
Definition: cuddSign.c:86
int * invperm
Definition: cuddInt.h:388
static int result
Definition: cuddGenetic.c:125
int isolated
Definition: cuddInt.h:385
#define STOREDD(i, j)
Definition: cuddGenetic.c:135
int * perm
Definition: cuddInt.h:386
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 192 of file cuddGenetic.c.

196 {
197  int i,n,m; /* dummy/loop vars */
198  int index;
199 #ifdef DD_STATS
200  double average_fitness;
201 #endif
202  int small; /* index of smallest DD in population */
203 
204  /* Do an initial sifting to produce at least one reasonable individual. */
205  if (!cuddSifting(table,lower,upper)) return(0);
206 
207  /* Get the initial values. */
208  numvars = upper - lower + 1; /* number of variables to be reordered */
209  if (table->populationSize == 0) {
210  popsize = 3 * numvars; /* population size is 3 times # of vars */
211  if (popsize > 120) {
212  popsize = 120; /* Maximum population size is 120 */
213  }
214  } else {
215  popsize = table->populationSize; /* user specified value */
216  }
217  if (popsize < 4) popsize = 4; /* enforce minimum population size */
218 
219  /* Allocate population table. */
220  storedd = ABC_ALLOC(int,(popsize+2)*(numvars+1));
221  if (storedd == NULL) {
222  table->errorCode = CUDD_MEMORY_OUT;
223  return(0);
224  }
225 
226  /* Initialize the computed table. This table is made up of two data
227  ** structures: A hash table with the key given by the order, which says
228  ** if a given order is present in the population; and the repeat
229  ** vector, which says how many copies of a given order are stored in
230  ** the population table. If there are multiple copies of an order, only
231  ** one has a repeat count greater than 1. This copy is the one pointed
232  ** by the computed table.
233  */
234  repeat = ABC_ALLOC(int,popsize);
235  if (repeat == NULL) {
236  table->errorCode = CUDD_MEMORY_OUT;
237  ABC_FREE(storedd);
238  return(0);
239  }
240  for (i = 0; i < popsize; i++) {
241  repeat[i] = 0;
242  }
244  if (computed == NULL) {
245  table->errorCode = CUDD_MEMORY_OUT;
246  ABC_FREE(storedd);
247  ABC_FREE(repeat);
248  return(0);
249  }
250 
251  /* Copy the current DD and its size to the population table. */
252  for (i = 0; i < numvars; i++) {
253  STOREDD(0,i) = table->invperm[i+lower]; /* order of initial DD */
254  }
255  STOREDD(0,numvars) = table->keys - table->isolated; /* size of initial DD */
256 
257  /* Store the initial order in the computed table. */
258  if ( st__insert(computed,(char *)storedd,(char *) 0) == st__OUT_OF_MEM) {
259  ABC_FREE(storedd);
260  ABC_FREE(repeat);
262  return(0);
263  }
264  repeat[0]++;
265 
266  /* Insert the reverse order as second element of the population. */
267  for (i = 0; i < numvars; i++) {
268  STOREDD(1,numvars-1-i) = table->invperm[i+lower]; /* reverse order */
269  }
270 
271  /* Now create the random orders. make_random fills the population
272  ** table with random permutations. The successive loop builds and sifts
273  ** the DDs for the reverse order and each random permutation, and stores
274  ** the results in the computed table.
275  */
276  if (!make_random(table,lower)) {
277  table->errorCode = CUDD_MEMORY_OUT;
278  ABC_FREE(storedd);
279  ABC_FREE(repeat);
281  return(0);
282  }
283  for (i = 1; i < popsize; i++) {
284  result = build_dd(table,i,lower,upper); /* build and sift order */
285  if (!result) {
286  ABC_FREE(storedd);
287  ABC_FREE(repeat);
289  return(0);
290  }
291  if ( st__lookup_int(computed,(char *)&STOREDD(i,0),&index)) {
292  repeat[index]++;
293  } else {
294  if ( st__insert(computed,(char *)&STOREDD(i,0),(char *)(long)i) ==
295  st__OUT_OF_MEM) {
296  ABC_FREE(storedd);
297  ABC_FREE(repeat);
299  return(0);
300  }
301  repeat[i]++;
302  }
303  }
304 
305 #if 0
306 #ifdef DD_STATS
307  /* Print the initial population. */
308  (void) fprintf(table->out,"Initial population after sifting\n");
309  for (m = 0; m < popsize; m++) {
310  for (i = 0; i < numvars; i++) {
311  (void) fprintf(table->out," %2d",STOREDD(m,i));
312  }
313  (void) fprintf(table->out," : %3d (%d)\n",
314  STOREDD(m,numvars),repeat[m]);
315  }
316 #endif
317 #endif
318 
319  small = find_best();
320 #ifdef DD_STATS
321  average_fitness = find_average_fitness();
322  (void) fprintf(table->out,"\nInitial population: best fitness = %d, average fitness %8.3f",STOREDD(small,numvars),average_fitness);
323 #endif
324 
325  /* Decide how many crossovers should be tried. */
326  if (table->numberXovers == 0) {
327  cross = 3*numvars;
328  if (cross > 60) { /* do a maximum of 50 crossovers */
329  cross = 60;
330  }
331  } else {
332  cross = table->numberXovers; /* use user specified value */
333  }
334 
335  /* Perform the crossovers to get the best order. */
336  for (m = 0; m < cross; m++) {
337  if (!PMX(table->size)) { /* perform one crossover */
338  table->errorCode = CUDD_MEMORY_OUT;
339  ABC_FREE(storedd);
340  ABC_FREE(repeat);
342  return(0);
343  }
344  /* The offsprings are left in the last two entries of the
345  ** population table. These are now considered in turn.
346  */
347  for (i = popsize; i <= popsize+1; i++) {
348  result = build_dd(table,i,lower,upper); /* build and sift child */
349  if (!result) {
350  ABC_FREE(storedd);
351  ABC_FREE(repeat);
353  return(0);
354  }
355  large = largest(); /* find the largest DD in population */
356 
357  /* If the new child is smaller than the largest DD in the current
358  ** population, enter it into the population in place of the
359  ** largest DD.
360  */
361  if (STOREDD(i,numvars) < STOREDD(large,numvars)) {
362  /* Look up the largest DD in the computed table.
363  ** Decrease its repetition count. If the repetition count
364  ** goes to 0, remove the largest DD from the computed table.
365  */
367  &index);
368  if (!result) {
369  ABC_FREE(storedd);
370  ABC_FREE(repeat);
372  return(0);
373  }
374  repeat[index]--;
375  if (repeat[index] == 0) {
376  int *pointer = &STOREDD(index,0);
377  result = st__delete(computed, (const char **)&pointer, NULL);
378  if (!result) {
379  ABC_FREE(storedd);
380  ABC_FREE(repeat);
382  return(0);
383  }
384  }
385  /* Copy the new individual to the entry of the
386  ** population table just made available and update the
387  ** computed table.
388  */
389  for (n = 0; n <= numvars; n++) {
390  STOREDD(large,n) = STOREDD(i,n);
391  }
392  if ( st__lookup_int(computed,(char *)&STOREDD(large,0),
393  &index)) {
394  repeat[index]++;
395  } else {
396  if ( st__insert(computed,(char *)&STOREDD(large,0),
397  (char *)(long)large) == st__OUT_OF_MEM) {
398  ABC_FREE(storedd);
399  ABC_FREE(repeat);
401  return(0);
402  }
403  repeat[large]++;
404  }
405  }
406  }
407  }
408 
409  /* Find the smallest DD in the population and build it;
410  ** that will be the result.
411  */
412  small = find_best();
413 
414  /* Print stats on the final population. */
415 #ifdef DD_STATS
416  average_fitness = find_average_fitness();
417  (void) fprintf(table->out,"\nFinal population: best fitness = %d, average fitness %8.3f",STOREDD(small,numvars),average_fitness);
418 #endif
419 
420  /* Clean up, build the result DD, and return. */
422  computed = NULL;
423  result = build_dd(table,small,lower,upper);
424  ABC_FREE(storedd);
425  ABC_FREE(repeat);
426  return(result);
427 
428 } /* end of cuddGa */
static int large
Definition: cuddGenetic.c:123
void st__free_table(st__table *table)
Definition: st.c:81
static int * storedd
Definition: cuddGenetic.c:120
int st__delete(st__table *table, const char **keyp, char **value)
Definition: st.c:375
int st__insert(st__table *table, const char *key, char *value)
Definition: st.c:171
int size
Definition: cuddInt.h:361
int cuddSifting(DdManager *table, int lower, int upper)
Definition: cuddReorder.c:508
int populationSize
Definition: cuddInt.h:430
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
int st__lookup_int(st__table *table, char *key, int *value)
Definition: st.c:134
static st__table * computed
Definition: cuddGenetic.c:121
static int cross
Definition: cuddGenetic.c:126
st__table * st__init_table(st__compare_func_type compare, st__hash_func_type hash)
Definition: st.c:72
static int find_best(void)
Definition: cuddGenetic.c:736
unsigned int keys
Definition: cuddInt.h:369
static int build_dd(DdManager *table, int num, int lower, int upper)
Definition: cuddGenetic.c:553
static int array_hash(const char *array, int modulus)
Definition: cuddGenetic.c:674
FILE * out
Definition: cuddInt.h:441
static int numvars
Definition: cuddGenetic.c:111
static int array_compare(const char *array1, const char *array2)
Definition: cuddGenetic.c:706
int numberXovers
Definition: cuddInt.h:431
static int popsize
Definition: cuddGenetic.c:110
#define st__OUT_OF_MEM
Definition: st.h:113
static int largest(void)
Definition: cuddGenetic.c:624
#define ABC_FREE(obj)
Definition: abc_global.h:232
static int * repeat
Definition: cuddGenetic.c:122
int * invperm
Definition: cuddInt.h:388
static int result
Definition: cuddGenetic.c:125
int isolated
Definition: cuddInt.h:385
#define STOREDD(i, j)
Definition: cuddGenetic.c:135
Cudd_ErrorType errorCode
Definition: cuddInt.h:447
static int make_random(DdManager *table, int lower)
Definition: cuddGenetic.c:449
static int PMX(int maxvar)
Definition: cuddGenetic.c:794
static int find_best ( void  )
static

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

Synopsis [Returns the index of the fittest individual.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 736 of file cuddGenetic.c.

737 {
738  int i,small;
739 
740  small = 0;
741  for (i = 1; i < popsize; i++) {
742  if (STOREDD(i,numvars) < STOREDD(small,numvars)) {
743  small = i;
744  }
745  }
746  return(small);
747 
748 } /* end of find_best */
static int numvars
Definition: cuddGenetic.c:111
static int popsize
Definition: cuddGenetic.c:110
#define STOREDD(i, j)
Definition: cuddGenetic.c:135
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 624 of file cuddGenetic.c.

625 {
626  int i; /* loop var */
627  int big; /* temporary holder to return result */
628 
629  big = 0;
630  while (repeat[big] > 1) big++;
631  for (i = big + 1; i < popsize; i++) {
632  if (STOREDD(i,numvars) >= STOREDD(big,numvars) && repeat[i] <= 1) {
633  big = i;
634  }
635  }
636  return(big);
637 
638 } /* end of largest */
static int numvars
Definition: cuddGenetic.c:111
static int popsize
Definition: cuddGenetic.c:110
static int * repeat
Definition: cuddGenetic.c:122
#define STOREDD(i, j)
Definition: cuddGenetic.c:135
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 449 of file cuddGenetic.c.

452 {
453  int i,j; /* loop variables */
454  int *used; /* is a number already in a permutation */
455  int next; /* next random number without repetitions */
456 
457  used = ABC_ALLOC(int,numvars);
458  if (used == NULL) {
459  table->errorCode = CUDD_MEMORY_OUT;
460  return(0);
461  }
462 #if 0
463 #ifdef DD_STATS
464  (void) fprintf(table->out,"Initial population before sifting\n");
465  for (i = 0; i < 2; i++) {
466  for (j = 0; j < numvars; j++) {
467  (void) fprintf(table->out," %2d",STOREDD(i,j));
468  }
469  (void) fprintf(table->out,"\n");
470  }
471 #endif
472 #endif
473  for (i = 2; i < popsize; i++) {
474  for (j = 0; j < numvars; j++) {
475  used[j] = 0;
476  }
477  /* Generate a permutation of {0...numvars-1} and use it to
478  ** permute the variables in the layesr from lower to upper.
479  */
480  for (j = 0; j < numvars; j++) {
481  do {
482  next = rand_int(numvars-1);
483  } while (used[next] != 0);
484  used[next] = 1;
485  STOREDD(i,j) = table->invperm[next+lower];
486  }
487 #if 0
488 #ifdef DD_STATS
489  /* Print the order just generated. */
490  for (j = 0; j < numvars; j++) {
491  (void) fprintf(table->out," %2d",STOREDD(i,j));
492  }
493  (void) fprintf(table->out,"\n");
494 #endif
495 #endif
496  }
497  ABC_FREE(used);
498  return(1);
499 
500 } /* end of make_random */
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
FILE * out
Definition: cuddInt.h:441
static int numvars
Definition: cuddGenetic.c:111
static int popsize
Definition: cuddGenetic.c:110
#define ABC_FREE(obj)
Definition: abc_global.h:232
static int rand_int(int a)
Definition: cuddGenetic.c:653
int * invperm
Definition: cuddInt.h:388
#define STOREDD(i, j)
Definition: cuddGenetic.c:135
Cudd_ErrorType errorCode
Definition: cuddInt.h:447
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 794 of file cuddGenetic.c.

796 {
797  int cut1,cut2; /* the two cut positions (random) */
798  int mom,dad; /* the two randomly chosen parents */
799  int *inv1; /* inverse permutations for repair algo */
800  int *inv2;
801  int i; /* loop vars */
802  int u,v; /* aux vars */
803 
804  inv1 = ABC_ALLOC(int,maxvar);
805  if (inv1 == NULL) {
806  return(0);
807  }
808  inv2 = ABC_ALLOC(int,maxvar);
809  if (inv2 == NULL) {
810  ABC_FREE(inv1);
811  return(0);
812  }
813 
814  /* Choose two orders from the population using roulette wheel. */
815  if (!roulette(&mom,&dad)) {
816  ABC_FREE(inv1);
817  ABC_FREE(inv2);
818  return(0);
819  }
820 
821  /* Choose two random cut positions. A cut in position i means that
822  ** the cut immediately precedes position i. If cut1 < cut2, we
823  ** exchange the middle of the two orderings; otherwise, we
824  ** exchange the beginnings and the ends.
825  */
826  cut1 = rand_int(numvars-1);
827  do {
828  cut2 = rand_int(numvars-1);
829  } while (cut1 == cut2);
830 
831 #if 0
832  /* Print out the parents. */
833  (void) fprintf(table->out,
834  "Crossover of %d (mom) and %d (dad) between %d and %d\n",
835  mom,dad,cut1,cut2);
836  for (i = 0; i < numvars; i++) {
837  if (i == cut1 || i == cut2) (void) fprintf(table->out,"|");
838  (void) fprintf(table->out,"%2d ",STOREDD(mom,i));
839  }
840  (void) fprintf(table->out,"\n");
841  for (i = 0; i < numvars; i++) {
842  if (i == cut1 || i == cut2) (void) fprintf(table->out,"|");
843  (void) fprintf(table->out,"%2d ",STOREDD(dad,i));
844  }
845  (void) fprintf(table->out,"\n");
846 #endif
847 
848  /* Initialize the inverse permutations: -1 means yet undetermined. */
849  for (i = 0; i < maxvar; i++) {
850  inv1[i] = -1;
851  inv2[i] = -1;
852  }
853 
854  /* Copy the portions whithin the cuts. */
855  for (i = cut1; i != cut2; i = (i == numvars-1) ? 0 : i+1) {
856  STOREDD(popsize,i) = STOREDD(dad,i);
857  inv1[STOREDD(popsize,i)] = i;
858  STOREDD(popsize+1,i) = STOREDD(mom,i);
859  inv2[STOREDD(popsize+1,i)] = i;
860  }
861 
862  /* Now apply the repair algorithm outside the cuts. */
863  for (i = cut2; i != cut1; i = (i == numvars-1 ) ? 0 : i+1) {
864  v = i;
865  do {
866  u = STOREDD(mom,v);
867  v = inv1[u];
868  } while (v != -1);
869  STOREDD(popsize,i) = u;
870  inv1[u] = i;
871  v = i;
872  do {
873  u = STOREDD(dad,v);
874  v = inv2[u];
875  } while (v != -1);
876  STOREDD(popsize+1,i) = u;
877  inv2[u] = i;
878  }
879 
880 #if 0
881  /* Print the results of crossover. */
882  for (i = 0; i < numvars; i++) {
883  if (i == cut1 || i == cut2) (void) fprintf(table->out,"|");
884  (void) fprintf(table->out,"%2d ",STOREDD(popsize,i));
885  }
886  (void) fprintf(table->out,"\n");
887  for (i = 0; i < numvars; i++) {
888  if (i == cut1 || i == cut2) (void) fprintf(table->out,"|");
889  (void) fprintf(table->out,"%2d ",STOREDD(popsize+1,i));
890  }
891  (void) fprintf(table->out,"\n");
892 #endif
893 
894  ABC_FREE(inv1);
895  ABC_FREE(inv2);
896  return(1);
897 
898 } /* end of PMX */
static int roulette(int *p1, int *p2)
Definition: cuddGenetic.c:914
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
static int numvars
Definition: cuddGenetic.c:111
static int popsize
Definition: cuddGenetic.c:110
#define ABC_FREE(obj)
Definition: abc_global.h:232
static int rand_int(int a)
Definition: cuddGenetic.c:653
#define STOREDD(i, j)
Definition: cuddGenetic.c:135
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 653 of file cuddGenetic.c.

655 {
656  return(Cudd_Random() % (a+1));
657 
658 } /* end of rand_int */
long Cudd_Random(void)
Definition: cuddUtil.c:2702
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 914 of file cuddGenetic.c.

917 {
918  double *wheel;
919  double spin;
920  int i;
921 
922  wheel = ABC_ALLOC(double,popsize);
923  if (wheel == NULL) {
924  return(0);
925  }
926 
927  /* The fitness of an individual is the reciprocal of its size. */
928  wheel[0] = 1.0 / (double) STOREDD(0,numvars);
929 
930  for (i = 1; i < popsize; i++) {
931  wheel[i] = wheel[i-1] + 1.0 / (double) STOREDD(i,numvars);
932  }
933 
934  /* Get a random number between 0 and wheel[popsize-1] (that is,
935  ** the sum of all fitness values. 2147483561 is the largest number
936  ** returned by Cudd_Random.
937  */
938  spin = wheel[numvars-1] * (double) Cudd_Random() / 2147483561.0;
939 
940  /* Find the lucky element by scanning the wheel. */
941  for (i = 0; i < popsize; i++) {
942  if (spin <= wheel[i]) break;
943  }
944  *p1 = i;
945 
946  /* Repeat the process for the second parent, making sure it is
947  ** distinct from the first.
948  */
949  do {
950  spin = wheel[popsize-1] * (double) Cudd_Random() / 2147483561.0;
951  for (i = 0; i < popsize; i++) {
952  if (spin <= wheel[i]) break;
953  }
954  } while (i == *p1);
955  *p2 = i;
956 
957  ABC_FREE(wheel);
958  return(1);
959 
960 } /* end of roulette */
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
long Cudd_Random(void)
Definition: cuddUtil.c:2702
static int numvars
Definition: cuddGenetic.c:111
static int popsize
Definition: cuddGenetic.c:110
#define ABC_FREE(obj)
Definition: abc_global.h:232
#define STOREDD(i, j)
Definition: cuddGenetic.c:135
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 517 of file cuddGenetic.c.

521 {
522  int y;
523  int size;
524 
525  y = cuddNextLow(table,x);
526  while (y >= x_low) {
527  size = cuddSwapInPlace(table,y,x);
528  if (size == 0) {
529  return(0);
530  }
531  x = y;
532  y = cuddNextLow(table,x);
533  }
534  return(1);
535 
536 } /* end of sift_up */
int cuddNextLow(DdManager *table, int x)
Definition: cuddReorder.c:738
static int size
Definition: cuddSign.c:86
int cuddSwapInPlace(DdManager *table, int x, int y)
Definition: cuddReorder.c:761

Variable Documentation

st__table* computed
static

Definition at line 121 of file cuddGenetic.c.

int cross
static

Definition at line 126 of file cuddGenetic.c.

ABC_NAMESPACE_IMPL_START 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 107 of file cuddGenetic.c.

int large
static

Definition at line 123 of file cuddGenetic.c.

int numvars
static

Definition at line 111 of file cuddGenetic.c.

int popsize
static

Definition at line 110 of file cuddGenetic.c.

int* repeat
static

Definition at line 122 of file cuddGenetic.c.

int result
static

Definition at line 125 of file cuddGenetic.c.

int* storedd
static

Definition at line 120 of file cuddGenetic.c.