二分决策图（Binary Decision Diagram，BDD)是一个用图来表示布尔函数的方法。因为对n个 变量有22n个布尔函数，没有哪种表示方法能够很简洁地表示所有的布尔函数。但是，在实践中出现的布尔函数常常具有很多规律。因此，人们常常可以找到一个BDD来简洁地表示他们想要表示的布尔函数。
我们为了分析程序而开发了一些Datalog程序。事实表明，用这些Datalog程序描述的布尔函数也不例外，也可以使用BDD简洁地表示。BDD方法在实践中是相当成功的，虽然我们需要通过商业BDD操作程序包中的一些启发式规则或技术才可以找到用以表示程序信息的简洁的BDD。值得一提的是，它比使用传统数据库管理系统的方法具有更好的性能，因为传统数据库管理系统是为了在典型商业数据中出现的更加不规则的数据模式而设计的。
