« 上一篇下一篇 »

使用BDD的Datalog的实现

二分决策图(Binary Decision Diagram,BDD)是一个用图来表示布尔函数的方法。因为对n个 变量有22n个布尔函数,没有哪种表示方法能够很简洁地表示所有的布尔函数。但是,在实践中出现的布尔函数常常具有很多规律。因此,们常常可以找到一个BDD来简洁地表示他们想要表示的布尔函数。

我们为了分析程序而开发了一些Datalog程序。事实表明,用这些Datalog程序描述的布尔函数也不例外,也可以使用BDD简洁地表示。BDD方法在实践中是相当成功的,虽然我们需要通过商业BDD操作程序包中的一些启发式规则或技术才可以找到用以表示程序信息的简洁的BDD。值得一提的是,它比使用传统数据库管理系统的方法具有更好的性能,因为传统数据库管理系统是为了在典型商业数据中出现的更加不规则的数据模式而设计的。

讨论经过多年开发才得到的所有BDD技术已经超出了本书的范围。我们将在这里介绍BDD的表示方法。然后,指出如何把一个关系数据表示成为BDD。在用算法来执行Dat-alog程序时需要进行某些运算。我们也指出了如何操作BDD来完成这些运算。最后,我们描述了如何在BDD中表示指数量级的上下文。这种表示法是在上下文相关性分析中成功应用BDD的关键。

二分决策图

一个BDD把一个布尔函数表示成为一个带根的DAG图。这个DAG的每个内部结点都用被表示函数的一个变量作为标号。在图的底部是两个叶子,一个标号为0,另一个标号为1。每个内部结点有两条指向子结点的边,这两条边分别称为“低边”和“高边”。低边对应于该结点对应变量取值为0时的情况,而高边对应于相应变量取值为1时的情况。

给定这些变量的一个真假赋值,我们可以从DAG的根开始确定函数的取值。在每个结点上,比如说标号为x的结点上,分别根据x的真假值为0或1来决定沿着相应的低边或高边前进。如果我们最后到达标号为1的叶结点,那么被表示的函数对于这个真假赋值取真值,否则该函数取假值。

« 上一篇下一篇 »