可满足赋值算子的设计与实现

摘要：

在很多应用领域中,我们都需要获取逻辑公式所有无冗余的可满足解集合,即集合中的任意两个解不能互相蕴涵.为了获取无冗余解集合,本文提出了两种实现方案.由于二叉决策图BDD具有对逻辑公式的高效表达特性,因此两种方案都是在逻辑公式转换成BDD的基础上实现的[1].一种方案是直接对该BDD进行遍历,获取从根节点到终端节点1的所有路径集合,然后借助一致性理论获取无冗余解的一致性算子的实现.另一种方案借助香农分解定理对BDD先进行逐层分解,然后对分解后的BDD再进行一致性运算的可满足赋值算子的实现.本文最后对两种方案的实验效果进行对比分析.

关键词：BDD、一致性理论、可满足赋值算子

所属期刊栏目：32

分类号：TP301(计算技术、计算机技术)

在线出版日期：2010-11-25（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：139-141,168