scholarly journals An n log n Algorithm for Online BDD Refinement

1995 ◽  
Vol 2 (29) ◽  
Author(s):  
Nils Klarlund
Keyword(s):  
Fixed Points ◽  
Boolean Functions ◽  
Linear Time ◽  
Canonical Representation ◽  
Decision Diagrams ◽  
Total Size ◽  
Binary Decision ◽  
Algebraic Framework ◽  
Verification Systems ◽  
Minimal Fixed Point

Binary Decision Diagrams are in widespread use in verification systems<br />for the canonical representation of Boolean functions. A BDD representing<br />a function phi : B^nu -> N can easily be reduced to its canonical form in<br />linear time.<br />In this paper, we consider a natural online BDD refinement problem<br />and show that it can be solved in O(n log n) if n bounds the size of the<br />BDD and the total size of update operations.<br />We argue that BDDs in an algebraic framework should be understood<br />as minimal fixed points superimposed on maximal fixed points. We propose<br />a technique of controlled growth of equivalence classes to make the<br />minimal fixed point calculations be carried out efficiently. Our algorithm<br />is based on a new understanding of the interplay between the splitting<br />and growing of classes of nodes.<br />We apply our algorithm to show that automata with exponentially<br />large, but implicitly represented alphabets, can be minimized in time<br />O(n log n), where n is the total number of BDD nodes representing the<br />automaton.

scholarly journals A Novel Graphical Technique for Combinational Logic Representation and Optimization

Complexity ◽  
2017 ◽  
Vol 2017 ◽  
pp. 1-12
Author(s):  
Vedhas Pandit ◽  
Björn Schuller
Keyword(s):  
Boolean Functions ◽  
Discrete Systems ◽  
Boolean Logic ◽  
Decision Diagrams ◽  
New Paradigm ◽  
Binary Decision ◽  
Graphical Technique ◽  
A New Technique ◽  
Logic Functions ◽  
Logical Functions

We present a new technique for defining, analysing, and simplifying digital functions, through hand-calculations, easily demonstrable therefore in the classrooms. It can be extended to represent discrete systems beyond the Boolean logic. The method is graphical in nature and provides complete ‘‘implementation-free” description of the logical functions, similar to binary decision diagrams (BDDs) and Karnaugh-maps (K-maps). Transforming a function into the proposed representations (also the inverse) is a very intuitive process, easy enough that a person can hand-calculate these transformations. The algorithmic nature allows for its computing-based implementations. Because the proposed technique effectively transforms a function into a scatter plot, it is possible to represent multiple functions simultaneously. Usability of the method, therefore, is constrained neither by the number of inputs of the function nor by its outputs in theory. This, being a new paradigm, offers a lot of scope for further research. Here, we put forward a few of the strategies invented so far for using the proposed representation for simplifying the logic functions. Finally, we present extensions of the method: one that extends its applicability to multivalued discrete systems beyond Boolean functions and the other that represents the variants in terms of the coordinate system in use.

scholarly journals Logic Synthesis for a Regular Layout

VLSI Design ◽  
1999 ◽  
Vol 10 (1) ◽  
pp. 35-55 ◽  
Author(s):  
Malgorzata Chrzanowska-Jeske ◽  
Yang Xu ◽  
Marek Perkowski
Keyword(s):  
Boolean Functions ◽  
Symmetric Functions ◽  
Logic Synthesis ◽  
Regular Structure ◽  
Theoretical Background ◽  
Device Performance ◽  
Decision Diagrams ◽  
Binary Decision ◽  
Function Representation ◽  
New Algorithms

New algorithms for generating a regular two-dimensional layout representation for multi-output, incompletely specified Boolean functions, called, Pseudo-Symmetric Binary Decision Diagrams (PSBDDs), are presented. The regular structure of the function representation allows accurate prediction of post-layout areas and delays before the layout is physically generated. It simplifies power estimation on the gate level and allows for more accurate power optimization. The theoretical background of the new diagrams, which are based on ideas from contact networks, and the form of decision diagrams for symmetric functions is discussed. PSBDDs are especially well suited for deep sub-micron technologies where the delay of interconnections limits the device performance. Our experimental results are very good and show that symmetrization of reallife benchmark functions can be done efficiently.

scholarly journals On the size of binary decision diagrams representing Boolean functions

1995 ◽  
Vol 145 (1-2) ◽  
pp. 45-69 ◽  
Author(s):  
Y. Breitbart ◽  
H. Hunt ◽  
D. Rosenkrantz
Keyword(s):  
Boolean Functions ◽  
Binary Decision Diagrams ◽  
Decision Diagrams ◽  
Binary Decision

scholarly journals Retrieving and Saving Meaningful Keywords in Unstructured PDF Documents using Binary Decision Diagrams

