Binary Decision Diagrams with Edge-Specified Reductions
Binary Decision Diagrams with Edge-Specified Reductions
复制标题
具有指定边缘归约的二元决策图
DOI：
10.1007/978-3-030-17465-1_17
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Miner, Andrew
中科院分区：
文献类型：
--
作者：
Babar, Junaid;Jiang, Chuan;Ciardo, Gianfranco;Miner, Andrew
过去已经提出了各种版本的二进制决策图（bdd），不同的是需要赋予边跳过水平意义的约简规则。最广泛采用的是完全简化bdd和零抑制bdd，它们擅长编码不同类型的布尔函数（如果函数包含独立于一个或多个底层变量的子函数，或者当它的一个参数是非零时，它的值往往为零）。最近，提出了新的bdd类，以增加复杂性和每个节点更大的内存需求为代价，利用了这两种情况。我们引入了一种新的BDD类型，我们认为它在概念上更简单，在节点大小方面具有较小的内存需求，倾向于产生更少的节点，并且可以很容易地使用额外的约简规则进一步扩展。我们提出了一个正式的定义，证明了规范性，并提供了实验结果来支持我们的效率声明。
Various versions of binary decision diagrams (BDDs) have been proposed in the past, differing in the reduction rule needed to give meaning to edges skipping levels. The most widely adopted, fully-reduced BDDs and zero-suppressed BDDs, excel at encoding different types of boolean functions (if the function contains subfunctions independent of one or more underlying variables, or it tends to have value zero when one of its arguments is nonzero, respectively). Recently, new classes of BDDs have been proposed that, at the cost of some additional complexity and larger memory requirements per node, exploit both cases. We introduce a new type of BDD that we believe is conceptually simpler, has small memory requirements in terms of node size, tends to result in fewer nodes, and can easily be further extended with additional reduction rules. We present a formal definition, prove canonicity, and provide experimental results to support our efficiency claims.
二元决策图和零抑制决策图的链约简
DOI：
--
发表时间：
2017
期刊：
Journal of automated reasoning
影响因子：
--
作者：
R. Bryant
通讯作者：
R. Bryant
标记 BDD：组合来自不同决策图类型的约简规则
DOI：
--
发表时间：
2017
期刊：
Formal Methods in Computer-Aided Design
影响因子：
--
作者：
T. V. Dijk;R. Wille;R. Meolic
通讯作者：
R. Meolic