Graph-Based Algorithms for Boolean Function Manipulation
1986/08/01 by Bryant · 129 citations
Engineering · Computer Science · #Low-power high-performance VLSI design #Formal Methods in Verification #VLSI and Analog Circuit Testing
paper · doi:10.1109/tc.1986.1676819
Abstract
In this paper we present a new data structure for representing Boolean functions and an associated set of manipulation algorithms. Functions are represented by directed, acyclic graphs in a manner similar to the representations introduced by Lee [1] and Akers [2], but with further restrictions on the ordering of decision variables in the graph. Although a function requires, in the worst case, a graph of size exponential in the number of arguments, many of the functions encountered in typical applications have a more reasonable representation. Our algorithms have time complexity proportional to the sizes of the graphs being operated on, and hence are quite efficient as long as the graphs do not grow too large. We present experimental results from applying these algorithms to problems in logic design verification that demonstrate the practicality of our approach.
Citations
Cited by
- A Fast Quantitative Analyzer for NetKAT
- A ProbLog program to infer individual genotypes from familial phenotypes in autosomal, X-linked, and Y-linked Mendelian disorders
- The 4/δ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee
- A Computational Proof of the Highest-Scoring Boggle Board
- Are You Satisfied by This Partial Assignment?
- Second-Order Value Numbering
- Data Exploration and Validation on dense knowledge graphs for biomedical\n research
- Scalable Approach to Uncertainty Quantification and Robust Design of\n Interconnected Dynamical Systems
- uvl2dimacs: Optimized translation from universal variability language into Boolean logic
- A Theory of Formal Synthesis via Inductive Learning
- Design, Implementation and Evaluation of MTBDD based Fuzzy Sets and Binary Fuzzy Relations
- Improving Web Database Access Using Decision Diagrams
- MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications
- Foundations of Symbolic Languages for Model Interpretability
- Relations between MDDs and Tuples and Dynamic Modifications of MDDs based constraints
- Prefix Trees Improve Memory Consumption in Large-Scale Continuous-Time Stochastic Models
- Infrastructure-based Autonomous Mobile Robots for Internal Logistics -- Challenges and Future Perspectives
- Bounded Dynamic Level Maintenance for Efficient Logic Optimization
- Dynamic Boolean Synthesis with Zero-suppressed Decision Diagrams
- Towards Verifying Nonlinear Integer Arithmetic
- Scoring-based Static Variable Ordering for Decision Diagram-based Quantum Circuit Simulation
- Comparing State-Representations for DEL Model Checking
- GROOT: Graph Edge Re-growth and Partitioning for the Verification of Large Designs in Logic Synthesis
- Profile Generators: A Link between the Narrative and the Binary Matrix Representation
- Nonuniform abstractions, refinement and controller synthesis with novel\n BDD encodings
- Synthesis of coordination programs from linear temporal logic
- Formal Analysis of Galois Field Arithmetics - Parallel Verification and Reverse Engineering
- Case-Factor Diagrams for Structured Probabilistic Modeling
- BDD2Seq: Enabling Scalable Reversible-Circuit Synthesis via Graph-to-Sequence Learning
- Approximate Equivalence Checking of Noisy Quantum Circuits
- Simulation-Checking of Real-Time Systems with Fairness Assumptions
- Janus: Leveraging Incremental Computation for Efficient DNS Verification
- Comparative Analysis of Discrete and Continuous Action Spaces in Reservoir Management and Inventory Control Problems
- Using ROBDDs for Inference in Bayesian Networks with Troubleshooting as\n an Example
- A Concept Learning Tool Based On Calculating Version Space Cardinality
- Symblicit algorithms for optimal strategy synthesis in monotonic Markov decision processes (extended version)
- Novel Direct Algorithm for Computing Simultaneous All-Levels Reliability of Multi-state Flow Networks
- Sciduction: Combining Induction, Deduction, and Structure for Verification and Synthesis
- On the Tractability of SHAP Explanations
- Logic Column 19: Symbolic Model Checking for Temporal-Epistemic Logics
- Symmetric Logic Synthesis with Phase Assignment
- Declarative Combinatorics: Boolean Functions, Circuit Synthesis and BDDs in Haskell
- Pragmatic random sampling of Kconfig-based systems: A unified approach
- Quantum Ordered Binary Decision Diagrams with Repeated Tests
- Boolean Equi-propagation for Optimized SAT Encoding
- Using binary decision diagrams for constraint handling in combinatorial\n interaction testing
- SICS: Secure In-Cloud Service Function Chaining
- Temporal Runtime Verification using Monadic Difference Logic
- ATL*AS: An Automata-Theoretic Approach and Tool for the Verification of Strategic Abilities in Multi-Agent Systems
- Corpus-compressed Streaming and the Spotify Problem
- On the Complexity of Symbolic Finite-State Automata
- On the Complexity of Language Membership for Probabilistic Words
- Breaking the Treewidth Barrier in Quantum Circuit Simulation with Decision Diagrams
- SPUDD: Stochastic Planning using Decision Diagrams
- On Continuous Optimization for Constraint Satisfaction Problems
- Embedding of Large Boolean Functions for Reversible Logic
- Exact Synthesis of Reversible Logic Circuits using Model Checking
- An Efficient Genetic Programming System with Geometric Semantic Operators and its Application to Human Oral Bioavailability Prediction
- Optimizing Memory Efficiency and Index Ordering to Simulate Quantum Circuits Using Tensor Decision Diagrams
- Determining the Most Promising Selective Backbone Size for Partial Knowledge Compilation
- Revisiting Pseudo-Boolean Encodings from an Integer Perspective
- Witness Generation for Classical JSON Schema
- Reactive synthesis specification review for validity and quality
- Proceedings of the Fifth International Workshop on Automated Debugging (AADEBUG 2003)
- From Boolean Functional Equations to Control Software
- A Map-Reduce Parallel Approach to Automatic Synthesis of Control\n Software
- Enhanced Formal Verification Flow for Circuits Integrating Debugging and Coverage Analysis
- Efficient & Correct Predictive Equivalence for Decision Trees
- Exact Computation of Influence Spread by Binary Decision Diagrams
- FeynmanDD: Quantum Circuit Analysis with Classical Decision Diagrams
- Context-Specific Independence in Bayesian Networks
- Automata-based Quantitative Verification
- PubTree: A Hierarchical Search Tool for the MEDLINE Database
- Probabilistic Inference for Datalog with Correlated Inputs
- Tuning Random Generators: Property-Based Testing as Probabilistic Programming
- CrocoPat 2.1 Introduction and Reference Manual
- Symbolic Synthesis of Knowledge-based Program Implementations with\n Synchronous Semantics
- On Compiling DNNFs without Determinism
- Quantum Algorithm for Optimization and Polynomial System Solving over Finite Field and Application to Cryptanalysis
- Numerical Considerations in Weighted Model Counting
- Quantum Spectral Reasoning: A Non-Neural Architecture for Interpretable Machine Learning
- Automatic predicate abstraction of C programs
- On Efficiently Explaining Graph-Based Classifiers
- A SAT-Based Algorithm for Computing Attractors in Synchronous Boolean Networks
- Resolution Simulates Ordered Binary Decision Diagrams for Formulas in Conjunctive Normal Form
- Binary Decision Diagrams for Bin Packing with Minimum Color\n Fragmentation
- Efficient Explanations for Knowledge Compilation Languages
- Model-based stochastic analysis with probabilistic graph query evaluation
- Processor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic
- AND/OR Multi-Valued Decision Diagrams (AOMDDs) for Weighted Graphical\n Models
- Ackermann Encoding, Bisimulations, and OBDDs
- Energy mu-Calculus: Symbolic Fixed-Point Algorithms for omega-Regular Energy Games
- Computation of the Activity-on-Node Binary-State Reliability with Uncertainty Components
- On the complexity of finite valued functions
- On Verifying Complex Properties using Symbolic Shape Analysis
- TCTL Inevitability Analysis of Dense-time Systems
- Universal Lossless Data Compression Via Binary Decision Diagrams
- Reasoning about Bayesian Network Classifiers
- Large Random Forests: Optimisation for Rapid Evaluation
- On Algorithms and Complexity for Sets with Cardinality Constraints
- Network-driven Boolean Normal Forms
- Development of SyReC based expandable reversible logic circuits
- Modeling component connectors in Reo by constraint automata
- Counting Independent Sets and Kernels of Regular Graphs
- On the Relationship between Sum-Product Networks and Bayesian Networks
- Declarative Combinatorics: Isomorphisms, Hylomorphisms and Hereditarily Finite Data Types in Haskell
- Neural, Symbolic and Neural-Symbolic Reasoning on Knowledge Graphs
- Bandwidth and Wavefront Reduction for Static Variable Ordering in\n Symbolic Model Checking
- Algorithms for reachability problems on stochastic Markov reward models
- Bounded Model Checking of RISC-V Machine Code with Context-Free-Language Ordered Binary Decision Diagrams
- BDD4BNN: A BDD-based Quantitative Analysis Framework for Binarized Neural Networks
- Symbolic Parametric Analysis of Embedded Systems with BDD-like Data-Structures
- Engineering an LTLf Synthesis Tool
- Compressing Binary Decision Diagrams
- Inferring the role of transcription factors in regulatory networks. [europepmc]
- BioQuali Cytoscape plugin: analysing the global consistency of regulatory networks. [europepmc]
- Nanowire systems: technology and design. [europepmc]
- An efficient algorithm for identifying primary phenotype attractors of a large-scale Boolean network. [europepmc]
- Shield synthesis. [europepmc]
- Performance heuristics for GR(1) synthesis and related algorithms. [europepmc]
- Notes on Computational Uncertainties in Probabilistic Risk/Safety Assessment. [europepmc]
- Incremental column-wise verification of arithmetic circuits using computer algebra. [europepmc]
- An Efficient, Parallelized Algorithm for Optimal Conditional Entropy-Based Feature Selection. [europepmc]
- Exploring attractor bifurcations in Boolean networks. [europepmc]
- A Kamm's Circle-Based Potential Risk Estimation Scheme in the Local Dynamic Map Computation Enhanced by Binary Decision Diagrams. [europepmc]
- Trap spaces of multi-valued networks: definition, computation, and applications. [europepmc]
- Logical Resolving-Based Methodology for Efficient Reliability Analysis. [europepmc]
- Combining greedy and evolutionary algorithms to maximize influence in networks under deterministic linear threshold model. [europepmc]
- Solving Bitvectors with MCSAT: Explanations from Bits and Pieces [europepmc]
Related