Exact minimization of binary decision diagrams using implicit techniques
See where this sits in the topic map →Summary AI-generated
- TL;DR
- This paper presents an exact algorithm for minimizing binary decision diagrams (BDDs) when working with incompletely specified functions and don't care sets.
- Problem
- Finding a minimum-size BDD representation for an incompletely specified function under a fixed variable ordering is challenging, and previous exact approaches relied on enumerating assignments within the don't care set.
- Method
- The authors formulate the BDD minimization problem as a binate covering problem, solving it using implicit enumeration techniques similar to those used for reducing incompletely specified finite state machines.
- Results
- The authors prove that the problem is NP-complete and demonstrate through experiments that their implicit algorithm can solve a class of interesting test cases exactly.
- Contributions
- The paper introduces the only known exact algorithm for this BDD minimization problem that avoids enumerating don't care set assignments, and provides a comparison against existing heuristic algorithms.
- Limitations
- Not specified in the abstract.
- Takeaways
- The proposed exact algorithm successfully finds minimum-sized BDDs and serves as a benchmark to measure the quality of existing heuristic approaches.
- Applications
- Not specified in the abstract.
- Topics
- Binary decision diagrams, logic minimization, implicit techniques, NP-completeness
- For industry
- Not specified in the abstract.
- Why it matters
- Not specified in the abstract.
Abstract
This paper addresses the problem of binary decision diagram (BDD) minimization in the presence of don't care sets. Specifically given an incompletely specified function g and a fixed ordering of the variables, we propose an exact algorithm for selecting f such that f is a cover for g and the binary decision diagram for f is of minimum size. The approach described is the only known exact algorithm for this problem not based on the enumeration of the assignments to the points in the don't care set. We show also that our problem is NP-complete. We show that the BDD minimization problem can be formulated as a binate covering problem and solved using implicit enumeration techniques. In particular, we show that the minimum-sized binary decision diagram compatible with the specification can be found by solving a problem that is very similar to the problem of reducing incompletely specified finite state machines. We report experiments of an implicit implementation of our algorithm, by means of which a class of interesting examples was solved exactly. We compare it with existing heuristic algorithms to measure the quality of the latter.