Investigation of a New Compressed Representation of Boolean Functions

代表，Thomas W.威斯康星大学麦迪逊分校布尔函数新压缩表示的研究提议项目的目标是通过研究布尔函数的新压缩表示（称为cflobdd）的特性来推进符号模型检查的最新技术，cflobdd是现在标准的有序二进制决策图（obdd）的替代方案。cflobdd具有obdd的许多优良特性，但是可以产生比obdd小得多的数据结构——实际上比obdd要小得多。也就是说，OBDD是一种数据结构，在最好的情况下，它会产生布尔函数表示大小的指数减少（即，与函数的决策树的大小相比）。相比之下，CFLOBDD（同样是在最好的情况下）在布尔函数表示的大小上产生双倍指数级的减少。虽然不是每个布尔函数都具有如此高度压缩的表示，但该项目将看看这种想法可以推进到什么程度。希望双指数压缩是一种工具，它将(a)允许更快地执行验证，并且(b)允许攻击比迄今为止可能的更大的验证问题。

CCR-9986308 Reps, Thomas W. University of Wisconsin-Madison Investigation of a New Compressed Representation of Boolean Functions The goal of the proposed project is to advance the state of the art in symbolic model checking by investigating the properties of a new compressed representation of Boolean functions, called CFLOBDDs, which are an alternative to the now-standard Ordered Binary Decision Diagrams (OBDDs). CFLOBDDs share many of the good properties of OBDDs, but can lead to data structures of drastically smaller size -- exponentially smaller than OBDDs, in fact. That is, an OBDD is a data structure that -- in the best case -- yields an exponential reduction in the size of the representation of a Boolean function (i.e., compared with the size of the decision tree for the function). In contrast, a CFLOBDD -- again, in the best case -- yields a doubly exponential reduction in the size of the representation of a Boolean function. Although not every Boolean function has such a highly compressed representation, the project with see how far this idea can be pushed. The hope is that doubly-exponential compression is a tool that would (a) permit verification to be performed much faster, and (b) allow much larger verification problems to be attacked than has heretofore been possible.