The Power of Nondeterminism and Randomness for Oblivious Branching Programs

Abstract. This paper abstracts and generalizes the known approaches for proving lower bounds on the size of various variants of oblivious branching programs (oblivious BPs for short), providing an easy-to-use technique which works for all nondeterministic and randomized modes of acceptance. The technique is applied to obtain the following results concerning the power of nondeterminism and randomness for oblivious BPs: <p>— Oblivious read-once BPs, better known as OBDDs (ordered binary decision diagrams), are used in many applications and their structure is well understood in the deterministic case. It has been open so far to compare the power of nondeterministic OBDDs with so-called partitioned BDDs which are a variant of nondeterministic branching programs also used in practice. A k -partitioned BDD has a nondeterministic node at the top by which one out of k deterministic OBDDs with possibly different variable orders is chosen. It is proven here that the two models are incomparable as long as k is bounded by a logarithmic function in the input length. <p>— It is shown that deterministic oblivious read-k -times BPs for an explicitly defined function require superpolynomial size, for k logarithmic in the input length, while there are Las Vegas oblivious read-twice BPs of linear size for this function. This is in contrast to the situation for OBDDs, for which the respective size measures are polynomially related. <p>— Furthermore, an explicitly defined function is presented for which randomized oblivious read-k -times BPs with bounded error require exponential size, while the function as well as its complement can be represented in polynomial size by nondeterministic oblivious read-k -times BPs and deterministic oblivious read-(k+1) -times BPs, where k=o(log n) .     

The Power of Nondeterminism and Randomness for Oblivious Branching Programs

Abstract. This paper abstracts and generalizes the known approaches for proving lower bounds on the size of various variants of oblivious branching programs (oblivious BPs for short), providing an easy-to-use technique which works for all nondeterministic and randomized modes of acceptance. The technique is applied to obtain the following results concerning the power of nondeterminism and randomness for oblivious BPs: <p>— Oblivious read-once BPs, better known as OBDDs (ordered binary decision diagrams), are used in many applications and their structure is well understood in the deterministic case. It has been open so far to compare the power of nondeterministic OBDDs with so-called partitioned BDDs which are a variant of nondeterministic branching programs also used in practice. A k -partitioned BDD has a nondeterministic node at the top by which one out of k deterministic OBDDs with possibly different variable orders is chosen. It is proven here that the two models are incomparable as long as k is bounded by a logarithmic function in the input length. <p>— It is shown that deterministic oblivious read-k -times BPs for an explicitly defined function require superpolynomial size, for k logarithmic in the input length, while there are Las Vegas oblivious read-twice BPs of linear size for this function. This is in contrast to the situation for OBDDs, for which the respective size measures are polynomially related. <p>— Furthermore, an explicitly defined function is presented for which randomized oblivious read-k -times BPs with bounded error require exponential size, while the function as well as its complement can be represented in polynomial size by nondeterministic oblivious read-k -times BPs and deterministic oblivious read-(k+1) -times BPs, where k=o(log n) .     

Nondeterministic ordered binary decision diagrams with repeated tests and various modes of acceptance

Ordered binary decision diagrams with repeated tests are considered both in complexity theory and in applications. Bollig et al. have proved in [B. Bollig, M. Sauerhoff, D. Sieling, I. Wegener, Hierarchy theorems of kOBDDs and kIBDDs, Theoret. Comput. Sci. 205 (1998) 45-60] a tight hierarchy result for the classes of functions representable by k layers of polynomial-size deterministic ordered binary decision diagrams. In this paper the nondeterministic case is investigated, where the layers are driven by one and the same variable ordering. For k being a constant, it is shown that for the existential, the parity-, and the majority acceptance mode the analogous hierarchy collapses.     

A Comparison of Free BDDs and Transformed BDDs

