OBDD转化为ROBDD

从普通有向无环图（Orderly Binary Decision Diagram，简称OBDD）转换成有序有向无环图（Reduced Ordered Binary Decision Diagram，简称ROBDD）的过程叫做OBDD的有序化。有序化的目标是消除多余的分支和节点，使得BDD更易于表示和分析，同时保持等价性。

以下是主要步骤：

1. **识别同构子树**：首先，通过比较节点的子节点结构，找到所有相同的子树。这是通过比较节点的`high`和`low`属性来实现的，如果两个子节点的结构完全一样，那么这两个节点就是同构的。

2. **标记已访问节点**：使用一个哈希表或者其他数据结构，如栈或队列，记录哪些节点已经被处理过，避免重复查找同构节点。

3. **合并同构节点**：对于每个同构节点，创建一个新的节点作为代表，将所有同构节点的`high`和`low`指向这个新的节点。这样做的目的是减少重复的决策路径，提高BDD的压缩程度。

4. **去除冗余节点**：遍历整个BDD，检查是否存在节点的子节点都是相同的叶子节点（也就是说，无论选择左边还是右边，最终都会到达同一个结果）。这样的节点被称为冗余节点，应该被删除。删除时，只需保留其中一个子节点，并更新其父节点的引用即可。

5. **确保顺序一致性**：最后一步是按照变量的顺序重新排列BDD，这样就得到了一个有序的BDD（ROBDD）。这是因为ROBDD的每个节点都有一个确定的变量，所以可以在变量的自然顺序下进行遍历。

6. **更新节点ID**：在重构过程中，确保给每个节点分配正确的ID，以便在生成DOT文件时正确地标记节点。

通过这些步骤，原始的OBDD会被转换成一个更紧凑、有序的形式，方便后续的分析和计算。注意，这个过程可能涉及复杂的循环和递归，因为需要反复检查和合并节点直到达到最优化状态。