Chain Reduction for Binary and Zero-Suppressed Decision Diagrams
Chain Reduction for Binary and Zero-Suppressed Decision Diagrams
复制标题
二元决策图和零抑制决策图的链约简
DOI：
--
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
R. Bryant
中科院分区：
文献类型：
--
作者：
R. Bryant
链归约使简化的有序二元决策图（BDD）和零抑制二元决策图（ZDD）能够利用对方的能力，以紧凑的形式符号化地表示布尔函数。对于任何布尔函数，它的链简化ZDD（CZDD）表示将不会大于它的ZDD表示，并且最多是它的BDD表示的两倍。一个函数的链约化BDD（CBDD）不会大于它的BDD表示，最多是它的CZDD表示的三倍。对BDD和ZDD上操作的标准算法的扩展使它们能够在链减少的版本上操作。代表性的基准编码的单词列表，解决组合问题，并在数字电路上操作的实验评估表明，链减少可以提供显着的好处，在内存和执行时间。实验结果进一步验证了一个量化模型的决策图如何编码时的序列集的规模。这个模型解释了为什么序列中符号的独热编码加上集合的CBDD、CZDD或ZDD表示的组合会产生最紧凑的形式。
Chain reduction enables reduced ordered binary decision diagrams (BDDs) and zero-suppressed binary decision diagrams (ZDDs) to each take advantage of the other’s ability to symbolically represent Boolean functions in compact form. For any Boolean function, its chain-reduced ZDD (CZDD) representation will be no larger than its ZDD representation, and at most twice the size of its BDD representation. The chain-reduced BDD (CBDD) of a function will be no larger than its BDD representation, and at most three times the size of its CZDD representation. Extensions to the standard algorithms for operating on BDDs and ZDDs enable them to operate on the chain-reduced versions. Experimental evaluations on representative benchmarks for encoding word lists, solving combinatorial problems, and operating on digital circuits indicate that chain reduction can provide significant benefits in terms of both memory and execution time. The experimental results are further validated by a quantitative model of how decision diagrams scale when encoding sets of sequences. This model explains why the combination of a one-hot encoding of the symbols in the sequences, plus a CBDD, CZDD, or ZDD representation of the set, yields the most compact form.
具有指定边缘归约的二元决策图
DOI：
10.1007/978-3-030-17465-1_17
发表时间：
2019
期刊：
Tools and Algorithms for the Construction and Analysis of Systems
影响因子：
--
作者：
Babar, Junaid;Jiang, Chuan;Ciardo, Gianfranco;Miner, Andrew
通讯作者：
Miner, Andrew