ABSTRACT

OBDD is an effective graphical representation of Boolean functions. The OBDD orders of a Boolean function are sensitive to the order of Boolean variables. In this paper, the Boolean functions of DNF type and CNF type are studied. The exact OBDD order values of these two types of functions in a particular variables order are given and the conclusion is proved.

Keywords:OBDD, Variable Order, DNF, CNF, Boolean Function

两类布尔函数的OBDD阶

张媛，江建国，胡晓璐

辽宁师范大学数学学院，辽宁 大连

收稿日期：2018年12月4日；录用日期：2018年12月20日；发布日期：2018年12月27日

摘 要

OBDD是布尔函数的一种有效的图形化表示形式。布尔函数的OBDD的阶数对布尔变量的序敏感。本文研究了DNF型和CNF型两种类型布尔函数，给出了这两类函数在一种特定变量序下的OBDD阶的准确值，并证明了这个结论。

关键词 :OBDD，变量序，DNF，CNF，布尔函数

Copyright © 2018 by authors and Hans Publishers Inc.

This work is licensed under the Creative Commons Attribution International License (CC BY).

http://creativecommons.org/licenses/by/4.0/

1. 引言

在多种硬件和软件系统中，布尔函数是一种重要的形式描述机制。布尔函数的有效表示是描述系统的关键。真值表和命题公式是布尔函数的两种表示形式。利用真值表能够显示的表示布尔函数，该方法虽运算简单但在空间方面却相当低效。命题公式通常能得到更有效紧凑的布尔函数形式，但判断任意命题公式的可满足性是及其困难的。CNF、DNF作为命题公式的子类，可以直接检测可满足性问题，却没有检测有效性的算法 [1] 。

二叉判定图(BDD)是另一种布尔函数的有效表示方法 [2] ，其特定类为符号模型检测算法提供实现框架，使得在模型检测中遇到的状态空间爆炸问题得以缓解 [3] [4] [5] 。为了进一步优化布尔函数的表示，Bryant等提出了一种自底向上的压缩算法。该方法通过冗余消除、合并同构树等方式将二叉判定图压缩成有序二叉判定图(OBDD) [6] [7] 。

有序二叉判定图是布尔函数的一种紧凑的规范化表示。相比以上布尔函数表示方法，它所需的存储空间小，运算效率高。在多种应用中，OBDD已被证明可以非常有效的表达和操作布尔函数 [8] [9] 。然而OBDD非常依赖变量序的选择，改变变量序有可能使得OBDD的阶数呈指数增长，因此寻找一个好的变量序对于建立布尔函数的高效判定图是至关重要的。

寻找变量最优序已被证明是NP-完备问题 [10] ，但仍存在一些良好的启发式算法可以给出较好的排序。目前变量排序方法主要分为两大类，一类是动态变量排序，另一类是静态变量启发式排序 [11] 。动态变量排序包含筛选排序算法、窗口置换排序算法、模拟退火排序算法和遗传排序算法等 [12] [13] 。动态排序与静态排序虽然分别在变量序的有效性和时间耗费上各具优势，然而目前却没有能够兼顾有效性和时间耗费的优越算法。

本文针对OBDD的阶强烈的依赖于变量序的选择这一缺陷，研究改变变量序对OBDD阶的影响因素，通过影响因素呈现的规律给出特定函数的变量排序方法。并在此基础上研究发现，两种类型布尔函数在给定序下的OBDD阶等于其变量数与终止结点数之和。

2. 基本概念

2.1. 布尔函数及其表示

定义1 布尔变量x是定义域为 $\left\{0,1\right\}$ 的变量。记x，y为布尔变量。定义集合 $\left\{0,1\right\}$ 上的函数如下：

1) $\bar{0}\triangleq 1$ 和 $\bar{1}\triangleq 0$ ；

2) 若 $x=y=1$ ，则 $x\cdot y\triangleq 1$ ；否则 $x\cdot y\triangleq 0$ ；

3) 若 $x=y=0$ ，则 $x+y\triangleq 0$ ；否则；

4) 若x和y恰有一个等于1，则 $x\oplus y\triangleq 1$ 。

n元布尔函数f是从 ${\left\{0,1\right\}}^n$ 到 ${\left\{0,1\right\}}^n$ 满足以上布尔运算的函数。基于布尔函数的结构特征，本文主要对两类布尔函数进行研究。一类是积和形式的DNF型布尔函数 $f={\displaystyle \underset{i=1}{\overset{n}{\sum }}{\displaystyle \underset{j=1}{\overset{n}{\prod }}{x}_{ij}}}\left(n,m\in N^{+}\right)$ ，另一类是和积形式的CNF型布尔函数 $g={\displaystyle \underset{i=1}{\overset{n}{\prod }}{\displaystyle \underset{j=1}{\overset{n}{\sum }}{x}_{ij}}}\left(n,m\in N^{+}\right)$ 。

