Investigation of a New Compressed Representation of Boolean Functions

Ccr-9986308代表，托马斯·W·威斯康星大学麦迪逊分校布尔函数新的压缩表示的研究本项目的目标是通过研究一种称为CFLOBDDS的布尔函数的新的压缩表示的性质来推进符号模型检测的技术水平，CFLOBDDS是现在标准的有序二分决策图(OBDDS)的替代。CFLOBDDs具有许多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.