同一变量排序下的多OBDD合并算法

Multiple OBDD merging algorithm under same variable ordering

有序决策图(OBDD)是一种用于表示布尔表达式的数据结构,并在许多领域得到了广泛应用。在分布式或者动态环境下,利用已知布尔表达式的OBDD构造目标布尔表达式的OBDD是一个决定实际问题解决效率的关键问题。基于Shannon分解原理提出了一个同一变量排序下的OBDD合并算法。该算法首先建立目标布尔表达式的表存储模型,然后按照变量排序的逆序,依次处理各个变量,并且合并取值相同的行,直到所有变量处理完毕。

Ordered Binary Decision Diagrams（OBDD）is a Boolean function representation data structure, and has been applied in many fields. In dynamic or distribute environment, how to efficiently build OBDD of the target Boolean expres-sion form the known Boolean expression’s OBDD is a frequent encountered problem. Under identical variable ordering, this paper puts forward a OBDD merging algorithm based on Shannon decomposition principle. In the algorithm, it firstly establishes a storage table for the target Boolean expression, and then under the reverse variable ordering it handles each variable in turn, and combines the rows with same values, until all the variables are handled.