-
题名一个高效BDD的简洁实现
被引量:2
- 1
-
-
作者
苏开乐
吕关锋
宋炯
-
机构
浙江师范大学数理信息工程学院
清华大学清华-阿姆斯特丹逻辑学联合研究中心
北京工业大学计算机学院
-
出处
《计算机学报》
EI
CSCD
北大核心
2014年第9期2021-2026,共6页
-
基金
国家“九七三”重点基础研究发展规划项目基金(2010CB328103)
国家自然科学基金(60725207)资助~~
-
文摘
二叉判定图BDD作为一种表示和操作布尔函数的数据结构,被广泛地应用在模型检测、系统验证等领域.在最坏情况下,BDD的空间规模是指数级的,因此为了设计和实现一个高效BDD包,研究者们做了大量技术性工作,同时涌现出多个高效BDD包.为了节省空间和提高运算速度,这些BDD包的实现都限定了一个较小的变量个数上限(不超过2^(16)),然而这种限定同时也限制了BDD包的适用性.为了突破这种限制,文中给出了一个高效的BDD包实现,该包在采纳了经典BDD包高效实现技术的同时,使用了内存分片分配、轻量级垃圾回收等技术.这些技术使得BDD包在保持高性能的情况下,将可处理的变量规模提高到2^(32),与现有BDD包的处理规模2^(16)相比,大大提高了BDD包的适用性.实验证明其性能非常接近可获得的最快的2^(16)变量规模的BDD包——CUDD.
-
关键词
二叉判定图
布尔函数
内存分配
-
Keywords
binary decision diagram
Boolean function
memory allocation
-
分类号
TP301
[自动化与计算机技术—计算机系统结构]
-