一个高效BDD的简洁实现

Succinct and Efficient Implementation of a BDD Package

二叉判定图BDD作为一种表示和操作布尔函数的数据结构,被广泛地应用在模型检测、系统验证等领域.在最坏情况下,BDD的空间规模是指数级的,因此为了设计和实现一个高效BDD包,研究者们做了大量技术性工作,同时涌现出多个高效BDD包.为了节省空间和提高运算速度,这些BDD包的实现都限定了一个较小的变量个数上限(不超过2^(16)),然而这种限定同时也限制了BDD包的适用性.为了突破这种限制,文中给出了一个高效的BDD包实现,该包在采纳了经典BDD包高效实现技术的同时,使用了内存分片分配、轻量级垃圾回收等技术.这些技术使得BDD包在保持高性能的情况下,将可处理的变量规模提高到2^(32),与现有BDD包的处理规模2^(16)相比,大大提高了BDD包的适用性.实验证明其性能非常接近可获得的最快的2^(16)变量规模的BDD包——CUDD.

As a data structure used for representing and manipulating Boolean functions, BDDs（Binary Decision Diagrams） are commonly used in many fields such as model checking, systemverification and so on. At the worst case, the space usage can reach exponential level; so manyresearchers have made a great deal of technical work on designing and implementing efficient BDDpackages. Up to today, many efficient BDD packages have been implemented. For saving spaceand improving manipulating speed, all these packages limit the number of variables to 216. How-ever, such a limitation also limits its applicability. In this paper, an efficient BDD package isproposed to break the limit of 216. This package not only adopts the technologies used in classicalBDD package implementation but also introduce some new techniques, such as sub-allocation ofmemory and lightweight garbage collection. Because of such effective scheme, the number ofvariables which BDD package can deal with reaches 232. Compared with other BDD packages withvariable number 216 , this BDD package can be more extensively used. Experiments show that itsperformance is nearly as the same as that of the best publicly available BDD package CUDD.