Indexed by：
Abstract：
在很多应用领域中,我们都需要获取逻辑公式所有无冗余的可满足解集合,即集合中的任意两个解不能互相蕴涵.为了获取无冗余解集合,本文提出了两种实现方案.由于二叉决策图BDD具有对逻辑公式的高效表达特性,因此两种方案都是在逻辑公式转换成BDD的基础上实现的[1].一种方案是直接对该BDD进行遍历,获取从根节点到终端节点1的所有路径集合,然后借助一致性理论获取无冗余解的一致性算子的实现.另一种方案借助香农分解定理对BDD先进行逐层分解,然后对分解后的BDD再进行一致性运算的可满足赋值算子的实现.本文最后对两种方案的实验效果进行对比分析.
Keyword：
Reprint Author's Address：
Email：
Source ：
计算机工程与科学
ISSN： 1007-130X
Year： 2010
Issue： 9
Volume： 32
Page： 139-141,168
Cited Count：
WoS CC Cited Count： 0
SCOPUS Cited Count：
ESI Highly Cited Papers on the List： 0 Unfold All
WanFang Cited Count： -1
Chinese Cited Count：
30 Days PV： 12
Affiliated Colleges：
