一个高效犅犇犇的简洁实现

• 作者: 吕关锋 宋炯 苏开乐
• 来源期刊: 计算机学报
• 学科: 工学
• 关键词: 二叉判定图 布尔函数 内存分配
• 年，卷（期）: 2014,（9）
• 所属期刊栏目: 计算机科学理论
• 页码范围: 2021-2026
• 页数: 6页
• 分类号: TP301
• 字数: 5114字
• 语种: 中文
• DOI: 10.3724/SP.J.1016.2014.02021

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	吕关锋	北京工业大学计算机学院	7	113	4.0	7.0
2	宋炯	浙江师范大学数理信息工程学院	4	17	2.0	4.0