二叉判定图是布尔函数的一种比较高效紧凑的表示方法，二叉判定树是其中一种较简单的图结构。

定义2 设T是一棵有限二叉判定树。满足如下规则，T确定以非终止结点为变量的唯一布尔函数。给定T中出现的布尔变量赋值0和1，从T的根开始，只要当前结点的变量值为0，则沿虚线走；否则沿实线走。函数值为所到达的终点值。

二叉判定树通过共享结点以及子图的简化方式得到BDD。如图1中左图表示一棵二叉判定树，右图表示由该二叉判定树消除冗余决策点得到的二叉判定图。

图1. 布尔函数的二叉判定树和二叉判定图

定义3 二叉判定图(Binary Decision Diagrams，简称BDD)是一个有限有向无环图G，满足以下条件：

1) 具有唯一初始结点；

2) 由布尔变量标记的非终止结点u恰有两条指向其他结点的边，且两条边分别由函数 $low\left(u\right)$ 和 $high\left(u\right)$ 表示(在G中，虚线表示 $low\left(u\right)$ ，实线表示 $high\left(u\right)$ 。)。变量 $var\left(u\right)$ 对应任意一个结点u。

3) 所有终止结点标记为0或1。

随着检测需求的提高，研究发现由BDD表示布尔函数仍然存在着一些缺陷，比如对于两个判定图是否代表同一布尔函数的算法相当复杂。因此通过给变量排序，消除冗余等方法得到一种更规范紧凑的表示形式，由此有序二叉判定图应运而生。

定义4 有序二叉判定图(Ordered Binary Decision Diagrams，简称OBDD)是任意路径变量排序一致的BDD。若G表示n元布尔函数的BDD，当图G中任意路径上的变量都满足 $x_1\prec x_2\prec \cdots \prec x_n$ 时，称G是以 $x_1\prec x_2\prec \cdots \prec x_n$ 为变量序的OBDD。G中所有结点个数之和称为OBDD的阶，用 $\left|G\right|$ 表示。

OBDD表示布尔函数相比BDD具有相当显著的优势，即能更紧凑规范的表示布尔函数，操作运算存在比较有效的算法，并具有唯一性。

2.2. 变量序对OBDD尺寸的影响

根据定义4，给出如下布尔函数 $f=x_1\cdot x_2+x_3\cdot x_4+x_5\cdot x_6$ 分别在序 $x_1\prec x_2\prec x_3\prec x_4\prec x_5\prec x_6$ 和 $x_1\prec x_4\prec x_2\prec x_5\prec x_3\prec x_6$ 下的OBDD。如图2，f在序 $x_1\prec x_2\prec x_3\prec x_4\prec x_5\prec x_6$ 下OBDD (图2左图)的阶 $\left|G_1\right|=8$ ，在序 $x_1\prec x_4\prec x_2\prec x_5\prec x_3\prec x_6$ 下OBDD (图2右图)的阶 $\left|G_2\right|=16$ 。图 $G_2$ 的阶比图 $G_1$ 的阶多8个。

推广到一般情况，取布尔函数 $f=x_1\cdot y_1+x_2\cdot y_2+\cdots +x_n\cdot y_n$ ，则f在序 $x_1\prec y_1\prec x_2\prec y_2\prec \cdots \prec x_n\prec y_n$ 下的OBDD阶数是 $2n+2$ 。布尔函数f在两个变量序下的阶可根据命题1推理得到。若不幸选择序 $x_1\prec x_2\prec \cdots \prec x_n\prec y_1\prec y_2\prec \cdots \prec y_n$ ，f的OBDD阶是 $2^{n+1}$ 。

通过以上示例分析，变量序对OBDD的影响是显著的，一个好的变量序可以使布尔函数对应的OBDD更紧凑，从而减少空间的占用。而如果不幸选择了坏序，则OBDD的阶可能随变量数增多呈指数增长。因此选择一个合适的变量序来构造布尔函数的OBDD显得尤为重要。

图2. OBDD尺寸依赖于变量序的示例

根据变量的排序对OBDD阶的影响以及选择好的变量序的重要性，在构造布尔函数的OBDD之前，本文首先介绍确定一类特定变量排序的方法。为了更方便快速的得到好的变量序，使得OBDD的阶是多项式相关的，本文基于积和形式布尔函数与和积形式布尔函数结构特点，得到以下变量排序策略：

1) 布尔函数中相邻的并且做相同运算的变量在排序时也要尽量相邻；

2) 整个布尔函数会被分成若干个具有同一属性的组成部分，对各个部分中的变量先排序再将各部分排列组合。

3. 两类布尔函数在特定序下的OBDD

