• 中国计算机学会会刊
  • 中国科技核心期刊
  • 中文核心期刊
论文

Design And Implementation of a Satisfiable Assignment Operator

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

Received date: 2010-03-14

  Revised date: 2010-06-12

  Online published: 2010-09-02

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.

Cite this article

WANG Qian1,CHEN Cai1,L Guanfeng1,SU Kaile2 . Design And Implementation of a Satisfiable Assignment Operator[J]. Computer Engineering & Science, 2010 , 32(9) : 139 -141 . DOI: 10.3969/j.issn.1007130X.2010.

Outlines

/