On the Relative Succinctness of Sentential Decision Diagrams
14
Citation
39
Reference
10
Related Paper
Citation Trend
Keywords:
Succinctness
Binary decision diagram
Nondeterministic algorithm
Representation
Boolean data type
Function representation
Sentential decision diagrams (SDDs) introduced by Darwiche in 2011 are a promising representation type used in knowledge compilation. The relative succinctness of representation types is an important subject in this area. The aim of the paper is to identify which kind of Boolean functions can be represented by SDDs of small size with respect to the number of variables the functions are defined on. For this reason the sets of Boolean functions representable by different representation types in polynomial size are investigated and SDDs are compared with representation types from the classical knowledge compilation map of Darwiche and Marquis. Ordered binary decision diagrams (OBDDs) which are a popular data structure for Boolean functions are one of these representation types. SDDs are more general than OBDDs by definition but only recently, a Boolean function was presented with polynomial SDD size but exponential OBDD size. This result is strengthened in several ways. The main result is a quasipolynomial simulation of SDDs by equivalent unambiguous nondeterministic OBDDs, a nondeterministic variant where there exists exactly one accepting computation for each satisfying input. As a side effect an open problem about the relative succinctness between SDDs and free binary decision diagrams (FBDDs) which are more general than OBDDs is answered.
Succinctness
Binary decision diagram
Nondeterministic algorithm
Representation
Cite
Citations (2)
The complexity of computing Boolean functions by different models of analog computation is studied. For the case of analog circuits of bounded fan-in, sharp upper bounds are obtained for the complexity of the most difficult Boolean function over certain bases. Bounds are given for the computational power gained by adding discontinuous gate functions and nondeterminism. Also explicit nonlinear lower bounds for the formula size of arithmetic circuits is proved. A size-depth trade-off is shown, and upper bounds for the VC-dimension of some classes of neural networks is given.
Then the complexity of computing Boolean functions by algebraic decision trees is studied. In this connection, separation results for algebraic decision trees over the binary field and the field of real numbers are proved.
Parity function
Binary decision diagram
Circuit complexity
Boolean network
Maximum satisfiability problem
Algebraic function
Cite
Citations (0)
Binary decision diagram
Boolean satisfiability problem
Product term
Formal equivalence checking
Satisfiability
Boolean data type
Cite
Citations (0)
With the rapid advances in computers, it becomes attractive to explore the use of computers to attack open problems in computational complexity. In this article, we concentrate on the problems of the complexity of Boolean functions, and overview several recent attempts to use computers in various ways to obtain concrete results on major problems in computational complexity. We discuss the problems on several computational models including ordered binary decision diagrams, Boolean circuits, and polynomial threshold representations of Boolean functions.
Binary decision diagram
Circuit complexity
Computational problem
Descriptive complexity theory
Complexity index
Cite
Citations (3)
A Binary Decision Diagram (BDD) is a data structure that can be used for efficient representation of Boolean functions. It allows storing a Boolean function of many variables and manipulating with it. For a given Boolean function, a BDD can be created statically or dynamically. The static creation has usually high demands on memory and time, therefore, it can be applied only to functions of few variables. On the other hand, the dynamic creation has less demands on computation time and memory, therefore, it is more preferable in case of real-world problems that usually deal with functions containing many variables. The dynamic creation is based on a fact that a function of many variables can be viewed as a composition of several smaller functions. Using this idea, BDDs of smaller functions are firstly created and then they are combined together to obtain a BDD of the whole function. The time needed for dynamic creation of a BDD depends on several factors. In case of a Boolean function that can be viewed as a composition of several smaller functions merged using an associative binary operation (e.g., AND, OR, NAND, NOR), time needed to create the final BDD can be influenced by the order in which the smaller functions are processed to obtain a BDD representing the whole function. This processing order is known as fold strategy and, generally, two basic strategies can be defined. These strategies are left (right) fold, in which the functions are processed from left to right (from right to left), and tree fold, when the functions at odd positions are merged with their right neighbors and this process is repeated until we obtain the final BDD. In this paper, we analyze influence of these two strategies on time needed to create a BDD representing Boolean function that is defined in a disjunctive normal form. The experimental analysis is primarily realized using our C++library for creation and manipulation with decision diagrams named as TeDDy (Templated Decision Diagram library).
Binary decision diagram
Boolean data type
Boolean network
Parity function
Boolean algebra
Product term
Function representation
Truth table
Cite
Citations (3)
Succinctness
Binary decision diagram
Nondeterministic algorithm
Representation
Boolean data type
Function representation
Cite
Citations (14)
Sentential decision diagrams (SDDs) introduced by Darwiche in 2011 are a promising representation type used in knowledge compilation. The relative succinctness of representation types is an important subject in this area. The aim of the paper is to identify which kind of Boolean functions can be represented by SDDs of small size with respect to the number of variables the functions are defined on. For this reason the sets of Boolean functions representable by different representation types in polynomial size are investigated and SDDs are compared with representation types from the classical knowledge compilation map of Darwiche and Marquis. Ordered binary decision diagrams (OBDDs) which are a popular data structure for Boolean functions are one of these representation types. SDDs are more general than OBDDs by definition but only recently, a Boolean function was presented with polynomial SDD size but exponential OBDD size. This result is strengthened in several ways. The main result is a quasipolynomial simulation of SDDs by equivalent unambiguous nondeterministic OBDDs, a nondeterministic variant where there exists exactly one accepting computation for each satisfying input. As a side effect an open problem about the relative succinctness between SDDs and free binary decision diagrams (FBDDs) which are more general than OBDDs is answered.
Succinctness
Binary decision diagram
Nondeterministic algorithm
Representation
Boolean data type
Netlist
Cite
Citations (0)
BDDs are the state-of-the-art technique for representing and manipulating Boolean functions. Their introduction caused a major leap forward in synthesis, verification, and testing. However, they are often unmanageable because of the large amount of nodes. To attack this problem, we insert auxiliary variables that decompose monolithic BDDs in smaller ones. This method works very well for Boolean function representation. As far as combinational circuits are concerned, representing their functions is the main issue. Going into the sequential domain, we focus on traversal techniques. We show that, once we have Boolean functions in decomposed form, symbolic manipulations are viable and efficient. We investigate the relation between auxiliary variables and static and dynamic ordering strategies. Experimental evidence shows that we achieve a certain degree of independence from variable ordering. Thus, this approach can be an alternative to dynamic re-ordering. Experimental results on Boolean function representation, and exact and approximate forward symbolic traversal of FSMs, demonstrate the benefits both in terms of memory requirements and of CPU time.
Binary decision diagram
Representation
Product term
Function representation
Boolean network
Implicant
Boolean data type
Cite
Citations (2)
Abstract Motivated by applications in boolean-circuit design, boolean synthesis is the process of synthesizing a boolean function with multiple outputs, given a relation between its inputs and outputs. Previous work has attempted to solve boolean functional synthesis by converting a specification formula into a Binary Decision Diagram (BDD) and quantifying existentially the output variables. We make use of the fact that the specification is usually given in the form of a Conjunctive Normal Form (CNF) formula, and we can perform resolution on a symbolic representation of a CNF formula in the form of a Zero-suppressed Binary Decision Diagram (ZDD). We adapt the realizability test to the context of CNF and ZDD, and show that the Cross operation defined in earlier work can be used for witness construction. Experiments show that our approach is complementary to BDD-based Boolean synthesis.
Binary decision diagram
Realizability
Conjunctive normal form
Boolean data type
Function representation
Representation
Standard Boolean model
Cite
Citations (0)
In this paper we introduce a nondeterministic counterpart to Reduced, Ordered Binary Decision Diagrams for the representation and manipulation of logic functions. ROBDDs are conceptually related to deterministic finite automata (DFA), accepting the language formed by the minterms of a function. This analogy suggests the use of nondeterministic devices as language recognizers. Unlike ROBDDs, the diagrams introduced in this paper allow multiple outgoing edges with the same label. By suitably restricting the degree of nondeterminism, we still obtain a canonical form for logic functions. Using PADs, we are able to reduce the memory occupation with respect to traditional ROBDDs for several benchmark functions. Moreover the analysis of the PAD graphs allowed us to sometimes identify new and better variable ordering for several benchmark circuits.
Nondeterministic algorithm
Binary decision diagram
Benchmark (surveying)
Representation
Boolean data type
Cite
Citations (5)