SVF
Macros | Functions | Variables
cuddGenetic.c File Reference
#include "CUDD/util.h"
#include "CUDD/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 (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.30 2012/02/05 01:07:18 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

◆ STOREDD

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

Definition at line 131 of file cuddGenetic.c.

Function Documentation

◆ array_compare()

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

708 {
709  int i;
710  int *intarray1, *intarray2;
711 
712  intarray1 = (int *) array1;
713  intarray2 = (int *) array2;
714 
715  for (i = 0; i < numvars; i++) {
716  if (intarray1[i] != intarray2[i]) return(1);
717  }
718  return(0);
719 
720 } /* end of array_compare */
static int numvars
Definition: cuddGenetic.c:107

◆ array_hash()

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

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

◆ build_dd()

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

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

◆ cuddGa()

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.

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

◆ find_best()

static int find_best ( void  )
static

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

Synopsis [Returns the index of the fittest individual.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 735 of file cuddGenetic.c.

736 {
737  int i,small;
738 
739  small = 0;
740  for (i = 1; i < popsize; i++) {
741  if (STOREDD(i,numvars) < STOREDD(small,numvars)) {
742  small = i;
743  }
744  }
745  return(small);
746 
747 } /* end of find_best */
static int numvars
Definition: cuddGenetic.c:107
static int popsize
Definition: cuddGenetic.c:106
#define STOREDD(i, j)
Definition: cuddGenetic.c:131

◆ largest()

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

624 {
625  int i; /* loop var */
626  int big; /* temporary holder to return result */
627 
628  big = 0;
629  while (repeat[big] > 1) big++;
630  for (i = big + 1; i < popsize; i++) {
631  if (STOREDD(i,numvars) >= STOREDD(big,numvars) && repeat[i] <= 1) {
632  big = i;
633  }
634  }
635  return(big);
636 
637 } /* end of largest */
static int numvars
Definition: cuddGenetic.c:107
static int popsize
Definition: cuddGenetic.c:106
static int * repeat
Definition: cuddGenetic.c:118
#define STOREDD(i, j)
Definition: cuddGenetic.c:131

◆ make_random()

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

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

◆ PMX()

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

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

◆ rand_int()

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

654 {
655  return(Cudd_Random() % (a+1));
656 
657 } /* end of rand_int */
long Cudd_Random(void)
Definition: cuddUtil.c:2710

◆ roulette()

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

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

◆ sift_up()

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

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

Variable Documentation

◆ computed

st_table* computed
static

Definition at line 117 of file cuddGenetic.c.

◆ cross

int cross
static

Definition at line 122 of file cuddGenetic.c.

◆ DD_UNUSED

char rcsid [] DD_UNUSED = "$Id: cuddGenetic.c,v 1.30 2012/02/05 01:07:18 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-2012, 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.

◆ large

int large
static

Definition at line 119 of file cuddGenetic.c.

◆ numvars

int numvars
static

Definition at line 107 of file cuddGenetic.c.

◆ popsize

int popsize
static

Definition at line 106 of file cuddGenetic.c.

◆ repeat

int* repeat
static

Definition at line 118 of file cuddGenetic.c.

◆ result

int result
static

Definition at line 121 of file cuddGenetic.c.

◆ storedd

int* storedd
static

Definition at line 116 of file cuddGenetic.c.