# JDD, a pure Java BDD and Z-BDD library

Binary Decision Diagrams (BDDs) are used in formal verification, CSP and optimisation. To work with BDDs, you need a BDD library. JDD is my java implementation of a decision diagram library inspired by BuDDy (a BDD package written in C). It also includes support for Zero-suppressed BDDs.

The recommended way of getting the code is to use git:

git clone git@bitbucket.org:vahidi/jdd.git

But if you are unfamiliar with git, you can use the download page.

## Examples

A number of examples have been including to get you started:

jdd/examples/BDDQueens.java     -- N-Queens problem solved with BDDs.
jdd/examples/ZDDQueens.java     -- N-Queens problem solved with Z-BDDs.
jdd/examples/ZDDCSPQueens.java  -- N-Queens problem solved with the CSP operators of Z-BDDs.
jdd/examples/Solitaire.java     -- The solitaire example from the BuDDy distribution.
jdd/examples/Adder.java         -- Yet another example stolen from the BuDDy distribution :)
jdd/examples/Milner.java        -- Milner's scheduler, from BuDDy...


JDD is free software under the zlib license. You may use it free of charge in research or even commercial projects.

## Citation

Feel free to use the following bibtex for citation:

@MISC{jdd,
author = {Arash Vahidi},
title = {JDD: a pure Java BDD and Z-BDD library},
howpublished = "\url{https://bitbucket.org/vahidi/jdd}",
year = 2015
}


Updated