Widening ROBDDs with Prime Implicants
Widening ROBDDs with Prime Implicants
复制标题
用素蕴涵拓宽 ROBDD
DOI：
--
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
Tadeusz Strzemecki
中科院分区：
文献类型：
--
作者：
N. Kettle;A. King;Tadeusz Strzemecki
尽管Robdds在程序分析中无处不在，并且有关ROBDD最小化的广泛文献，但对近似RobDD的工作仍缺乏工作。出现近似值的需求是因为许多ROBDD操作导致一个Robdd，其大小在输入的大小上是二次的。此外，如果在抽象解释中使用ROBDD，则分析的运行时间不仅与单个ROBDD操作的复杂性有关，还与应用的操作数量有关。依次，操作的数量受到布尔函数在实现稳定性之前可以削弱的次数的限制。本文提出了一种可以用来限制ROBDD的大小的扩大，还可以确保其弱化的次数受到给定常数的限制。延伸可用于系统地从上方（即得出较弱的函数）或以下（即推断功能更强大）。
Despite the ubiquity of ROBDDs in program analysis, and extensive literature on ROBDD minimisation, there is a dearth of work on approximating ROBDDs. The need for approximation arises because many ROBDD operations result in an ROBDD whose size is quadratic in the size of the inputs. Furthermore, if ROBDDs are used in abstract interpretation, the running time of the analysis is related not only to the complexity of the individual ROBDD operations but also the number of operations applied. The number of operations is, in turn, constrained by the number of times a Boolean function can be weakened before stability is achieved. This paper proposes a widening that can be used to both constrain the size of an ROBDD and also ensure that the number of times that it is weakened is bounded by some given constant. The widening can be used to either systematically approximate from above (i.e. derive a weaker function) or below (i.e. infer a stronger function).