Ordered binary decision diagrams (OBDDs) introduced by Bryant (IEEE Trans. on Computers, Vol. 35, pp. 677–691, 1986) have found a lot of applications in verification and CAD. Their use is limited if the OBDD size of the considered functions is too large. Therefore, a variety of generalized BDD models has been presented, among them FBDDs (free BDDs) and TBDDs (transformed BDDs). Here the quite tight relations between these models are revealed and their advantages and disadvantages are discussed.     

Zero-suppressed BDDs and their applications

In many real-life problems, we are often faced with manipulating sets of combinations. In this article, we study a special type of ordered binary decision diagram (OBDD), called zero-suppressed BDDs (ZBDDs). This data structure represents sets of combinations more efficiently than using original OBDDs. We discuss the basic data structures and algorithms for manipulating ZBDDs in contrast with the original OBDDs. We also present some practical applications of ZBDDs, such as solving combinatorial problems with unate cube set algebra, logic synthesis methods, Petri net processing, etc. We show that a ZBDD is a useful option in OBDD techniques, suitable for a part of the practical applications. Published online: 15 May 2001     

Short-Time Scaling of Variable Orderingof OBDDs

A short-time scaling criterion of variable ordering of OBDDs is proposed.By this criterion it is easy and fast to determine which one is better when several variable orders are given,especially when they differ 10% or more in resulted BDD size from each other.An adaptive variable order selection method,based on the short-time scaling criterion,is also presented.The experimental results show that this method is efficient and it makes the heuristic variable ordering methods more practical.     

On the Minimization of (Complete) Ordered Binary Decision Diagrams

Ordered binary decision diagrams (OBDDs) are a popular data structure for Boolean functions. Some applications work with a restricted variant called complete OBDDs which is strongly related to nonuniform deterministic finite automata. One of its complexity measures is the width which has been investigated in several areas in computer science like machine learning, property testing, and the design and analysis of implicit graph algorithms. For a given function the size and the width of a (complete) OBDD is very sensitive to the choice of the variable ordering but the computation of an optimal variable ordering for the OBDD size is known to be NP-hard. Since optimal variable orderings with respect to the OBDD size are not necessarily optimal for the complete model or the OBDD width and hardly anything about the relation between optimal variable orderings with respect to the size and the width is known, this relationship is investigated. Here, using a new reduction idea it is shown that the size minimization problem for complete OBDDs and the width minimization problem are NP-hard.     

A PENALTY-LOGIC SIMPLE-TRANSITION MODEL FOR STRUCTURED SEQUENCES

We study the problem of learning to infer hidden-state sequences of processes whose states and observations are propositionally or relationally factored. Unfortunately, standard exact inference techniques such as Viterbi and graphical model inference exhibit exponential complexity for these processes. The main motivation behind our work is to identify a restricted space of models, which facilitate efficient inference, yet are expressive enough to remain useful in many applications. In particular, we present the penalty-logic simple-transition model, which utilizes a very simple-transition structure where the transition cost between any two states is constant. While not appropriate for all complex processes, we argue that it is often rich enough in many applications of interest, and when it is applicable there can be inference and learning advantages compared to more general models. In particular, we show that sequential inference for this model, that is, finding a minimum-cost state sequence, efficiently reduces to a single-state minimization (SSM) problem. We then show how to define atemporal-cost models in terms of penalty logic, or weighted logical constraints, and how to use this representation for practically efficient SSM computation. We present a method for learning the weights of our model from labeled training data based on Perceptron updates. Finally, we give experiments in both propositional and relational video-interpretation domains showing advantages compared to more general models.     

On the Expressive Power of OKFDDs

Ordered Decision Diagrams (ODDs) as a means for the representation of Boolean functions are used in many applications in CAD. Depending on the decomposition type, various classes of ODDs have been defined, among them being the Ordered Binary Decision Diagrams (OBDDs), the Ordered Functional Decision Diagrams (OFDDs) and the Ordered Kronecker Functional Decision Diagrams (OKFDDs).Based on a formalization of the concept decomposition type we first investigate all possible decomposition types and prove that already OKFDDs, which result from the application of only three decomposition types, result in the most general class of ODDs. We then show from a (more) theoretical point of view that the generality of OKFDDs is really needed. We prove several exponential gaps between specific classes of ODDs, e.g. between OKFDDs on the one side and OBDDs, OFDDs on the other side. Combining these results it follows that a restriction of the OKFDD concept to subclasses, such as OBDDs and OFDDs as well, results in families of functions which lose their efficient representation.     

