On the influence of the variable ordering for algorithmic learning using OBDDs

OBDDs with a fixed variable ordering are used successfully as data structure in experiments with learning heuristics based on examples. In this paper, it is shown that, for some functions, it is necessary to develop an algorithm to learn also a good OBDD variable ordering. There are functions with the following properties. They have OBDDs of linear size for optimal variable orderings. But for all but a small fraction of all variable orderings one needs large size to represent a list of randomly chosen examples. These properties are shown for simple functions like the multiplexer and the inner product.     

一种基于熵的OBDD变量排序算法

有序二叉决策图（OBDD）是一种有效表示布尔函数的数据结构,其大小依赖于所采用的变量序。熵是定量描述布尔函数中变量重要性的一种方法。基于变量的熵值分析了高质量变量序的特征,给出了一种基于熵的OBDD变量排序算法。实验结果表明：该算法与模拟退火算法和遗传算法结果相当。时间仅为相应算法的80．84％和29．79％。     

A simpler counterexample to a long-standing conjecture on the complexity of Bryantʼs apply algorithm

In 1986 in his seminal paper Bryant has introduced Ordered Binary Decision Diagrams (OBDDs) as a dynamic data structure for the representation and manipulation of Boolean functions which allow efficient algorithms for important operations like synthesis, the combination of two Boolean functions by a Boolean operator, and equivalence checking. Based on his empirical evaluation he has conjectured that his apply algorithm for the synthesis works in linear time with respect to the input and output size. Recently in 2012, Yoshinaka et al. have presented a counterexample which contradicts this conjecture but their example has the drawback that the chosen variable ordering for the OBDD representation of the input and output is bad. Therefore, they have raised the question whether Bryant?s conjecture may still stand for reasonable variable orderings. Here, a negative answer is given by presenting a simple counterexample which works for such kind of variable orderings.     

Complexity Theoretical Results on Partitioned (Nondeterministic) Binary Decision Diagrams

Ordered binary decision diagrams (OBDDs) have found many applications in the verification of combinational and sequential circuits, protocols, and the synthesis and analysis of systems. The applications are limited, since the expressive power of polynomial-size OBDDs is too restricted. Therefore, several more general BDD models are used. Partitioned OBDDs are OBDD models allowing restricted use of nondeterminism and different variable orderings. They are restricted enough such that the essential operations can be performed efficiently and they allow polynomial-size representations for many more functions than OBDDs. Here the expressive power of polynomial-size partitioned OBDDs is investigated. A tight hierarchy with respect to the number of parts in the partition is proved and partitioned OBDDs are compared with other BDD models. Received April 1998, and in final form September 1998.     

Efficient algorithms for the transformation between different types of binary decision diagrams

The problem of transforming an FBDD (free binary decision diagram) on variables or a OBDD (ordered binary decision diagram with respect to the variable ordering ) for the Boolean function into the reduced OBDD for is considered. The algorithms run in time (where, e.g., is the size of ) and need space , if may be an FBDD, or , if is known to be an OBDD. The problem is important for the improvement of given variable orderings, e.g., by simulated annealing or genetic algorithms, and in the situation where incompatible representations of functions have to be made compatible. Received: 13 October 1994 / 7 November 1995     

The Nonapproximability of OBDD Minimization

The size of ordered binary decision diagrams (OBDDs) is determined by the chosen variable ordering. A poor choice may cause an OBDD to be too large to fit into the available memory. The decision variant of the variable ordering problem is known to be NP-complete. We strengthen this result by showing that, unless P=NP, for each constant c>1 there is no polynomial time approximation algorithm with the performance ratio c for the variable ordering problem, i.e., no polynomial time algorithm that guarantees the computation of a variable ordering so that the resulting OBDD size is larger than the minimum size by a factor of at most c. This result justifies, also from a theoretical point of view, the use of heuristics for the variable ordering problem.     

Translation among CNFs, characteristic models and ordered binary decision diagrams

