BDD - Binary Decision Diagrams

bdd.md

Table of Contents

• Python
• Ruby
• LISP
• C
• C#
• Clojure
• Java
• Javascript
• Julia
• ML
• OCaml
• Haskell
• Isabelle/HOL
• Prolog
• Lua
• Erlang
• Rust
• PHP
• other
• Unsorted
• Abbreviations

Python

• dd (BSD-3, Python):
  • BDD and MDD pure Python implementation
  • Cython interface to CUDD in dd.cudd
  • Cython interface to Sylvan in dd.sylvan
  • Cython interface to BuDDy in dd.buddy
• pyEDA (BSD, Python): BDD implementation without a manager
• PyCUDD (?, Python): SWIG-generated bindings to CUDD
  • rePyCUDD: reentrant version
  • PyCUDD packaging
• marduk in RATSY (LGPL, Python): Wrappers of NuSMV (which uses CUDD) (TU Graz)
  • marduk/src/bddwrap.py: Wraps BDD manager
  • marduk/src/zddwrap.py: Wraps ZDD manager
• mccarthy-to-bryant (GPL-3, Python) (mainly educational)
• PBDD (BSD, Python) (mainly educational)
• robdd (?, Python)

Ruby

• CUDD-rb (MIT, Ruby): bindings to CUDD
• Ruby-BDD: bindings to Buddy

LISP

• CL-CUDD (Lisp, BSD): bindings to CUDD
• clj-bdd (EPL, Clojure)
• bdd (EPL, Clojure)

C

• CUDD (BSD): (Colorado U)
  • DDDMP (BSD): Decision Diagram DuMP package
  • cnf2obdd (same as MiniSAT)
  • windows port
  • Chain-CUDD (BSD-3, C): Extension of CUDD to support BDD with chain nodes
  • Cloud-BDD (?, C): Distributed implementation of BDD package, using CUDD
  • Python:
    • dd.cudd
    • PyCUDD
    • marduk
  • Ruby:
    • CUDD-rb
  • LISP:
    • CL-CUDD
  • OCaml:
    • MLCuddIDL
  • Haskell:
    • hBDD
    • hs-cudd
    • Haskell-CUDD
  • Java:
    • JBDD
    • Jedd
  • C#:
    • PAT.BDD
  • Prolog:
    • swipl_cudd
  • Rust:
    • cudd_rust
• BuDDy (Public domain): (UMichigan)
  • fork UTwente
  • fork: re-entrant version
  • Python:
    • dd.buddy
  • ML:
    • muddy
  • OCaml:
    • ocaml-buddy
  • Java:
    • JBDD
  • Ruby:
    • Ruby-BDD
  • C#
    • BuDDySharp
• Cal BDD (BSD): (UC Berkeley)
• ABCD (?): (JKU)
• CMU BDD: (CMU)
  • hBDD
• Geert Janssen: package used in PVS and available here: ftp://ftp.ics.ele.tue.nl/pub/users/geert/ (Eindhoven)
• MONA
• TiGeR (C): BDDs and compacted Boolean functions (DEC)
• PPBF (C): parallel BDD package based on partial BFS expansion (CMU)
• Sylvan (Apache-2): Multi-core library using work-stealing framework and lock-less hash table
  • Python:
    • dd
  • Haskell:
    • Sylvan-Haskell
  • Java:
    • jSylvan
    • cpachecker
  • C#
    • SylvanSharp
