论文部分内容阅读
BDD作为布尔函数的一种等价表示形式,最初被成功应用在模型检测、系统验证等领域。由于BDD所具有的压缩表示特点,使其作为一种重要的数据结构得到了越来越广泛的应用,如知识表达与推理、命题公式可满足问题(SAT)、安全协议验证等。该领域吸引了越来越多的研究者进行此项研究,也出现了多种BDD包,例如CUDD,More-BDD。
尽管BDD是对布尔函数的一种压缩表示方法,但对空间的需求仍然很高,最坏情况下可达到指数级;同时时间复杂度在最坏情况下也可达指数级。进一步提高BDD的性能依然存在很大的挑战性。现有的BDD包为了降低空间和时间复杂度,往往使用16位比特来表示变量,使得目前BDD包所能够支持的变量个数最多为216(65536)。但是此种方式很大程度上限制了BDD的应用范围,例如在命题公式可满足问题(SAT)领域,安全协议验证等多个问题中,为了提高处理速度和压缩空间,可能需要使用BDD作为处理工具。但这些问题的规模往往很大,很难将BDD作为处理工具,因此一个可处理大规模变量BDD包的高效设计和实现具有很好的应用价值。
本文以现有BDD包的高效实现技术为理论基础,设计并实现了一款可处理大规模变量(232)的BDD包——MiniBdd。随着处理规模的大幅度提高,性能必然会受到影响。如何解决空间消耗与性能之间矛盾,使得在提高处理规模的同时,而不影响BDD的运算性能是本文研究的重点。
针对此目标,本文主要做了以下几个方面的研究工作:
1.设计并实现了一个可处理大规模变量的高效BDD包。
2.研究了BDD包的高效实现技术,包括:ITE算子,唯一表,计算表,补边,垃圾回收机制。
3.研究了的高效内存管理机制在BDD包中的应用,包括:内存分片分配的节点管理方式和轻量级垃圾回收机制的实现。
4.设计并实现了动态唯一表。
5.设计并实现了可满足赋值算子:该算子可应用于获取布尔公式的所有不互相蕴含的本质解。