Computational Power of Nondeterministic Ordered Binary Decision Diagrams and Their Subclasses

Kazuyoshi TAKAGI  Koyo NITTA  Hironori BOUNO  Yasuhiko TAKENAGA  Shuzo YAJIMA  

IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences   Vol.E80-A   No.4   pp.663-669
Publication Date: 1997/04/25
Online ISSN: 
Print ISSN: 0916-8508
Type of Manuscript: Special Section PAPER (Special Section on Discrete Mathematics and Its Applications)
computational complexity,  Boolean function,  ordered binary decision diagram,  satisfiability,  combinational circuit,  cutwidth,  sum-of-product form,  zero-suppressed binary decision diagrams (BDD),  ternary decision diagram,  

Full Text: PDF>>
Buy this Article

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.