LaVaBDD : Lattice-Valued Binary Decision Diagrams Template Library

0.1

Version:

0.1

Date:

February 23rd, 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;

size_t bdd_hash(const bdd& x); // ommited for the sake of brevity

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 bdd_hash(x); }
    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;

size_t byte_hash(const byte& x); // ommited for the sake of brevity

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 byte_hash(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();
}