We consider translation among conjunctive normal forms (CNFs), characteristic models, and ordered binary decision diagrams (OBDDs) of Boolean functions. It is shown in this paper that Horn OBDDs can be translated into their Horn CNFs in polynomial time. As for the opposite direction, the problem can be solved in polynomial time if the ordering of variables in the resulting OBDD is specified as an input. In case that such ordering is not specified and the resulting OBDD must be of minimum size, its decision version becomes NP-complete. Similar results are also obtained for the translation in both directions between characteristic models and OBDDs. We emphasize here that the above results hold on any class of functions having a basis of polynomial size.     

String-matching with OBDDs

Ordered binary decision diagrams (OBDDs) are a very popular graph representation for Boolean functions. They can be viewed as finite automata recognizing sets of strings of a fixed length, where the letters of the input strings are read at most once in a predefined ordering. The string matching problem with string w as pattern, consists of determining, given an input string, whether or not it contains w as substring. We show that for a fraction of orderings tending to 1 when n increases arbitrarily, the minimal size of an OBDD solving the string matching problem for strings of length n has a growth which is an exponential in n.     

Lower bounds on the OBDD size of two fundamental functions' graphs

Ordered Binary Decision Diagrams (OBDDs) are a data structure for Boolean functions which supports many useful operations. Among others it finds applications in CAD, model checking, and symbolic graph algorithms. Nevertheless, many simple functions are known to have exponential OBDD size with respect to their number of variables. In order to investigate the limits of symbolic graph algorithms which work on OBDD-represented graph instances, it is useful to have simply-structured graphs whose OBDD representation has exponential size. Therefore, we consider two fundamental functions with exponential lower bounds on their OBDD size and transfer these results to their corresponding graphs. Concretely, we consider the Indirect Storage Access function and the Hidden Weighted Bit function.     

OBDDs of a Monotone Function and Its Prime Implicants

Coudert made a breakthrough in the two-level logic minimization problem with Ordered Binary Decision Diagrams (OBDDs for short) recently [3]. This paper discusses the relationship between the two OBDDs of a monotone function and its prime implicant set to clarify the complexity of this practically efficient method. We show that there exists a monotone function which has an O(n) size sum-of-products but cannot be represented by a polynomial size OBDD. In other words, we cannot obtain the OBDD of the prime implicant set of a monotone function in an output-size sensitive manner once we have constructed the OBDD of that function as in [3], in the worst case. A positive result is also given for a meaningful class of matroid functions. Received April 1997, and in revised form December 1997, and in final form February 1998.     

Exact OBDD Bounds for Some Fundamental Functions

Ordered binary decision diagrams (OBDDs) are nowadays one of the most common dynamic data structures or representation types for Boolean functions. Among the many areas of application are verification, model checking, computer aided design, relational algebra, and symbolic graph algorithms. Although many exponential lower bounds on the OBDD size of Boolean functions are known, there are only few functions where the OBDD size is asymptotically known exactly. In this paper the exact OBDD sizes of the fundamental functions multiplexer and addition of n-bit numbers are determined.     

Size of ordered binary decision diagrams representing threshold functions

An ordered binary decision diagram (OBDD) is a graph representation of a Boolean function. In this paper, the size of ordered binary decision diagrams representing threshold functions is discussed. We consider two cases: the case when a variable ordering is given and the case when it is adaptively chosen. We show 1) O(2^n/2) upper bound for both cases, 2) Ω(2^n/2) lower bound for the former case and 3) Ω(n2^√n/2) lower bound for the latter case. We also show some relations between the variable ordering and the size of OBDDs representing threshold functions.     

On the size of (generalized) OBDDs for threshold functions

Ordered binary decision diagrams (OBDDs) are one of the most common dynamic data structures for Boolean functions. Among the many areas of application are hardware verification, model checking, and symbolic graph algorithms. Threshold functions are the basic functions for discrete neural networks and are used as building blocks in the design of some symbolic graph algorithms. In this paper the first exponential lower bound on the size of a more general model than OBDDs and the first nontrivial asymptotically optimal bound on the OBDD size for a threshold function are presented.     

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

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

