10.3969/j.issn.1007-130X.2010.09.036
可满足赋值算子的设计与实现
在很多应用领域中,我们都需要获取逻辑公式所有无冗余的可满足解集合,即集合中的任意两个解不能互相蕴涵.为了获取无冗余解集合,本文提出了两种实现方案.由于二叉决策图BDD具有对逻辑公式的高效表达特性,因此两种方案都是在逻辑公式转换成BDD的基础上实现的[1].一种方案是直接对该BDD进行遍历,获取从根节点到终端节点1的所有路径集合,然后借助一致性理论获取无冗余解的一致性算子的实现.另一种方案借助香农分解定理对BDD先进行逐层分解,然后对分解后的BDD再进行一致性运算的可满足赋值算子的实现.本文最后对两种方案的实验效果进行对比分析.
BDD、一致性理论、可满足赋值算子
32
TP301(计算技术、计算机技术)
2010-11-25(万方平台首次上网日期,不代表论文的发表时间)
共4页
139-141,168