A Technique for Reordering Variables in an SBDD to Reduce the Size of BDD
简化BDD的SBDD和变量重排序结合算法

Binary Decision Diagram is a graph-based data structure for representing Boolean function. They have found widespread use in computer-aided design and in formal verification of digital circuits. We mainly investigate how to store BDD and to reduce the size of BDD. Firstly, we mainly introduce some background knowledge about Binary Decision Diagrams (BDD) in this paper. Secondly, we describe the ITE algorithm. Finally, we provide a technique for reordering variables in an SBDD to reduce the size of BDD.