Investigation of a New Compressed Representation of Boolean Functions

CCR-9986308 威斯康星大学麦迪逊分校托马斯 W. 代表 对布尔函数新压缩表示的研究 拟议项目的目标是通过研究布尔函数新压缩表示（称为 CFLOBDD）的属性来推进符号模型检查的最新技术，CFLOBDD 是现在标准的有序二元决策图 (OBDD) 的替代方案。 CFLOBDD 具有 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.