Skip to content

Latest commit

 

History

History
249 lines (224 loc) · 14.8 KB

bdd.md

File metadata and controls

249 lines (224 loc) · 14.8 KB
Raw

Table of Contents

Python

  • dd (BSD-3, Python):
    • BDD and MDD pure Python implementation
    • Cython interface to BDDs and ZDDs of CUDD in dd.cudd
    • Cython interface to BDDs of Sylvan in dd.sylvan
    • Cython interface to BDDs of BuDDy in dd.buddy
  • pyEDA (BSD, Python): BDD implementation without a BDD manager
  • PyCUDD (BSD-3, Python): SWIG-generated bindings to CUDD
  • marduk in RATSY (LGPL, Python): Wrappers of NuSMV (which uses CUDD) (TU Graz)
  • mccarthy-to-bryant (GPL-3, Python) (mainly educational)
  • PBDD (BSD, Python) (mainly educational)
  • robdd (?, Python)
  • py-ydd (Apache-2, Python/C++): YDDs (Yet another Decision Diagram), a data structure that allows to efficiently store extremely large families of sets, and perform various operations on them quiete efficiently.
  • Graphillion (MIT, Python/C++): Graphset operations library using TdZDD

Ruby

LISP

  • CL-CUDD (Lisp, BSD): bindings to CUDD
  • trivialib.bdd (Common Lisp, LLGPL): Functional implementation of BDDs and ZDDs (Univ. of Tokyo)
  • clj-bdd (EPL, Clojure)
  • bdd (EPL, Clojure)

CWEB

  • bdd14.w: BDD package by Donald Knuth
  • bdd15.w: ZDD package by Donald Knuth

C

  • CUDD (BSD): (Colorado U)
    • EXTRA v2.0, v1.3(?, C): extends the functionality of CUDD, contains additional {A,B,Z}DD operators and routines, most of the code is meant to enhance the manipulation of ZDDs (UC Berkeley)
    • DDDMP (BSD): Decision Diagram DuMP package
    • CUDDaux (LGPL-2.1, C): library that implements additional ADD functions for CUDD (INRIA)
    • 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
    • SimpleCUDD (Artistic License 2.0, C): A simplified fast interface for the use of CUDD for Binary Decision Diagrams
    • 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
    • libbdd-dev: Debian Linux package
    • 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
  • MEDDLY (also) (LGPLv3, C++): Multi-terminal and Edge-valued Decision Diagram LibrarY, including BDDs (Iowa State Univ.)
  • libDDD (LGPLv3, C++): integer-valued data decision diagrams and hierarchical set decision diagrams (LIP6, Sorbonne Univ., 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)
  • zddfun (?, C): Logic puzzle solvers using ZDDs, inspired by TAOCP 4.1
  • ZDD (?, C++): Multi-terminal ZDDs

C#

  • PAT BDD library (?, C#): BDD library for symbolic model checking of hierarchical systems, with a C# interface to CUDD version 2.4.2
  • SylvanSharp (?, C#): bindings to Sylvan
  • BuDDySharp (?, C#): bindings to BuDDy

Clojure

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
  • HumbleBDD (MIT, Java): BDDs, ZDD

Javascript

  • binary decision diagram (Apache-2, JavaScript): A library to create, minimize and optimize binary decision diagrams
  • BDD (?, Javascript)

Julia

ML

OCaml

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

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

other

Unsorted

Abbreviations

  • BDD = Binary Decision Diagrams
  • ZDD = Zero-suppressed BDD