LaVaBDD : Lattice-Valued Binary Decision Diagrams Template Library

Version:: 0.2

Date:: February 26th, 2010

Author:: Nicolas Maquet

This version of LaVaBDD is deprecated. Please use the most recent version.

Introduction

LaVaBDD is C++ template library for Lattice-Valued Binary Decision Diagrams. The goal of this implementation is to be as simple as possible and reasonably efficient.

The LaVaBDD library is composed of a single C++ header file : lavabdd.h

Installation

The only dependency of the LaVaBDD library is Google's SparseHash. SparseHash is an efficient hash map implementation.

You can download it here : http://code.google.com/p/google-sparsehash/

How to use the library

Lattice-Valued Binary Decision Diagrams (LVBDD for short) encode functions of the form V(p₁,...,p_n) → L where:

p₁,...,p_n is a finite set of propositional variables

V(p₁,...,p_n) is the set of valuations over p₁,...,p_n

L is a finite distributive lattice

Step 1 : define your lattice class

The first step to use LaVaBDD is to define your own lattice class. This class must follow the lava::Lattice interface defined in the package.

The lava::Lattice class is a class template. To define your lattice class, you must subclass this template as in the following example:

 #include <stdexcept> // for logic_error
 #include <bdd.h> // the BuDDy ROBDD library defines the "bdd" type
 #include "lavabdd.h"

 using namespace std;

 class BDDLattice : lava::Lattice<bdd> {

 public:

     static bool less(const bdd& x, const bdd& y) { return (x & bdd_not(y)) == bddfalse; }
     static bool equal(const bdd& x, const bdd& y) { return x == y; }
     static void join(const bdd& x, const bdd& y, bdd& z) { z = x | y; }
     static void meet(const bdd& x, const bdd& y, bdd& z) { z = x & y; }
     static void rpc(const bdd& x, const bdd& y, bdd& z) { z = bdd_not(x) | y; }
     static void drpc(const bdd& x, const bdd& y, bdd& z) { z = y & bdd_not(x); }
     static void top(bdd& x) { x = bddtrue; }
     static void bot(bdd& x) { x = bddfalse; }
     static size_t hash(const bdd& x) { return lava::hash_int(x.id()); }
     static void print(const bdd& x, ostream& out) { out << x; }
     static int size(const bdd& x) { return bdd_nodecount(x); }

     // not implemented here for the sake of brevity
     static int list_size(const list<bdd>& dds) { throw logic_error("not implemented"); }

 };

Here is another, simpler example.

 #include <algorithm> // for min() and max()
 #include "lavabdd.h"

 using namespace std;

 typedef unsigned char byte;

 class ByteLattice : lava::Lattice<byte> {

 public:

     static bool less(const byte& x, const byte& y) { x < y; }
     static bool equal(const byte& x, const byte& y) { return x == y; }
     static void join(const byte& x, const byte& y, byte& z) { z = max(x, y); }
     static void meet(const byte& x, const byte& y, byte& z) { z = min(x, y); }
     static void rpc(const byte& x, const byte& y, byte& z) { z = y; }
     static void drpc(const byte& x, const byte& y, byte& z) { z = y; }
     static void top(byte& x) { x = 255; }
     static void bot(byte& x) { x = 0; }
     static size_t hash(const byte& x) { return lava::hash_int((int) x); }
     static void print(const byte& x, ostream& out) { out << x; }
     static int size(const byte& x) { return 1; }
     static int list_size(const list<byte>& xs) { return xs.size(); }

 };

Step 2 : Choose an LVBDD normal form

There are three available normal forms for LVBDD defined in the package.

the Unshared Normal Form (lava::UNF)
the meet-semantics Shared Normal Form (lava::SNF_MEET)
the join-semantics Shared Normal Form (lava::SNF_JOIN)

For a full comparison of each, see the paper. Here is a quick bottom line:

both SNF are potentially exponentially more compact than UNF
the meet and join are both quadratic-time for UNF
the meet for meet-semantics SNF is polynomial, join is exponential
the join for join-semantics SNF is polynomial, meet is exponential

Step 3 : Define your LVBDD type

Since the LVBDD class template takes two parameters, it is convenient to define your own LVBDD type. This is done simply as follows :

  class BDDLattice; // as defined above

  typedef lava::LVBDD<BDDLattice, lava::SNF_MEET> LVBDD;

Step 4 : Initialize your LVBDD type

Every LVBDD type must be initialized before use. See lava::LVBDD::init.

Step 5 : You're good to go !

You can now use your LVBDD type. See lava::LVBDD for a complete reference on the available methods.

A good starting point is lava::LVBDD::terminal and lava::LVBDD::literal.

To help you, here is a short example.

 #include <bdd.h> // BuDDy
 #include "lavabdd.h"

 using namespace std;

 class BDDLattice; // as defined above

 typedef lava::LVBDD<BDDLattice, lava::SNF_MEET> LVBDD;

 int main() {
     LVBDD::init();              // initialize the LVBDD type
     bdd_init(10000, 10000);     // initialize the BuDDy library
     bdd_setvarnum(4);

     LVBDD p1 = LVBDD::literal(1, true);
     LVBDD p2 = LVBDD::literal(2, true);
     LVBDD p3 = LVBDD::literal(3, true);
     LVBDD c1 = LVBDD::terminal(bdd_ithvar(1));
     LVBDD c2 = LVBDD::terminal(bdd_ithvar(2));
     LVBDD c3 = LVBDD::terminal(bdd_ithvar(3));

     LVBDD dd = (p1 | c1) & (p2 | c2) & (p3 | c3);

     dd.print_graphviz();
 }

Added a changelog to the documentation ;-)
Lots of bugfixes / typos
lava::hash_int is now a global function and not a static member of lava:LVBDD
Added a definition for operator<< for writing LVBDD on output streams
Added a definition for operator< in lava::NodePtr to allow std::set<NodePtr>