Clone wiki

JDD / Home

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.

Download

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...

License

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