Hits :

First Author : 苏开乐

Affiliation of Author(s): 数理与信息工程学院

Date of Publication : 2014-01-01

Document Type : 期刊

Journal : 计算机学报

Volume: 第37卷

Issue : 第9期

Page Number : 2021-2026

ISSN : 0254-4164

Translation or Not : no

Key Words : 二叉判定图；布尔函数；内存分配

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