Variable Ordering of BDDs with Parallel Genetic Algorithms

摘要

Binary Decision Diagrams (BDDs) have proved to be a powerful representation for Boolean functions. More specifically, they form a data structure with an associated set of handling algorithms very useful for the automatic formal verification of digital circuits and other finite state systems. Nevertheless, the size of the BDD representation of these functions is highly dependent on the order of the function arguments, also called variables, and to find such good ordering has been shown to be a NP-Complete problem. In this work we present an heuristic based on Parallel Genetic Algorithms to solve this problem together with experimental results.