Exponential space complexity for OBDD-based reachability analysis

Ordered binary decision diagrams (OBDDs) are one of the most common dynamic data structures for Boolean functions. Nevertheless, many basic graph problems are known to be PSPACE-hard if their input graphs are represented by OBDDs. Computing the set of nodes that are reachable from some source s∈V in a digraph G=(V,E) is an important problem in computer-aided design, hardware verification, and model checking. Until now only exponential lower bounds on the space complexity of a restricted class of OBDD-based algorithms for the reachability problem have been known. Here, the result is extended by presenting an exponential lower bound for the general reachability problem. As a by-product a general exponential lower bound is obtained for the computation of OBDDs representing all connected node pairs in a graph, the transitive closure.     

凹形区域和带单洞区域间拓扑关系的表示

现有空间拓扑关系模型多针对同种类的空间对象进行处理,在实际应用中具有一定的局限性.本文在4-交集模型的基础上,通过扩展4-交集矩阵,对凹形区域和带单洞区域间的拓扑关系进行了表示,得到凹形区域和带单洞区域间161种拓扑关系,并给出前10种拓扑关系的示意图.提出算法,并通过程序验证161种拓扑关系均可实现.证明所获得的161种基本关系的完备性和互斥性,通过与相关工作的比较可知该表示模型比其它相关模型表达力更强.     

On Symmetric Circuits and Fixed-Point Logics

We study properties of relational structures, such as graphs, that are decided by families of Boolean circuits. Circuits that decide such properties are necessarily invariant to permutations of the elements of the input structures. We focus on families of circuits that are symmetric, i.e., circuits whose invariance is witnessed by automorphisms of the circuit induced by the permutation of the input structure. We show that the expressive power of such families is closely tied to definability in logic. In particular, we show that the queries defined on structures by uniform families of symmetric Boolean circuits with majority gates are exactly those definable in fixed-point logic with counting. This shows that inexpressibility results in the latter logic lead to lower bounds against polynomial-size families of symmetric circuits.

     

Representing uncertain data: models, properties, and algorithms

In general terms, an uncertain relation encodes a set of possible certain relations. There are many ways to represent uncertainty, ranging from alternative values for attributes to rich constraint languages. Among the possible models for uncertain data, there is a tension between simple and intuitive models, which tend to be incomplete, and complete models, which tend to be nonintuitive and more complex than necessary for many applications. We present a space of models for representing uncertain data based on a variety of uncertainty constructs and tuple-existence constraints. We explore a number of properties and results for these models. We study completeness of the models, as well as closure under relational operations, and we give results relating closure and completeness. We then examine whether different models guarantee unique representations of uncertain data, and for those models that do not, we provide complexity results and algorithms for testing equivalence of representations. The next problem we consider is that of minimizing the size of representation of models, showing that minimizing the number of tuples also minimizes the size of constraints. We show that minimization is intractable in general and study the more restricted problem of maintaining minimality incrementally when performing operations. Finally, we present several results on the problem of approximating uncertain data in an insufficiently expressive model.     

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.     

On the expressive power of behavioral profiles