结合以上示例和分析，取DNF型布尔函数 $f={\displaystyle \underset{i=1}{\overset{n}{\sum }}{\displaystyle \underset{j=1}{\overset{n}{\prod }}{x}_{ij}}}\left(n,m\in N^{+}\right)$ ，CNF型布尔函数 $g={\displaystyle \underset{i=1}{\overset{n}{\prod }}{\displaystyle \underset{j=1}{\overset{n}{\sum }}{x}_{ij}}}\left(n,m\in N^{+}\right)$ 。给出如下两种类型布尔函数在特定序下的OBDD的命题及证明。

命题1 给定DNF型布尔函数 $f={\displaystyle \underset{i=1}{\overset{n}{\sum }}{\displaystyle \underset{j=1}{\overset{n}{\prod }}{x}_{ij}}}\left(n,m\in N^{+}\right)$ ，在变量序 $x_{11}\prec \cdots \prec x_{1m}\prec \cdots \prec x_{n1}\prec \cdots \prec x_{nm}$ 下的OBDD阶为 $nm+2$ 。

证明：采用数学归纳法。

基础步 取 $m\left(m\in N{}^{+}\right)$ 为定值，当 $i=1$ 时，布尔函数 $f=x_{11}\cdot x_{12}\cdots x_{1m}$ 。则f在序 $x_{11}\prec x_{12}\prec \cdots \prec x_{1m}$ 下的OBDD中阶 $\left|G_1\right|=m+2$ (如图3所示)，命题成立。

归纳步 假设 $k=n-1\left(n\ge 2\right)$ 时命题成立，即此时DNF型布尔函数 $f={\displaystyle \underset{i=1}{\overset{n}{\sum }}{\displaystyle \underset{j=1}{\overset{n}{\prod }}{x}_{ij}}}$ 在序 $\left[x_{11},x_{12},\cdots ,x_{1m},\cdots ,x_{\left(n-1\right)1},x_{\left(n-1\right)2},\cdots ,x_{\left(n-1\right)m}\right]$ 下的OBDD中阶 $\left|G_k\right|=\left(n-1\right)m+2$ (如图4左图所示)。

取 $k=n$ ，依据变量的序关系得知，OBDD的前 $\left(n-1\right)m$ 行已经确定，故只需按序做出余下OBDD的子树即可。如图4中右图虚线方框中所示，在最后的增加的m行中，新增的阶为m。故阶 $\left|G\right|=\left(n-1\right)m+m+2$ ，即 $\left|G\right|=nm+2$ ，命题得证。

命题2 给定CNF型布尔函数 $g={\displaystyle \underset{i=1}{\overset{n}{\prod }}{\displaystyle \underset{j=1}{\overset{n}{\sum }}{x}_{ij}}}\left(n,m\in N^{+}\right)$ ，在变量序 $x_{11}\prec \cdots \prec x_{1m}\prec \cdots \prec x_{n1}\prec \cdots \prec x_{nm}$ 下的OBDD阶为 $nm+2$ 。

证明：根据CNF布尔函数与DNF布尔函数结构上的对偶关系，在相同变量排序情况下，得到的OBDD结构相似。即阶仍为 $\left|G\right|=nm+2$ 。

例1 求出布尔函数 $f_1=\left(x_1+x_2+x_3\right)\cdot \left(x_4+x_5\right)\cdot \left(x_6+x_7+x_8\right)$ 在序 $x_1\prec x_2\prec \cdots \prec x_8$ 下的OBDD的阶，并作图。

首先根据函数类型分类，布尔函数 $f_1=\left(x_1+x_2+x_3\right)\cdot \left(x_4+x_5\right)\cdot \left(x_6+x_7+x_8\right)$ 是CNF型布尔函数，因此根据命题2，得其OBDD的阶 $\left|G\right|=10$ (如图5所示)。

图3. 布尔函数 $f=x_{11}\cdot x_{12}\cdots x_{1m}$ 在规定序下的OBDD

图4. 布尔函数f在特定序下的OBDD

图5. 布尔函数 $f_1$ 在序 $x_1\prec x_2\prec \cdots \prec x_8$ 下的OBDD

4. 结论

本文通过不同变量序对积和形式布尔函数OBDD的示例，给出两类特殊类型的布尔函数在特定序下OBDD阶的计算方法。在特定的情况下，可以快速准确的得到布尔函数的OBDD简洁表示和其与多项式相关的阶。但对于结构复杂的布尔函数，如何排序使得其OBDD的阶优化还有待进一步研究。

文章引用

张媛,江建国,胡晓璐. 两类布尔函数的OBDD阶
The OBDD Orders of Two Types of Boolean Functions[J]. 软件工程与应用, 2018, 07(06): 283-288. https://doi.org/10.12677/SEA.2018.76032

参考文献