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

doi:10.3969/j.issn.1007130X.2010.

J4 ›› 2010, Vol. 32 ›› Issue (9): 139-141.doi: 10.3969/j.issn.1007130X.2010.

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

王倩1，陈彩1，吕关锋1，苏开乐2

（1.北京工业大学计算机学院，北京 100124;2.北京大学信息科学技术学院，北京 100871）

收稿日期:2010-03-14 修回日期:2010-06-12 出版日期:2010-09-02 发布日期:2010-09-02
作者简介:王倩(1985),女,河北保定人，硕士生，研究方向为计算机软件与理论；陈彩,硕士,副教授,研究方向为计算机软件与理论；吕关锋，博士，讲师，研究方向为模型检测和分布式计算；苏开乐，教授，研究方向为模型检测、知识推理与表达。

Design And Implementation of a Satisfiable Assignment Operator

WANG Qian1，CHEN Cai1，L Guanfeng1，SU Kaile2

(1.School of Computer Science,Beijing University of Technology,Beijing 100124;2.School of Information Science and Technology,Peking University,Beijing 100871,China）

Received:2010-03-14 Revised:2010-06-12 Online:2010-09-02 Published:2010-09-02

摘要/Abstract

摘要：

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

关键词: BDD, 一致性理论, 可满足赋值算子

Abstract:

In some applications, we need to obtain the set of all satisfiable assignments of a Boolean function, in which assignments can not imply each other. Therefore, we introduce two solutions based on the expression of BDD for the Boolean function. One of the solutions is the Consensus Operator. In order to do that, what we need to do is to obtain all the paths starting from the root node to the terminal node that is labeled with 1 because it is very trivial to see that every path represents a satisfiable assignment. Then we will get the unredundant assignment by the consensus law. The other solution is the satisfiable assignment operator. We need to to decompose BDD by the Shannon’s decomposition and then execute the consensus operator. Finally, the paper will present some of our experimental results for the two schemes respectively.

Key words: BDD;consensus law;satisfiable assignment operator

王倩1，陈彩1，吕关锋1，苏开乐2. 可满足赋值算子的设计与实现[J]. J4, 2010, 32(9): 139-141.

WANG Qian1，CHEN Cai1，L Guanfeng1，SU Kaile2. Design And Implementation of a Satisfiable Assignment Operator[J]. J4, 2010, 32(9): 139-141.

[1]	孟礼，武小悦. 带有互补边的共享OBDDs及数据结构[J]. J4, 2013, 35(1): 180-184.
[2]	史玉芳1，陆宁2，李慧民3. 基于改进的不交化最小路集的网络系统可靠性算法[J]. J4, 2011, 33(1): 31-35.

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

Design And Implementation of a Satisfiable Assignment Operator

PDF

可视化

摘要/Abstract

引用本文

使用本文

相关文章 2

编辑推荐

Metrics

本文评价