Behavioral profiles have been proposed as a behavioral abstraction of dynamic systems, specifically in the context of business process modeling. A behavioral profile can be seen as a complete graph over a set of task labels, where each edge is annotated with one relation from a given set of binary behavioral relations. Since their introduction, behavioral profiles were argued to provide a convenient way for comparing pairs of process models with respect to their behavior or computing behavioral similarity between process models. Still, as of today, there is little understanding of the expressive power of behavioral profiles. Via counter-examples, several authors have shown that behavioral profiles over various sets of behavioral relations cannot distinguish certain systems up to trace equivalence, even for restricted classes of systems represented as safe workflow nets. This paper studies the expressive power of behavioral profiles from two angles. Firstly, the paper investigates the expressive power of behavioral profiles and systems captured as acyclic workflow nets. It is shown that for unlabeled acyclic workflow net systems, behavioral profiles over a simple set of behavioral relations are expressive up to configuration equivalence. When systems are labeled, this result does not hold for any of several previously proposed sets of behavioral relations. Secondly, the paper compares the expressive power of behavioral profiles and regular languages. It is shown that for any set of behavioral relations, behavioral profiles are strictly less expressive than regular languages, entailing that behavioral profiles cannot be used to decide trace equivalence of finite automata and thus Petri nets.     

多智能体系统时态认知规范高效符号模型检测的算法研究

Clarke和McMillan提出了利用mu演算和OBDDs符号模型检测时态逻辑的方法.这些方法是非常有效的,能用于验证许多具有极大状态空间的实际系统(状态个数可以超过1020).但是,这些方法不能检测知识逻辑.而时态认知逻辑能更精确地描述分布式领域中系统和协议的规范.文章首先讨论了Kripke结构和mu演算的扩展,然后提出了利用扩展mu演算和OBDDs符号模型检测时态认知逻辑的方法.     

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.     

On the size of randomized OBDDs and read-once branching programs for k-stable functions

In this paper, a simple technique which unifies the known approaches for proving lower bound results on the size of deterministic, nondeterministic, and randomized OBDDs and kOBDDs is described.?As an application of this technique, a generic lower bound on the size of randomized OBDDs with bounded error is established for a class of functions which has been studied in the literature on branching programs for a long time. These functions have been called “k-stable” by Jukna. It follows that several standard functions are not contained in the analog of the class BPP for OBDDs. Furthermore, exponential lower bounds on the size of randomized kOBDDs are presented.?It is well known that k-stable functions with large k are hard for deterministic read-once branching programs. This is no longer true in the randomized case. It is shown here that a certain k-stable function due to Jukna, Razborov, Savicky, and Wegener has randomized branching programs of polynomial size, even with zero error. It follows that for the analogs of these classes defined in terms of the size of read-once branching programs. Received: September 3, 1998.     

Memory optimization in function and set manipulation with BDDs

Binary Decision Diagrams (BDDs) are the state-of-the-art technique for many synthesis, verification and testing problems in CAD for VLSI. Many researchers proposed optimized BDD—based representations, but in many complex applications the (working) memory required is still too much. Virtual memory is no alternative solution, because if the working set size for a program is large and memory accesses are random, an extremely large number of page faults significantly modifies the performance of the software. This paper proposes a solution to this problem for a specific application, namely BDD—based exploration of large state spaces, an issue often found in CAD for VLSI. Our ‘divide—and—conquer’ approach for reachability analysis is based on decomposition of state sets carried out at different levels and on an effective use of mass memory. As a result, we are able to explore the state space of large Finite State Machines. At the same time, the technique we develop is orthogonal to a variety of symbolic techniques and graph manipulation procedures and it allows reducing complexity of very common operations. Experimental results, on well known synchronous benchmarks usually used in the field of CAD for VLSI, show that this approach is particularly effective on larger problems as decomposition decreases the amount of working memory, avoids page faulting and makes the overall process more efficient. © 1998 John Wiley & Sons, Ltd.     

Computational power of two stacks with restricted communication

Rewriting systems working on words with a center marker are considered. The derivation is done by erasing a prefix or a suffix and then adding a prefix or a suffix. This models a communication of two stacks according to a fixed protocol defined by the choice of rewriting rules. The paper systematically considers different cases of these systems and determines their expressive power. Several cases are identified where very restricted communication surprisingly yields computational universality.