Ordered Binary Decision Diagrams (OBDDs) are graph-based representations of Boolean functions which are widely used because of their good properties. In this paper, we introduce nondeterministic OBDDs (NOBDDs) and their restricted forms, and evaluate their expressive power. In some applications of OBDDs, canonicity, which is one of the good properties of OBDDs, is not necessary. In such cases, we can reduce the required amount of storage by using OBDDs in some non-canonical form. A class of NOBDDs can be used as a non-canonical form of OBDDs. In this paper, we focus on two particular methods which can be regarded as using restricted forms of NOBDDs. Our aim is to show how the size of OBDDs can be reduced in such forms from theoretical point of view. Firstly, we consider a method to solve satisfiability problem of combinational circuits using the structure of circuits as a key to reduce the NOBDD size. We show that the NOBDD size is related to the cutwidth of circuits. Secondly, we analyze methods that use OBDDs to represent Boolean functions as sets of product terms. We show that the class of functions treated feasibly in this representation strictly contains that in OBDDs and contained by that in NOBDDs.

This paper proposes a unified approach by means of the binary decision diagram, BDD in short, to solve #P-hand problems of counting the number of paths between two terminals in undirected and directed graphs. Our approach provides algorithms running in O (2O (n) ) time for typical planar graphs such as grid graphs. In fact, for any class of graphs having a good elimination ordering, this paradigm provides efficient solutions.

Recently, various efficient algorithms for solving combinatorial optimization problems using BDD-based set manipulation techniques have been developed. Minato proposed O-suppressed BDDs (ZBDDs) which is suitable for set manipulation, and it is utilized for various search problems. In terms of practical limits of space, however, there are still many search problems which are solved much better by using conventional branch-and-bound techniques than by using BDDs or ZBDDs, while the ability of conventional branch-and-bound approaches is limited by computation time. In this paper, an extension of APPLY operation, named APPRUNE (APply + PRUNE) operation, is proposed, which performs APPLY operation (ZBDD construction) and pruning simultaneously in order to reduce the required space for intermediate ZBDDs. As a prototype, a specific algorithm of APPRUNE operation is shown by assuming that the given condition for pruning is a threshold function, although it is expected that APPRUNE operation will be more effective if more sophisticated condition are considered. To reduce size of ZBDDs in intermediate steps, this paper also pay attention to the number of cared variables. As an application, an exact-minimization algorithm for generalized Reed-Muller expressions (GRMs) is implemented. From experimental results, it is shown that time and memory usage improved 8.8 and 3.4 times, respectively, in the best case using APPRUNE operation. Results on generating GRMs of exact-minimum number of not only product terms but also literals is also shown.

Exploring enormous state graphs represented implicitly by ordered binary decision diagrams (OBDDs) is one of the most successful applications of OBDDs. However, our worst-case analysis of implicit graph representations by OBDDs shows that there are cases where OBDD representations are not optimal and require more space than adjacency lists. As an improvement, we propose a new type of BDDs, called Patricia BDDs, which are capable of implicit representation of graphs while their worst-case sizes are kept equal or less than adjacency lists and OBDDs.

This paper presents implicit representation of binary decision diagrams (implicit BDDs) as a new effecient data structure for Boolean functions. A well-known method of representing graphs by binary decision diagrams (BDDs) is applied to BDDs themselves. Namely, it is a BDD representation of BDDs. Regularity in the structure of BDDs representing certain Boolean functions contributes to significant reduction in size of the resulting implicit BDD repersentation. Since the implicit BDDs also provide canonical forms for Boolean functions, the equivalence of the two implicit BDD forms is decided in time proportional to the representation size. We also show an algorithm to maniqulate Boolean functions on this implicit data structure.

Complexity of Boolean functions satisfying the propagation criterion (PC), an extended notion of the perfect nonlinearity, is discussed on several computation models. The following topics are investigated: (i) relationships between the unateness and the degree of the PC, (ii) the inversion complexity of perfectly nonlinear Boolean functions, (iii) the formula size of Boolean functions that satisfy the PC of degree 1, (iv) the area-time-square complexity of VLSI circuits computing perfectly nonlinear Boolean functions, (v) the OBDD size perfectly nonlinear Boolean functions.

Recently, there has been a lot of research on solving combinatorial problems using Binary Decision Diagrams (BDDs), which are very efficient representations of Boolean functions. We have already developed a Boolean Expression Manipulator, which calculates and reduces Boolean expressions quickly based on BDD techniques. This greatly aids our works on developing VLSI CAD systems and solving combinatorial problems. Any combinatorial problem can be described in Boolean expressions; however, arithmetic operations, such as addition, subraction, multiplication, equality and inequality, are also used for describing many practical problems. Arithmetic operations provide simple descriptions of problems in many cases. In this paper, we present an arithmetic Boolean expression manipulator (BEM-), based on BDD techniques. BEM- calculates Boolean expressions containing arithmetic operations and then displays the results in various formats. It can solve problems represented by a set of equalities and inequalities, which are dealt with using 0-1 linear programming. We show the efficient data structure based on BDD representation, algorihms for manipulating Boolean expressions with arithmetic operations, and good formats for displaying the results. Finally we present the specification of BEM- and an example of application to the 8-Queens problem. BEM- is customizable to various applicationa. It has good computation performance in terms of the total time for programming and execution. We expect BEM- to be a helpful tool in research and development on digital systems.

Manipulation of Boolean functions is one of the most important techniques for implementing of VLSI logic design systems. This paper presents a fast method for generating prime-irredundant covers from Binary Decision Diagrams (BDDs), which are efficient representation of Boolean functions. Prime-irredundant covers are forms in which each cube is a prime implicant and no cube can be eliminated. This new method generates compact cube sets from BDDs directly, in contrast to the conventional cube set reduction algorithms, which commonly manipulate redundant cube sets or truth tables. Our method is based on the idea of a recursive operator, proposed by Morreale. Morreale's algorithm is also based on cube set manipulation. We found that the algorithm can be improved and rearranged to fit BDD operations efficiently. The experimental results demonstrate that our method is efficient in terms of time and space. In practical time, we can generate cube sets consisting of more than 1,000,000 literals from multi-level logic circuits which have never previously been flattened into two-level logics. Our method is more than 10 times faster than ESPRESSO in large-scale examples. It gives quasi-minimum numbers of cubes and literals. This method should find many useful applications in logic design systems.

This paper describes two algorithms based on Boolean formulations aimed at solving scheduling, the main subtask of data path synthesis. Using the first algorithm, all possible scheduling solutions can be obtained under a time constraint, something that cannot be accomplished with other available systems. The second algorithm produces feasible solutions without increasing the complexity of the problem. The effectiveness of the algorithms is confirmed through experimental studies.