Binary Decision Diagrams for Affine Approximation
0
Citation
0
Reference
10
Related Paper
Abstract:
Selman and Kautz's work on ``knowledge compilation'' established how approximation (strengthening and/or weakening) of a propositional knowledge-base can be used to speed up query processing, at the expense of completeness. In this classical approach, querying uses Horn over- and under-approximations of a given knowledge-base, which is represented as a propositional formula in conjunctive normal form (CNF). Along with the class of Horn functions, one could imagine other Boolean function classes that might serve the same purpose, owing to attractive deduction-computational properties similar to those of the Horn functions. Indeed, Zanuttini has suggested that the class of affine Boolean functions could be useful in knowledge compilation and has presented an affine approximation algorithm. Since CNF is awkward for presenting affine functions, Zanuttini considers both a sets-of-models representation and the use of modulo 2 congruence equations. In this paper, we propose an algorithm based on reduced ordered binary decision diagrams (ROBDDs). This leads to a representation which is more compact than the sets of models and, once we have established some useful properties of affine Boolean functions, a more efficient algorithm.Keywords:
Binary decision diagram
Completeness (order theory)
Conjunctive normal form
Function representation
Representation
Base (topology)
Abstract : Boolean bent functions have desirable cryptographic properties in that they have maximum nonlinearity, which hardens a cryptographic function against linear cryptanalysis attacks. Furthermore, bent functions are extremely rare and difficult to find. Consequently, little is known generally about the characteristics of bent functions. One method of representing Boolean functions is with a reduced ordered binary decision diagram. Binary decision diagrams (BDD) represent functions in a tree structure that can be traversed one variable at a time. Some functions show speed gains when represented in this form, and binary decision diagrams are useful in computer aided design and real-time applications. This thesis investigates the characteristics of bent functions represented as BDDs, with a focus on their complexity. In order to facilitate this, a computer program was designed capable of converting a function's truth table into a minimally realized BDD. Disjoint quadratic functions (DQF), symmetric bent functions, and homogeneous bent functions of 6-variables were analyzed, and the complexities of the minimum binary decision diagrams of each were discovered. Specifically, DQFs were found to have size 2n - 2 for functions of n-variables; symmetric bent functions have size 4n - 8, and all homogeneous bent functions of 6-variables were shown to be P-equivalent.
Binary decision diagram
Bent function
Disjoint sets
Cite
Citations (1)
In this paper, we compare two different Boolean function reduction methods in order to justify the analytical model of the Monte Carlo data for Boolean function complexity. We use a binary decision diagram (BDD) complexity model (proposed earlier) and weigh it against the complexity behavior generated by Synopsys Design Compiler (DC). We use this synthesis tool (that utilizes a standard cell library) to generate RTL hardware description of Monte Carlo circuits as gate-level netlists. The two reduction methods (model and DC) transform an arbitrary function into a much-reduced representation of the same function. The comparison confirms that the behavior of Boolean function complexity using the model and the DC is visually and statistically similar; the similarity holds true for BDDs representing functions comprising a wide range of variables and minterms.
Binary decision diagram
Circuit complexity
Function representation
Combinational logic
Representation
Cite
Citations (1)
Binary decision diagram
Symmetric function
Representation
Canonical normal form
Function representation
Cite
Citations (12)
AbstractSystem reliability can be modeled through an analysis of the Boolean function that encodes the structure of a system. This relationship between the system structure and its corresponding Boolean function provides the foundation for the BSV analysis technique described in Chapter 3. The state-of-the-art technique for manipulating Boolean functions is the reduced order binary decision diagram (ROBDD)—often referred to simply as BDD. This chapter includes a brief overview of the BDD technique and provides BDD-based algorithms for the assessment of k-out-of-n:G structures for systems with both perfect and imperfect fault coverage.
Binary decision diagram
Product term
Cite
Citations (0)
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)
Ordered binary decision diagram representing a Boolean function to a directed_acyclic_diagram is a data structure of Boolean function canonical representation . We can check some properties of Boolean function such as satisfiablity, equivalence, ect. This article focuses on data structure of OBDD and operations based on OBDD in detail and reveals arithmetic improved of constructing OBDD.
Binary decision diagram
Representation
Product term
Logical equivalence
Function representation
Cite
Citations (0)
Succinctness
Binary decision diagram
Nondeterministic algorithm
Representation
Boolean data type
Function representation
Cite
Citations (14)
Binary decision diagrams (BDD) have made a noticeable entry in the RAMS field. This kind of representation for Boolean functions makes possible the assessment of complex fault-trees, both qualitatively (minimal cutsets search) and quantitatively (exact calculation top event probability). Any Boolean function, and in particular any fault-tree, whether coherent or not, can be represented by a BDD. The BDD is a canonical representation of the function, as soon as one has chosen a variable (i.e., in the fault-tree case, basic event) ordering. Tools based on the use of BDDs, like METAPRIME, or ARALIA, can in some cases give more accurate results than conventional tools, while running 1000 times faster. EDF has investigated this kind of technology, and tested METAPRIME, ARALIA, and other tools based on BDDs, in the framework of cooperations with the BULL company and with the Bordeaux University. These tests have demonstrated that the size of the BDD, that has to be built thoroughly before any kind of assessment can begin, is dramatically sensitive to the ordering chosen for the variables. For a given fault-tree, this size may vary by several orders of magnitude. This can lead to excessive needs, both in terms of memory and CPU time. The problem of finding an optimal ordering being untractable for real applications, many heuristics have been proposed, in order to find acceptable orderings, at low cost (in terms of computing requirements).
Binary decision diagram
Heuristics
Representation
Function representation
Cite
Citations (52)
Lower-bound results on Boolean-function complexity under two different models are discussed. The first is an abstraction of tradeoffs between chip area and speed in very-large-scale-integrated (VLSI) circuits. The second is the ordered binary decision diagram (OBDD) representation used as a data structure for symbolically representing and manipulating Boolean functions. The lower bounds demonstrate the fundamental limitations of VLSI as an implementation medium, and that of the OBDD as a data structure. It is shown that the same technique used to prove that any VLSI implementation of a single output Boolean function has area-time complexity AT/sup 2/= Omega (n/sup 2/) also proves that any OBDD representation of the function has Omega (c/sup n/) vertices for some c>1 but that the converse is not true. An integer multiplier for word size n with outputs numbered 0 (least significant) through 2n-1 (most significant) is described. For the Boolean function representing either output i-1 or output 2n-i-1, where 1>
Binary decision diagram
Function representation
Converse
Cite
Citations (531)
A new Boolean function representation scheme, the Indexed Binary Decision Diagram (IBDD), is proposed to provide a compact representation for functions whose Ordered Binary Decision Diagram (OBDD) representation is intractably large. We explain properties of IBDDs and present algorithms for constructing IBDDs from a given circuit. Practical and effective algorithms for satisfiability testing and equivalence checking of IBDDs, as well as their implementation results, are also presented. The results show that many functions, such as multipliers and the hidden-weighted-bit function, whose analysis is intractable using OBDDs, can be efficiently accomplished using IBDDs. We report efficient verification of Booth multipliers, as well as a practical strategy for polynomial time verification of some classes of unsigned array multipliers.
Binary decision diagram
Representation
Formal equivalence checking
Boolean satisfiability problem
Function representation
Satisfiability
Cite
Citations (40)