mlbdd

An OCaml library for Binary Decision Diagrams (BDDs)
README

The mlbdd library provides a simple, easy-to-use, easy-to-extend implementation
of binary decision diagrams (BDDs) in OCaml. It is well tested and well
documented. The library itself has no dependencies and is thus easy to include
in applications that might, for example, be compiled with js_of_ocaml or other
tools that rely on pure OCaml. It is also easier to integrate with existing
projects due to its lack of dependencies.

To build this library, ensure that OCaml 4.01 or greater and findlib is
installed and run

make

To test this library, ensure that ocamlfind and ounit is installed and run

make test

Examples of usage are included in the documentation.

Rationale

There are currently several implementations of BDDs for OCaml. These include
the following:

  • John Harrison: http://www.cl.cam.ac.uk/~jrh13/atp/OCaml/bdd.ml

  • Jean-Christophe Filliâtre: https://www.lri.fr/~filliatr/ftp/ocaml/bdd

  • Xavier Leroy: https://gforge.inria.fr/scm/viewvc.php/attic/xlsat/?root=sodiac

While there are many nice design aspects of these packages, there are also
significant problems with all of them including lack of performance and API
limitations. To solve these problems this library implements BDDs in OCaml
combining ideas from commercial-grade C BDD implementations with good ideas
from the above libraries.

There are two performance problems associated with the above BDD
implementations. The first is indirection inefficiency and the second is
algorithmic inefficiency. Indirection inefficiency arises when extra
indirections are introduced when they are not required. The first BDD
implementation suffer from this problem due to the implementation of hash
consing that it uses.

Efficient Hash Consing

Hash consing is required for the implementation of BDDs. Hash consing ensures
that the same node in the diagram is only created once and that traversal
algorithms need not handle the same logical expression more than once.
Typically hash consing is implemented with a hash table, where the table maps
unique identifiers (usually integers) to nodes of the BDD. For example:

type node =
  | True
  | False
  | If of int * var * int

where the two integers are the unique identifiers for the left and the right
branches of the If node. Then there is a hash table that maps these integers
into nodes:

type hash = (int,node) Hashtbl.t

Unfortunately, when traversing this BDD, every dereference requires a hash table
lookup. For example, to find the left child of an If node requires the following
sequence of operations:

  1. Fetch integer id from If data structure

  2. Find integer id in hash table

  3. Dereference the pointer found in the hash table

A much better solution is to have the type directly represented:

type node =
  | True
  | False
  | If of node * var * node

This means that this extra hash table lookup, which is a significant operation can be
avoided:

  1. Fetch pointer from If data structure

  2. Dereference the pointer

The problem is getting the sharing that the hash table provided above without
losing direct pointers. The solution to this is to add an extra field to each
(or at least recursive) nodes to give a unique id for that node and then to do
the appropriate dereferencing when constructing a node rather than when
accessing it.

type node =
  | True
  | False
  | If of node * var * node * int

type hash = (int * var * int, node) Hashtbl.t

Using this structure, the pointers are direct, but hash consing is still possible.
When constructing a new node, the ids of the two children are looked up and then
the hash of those ids and the var are used to determine if the node has already been
created. If so, existing pointer is returned, otherwise a new node is constructed
and returned.

This solution, which is employed by the latter two BDDs improves the performance
of traversing BDDs without complicating the structure. The exact structure employed
by mlbdd is borrowed from Xavier Leroy's BDD implementation in xlsat.

BDD Algorithm Improvements

The biggest performance improvement for the BDD structures comes from the
addition of complement edges. Complement edges enable each nested BDD to be
either a BDD or its complement. This means that there is a potential size
improvement for BDDs. Since the each BDD represents itself and its complement,
the total size of a BDD can require half the nodes. More importantly,
complement edges mean that computing the complement of a BDD is an O(1)
operation instead of an O(n) operation where n is the number of nodes in the
BDD. This reduction in complexity for negation makes many operations
significantly faster.

The trick with complement edges is ensuring canonicity. To do this the form of
BDDs is changed to the following, where a BDD is a cnode.

type node =
  | False
  | If of node * var * cnode * int

and cnode = bool * node

There are several simplifications that come out of this form. First, there is
no True anymore. The False node complemented gives a representation of
true, so, True was redundant. Second, complement edges are not allowed
everywhere. Note that a BDD is a cnode, but If take a node and a cnode.
The restriction here is that the negative edge out of a node cannot be
complemented. This can be guaranteed by the following conversion:

    |               |
    |               o
    |               |
    V      ==>      V
   / \             / \
  o   \           /   o
 /     \         /     \
V0     V1       V0     V1

Where o is used on an edge to represent complement.

The resulting BDD implementation is significantly faster, and because
complement is essentially free, most operations can be implemented in a simpler
fashion using combinations of other operations without the typical overhead of
all of the negation operations that are required. For example, using just the
and operation it is efficient and easy to provide or, nand, nor, and
implies.

Install
Published
29 Jan 2022
Sources
v0.7.3.tar.gz
md5=6cf89d1cf763e89687f3b45ac80bd614
sha512=81987d086a2370e6c53eb9f549edf9d863aa915b7723714c3147b30dec9c2b763d54df0de8c4919412bd7e9942f6cc9558db855c186f1b3844f904419e09c7a3
Dependencies
odoc
with-doc
ocaml
>= "4.04.0"
ounit2
with-test
dune
>= "2.7"
Reverse Dependencies