• libDDD (LGPL, C++): (CNRS)
• TdZdd (MIT, C++): top-down breadth-first n-ary DD/ZDD manipulation, parallel processing with OpenMP
• CacBDD (BSD-3, C++)
• BDDSharp (MIT, C#): (U Catholique Louvain)
• LaVaBDD (?, C++): Lattice-valued BDDs (ULB)
• wld (FUSC, C++): word-level DDs (UFreiburg)
• BDS (FUSC, C): (UMass)
• Biddy (GPL-2, C): a multi-platform academic BDD package (UMaribor)
• list of BDD packages with comparisons
• BBDD (?, ?): biconditional BDDs
• RicBDD (GPL, C++)
• LiBDD (BSD, C): multi-platform BDDs package
• BDDC: BDD-based logical calculator
• EHV: Eindhoven BDD package
• libvata/src/mtbdd (C++, GPL-3)

C#

• PAT.BDD (?, C#): interface to CUDD
• SylvanSharp (?, C#): bindings to Sylvan
• BuDDySharp (?, C#): bindings to BuDDy

Clojure

• clj-bdd (EPL, Clojure)
• bdd (EPL)

Java

• JavaBDD (GPL-2 or LGPL-2, Java)
• JDD (zlib, Java): BDD and ZDD support, inspired by Buddy
• JBDD (zlib, Java): bindings to CUDD, Buddy
• BeeDeeDee (GPL-2, Java): Multi-thread library
• LightBDD (?, Java): simple library
• jSylvan (Apache-2, C/C++/Java): JNI bindings for Sylvan
• cpachecker (Apache-2, Java): Java bindings for Sylvan
• JADE (custom, Java) (UFreiburg)
• JINC (GPL-2, C++): utilizes multi-threading, has BDD, ADD, NADD, ZADD, TADD, MDD (UBonn)
• djbdd (Java 7, GPL-3)
• Java applet (?, Java) (UHamburg)
• SableJBDD (LGPL): (McGill Univ.)
• Jedd (Java, LGLPL-2): Java Extension for Decision Diagrams based on the polyglot framework, supports as backends: CUDD, BuDDy, SableJBDD, JavaBDD
• zdd_java: educational ZDD implementation

Javascript

• BDD (?, Javascript)

Julia

• BinaryDecisionDiagrams (MIT, Julia)

ML

• muddy (MIT, ML): bindings to Buddy (older home) (UCopenhagen)

OCaml

• MLCuddIDL (LGPL-2.1, C/OCaml): bindings to CUDD (mirror) (INRIA)
• ocaml-buddy (LGPL, OCaml): bindings to Buddy (Paris 7)
• MLBDD (MIT, OCaml)
• Symbolickat.bdd (?, OCaml): pure-OCaml library (ENS de Lyon)
• John Harrison (BSD-3, Ocaml)
• Jean-Christophe Filliatre (GPL-2, Ocaml)
• xlasat (? , Ocaml) (INRIA)
• OcamlBdd

Haskell

• hBDD (GPL-2, Haskell): bindings to CUDD and CMU-BDD (Australian National Univ.)
• hs-cudd (BSD-3, Haskell): bindings to CUDD (Veracode)
• Haskell-CUDD (BSD-3, Haskell): bindings to CUDD (NICTA)
• HasCacBDD (GPL-2, Haskell): bindings to CacBDD (ILLC, University of Amsterdam)
• Sylvan-Haskell (BSD-3, Haskell/C): bindings to Sylvan (NICTA)
• termite2.bdd (?, Haskell): BDD abstraction layer (NICTA)
• robbed (BSD-3, Haskell): (Galois)
• haskell-obdd (GPL-2, Haskell): (Leipzig Univ. for Applied Sciences)
• robdd (BSD-3, Haskell)
• bdd (BSD-3, Haskell)
• robdd (?, Haskell)

Isabelle/HOL

• bdd (BSD, Isabelle/HOL/Haskell): verified and executable implementation of ROBDDs in Isabelle/HOL, archived proofs (TUM)

Prolog

• swipl_cudd (?, C/Prolog): bindings to CUDD
• upbdd (?, Prolog/C++): UP-BDD data structure implementation

Lua

• mccarthy-to-bryant/lua (GPL-3, Lua)
• lua-bdd (BSD, Lua)

Erlang

• seqbdd (BSD-like, Erlang): Sequence BDD data structure

Rust

• boolean_expressions (MIT, Rust): BDD implementation, conversion from/to formulae with cubelist-based minimization
• cudd_rust (BSD-3, Rust): bindings to CUDD

PHP

• BDD (?, PHP)

other

• BDD papers, links

Unsorted

• QuIDDPro
• BDS
• MEDDLY
• EVMDD
• ZBDD
• libsdd

Abbreviations

• BDD = Binary Decision Diagrams

This list appears to be based on: https://github.com/johnyf/tool_lists/blob/master/bdd.md