2019 ◽  
Vol 8 (3) ◽  
pp. 1950-1955
Keyword(s):  
Boolean Functions ◽  
Binary Decision Diagrams ◽  
Portable Document Format ◽  
Unstructured Data ◽  
Decision Diagrams ◽  
Boolean Operations ◽  
Binary Decision ◽  
Binary Diagram ◽  
Textual Data ◽  
New Framework

With the growing intricacy in data engendered and processed across sundry platforms today, the desideratum for consistency has grown. Structured data is utilized for a number of purposes which is not feasible with unstructured data. The purpose of this study was to convert data from unstructured format to structured in portable document format with the help of new framework using the concept of Binary Decision Diagrams and Boolean operations. Binary decision diagrams are data structures for representing Boolean functions taking Boolean as input and generating Boolean as output and hence creating a binary diagram. This research is mainly carried out to show how we can store large number of data easily in the form of bits. The entire focus is on retrieving the meaningful information from unstructured textual data in PDF documents using Boolean operations and bag model, thus, saving the meaningful keywords in the form of binary decision trees. Later on clustering the documents based on commonalities between the documents. This research presents a way for increasing the efficiency of converting unstructured data to structured in PDF and saving huge number of data in the form of bits using this novel framework

scholarly journals Bi-Kronecker Functional Decision Diagrams: A Novel Canonical Representation of Boolean Functions

2019 ◽  
Vol 33 ◽  
pp. 2867-2875 ◽  
Author(s):  
Xuanxiang Huang ◽  
Kehang Fang ◽  
Liangda Fang ◽  
Qingliang Chen ◽  
Zhao-Rong Lai ◽  
...  
Keyword(s):  
Data Structure ◽  
Boolean Functions ◽  
Canonical Representation ◽  
Experimental Results ◽  
Compact Representation ◽  
Decision Diagrams ◽  
Canonical Forms

In this paper, we present a novel data structure for compact representation and effective manipulations of Boolean functions, called Bi-Kronecker Functional Decision Diagrams (BKFDDs). BKFDDs integrate the classical expansions (the Shannon and Davio expansions) and their bi-versions. Thus, BKFDDs are the generalizations of existing decision diagrams: BDDs, FDDs, KFDDs and BBDDs. Interestingly, under certain conditions, it is sufficient to consider the above expansions (the classical expansions and their bi-versions). By imposing reduction and ordering rules, BKFDDs are compact and canonical forms of Boolean functions. The experimental results demonstrate that BKFDDs outperform other existing decision diagrams in terms of sizes.

scholarly journals Compressing Exact Cover Problems with Zero-suppressed Binary Decision Diagrams

2021 ◽  
Author(s):  
Masaaki Nishino ◽  
Norihito Yasuda ◽  
Kengo Nakamura
Keyword(s):  
Data Structure ◽  
State Of The Art ◽  
Linear Time ◽  
Binary Decision Diagrams ◽  
Experimental Results ◽  
Decision Diagrams ◽  
Binary Decision ◽  
Running Time ◽  
Order Of Magnitude ◽  
Exact Cover

Exact cover refers to the problem of finding subfamily F of a given family of sets S whose universe is D, where F forms a partition of D. Knuth’s Algorithm DLX is a state-of-the-art method for solving exact cover problems. Since DLX’s running time depends on the cardinality of input S, it can be slow if S is large. Our proposal can improve DLX by exploiting a novel data structure, DanceDD, which extends the zero-suppressed binary decision diagram (ZDD) by adding links to enable efficient modifications of the data structure. With DanceDD, we can represent S in a compressed way and perform search in linear time with the size of the structure by using link operations. The experimental results show that our method is an order of magnitude faster when the problem is highly compressed.

scholarly journals Authorization Enforcement in Workflows: Maintaining Realizability Via Automated Reasoning

10.29007/n6nv ◽  
2018 ◽  
Author(s):  
Jason Crampton ◽  
Michael Huth ◽  
Jim Huan-Pu Kuo
Keyword(s):  
Task Allocation ◽  
Automated Reasoning ◽  
Linear Time ◽  
Workflow Management ◽  
Bounded Model Checking ◽  
Management Systems ◽  
Decision Diagrams ◽  
Workflow Management Systems ◽  
Binary Decision ◽  
Linear Time Temporal Logic

We investigate automated reasoning techniques as a means of supporting authorization enforcement functions of security-aware workflow management systems. The aim of such support is that one may statically or dynamically guarantee the realizability of a workflow instance given the security constraints of the underlying workflow specification. We develop two such automated reasoning methods and experimentally evaluate their suitability for giving such support. One method uses a propositional encoding of realizability implemented through binary decision diagrams, another method uses a linear-time temporal logic encoding implemented via bounded model checking. Preliminary experimental results identify issues of scalability and of balancing flexibility in task allocation with complexity of computing such allocations.

Sign in / Sign up

Export Citation Format

Share Document