| The Binary Decision Diagrams is a description of data structure for Booleanfunction or combinational logic circuit, which is widely used in formal verification,such as combinational logic circuits, sequential logic circuit, as well as equivalencechecking, model checking. It is also used as the underlying data structure by manyCAD system in circuit design. However, in practice, it is heavily depended on therequired storage space, named BDD node size, while using the correlation algorithm.And the researchers found that, the BDD node sizes heavily depend on the ordering ofthe variables. Therefore, the research on variable ordering problem, can minizate thBDD nodes, and ti can alleviate the states explosion in model checking, whilch is veryimportant significance.The theory of BDD and the variable ordering is introduced, and that, a newadaptive catastrophe genetic algorithm is presented for minimizing the BinaryDecision Diagrams, inspired by the basic genetic algorithm. It can not onlydynamically adjust the probability of the crossover and mutation, whilch reduce thedependence on the initial parameters, while reducing the consumption of thealgorithm, but that it can increase the diversity of individuals without expanding thepopulation size, which can improve the local convergence. Furthermore, the algorithmhas good extensibility, it is easy to combine with other improvement strategiestogether, especially some algorithms that efficiently in local search, to improve theglobal advantage, because the evolutionary strategy does not affect the catastropheoccurred.Some benchmarks of the Uniform Random-3-SAT set are used for theexperimental evaluation, which reveals that the catastrophe algorithm proves betterresults than the basic genetic algorithm on global optimization and reduce the nodesize additionally by11%averagely and25%mostly. Furthermore, the catastropheadaptive algorithm reduce the node size additionally by12.82%averagely and26.9%mostly. |
PDF Full Text Request