论文部分内容阅读
本文对有序二元决策图（ordered binary decision diagram，OBDD）进行了泛化，提出了一种新的知识编译语言—带蕴含文字的有序二元决策图（OBDD with impliedliterals，OBDD-L）。本文将OBDD-L上的蕴含文字约束为所有潜在的蕴含文字中对应变量最小的前i（0≤i≤∞）个文字而得到了子集OBDD-L_i，其中OBDD-L0同构于OBDD，进一步对OBDD-L_i附加精简性（reducedness）得到子集ROBDD-L_i。本文证明了在给定变量序下，任意命题知识库对应唯一的ROBDD-L_i（0≤i≤∞），其中ROBDD-L0和ROBDD-L_∞分别在所有OBDD-L0和OBDD-L_∞中节点数最少。本文证明了ROBDD-L_∞的简洁性严格强于ROBDD-L_i（0≤i <∞），且任意OBDD-L都能在多项式时间内转化为ROBDD-L_∞。本文提出了多个能为OBDD-L及其子集执行多项式时间逻辑操作的算法。本文证明了若ROBDD-L0能在其规模的多项式时间内支持某个操作，则ROBDD-L_∞也能在等价的ROBDD-L0的规模的多项式时间内支持该个操作，同时本文提出了一个ROBDD-L_∞合取算法，其时间复杂度最坏情况下不多于ROBDD-L0的合取算法的n倍（n表示变量数），但在某些情况下存在指数形式的加速。本文给出了一个ROBDD-L_i（0≤i≤∞）编译算法Build和ROBDD-L_∞编译算法BuildInfty，并结合OBDD-L支持的逻辑操作实现了OBDD-L包BDDjLu。实验结果表明，BDDjLu中的ROBDD-L_∞编译器的时间和空间效率与确定型可分解否定范式的编译器c2d相当，且优于已有的ROBDD编译器；BDDjLu中的ROBDD-L0编译器的时间效率在大部分问题上优于已有的ROBDD编译器。