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

• 作者: 吕关锋 王倩 苏开乐 陈彩
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: BDD 一致性理论 可满足赋值算子
• 年，卷（期）: 2010,（9）
• 页码范围: 139-141,168
• 分类号: TP301
• 字数: 2265字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2010.09.036

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	苏开乐	北京大学信息科学技术学院	8	82	5.0	8.0
2	吕关锋	北京工业大学计算机学院	7	113	4.0	7.0
3	陈彩	北京工业大学计算机学院	12	58	4.0	7.0
4	王倩	北京工业大学计算机学院	5	14	3.0	3.0