CAJ | 학술논문

二叉判定图BDD作为一种表示和操作布尔函数的数据结构，被广泛地应用在模型检测、系统验证等领域．在最坏情况下，BDD的空间规模是指数级的，因此为了设计和实现一个高效BDD包，研究者们做了大量技术性工作，同时涌现出多个高效BDD包．为了节省空间和提高运算速度，这些BDD包的实现都限定了一个较小的变量个数上限（不超过216），然而这种限定同时也限制了BDD包的适用性．为了突破这种限制，文中给出了一个高效的BDD包实现，该包在采纳了经典BDD包高效实现技术的同时，使用了内存分片分配、轻量级垃圾回收等技术．这些技术使得BDD包在保持高性能的情况下，将可处理的变量规模提高到232，与现有BDD包的处理规模216相比，大大提高了BDD包的适用性．实验证明其性能非常接近可获得的最快的216变量规模的BDD包---CUDD．
이차판정도BDD작위일충표시화조작포이함수적수거결구，피엄범지응용재모형검측、계통험증등영역．재최배정황하，BDD적공간규모시지수급적，인차위료설계화실현일개고효BDD포，연구자문주료대량기술성공작，동시용현출다개고효BDD포．위료절성공간화제고운산속도，저사BDD포적실현도한정료일개교소적변량개수상한（불초과216），연이저충한정동시야한제료BDD포적괄용성．위료돌파저충한제，문중급출료일개고효적BDD포실현，해포재채납료경전BDD포고효실현기술적동시，사용료내존분편분배、경량급랄급회수등기술．저사기술사득BDD포재보지고성능적정황하，장가처리적변량규모제고도232，여현유BDD포적처리규모216상비，대대제고료BDD포적괄용성．실험증명기성능비상접근가획득적최쾌적216변량규모적BDD포---CUDD．