Investigation of a New Compressed Representation of Boolean Functions

布尔函数新压缩表示的研究

• 批准号: 9986308
• 负责人: Thomas Reps
• 金额: $ 20万
• 依托单位: University of Wisconsin-Madison
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2000
• 资助国家: 美国
• 起止时间: 2000-09-01 至 2006-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9986308&HistoricalAwards=false
• 关键词: Investigation; New; Compressed; Representation; Boolean

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.

CCR-9986308 威斯康星大学麦迪逊分校托马斯 W. 代表 对布尔函数新压缩表示的研究 拟议项目的目标是通过研究布尔函数新压缩表示（称为 CFLOBDD）的属性来推进符号模型检查的最新技术，CFLOBDD 是现在标准的有序二元决策图 (OBDD) 的替代方案。 CFLOBDD 具有 OBDD 的许多优良特性，但可以导致数据结构的大小大大减小——事实上，比 OBDD 小得多。 也就是说，OBDD 是一种数据结构，在最好的情况下，布尔函数表示的大小会呈指数减小（即与函数的决策树的大小相比）。 相比之下，CFLOBDD（同样，在最好的情况下）会导致布尔函数表示的大小呈双指数减小。 尽管并非每个布尔函数都具有如此高度压缩的表示形式，但该项目可以将这个想法推向多远。 人们希望双指数压缩是一种工具，它能够（a）允许更快地执行验证，并且（b）允许解决比迄今为止可能的更大的验证问题。