• Complex
  • Title
  • Keyword
  • Abstract
  • Scholars
  • Journal
  • ISSN
  • Conference
搜索

Author:

苏开乐 (苏开乐.) | 吕关锋 (吕关锋.) | 宋炯 (宋炯.)

Indexed by:

EI Scopus PKU CSCD

Abstract:

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

Keyword:

二叉判定图 布尔函数 内存分配

Author Community:

  • [ 1 ] [苏开乐]浙江师范大学
  • [ 2 ] [吕关锋]北京工业大学
  • [ 3 ] [宋炯]浙江师范大学

Reprint Author's Address:

Email:

Show more details

Related Keywords:

Source :

计算机学报

ISSN: 0254-4164

Year: 2014

Issue: 9

Page: 2021-2026

Cited Count:

WoS CC Cited Count:

SCOPUS Cited Count:

ESI Highly Cited Papers on the List: 0 Unfold All

WanFang Cited Count: -1

Chinese Cited Count:

30 Days PV: 1

Affiliated Colleges:

Online/Total:520/5283738
Address:BJUT Library(100 Pingleyuan,Chaoyang District,Beijing 100124, China Post Code:100124) Contact Us:010-67392185
Copyright:BJUT Library Technical Support:Beijing Aegean Software Co., Ltd.