LightBDD is a bare-bones library for building and combining Reduced Ordered Binary Decision Diagrams, which are memory-efficient data structures for storing the truth tables of large boolean functions.
Have a look at the Example class too see how it works.
BDDs are used extensively in logic circuit design software and select computer science problems. They can be seen as a binary analog to Directed Acyclic Word Graphs (DAWGs), which use the same graph-based mechanism to reduced the memory footprint of, for instance, spelling dictionaries. For more on BDDs, see Henrik Reif Anderson's excellent Introduction to Binary Decision Diagrams
LightBDD's aim is to be easy to use for basic tasks, and has no pretense of competing with industrial-strength BDD libraries in terms of efficiency or completeness. It has the following capabilities:
- Build a BDD from a boolean function
- Apply, Restrict, and Compose operations (See Bryant, 1986)
- Automatic generation of
dotcode for graph visualization by Graphiz - Multiple-output boolean function support (the MultiBDD class)