Graph-Based Algorithms for Boolean Function Manipulation

DOI10.1109/TC.1986.1676819zbMath0593.94022OpenAlexW2080267935WikidataQ56028213 ScholiaQ56028213MaRDI QIDQ3724245

Randal E. Bryant

Publication date: 1986

Published in: IEEE Transactions on Computers (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1109/tc.1986.1676819

zbMATH Keywords

time complexitydata structure for representing Boolean functionsdirected, acyclic graphslogic design verification

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Symbolic computation and algebraic computation (68W30) Applications of graph theory to circuits and networks (94C15)

Related Items

The complexity of minimizing and learning OBDDs and FBDDs, An exercise in the automatic verification of asynchronous designs, Constraint programming and operations research, On the complexity of analysis and manipulation of Boolean functions in terms of decision graphs, Introduction to the OBDD algorithm for the ATP community, Randomized OBDD-based graph algorithms, Efficient approach of translating LTL formulae into Büchi automata, Weighted \(A^*\) search - unifying view and application, Efficient data structures for Boolean functions, Property preserving abstractions for the verification of concurrent systems, Using integer programming to verify general safety and liveness properties, SAT-solving in practice, with a tutorial example from supervisory control, Nondeterministic ordered binary decision diagrams with repeated tests and various modes of acceptance, Why does Astrée scale up?, A rewriting approach to binary decision diagrams, Practical verification of multi-agent systems against \textsc{Slk} specifications, Applying ad-hoc global constraints with the case constraint to still-life, Symbolic perimeter abstraction heuristics for cost-optimal planning, Deriving escape analysis by abstract interpretation, A reducibility concept for problems defined in terms of ordered binary decision diagrams, Symbolic techniques in satisfiability solving, The formal-CAFE methodology and model checking patterns in the specification of e-commerce systems, Data structures for symbolic multi-valued model-checking, State based control of timed discrete event systems using binary decision diagrams, TPS: A hybrid automatic-interactive system for developing proofs, Approximating Boolean functions by OBDDs, A novel OBDD-based reliability evaluation algorithm for wireless sensor networks on the multicast model, A BDD SAT solver for satisfiability testing: An industrial case study, Providing a formal linkage between MDG and HOL, A theory of formal synthesis via inductive learning, Exponential space complexity for OBDD-based reachability analysis, Weighted positive binary decision diagrams for exact probabilistic inference, Size of ordered binary decision diagrams representing threshold functions, Petri nets, traces, and local model checking, An improved algorithm for the evaluation of fixpoint expressions, Lagrangian bounds from decision diagrams, Decomposition of a system of incompletely specified Boolean functions defined with a binary decision diagram, On the non-termination of MDG-based abstract state enumeration, On the use of MTBDDs for performability analysis and verification of stochastic systems., Model-checking large structured Markov chains., Guess-and-verify versus unrestricted nondeterminism for OBDDs and one-way Turing machines., Forms of representation for simple games: sizes, conversions and equivalences, The complexity of reasoning with FODD and GFODD, Shield synthesis, Approximating minimal unsatisfiable subformulae by means of adaptive core search, How to fake an RSA signature by encoding modular root finding as a SAT problem, Resolution and binary decision diagrams cannot simulate each other polynomially, A satisfiability procedure for quantified Boolean formulae, A unifying view on SMT-based software verification, An explicit transition system construction approach to LTL satisfiability checking, A lower bound for integer multiplication on randomized ordered read-once branching programs., Logic programs as compact denotations., Binary decision diagrams for first-order predicate logic., Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors., BDDs -- design, analysis, complexity, and applications., Synthesis of autosymmetric functions in a new three-level form, Relational semigroupoids: abstract relation-algebraic interfaces for finite relations between infinite types, Symbolic state-space exploration and numerical analysis of state-sharing composed models, Automatic symbolic compositional verification by learning assumptions, Minimisation of acyclic deterministic automata in linear time, Efficient SAT-based bounded model checking for software verification, Symbolic model checking: \(10^{20}\) states and beyond, Automatic verification of distributed systems: the process algebra approach., On the computational power of binary decision diagram with redundant variables., Hiding propositional constants in BDDs., Decision-making coordination and efficient reasoning techniques for feature-based configuration, An MDD-based generalized arc consistency algorithm for positive and negative table constraints and some global constraints, Deciding effectively propositional logic using DPLL and substitution sets, A note on the size of OBDDs for the graph of integer multiplication, Solving games via three-valued abstraction refinement, A direct construction of polynomial-size OBDD proof of pigeon hole problem, On the size of (generalized) OBDDs for threshold functions, Information loss in knowledge compilation: a comparison of Boolean envelopes, Causal analysis with chain event graphs, Binary superposed quantum decision diagrams, Representation of graphs by OBDDs, Translation among CNFs, characteristic models and ordered binary decision diagrams, A very simple function that requires exponential size nondeterministic graph-driven read-once branching programs, Compressing probabilistic Prolog programs, On the OBDD size for graphs of bounded tree- and clique-width, On threshold BDDs and the optimal variable ordering problem, Completeness and non-completeness results with respect to read-once projections, Hierarchy theorems for \(k\)OBDDs and \(k\)IBDDs, The symbolic OBDD scheme for generating mechanical assembly sequences, AND/OR search spaces for graphical models, Polybori: A framework for Gröbner-basis computations with Boolean polynomials, STG decomposition strategies in combination with unfolding, Optimal ordered binary decision diagrams for read-once formulas, Simplification of boolean verification conditions, Automata of asynchronous behaviors, Automating the addition of fault tolerance with discrete controller synthesis, Bypassing BDD construction for reliability analysis, Stochastic dynamic programming with factored representations, Simplification in a satisfiability checker for VLSI applications, Reduction of OBDDs in linear time, Time-space tradeoffs for branching programs, Ordered binary decision diagrams as knowledge-bases, On the evolution of the worst-case OBDD size, Lower bounds for linearly transformed OBDDs and FBDDs, An experience in proving regular networks of processes by modular model checking, Pair-independence and freeness analysis through linear refinement., Ordered binary decision diagrams and the Shannon effect, Reasoning with ordered binary decision diagrams, A layered algorithm for quantifier elimination from linear modular constraints, Generating BDDs for symbolic model checking in CCS, FPT algorithms to enumerate and count acyclic and totally cyclic orientations, An efficient algorithm for computing bisimulation equivalence, Bounded model checking of infinite state systems, Better upper bounds on the QOBDD size of integer multiplication, Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams, Partition search for non-binary constraint satisfaction, Implementing semantic merging operators using binary decision diagrams, Running time experiments on some algorithms for solving propositional satisfiability problems, Variable ordering for decision diagrams: a portfolio approach, Symbolic model checking for channel-based component connectors, State-set branching: leveraging BDDs for heuristic search, On propositional definability, The footprint form of a matrix: definition, properties, and an application, Classical length-5 pattern-avoiding permutations, Efficient operations between MDDs and constraints, Dealing with the product constraint, Using ordered binary decision diagrams to factorize multi-level logic, Relation-algebraic modeling and solution of chessboard independence and domination problems, Compact representation of near-optimal integer programming solutions, Symbolic synthesis of masking fault-tolerant distributed programs, Integrated integer programming and decision diagram search tree with an application to the maximum independent set problem, Synthesis of least restrictive controllable supervisors for extended finite-state machines with variable abstraction, Randomized OBDDs for the most significant bit of multiplication need exponential space, \(k\)-optimal: a novel approximate inference algorithm for ProbLog, Optimal Boolean lattice-based algorithms for the U-curve optimization problem, Formal verification based on Boolean expression diagrams, Exact OBDD bounds for some fundamental functions, The \(Multi\)-SAT algorithm, Incremental column-wise verification of arithmetic circuits using computer algebra, Exact quantitative probabilistic model checking through rational search, Extracting co-occurrence relations from ZDDs, Model checking properties on reduced trace systems, Symbolic coloured SCC decomposition, Outlier detection using binary decision diagrams, GR(1)*: GR(1) specifications extended with existential guarantees, Model checking temporal properties of reaction systems, Star-topology decoupled state space search, Code aware resource management, Verification and enforcement of access control policies, Binary decision diagrams for generating and storing non-dominated project portfolios with interval-valued project scores, Learning from interpretation transition, Computation of signal output probability for Boolean functions represented by OBDD, MDDs are efficient modeling tools: an application to some statistical constraints, On finding the optimal BDD relaxation, A deterministic algorithm for testing the equivalence of read-once branching programs with small discrepancy, Combinatorics and algorithms for low-discrepancy roundings of a real sequence, Compositional verification and 3-valued abstractions join forces, Minimization of binary decision diagrams for systems of incompletely defined Boolean functions, On the order of test goals in specification-based testing, Dynamic programming algorithms for computing power indices in weighted multi-tier games, Minimization problems for parity OBDDs, \( \mathrm{A}^*\) -based construction of decision diagrams for a prize-collecting scheduling problem, An analysis of root functions -- a subclass of the impossible class of faulty functions (ICFF), A probabilistic interval-based event calculus for activity recognition, FCA for software product line representation: mixing configuration and feature relationships in a unique canonical representation, Extending greedy feature selection algorithms to multiple solutions, Computing AES related-key differential characteristics with constraint programming, On the computation of the Möbius transform, Generating extended resolution proofs with a BDD-based SAT solver, Boolean functional synthesis: hardness and practical algorithms, A complete adaptive algorithm for propositional satisfiability, Performance heuristics for GR(1) synthesis and related algorithms, Binary-decision-diagram-based decomposition of Boolean functions into reversible logic elements, Non-clausal redundancy properties, Dual proof generation for quantified Boolean formulas with a BDD-based solver, A compositional approach to probabilistic knowledge compilation, Boolean unification - the story so far, A 3D 12-subiteration thinning algorithm based on \(P\)-simple points, On the relative succinctness of sentential decision diagrams, A framework for memory efficient context-sensitive program analysis, From MDD to BDD and arc consistency, Hardness of indentifying the minimum ordered binary decision diagram, DenseZDD: a compact and fast index for families of sets, Nonblocking supervisory control of state-tree structures with event forcing, Solving bitvectors with MCSAT: explanations from bits and pieces, Reordering decision diagrams for quantum computing is harder than you might think, A combinatorial cut-and-lift procedure with an application to 0-1 second-order conic programming, On the descriptive and algorithmic power of parity ordered binary decision diagrams, On the power of Las Vegas for one-way communication complexity, OBDDs, and finite automata, The nonapproximability of OBDD minimization, The small model property: How small can it be?, Is your model checker on time? On the complexity of model checking for timed modal logics, Symbolic model checking of timed guarded commands using difference decision diagrams, Iterating transducers, Syntax-directed model checking of sequential programs, Variable stabilisation in Boolean monotonic model pools, State complexity of finite partial languages, On the error resilience of ordered binary decision diagrams, Checking constraint satisfaction, Improving branch-and-bound using decision diagrams and reinforcement learning, Graph coloring with decision diagrams, Davis and Putnam meet Henkin: solving DQBF with resolution, ProCount: weighted projected model counting with graded project-join trees, Proof complexity of symbolic QBF reasoning, DQBDD: an efficient BDD-based DQBF solver, Incorporating bounds from decision diagrams into integer programming, \textsf{BDD4BNN}: a BDD-based quantitative analysis framework for binarized neural networks, Computing bottom SCCs symbolically using transition guided reduction, Adapting behaviors via reactive synthesis, Model checking \(\omega \)-regular properties with decoupled search, Boolean polynomials, BDDs and CRHS equations -- connecting the dots with CryptaPath, Using OBDDs to handle dynamic constraints, Parity OBDDs cannot be handled efficiently enough, Worst case examples for operations on OBDDs, On the computational power of linearly transformed BDDs, Fast computation of bounds for two-terminal network reliability, Synthesizing efficient systems in probabilistic environments, Sequence binary decision diagram: minimization, relationship to acyclic automata, and complexities of Boolean set operations, Complex event processing over distributed probabilistic event streams, On the OBDD representation of some graph classes, Augmenting measure sensitivity to detect essential, dispensable and highly incompatible features in mass customization, Probabilistic abductive logic programming using Dirichlet priors, Degeneralization algorithm for generation of Büchi automata based on contented situation, On a class of decision diagrams, Efficient symbolic search for cost-optimal planning, Decomposition of systems of Boolean functions determined by binary decision diagrams, Knowledge compilation meets database theory: compiling queries to decision diagrams, Towards the hierarchical verification of reactive systems, String-matching with OBDDs, Bounded model checking of ETL cooperating with finite and looping automata connectives, An information statistics approach to data stream and communication complexity, Partially-shared zero-suppressed multi-terminal BDDs: Concept, algorithms and applications, Computing and visualizing Banks sets of dominance relations using relation algebra and RelView, Enumerative encoding of correlation-immune Boolean functions, A characteristic set method for solving Boolean equations and applications in cryptanalysis of stream ciphers, CGMurphi: automatic synthesis of numerical controllers for nonlinear hybrid systems, Decomposition representations of logical equations in problems of inversion of discrete functions, Characteristics of the maximal independent set ZDD, Stochastic relational processes: efficient inference and applications, Constraint-based probabilistic modeling for statistical abduction, Decision-theoretic planning with generalized first-order decision diagrams, MDD propagators with explanation, Symbolic supervisory control of infinite transition systems under partial observation using abstract interpretation, On symbolic OBDD-based algorithms for the minimum spanning tree problem, Efficient solutions to factored MDPs with imprecise transition probabilities, Symbolic bounded synthesis, Counterexamples to the long-standing conjecture on the complexity of BDD binary operations, Linear temporal logic symbolic model checking, Automatic verification of reduction techniques in higher order logic, Efficient verification of distributed real-time systems with broadcasting behaviors, Magic-sets for localised analysis of Java bytecode, Message-passing algorithms for inference and optimization, Curriculum-based course timetabling with SAT and MaxSAT, On efficient implicit OBDD-based algorithms for maximal matchings, Implicit computation of maximum bipartite matchings by sublinear functional operations, Quantifier elimination by dependency sequents, Verification of Galois field based circuits by formal reasoning based on computational algebraic geometry, De Bruijn sequences and complexity of symmetric functions, Bounded semantics, Formal reliability analysis of redundancy architectures, Ancilla-free synthesis of large reversible functions using binary decision diagrams, Proving implications by algebraic approximation, On the effect of local changes in the variable ordering of ordered decision diagrams, On the size of binary decision diagrams representing Boolean functions, Graph driven BDDs -- a new data structure for Boolean functions, On the minimization of (complete) ordered binary decision diagrams, Component-wise incremental LTL model checking, A novel graphical technique for combinational logic representation and optimization, Compact representations of all members of an independence system, Dualization of Boolean functions using ternary decision diagrams, State space search nogood learning: online refinement of critical-path dead-end detectors in planning, Synthesis of obfuscation policies to ensure privacy and utility, Gate-delay-fault testability properties of multiplexor-based networks, A model for synchronous switching circuits and its theory of correctness, Probabilistic verification of Boolean functions, Symbolic trajectory evaluation for word-level verification: theory and implementation, A novel node-based sequential implicit enumeration method for finding all \(d\)-MPs in a multistate flow network, A symbolic model for timed concurrent constraint programming, Power indices of simple games and vector-weighted majority games by means of binary decision diagrams, Dynamically consistent reduction of logical regulatory graphs, Z2SAL: a translation-based model checker for Z, SampleSearch: importance sampling in presence of determinism, State agnostic planning graphs: deterministic, non-deterministic, and probabilistic planning, IDD-based model validation of biochemical networks, Larger lower bounds on the OBDD complexity of integer multiplication, Performance assessment and reliability analysis of dependable and distributed computing systems based on BDD and recursive merge, Abstract reduction in directed model checking CCS processes, Conditional independence and chain event graphs, A moderately exponential time algorithm for \(k\)-IBDD satisfiability, SCIP: solving constraint integer programs, On best-possible obfuscation, A symbolic shortest path algorithm for computing subgame-perfect Nash equilibria, Symbolic constraint handling through unification in finite algebras, Game-theoretic simulation checking tool, On limitations of structured (deterministic) DNNFs, Handling high dimensionality contexts in formal concept analysis via binary decision diagrams, CPCES: a planning framework to solve conformant planning problems through a counterexample guided refinement, Weak, strong, and strong cyclic planning via symbolic model checking, On the computational complexity of qualitative coalitional games, Conformant planning via symbolic model checking and heuristic search, Polynomials for classification trees and applications, Distributed symbolic model checking for \(\mu\)-calculus, Combining symmetry reduction and under-approximation for symbolic model checking, A formal framework for verification of embedded custom memories of the Motorola MPC7450 microprocessor, Constraint solving in uncertain and dynamic environments: A survey, On the Influence of the State Encoding on OBDD-Representations of Finite State Machines, REGULAR STATE MACHINES, Graph Coloring Lower Bounds from Decision Diagrams, Property preserving abstractions under parallel composition, Lifting for Simplicity: Concise Descriptions of Convex Sets, On the Complexity of the Hidden Weighted Bit Function for Various BDD Models, Compacting Boolean Formulae for Inference in Probabilistic Logic Programming, A Moderately Exponential Time Algorithm for k-IBDD Satisfiability, Characterizing the Complexity of Boolean Functions represented by Well-Structured Graph-Driven Parity-FBDDs, Unnamed Item, Symbolic Termination and Confluence Checking for ECA Rules, Evaluating CDCL Variable Scoring Schemes, Compositional Reasoning for Multi-modal Logics, Improving Variable Orderings of Approximate Decision Diagrams Using Reinforcement Learning, Symbolic Model Checking for Dynamic Epistemic Logic, Randomized OBDD-Based Graph Algorithms, Symbolic Model Checking for Alternating Projection Temporal Logic, Unnamed Item, Symbolic model checking for probabilistic processes, Network Models for Multiobjective Discrete Optimization, Models and Algorithms for the Bin-Packing Problem with Minimum Color Fragmentation, On the Tractability of SHAP Explanations, Ordered Binary Decision Diagrams and the Davis-Putnam procedure, Verification of asynchronous circuits by BDD-based model checking of Petri nets, Synthesis for testability: Binary Decision Diagrams, On the complexity of constructing optimal ordered binary decision diagrams, Graph models for PLA folding problems, Exploiting symmetry of state tree structures for discrete-event systems with parallel components, On the OBDD Complexity of the Most Significant Bit of Integer Multiplication, A probabilistic logic programming event calculus, Inference and learning in probabilistic logic programs using weighted Boolean formulas, Knowledge compilation of logic programs using approximation fixpoint theory, Decision Diagrams for Discrete Optimization: A Survey of Recent Advances, A Symbolic Algorithm for the Synthesis of Bounded Petri Nets, Hierarchical Set Decision Diagrams and Automatic Saturation, A View from the Engine Room: Computational Support for Symbolic Model Checking, Transitive q-Ary Functions over Finite Fields or Finite Sets: Counts, Properties and Applications, Shared Ordered Binary Decision Diagrams for Dempster-Shafer Theory, Unnamed Item, A Theoretical and Numerical Analysis of the Worst-Case Size of Reduced Ordered Binary Decision Diagrams, Properties of Switch-List Representations of Boolean Functions, Improved BDD Algorithms for the Simulation of Quantum Circuits, Deciding Effectively Propositional Logic Using DPLL and Substitution Sets, Target Cuts from Relaxed Decision Diagrams, Incremental hierarchical construction of modular supervisors for discrete-event systems, Une approche intentionnelle du calcul des implicants premiers et essentiels des fonctions booléennes, Reduced state space representation for unbounded vector state spaces, OKFDDs versus OBDDs and OFDDs, Formal Verification of Integer Multiplier Circuits Using Algebraic Reasoning: A Survey, GenMul: Generating Architecturally Complex Multipliers to Challenge Formal Verification Tools, Assume–guarantee verification of nonlinear hybrid systems with <scp>Ariadne</scp>, On random orderings of variables for parity ordered binary decision diagrams, Rank-Based Symbolic Bisimulation, A New 3D 12-Subiteration Thinning Algorithm Based on P-Simple Points, Unnamed Item, Unnamed Item, IMPLEMENTING COMPLEX DOMAINS OF APPLICATION IN AN EXTENDED PROLOG SYSTEM, Dynamic processor allocation in scalable multiprocessors using boolean algebra^*, FSM Encoding for BDD Representations, Decomposition-based logic synthesis for PAL-based CPLDs, A Scalable Segmented Decision Tree Abstract Domain, What Is in a Step: New Perspectives on a Classical Question, The Mechanical Verification of a DPLL-Based Satisfiability Solver, Meanings of Model Checking, On the OBDD Complexity of Threshold Functions and the Variable Ordering Problem, Symbolic State-Space Generation of Asynchronous Systems Using Extensible Decision Diagrams, Symbolic Reachability Analysis of Integer Timed Petri Nets, Tutorial on Model Checking: Modelling and Verification in Computer Science, From Philosophical to Industrial Logics, A Unified Framework for Certificate and Compilation for QBF, Unnamed Item, Exact OBDD Bounds for Some Fundamental Functions, On the descriptive and algorithmic power of parity ordered binary decision diagrams, Optimized Colored Nets Unfolding, From Monadic Logic to PSL, Automata-Theoretic Model Checking Revisited, Probabilistic DL Reasoning with Pinpointing Formulas: A Prolog-based Approach, Hierarchical Set Decision Diagrams and Regular Models, Larger Lower Bounds on the OBDD Complexity of Integer Multiplication, Proving with BDDs and control of information, Does My Service Have Partners?, An Operator for Removal of Subsumed Clauses, New dimensions in non‐classical neural computing, Complexity Theoretical Results on Nondeterministic Graph-driven Read-Once Branching Programs, PITL2MONA: Implementing a Decision Procedure for Propositional Interval Temporal Logic, A New Algorithm for Partitioned Symbolic Reachability Analysis, LCF-style Platform based on Multiway Decision Graphs, An efficient relational deductive system for propositional non-classical logics, BDD-based decision procedures for the modal logic K ★, Symbolic CTL Model Checking of Asynchronous Systems Using Constrained Saturation, Discrete-Event Systems Fault Diagnosis, Unnamed Item, Exact Multiple Sequence Alignment by Synchronized Decision Diagrams, Unnamed Item, Unnamed Item, On the relation between BDDs and FDDs, FINDING SMALL EQUIVALENT DECISION TREES IS HARD, Implementing Efficient All Solutions SAT Solvers, Decision diagrams for solving a job scheduling problem under precedence constraints, On Quantifying Literals in Boolean Logic and its Applications to Explainable AI, Using variable-entered Karnaugh maps to produce compact parametric general solutions of Boolean equations, Model checking workflow net based on Petri net, Implicit Computation of Maximum Bipartite Matchings by Sublinear Functional Operations, Efficient Problem Solving on Tree Decompositions Using Binary Decision Diagrams, Modeling for Verification, Binary Decision Diagrams, BDD-Based Symbolic Model Checking, Propositional SAT Solving, SAT-Based Model Checking, Combining Model Checking and Data-Flow Analysis, Transfer of Model Checking to Industrial Practice, Symbolic Model Checking in Non-Boolean Domains, Factorization using binary decision diagrams, Structure-based deadlock checking of asynchronous circuits, A Fast Symbolic Transformation Based Algorithm for Reversible Logic Synthesis, Checking Reversibility of Boolean Functions, Relation Algebras, Matrices, and Multi-valued Decision Diagrams, Exploiting interleaving semantics in symbolic state-space generation, Probabilistic argumentation, Quantum adiabatic machine learning, Theoretical insights and algorithmic tools for decision diagram-based optimization, Unnamed Item, Efficient incremental planning and learning with multi-valued decision diagrams, Symblicit algorithms for mean-payoff and shortest path in monotonic Markov decision processes, Exact stochastic constraint optimisation with applications in network analysis, Processing succinct matrices and vectors, Finding suitable variability abstractions for lifted analysis, Algebraic Attacks Using Binary Decision Diagrams, A realistic involvement of formal methods, Formal verification of synchronous data-flow program transformations toward certified compilers, The Minimal Hitting Set Generation Problem: Algorithms and Computation, Advanced exact synthesis of Clifford+T circuits, Efficiently Deciding μ-Calculus with Converse over Finite Trees, Model checking of pushdown systems for projection temporal logic, Tight upper bounds for the expected loss of lexicographic heuristics in binary multi-attribute choice, Optimization Bounds from Binary Decision Diagrams, New results on the most significant bit of integer multiplication, On the OBDD complexity of the most significant bit of integer multiplication, SILVER -- statistical independence and leakage verification, The symbolic algorithms for maximum flow in networks, Representing abstract dialectical frameworks with binary decision diagrams, Minimizing binary decision diagrams for systems of incompletely defined Boolean functions using algebraic cofactor expansions, NuMDG: a new tool for multiway decision graphs construction, OBDD-Based Load Shedding Algorithm for Power Systems, Unnamed Item, Deadlock-freedom in component systems with architectural constraints, Optimized temporal monitors for SystemcC, Priority functions for the approximation of the metric TSP, A simpler counterexample to a long-standing conjecture on the complexity of Bryant's apply algorithm, Strong planning under partial observability, A formal framework for the decentralised diagnosis of large scale discrete event systems and its application to telecommunication networks, Symbolic Model Checking the Knowledge in Herbivore Protocol, Towards Parallel Boolean Functional Synthesis, Forward Bisimulations for Nondeterministic Symbolic Finite Automata, Case-factor diagrams for structured probabilistic modeling, Visualizing SAT instances and runs of the DPLL algorithm, Optimality and condensing of information flow through linear refinement, BDDs for Pseudo-Boolean Constraints – Revisited, DPLL+ROBDD Derivation Applied to Inversion of Some Cryptographic Functions, πDD: A New Decision Diagram for Efficient Problem Solving in Permutation Space, Symbolic topological sorting with OBDDs, Modeling and Verification of a Protocol for Operational Support Using Coloured Petri Nets, Importance Sampling on Bayesian Networks with Deterministic Causalities, Symbolic graphs: Linear solutions to connectivity related problems, Using variable-entered karnaugh maps to solve boolean equations, MONA IMPLEMENTATION SECRETS, Unnamed Item, Construction of the tests of combinational circuit failures by analyzing the orthogonal disjunctive normal forms represented by the alternative graphs, On-line resources allocation for ATM networks with rerouting, Restricted Nondeterministic Read-Once Branching Programs and an Exponential Lower Bound for Integer Multiplication, Learning probabilistic decision graphs, Lower bounds for restricted read-once parity branching programs, An algorithm for strongly connected component analysis in \(n \log n\) symbolic steps, Compositional SCC analysis for language emptiness, Constructing efficient formal models from high-level descriptions using symbolic simulation, Embedded software verification using symbolic execution and uninterpreted functions, Boolean expression diagrams, Parity graph-driven read-once branching programs and an exponential lower bound for integer multiplication, The Boolean Constraint Solver of SWI-Prolog (System Description), Mutation-Based Test Case Generation for Simulink Models, Discrete Optimization with Decision Diagrams, Solving the Pricing Problem in a Branch-and-Price Algorithm for Graph Coloring Using Zero-Suppressed Binary Decision Diagrams, Randomized OBDDs for the Most Significant Bit of Multiplication Need Exponential Size, Finding the Description of Structure by Counting Method: A Case Study, On the automatic HDL bug identification, Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams, DRAT Proofs for XOR Reasoning, On the Structure of Counterexamples to Symmetric Orderings for BDD's, On the Relationship between LTL Normal Forms and Büchi Automata, A hierarchy result for read-once branching programs with restricted parity nondeterminism, On the influence of the variable ordering for algorithmic learning using OBDDs, A 3D 6-subiteration curve thinning algorithm based on \(P\)-simple points, Using heuristic search for finding deadlocks in concurrent systems, ACTION FAILURE RECOVERY VIA MODEL-BASED DIAGNOSIS AND CONFORMANT PLANNING, Bounds on the OBDD-size of integer multiplication via universal hashing, On the properties of combination set operations., Distributing the Workload in a Lazy Theorem-Prover, Automated formal analysis and verification: an overview, Modular supervisory control and coordination of state tree structures, Implementing Relational Specifications in a Constraint Functional Logic Language, Be lazy and don't care: faster CTL model checking for recursive state machines, ZDD-based algorithmic framework for solving shortest reconfiguration problems, Combining incomplete search and clause generation: an application to the orienteering problems with time windows, A survey on compositional algorithms for verification and synthesis in supervisory control, Generating Extended Resolution Proofs with a BDD-Based SAT Solver, Output-size sensitiveness of OBDD construction through maximal independent set problem, Functional synthesis via input-output separation, Partially unate Boolean functions: properties of their sum-of-products representations, Symbolic verification and strategy synthesis for turn-based stochastic games, On computing probabilistic abductive explanations, On the (complete) reasons behind decisions, Exploiting Asymmetry in Logic Puzzles: Using ZDDs for Symbolic Model Checking Dynamic Epistemic Logic, Evasiveness through binary decision diagrams, Phenotype control of partially specified Boolean networks, Symbolic abstract heaps for polymorphic information-flow guard inference, Boolean functional synthesis: from under the hood of solvers, A decision diagram operation for reachability, Inferring Symbolic Automata, The size of reduced OBDDs and optimal read-once branching programs for almost all Boolean functions, Dissecting \texttt{ltlsynt}, Equivalence checking 40 years after: a review of bisimulation tools, Representing the integer factorization problem using ordered binary decision diagrams, Unnamed Item, Calculational design of a regular model checker by abstract interpretation, Optimization of fixed-polarity Reed-Muller circuits using dual-polarity property, Asymptotically optimal bounds for OBDDs and the solution of some basic OBDD problems, New lower bounds and hierarchy results for restricted branching programs, Size of OBDD representation of 2-level redundancies functions, Ensuring completeness of symbolic verification methods for infinite-state systems, Monotone term decision lists, State complexity of finite partial languages, Lazy regular sensing, Consistency restoration and explanations in dynamic CSPs---Application to configuration, Program Analysis Using Weighted Pushdown Systems, Chain reduction for binary and zero-suppressed decision diagrams, On the Efficient Execution of ProbLog Programs, Symbolic Reachability for Process Algebras with Recursive Data Types, A New Approach for the Construction of Multiway Decision Graphs, The Computational Complexity of Understanding Binary Classifier Decisions, Strategy Graphs for Influence Diagrams, On the upper bounds for complexities of discrete functions