BDD简介 ---1

BDD(Binary Decision Digrams)是最新流行于人工智能模型诊断方面的一种求解算法,主要用于诊断求解,配置和约束满足等方面,下面我将对BDD做一下简单的介绍.
    在学习BDD之前首先要有一点离散数学的基本概念,知道∧,∨,﹁,=>,<=>等基本符号的意义和各范式的表达,定义if-then-else 操作为:  x=>y0,y1 = (x∧y0) ∨(x∧y1)
所以x=>y0,y1 为真时当且仅当x ,y0同为真或x为假,y1为真.从这种if-then-else 操作演化来的形式被称作if-then-else Normal Form(INF).我们指定布尔表达式t[0/x],不难发现,对于t的山农扩展 t = x =>t[1/x],t[0/x] 是基于x的布尔值的,而对于任何的布尔表达式都可以转化为INF的表示方式.
例如:给定布尔表达式 t = (x1<=>y1) ∧(x2<=>y2) .我们可以通过对变量x1,x2,y1,y2的选择设定找到一个INF表达从而实现山农扩展.我们给定:
      t    =  x1  => t1  ,  t0
      t0   =  y1  => 0   ,  t00
      t1   =  y1  => t11  ,  0
      t00  =  x2  => t001 ,  t000
      t11  =  x2  => t111 ,  t110
      t000 =  y2 => 0 , 1
      t001 =  y2 => 1 ,0
      t110 =  y2 => 0 ,1
      t111 =  y2 => 1,0

               图1 决策树
    从上图我们可以看到决策树其实就是一个完全的二叉树,可以说是对所有可能性的一种枚举,但是不难发现,给定中很多变量取值都是相同的,如我们可以用t000取代t110…,而对于子表达式的等价取代我们就可以得到一个图,BDD(Binary Decision Digrams)图! 通过取代,我们可以得到:
      t    =  x1  => t1  ,  t0
      t0   =  y1  => 0   ,  t00
      t1   =  y1  => t00  ,  0
      t00  =  x2  => t001 ,  t000
      t000 =  y2 => 0 , 1
      t001 =  y2 => 1 ,0

    从而一个简单的BDD就出来了.