Larger lower bounds on the OBDD complexity of integer multiplication

Integer multiplication as one of the basic arithmetic functions has been in the focus of several complexity theoretical investigations and ordered binary decision diagrams (OBDDs) are one of the most common dynamic data structures for Boolean functions. Recently, the question whether the OBDD complexity of the most significant bit of integer multiplication is exponential has been answered affirmatively. In this paper a larger general lower bound is presented using a simpler proof. Furthermore, we prove a larger lower bound for the variable order assumed to be one of the best ones for the most significant bit. Moreover, the best known lower bound on the OBDD complexity for the so-called graph of integer multiplication is improved.     

Minimization Problems for Parity OBDDs

Parity Ordered Binary Decision Diagrams (⊕OBDDs) are a data structure for boolean functions that extends the well-known OBDDs and reduces the representation size for several functions. Both data structures share the problem that the representation size strongly depends on the chosen variable order. For ⊕OBDDs the number of edges and thus the representation size is also influenced by the choice of the basis of the represented vector space. In this paper the hardness of some minimization problems for ⊕OBDDs is proven, namely, that there is no polynomial time approximation scheme for minimizing the number of nodes by choosing the variable order and for minimizing the number of edges, where the variable order may be changed or is fixed, unless P=NP.     

On the use of OBDDs in model-based diagnosis: An approach based on the partition of the model

In this paper, we discuss how Ordered Binary Decision Diagrams (OBDDs) can be exploited for the computation of consistency-based diagnoses in model-based diagnosis. Since it is not always possible to efficiently encode the whole system model within a single OBDD, we propose to build a set of OBDDs, each one encoding a portion of the original model. For each portion of the model, we compute an OBDD encoding the set of local diagnoses; the OBDD encoding global diagnoses is then obtained by merging all the local-diagnoses OBDDs. Finally, minimal-cardinality diagnoses can be efficiently computed and extracted.The paper reports formal results about soundness, completeness and computational complexity of the proposed algorithm. Thanks to the fact that encoding diagnoses is in general much simpler than encoding the whole system model, this approach allows for the successful computation of global diagnoses even if the system model could not be compiled into a single OBDD. This is exemplified referring to a challenging combinatorial digital circuit taken from the ISCAS85 benchmark.     

基于重量分析的OBDD变量排序算法

有序的二叉判决图（ＯＢＤＤ）是布尔表达式的一种有效表示方法，但它的体积对变量排序具有较强的依赖性。本文提出一种电路结构图，并在此基础上定义了原始输入重量和节点重量等参数，并建立了用重量分析来指导的ＯＢＤＤ变量排序算法。由于从考虑变量对输出函数的影响出发与从考虑ＯＢＤＤ节点共享性出发对变量排序的要求不同，本文分别设计了两类算法。实验结果表明，本文对大多数标准电路变量排序的效果都优于国际上的同类算法，     

基于OBDD的编码算法

论文提出一个新的无损图像压缩算法,主要是通过有序二叉决策图(OBDD)的方法,寻找图像中重复的模式来减少其存储空间的一种变换编码,因而成为表示图像的另一种数据结构。我们通过该算法来寻找OBDD以精确地表示图像,并给出了其OBDD的有效编码,所获得的结果表明,所提出的算法及其编码是实现无损图像压缩的一种有效的方法。     

An efficient query learning algorithm for ordered binary decision diagrams

In this paper, we propose a new algorithm that exactly learns ordered binary decision diagrams (OBDDs) with a given variable ordering via equivalence and membership queries. Our algorithm uses at most n equivalence queries and at most 2n (log₂ m + 3n) membership queries, where n is the number of nodes in the target-reduced OBDD and m is the number of variables. The upper bound on the number of membership queries is smaller by a factor of O(m) compared with that for the previous best known algorithm proposed by [R. Gavaldà, D. Guijarro, Learning Ordered Binary Decision Diagrams, Proceedings of the 6th International Workshop on Algorithmic Learning Theory, 1995, pp. 228–238].