发表机构
College of Computer Science, Nankai University; Arclight Quantum Computing Inc.; Key Laboratory of System Software (Chinese Academy of Sciences); Institute of Software, Chinese Academy of Sciences（南开大学计算机学院; 光量子计算有限公司; 中国科学院系统软件重点实验室; 中国科学院软件研究所）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
提出XBDD，一种引入逐边变量翻转映射的高度优化ROBDD，通过合并局部极性不同的节点减少节点数，实现指数级压缩，并以可控时间成本换取显著空间收益。
AI 中文摘要
简化有序二元决策图（ROBDD）是布尔函数的规范表示形式，广泛用于组合电路的等价性检查和可满足性检查等任务。经典的ROBDD软件包通过一系列优化技术极大地提高了构建ROBDD的效率，并通过补边压缩了ROBDD的节点规模。然而，现有实现未考虑同构布尔函数的局部极性差异，仍为每种极性组合生成一个不同的节点，从而导致节点数量爆炸。本文提出XBDD，一种高度优化的ROBDD，在完全实现补边及其配套工程技术的基础上，引入了逐边变量翻转映射。XBDD为每条边附加一个翻转映射，以指示当沿该边遍历时哪些输入变量必须被取反。这使得仅在局部输入极性上不同的节点可以被合并，进一步减少节点数量。对于某些函数族，这种共享甚至产生指数级压缩。我们还提出了使用位图和映射池的方法，以大幅减少映射带来的额外开销，并提出了映射的规范化和余因子算子。此外，XBDD实现了其他几项工程优化，以进一步提高时间和空间效率。实验表明，XBDD以可控的时间成本换取了显著的空间收益，验证了逐边变量翻转映射的有效性。
英文摘要
The Reduced Ordered Binary Decision Diagram (ROBDD) is a canonical representation of Boolean functions and is widely used in tasks such as equivalence checking and satisfiability checking of combinational circuits. Classical ROBDD packages greatly improve the efficiency of building ROBDDs through a series of optimization techniques, and compress the node scale of the ROBDD through complement edges. However, existing implementations do not take into account the local polarity differences of isomorphic Boolean functions, and still produce a distinct node for each polarity combination, thereby causing an explosion in the number of nodes. This paper proposes XBDD, a highly optimized ROBDD that, on the basis of fully implementing complement edges and their accompanying engineering techniques, introduces a per-edge variable-flip map. XBDD attaches a flip map to each edge to indicate which input variables must be negated when that edge is followed. This allows nodes that differ only in local input polarities to be merged, further reducing the node count. For certain function families, this sharing even yields exponential compression. We also propose methods that use a bitmap and a map pool to substantially reduce the extra overhead brought by the map, and propose normalization and cofactor operators for the map. In addition, XBDD implements several other engineering optimizations to further improve both time and space efficiency. Experiments show that XBDD trades a controllable time cost for a significant space gain, validating the effectiveness of the per-edge variable-flip map.
