一个高效BDD的简洁实现  

Succinct and Efficient Implementation of a BDD Package

作　　者：苏开乐[1,2] 吕关锋[3] 宋炯[1] 

机构地区：[1]浙江师范大学数理信息工程学院,浙江金华312004 [2]清华大学清华-阿姆斯特丹逻辑学联合研究中心,北京100084 [3]北京工业大学计算机学院,北京100022

出　　处：《计算机学报》2014年第9期2021-2026,共6页Chinese Journal of Computers

基　　金：国家“九七三”重点基础研究发展规划项目基金(2010CB328103);国家自然科学基金(60725207)资助~~

摘　　要：二叉判定图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.

关 键 词：二叉判定图 布尔函数 内存分配 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]