Graph-Based Algorithms for Boolean Function Manipulation
1986/08/01 by Bryant · 8,936 citations
Computer Science · Engineering · Mathematics · #Algorithm #And-inverter graph #Boolean circuit #Boolean function #Computer science #Exponential function #Formal Methods in Verification #Graph #Low-power high-performance VLSI design #Mathematics #Theoretical computer science #VLSI and Analog Circuit Testing
paper · open access · doi:10.1109/tc.1986.1676819
published in IEEE Transactions on Computers C-35(8), 677-691 (Institute of Electrical and Electronics Engineers)
openalex publication_date 1986/08/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/29
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 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 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 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
- FourierCSP: Differentiable Constraint Satisfaction Problem Solving by Walsh-Fourier Expansion
- 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 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 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 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 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
- Complexity of Verifying Nonblockingness in Modular Supervisory Control
- Model checking of spacecraft operational designs: a scalability analysis
- Control Plane Compression
- BDDs Naturally Represent Boolean Functions, and ZDDs Naturally Represent Sets of Sets
- Ordered AND, OR-Decomposition and Binary-Decision Diagram
- On Tractable Representations of Binary Neural Networks
- Binary Decision Diagrams are a Subset of Bayesian Nets
- Partial Quantifier Elimination With Learning
- Novel Bounded Binary-Addition Tree Algorithm for Binary-State Network Reliability Problems
- What's hard about Boolean Functional Synthesis
- On Top-Down Pseudo-Boolean Model Counting
- A static analyzer for large safety-critical software
- Towards Verified Artificial Intelligence
- Properties and constructions of coincident functions
- Efficient Message Passing for 0-1 ILPs with Binary Decision Diagrams
- Symbolic Generalization for On-line Planning
- The trace partitioning abstract domain
- Reverse Engineering of Irreducible Polynomials in GF(2m) Arithmetic
- Weighted Positive Binary Decision Diagrams for Exact Probabilistic Inference
- Scenario Aggregation using Binary Decision Diagrams for Stochastic Programs with Endogenous Uncertainty
- Towards LLM-based Generation of Human-Readable Proofs in Polynomial Formal Verification
- The Mathematical Foundations of Physical Systems Modeling Languages
- Predicate abstraction for software verification
- On the Role of Canonicity in Bottom-up Knowledge Compilation
- Conditioning Probabilistic Databases
- Outsourcing SAT-based Verification Computations in Network Security
- Nearly-Exponential Size Lower Bounds for Symbolic Quantifier Elimination Algorithms and OBDD-Based Proofs of Unsatisfiability
- Removal of Quantifiers by Elimination of Boundary Points
- Partial Quantifier Elimination By Certificate Clauses
- Symbolic Model Checking in External Memory
- Lazy model checking for recursive state machines
- Aggressive Aggregation: a New Paradigm for Program Optimization
- Logic Locking for Secure Outsourced Chip Fabrication: A New Attack and\n Provably Secure Defense Mechanism
- Pairing Functions, Boolean Evaluation and Binary Decision Diagrams in Prolog
- Satisfiability-Based Methods for Reactive Synthesis from Safety Specifications
- Model Checking of Statechart Models: Survey and Research Directions
- A Matrix Product State Representation of Boolean Functions
- Counterexample-guided Planning
- Processing Succinct Matrices and Vectors
- Application of Binary Decision Diagram Approach for Fault Tree Quantification in Seismic Probabilistic Safety Analysis of a Research Reactor
- A Static Analyzer for Large Safety-Critical Software
- A Brief Tour of Logic and Optimization
- Boolean matching for complex PLBs in LUT-based FPGAs with application to architecture evaluation
- The pointer assertion logic engine
- Algebraic decision diagrams and their applications
- Synthesis for testability and verifiability: Polynomial formal verification and test pattern generation for KFDD circuits
- A decade of software model checking with SLAM
- Multi-Terminal Binary Decision Diagrams: An Efficient Data Structure for Matrix Representation
- Decision-Theoretic Planning: Structural Assumptions and Computational Leverage
- State Space Reduction for Reachability Graph of CSM Automata
- Bounded Model Checking Using Satisfiability Solving
- Logical Cryptanalysis as a SAT Problem
- A new FPGA detailed routing approach via search-based Boolean satisfiability
- Boolean Satisfiability Solvers and Their Applications in Model Checking
- Complex Qualitative Models in Biology: a new approach
- Relating biomarkers and phenotypes using dynamical trap spaces
- Minimisation of acyclic deterministic automata in linear time
- Do CFLOBDDs Actually Make Use of Linear Structure?
- Constraint logic programming: a survey
- Constraint Logic Programming
- Fast Obligation Translation and Synthesis
- Use of Rapid Probabilistic Argumentation for Ranking on Large Complex Networks
- Synthesis and optimization of reversible circuits—a survey
- XML Static Analyzer User Manual
- The Beginning of Model Checking: A Personal Perspective
- Model Checking
- Model-Checking
- Computing the Tutte polynomial of a graph of moderate size
- Advanced Many-Valued Logics
- Towards Parallel Boolean Functional Synthesis
- Reliability Evaluation for Demand-Based Warm Standby Systems Considering Degradation Process
- Inference and learning in probabilistic logic programs using weighted Boolean formulas
- A probabilistic logic programming event calculus
- Model Checking in Multiplayer Games Development
- Causality in Configurable Software Systems
- Linear Encodings of Bounded LTL Model Checking
- Predicate Abstraction via Symbolic Decision Procedures
- Knowledge compilation of logic programs using approximation fixpoint theory
- Lower Bounds for Approximate Knowledge Compilation
- Implicit Computation of Filtered Prime Implicants
- 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