BDDSharp is a C# library for manipulating roBDDs (Reduced Ordered Binary Decision Diagrams).

Currently, the library is not intended to be memory efficient. Implementing complemented edges and shared BDDs might greatly improve the memory footprint.

Christoph Meinel and Thorsten Theobald. 1998. Algorithms and Data Structures in VLSI Design (1st ed.). Springer-Verlag New York, Inc., Secaucus, NJ, USA.

Randal E. Bryant. 1986. Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans. Comput. 35, 8 (August 1986), 677-691. DOI=10.1109/TC.1986.1676819 http://dx.doi.org/10.1109/TC.1986.1676819

Tony Stornetta and Forrest Brewer. 1996. Implementation of an efficient parallel BDD package. In Proceedings of the 33rd annual Design Automation Conference (DAC '96). ACM, New York, NY, USA, 641-644. DOI=10.1145/240518.240639 http://doi.acm.org/10.1145/240518.240639

Just add the project to your solution and reference it. You can also compile it and reference ``BDDSharp.dll`.

The library is intended to be simple to use and extend. Performance, even if taken into account, is not the primary goal. The library is fully developed in C# and requires no external dependencies (like CUDD).

To build a BDD, you can create your nodes by instancing ``BDDNode. All operations on BDD are located in the BDDManager` class. When calling a function of the manager, it is your responsibility that BDDs were created using the same manager.

For instance, to represents the following BDD,

you could type the following code

var manager = new BDDManager (3);
var n3 = new BDDNode (2, manager.One, manager.One);
var n4 = new BDDNode (1, n3, manager.Zero);
var n2 = new BDDNode (1, n3, manager.Zero);
var root = new BDDNode (0, n2, n4);

To reduce a BDD, you can call BDDManager.Reduce (BDDNode).

manager.Reduce (root);

Applied to the previous example, you ends up with the following BDD

To combine multiple BDDs using the ITE operator, just call the corresponding function

manager.ite (f, g, h)

For instance, consider the following BDDs (f, g and h respectively)

The resulting BDDs returned by applying ITE operator is given by