Binary Decision Diagrams (BDD) and Zero-suppressed Binary Decision Diagrams (ZDD) implementation in Haskell.
BDD is a data structure suitable for representing boolean functions (can be thought as a compressed representation of truth tables) and many operations on boolean functions can be performed efficiently. ZDD is a variant of BDD suitable for representing (sparse) families of sets compactly.
BDD/ZDD uses hash-consing for compact representation and efficient comparison, and we use intern package for implementing hash-consing.
Package name | Repository | License | BDD | ZDD | Style | Implementation | Hash-consing / Fast equality test | Dynamic variable reordering |
---|---|---|---|---|---|---|---|---|
decision-diagrams (this package) | GitHub | BSD | ✔️ | ✔️ | pure | pure Haskell | ✔️ | - |
zsdd | GitHub (deleted?) | BSD | ✔️ | ✔️ | monadic | pure Haskell | ✔️ | - |
obdd | GitHub | GPL | ✔️ | - | pure | pure Haskell | - | - |
HasCacBDD | GitHub | GPL | ✔️ | - | pure | FFI | ✔️ | - |
hBDD (hBDD-CUDD, hBDD-CMUBDD) | GitHub | LGPL | ✔️ | - | pure | FFI | ✔️ | ✔️ |
cudd | GitHub | BSD | ✔️ | - | both pure*1 and monadic | FFI | ✔️ | ✔️ |
*1: cudd
's pure interface is different from normal Haskell data types (like ones in the containers package, for example) because it requires DDManager
argument.
Please feel free to make a pull request for addition or correction to the comparison.