DJBDD

What's this?

A Java 7 BDD package with the GPL with classpath linking exception license based on GPL version 2 or later, as you prefer. See this explanation about the license. Howeer, if your use case requires other license, I can re-license this project for you, please write me to my email (at the botton of this README).

This package provides a Binary Decision Diagram library you can use to make operations with boolean logical formulas and study its properties.

This software has been developed by Diego J. Romero-López as a tool for his Master's Thesis.

Hay una versión en español de este documento aquí.

Introduction

A Binary Decision Diagram is a complete truth table of a boolean expression in a reduced graph form. For an introduction, see Binary Decision Diagram on Wikipedia.

This library provides all the operations you need to work with them.

How to use it

// These are the boolean variables used in our formulas
// They can have any alphanumeric name you want starting with a letter and
// being unique variable names.
String[] variables={"a", "b", "c", "d", "e", "f"};

// You always have to initialize the BDD system before you create any
// BDD object. Be careful with that.
BDD.init(variables);

// The functions are specified as boolean expressions with Java syntax
// adding the operators -> (implication) and <-> (double implication)
String function = "(a && b) || (c && d)";

// The variable ordering is given by the order
// of variables in the array of strings 'variables'.

// Construction of a new BDD
BDD bdd = new BDD(function);

// Printing the BDD in the standard output
// The internal table node will be shown by stdout
bdd.print();

// You can print it as a image PNG using a dot library
Printer.printBDD(bdd, "bdd_"+bdd.size());

// Creating other BDDs:
String function2 = "(a && e) || f"
BDD bdd2 = new BDD(function2);
bdd2.print();

// Operations with BDDs

// This BDD is the logical AND between bdd and bdd2
BDD bdd3 = bdd.apply("and", bdd2);

// This BDD is the logical OR between bdd and bdd2
BDD bdd4 = bdd.apply("or", bdd2);

// Destroy explicitly bdd2
// In case we need to compute sizes, reduce the global graph or print it
bdd2.delete();

// If you think you can have few free memory,
// you would have to free by calling the garbage collector
BDD.gc();

Complete tests

The main program of this library is full of examples. The all-in-one jar version is located in store/DJBDD.jar, the dependant on libraries jar one is in dist/DJBDD.jar. You should use store/DJBDD.jar for your experiments.

Easiest option is opening this project with Netbeans. There are several executing configurations:

Two examples of computing consistency in the real world.
Six benchmark of BDD-reducing algorithms.
Tests that you can execute to verify BDD operations.

Basic Options

Output

BDD print as image

java -jar DJBDD.jar --image --<format> <file>

Note that this option will work only if you are in a Linux/UNIX system with the dot tool to draw graphs in the path /usr/bin/dot.

BDD printing

java -jar DJBDD.jar --print --<format> <file>

Prints a BDD in the standard output.

Restriction on BDD formats allowed

dimacs: Dimacs CNF format. See SAT format or CNF for more information.
cstyle: C-style boolean expression preceded by a line with all variables separated by commas. For example:
- a && !b
- a -> (!b && (c || d))
- a <-> (b && !c)
- a != (b && !c)

Restriction on variable naming

IMPORTANT: for each variable there can no be any other that contains it as substring from the left. That is, if we have a variable with the name 'x1' we cannot use other variable with the name 'x11'. It's not in my future plans to change that, so name your variables with names like:

{x1}
{x11}
{x12}

Other notes

Example source data: directory data has some examples of each format (look the extension).

BDD reduction benchmarks

See below for a description of each reduction method.

# Sifting Algorithm
java -jar ./DJBDD/store/DJBDD.jar --memory-optimization-benchmark --dimacs ./data/benchmarks/ sifting
# Window Permutation Algorithm (window size = 2)
java -jar ./DJBDD/store/DJBDD.jar --memory-optimization-benchmark --dimacs ./data/benchmarks/ window_permutation window_size=2
# Random Swapper
java -jar ./DJBDD/store/DJBDD.jar --memory-optimization-benchmark --dimacs ./data/benchmarks/ random_swapper random_seed=121481 iterations=100
# Genetic Algorithm
java -jar ./DJBDD/store/DJBDD.jar --memory-optimization-benchmark --dimacs ./data/benchmarks-genetic genetic random_seed=10 population=8 generations=10 selection_percentage=0.2 mutation_probability=0.1
# Memetic Algorithm
java -jar ./DJBDD/store/DJBDD.jar --memory-optimization-benchmark --dimacs ./data/benchmarks-memetic memetic random_seed=121481 population=8 generations=10 selection_percentage=0.2 mutation_probability=0.1
## Iterative Sifting
java -jar ./DJBDD/store/DJBDD.jar --memory-optimization-benchmark --dimacs ./data/benchmarks/ isifting iterations=100

Features

Shared hash table

All BDDs use the same hash table, sharing the vertices and subgraphs. The goal for using this data structure is reducing the number of repeated vertices. Each BDD has one root vertex though.

Rich I/O API

This library provides method to load logical clausules in DIMACS format and Java native, includen implication and double implication operators.

Memory efficient

This library shares vertices between different BDDs.

Vertices grouped by levels

You can access the vertices that has each variable in an efficient way. This will be used for BDD-reducing algorithms.

Operations implemented

Apply [6] [3].
Restrict. [2].
Swapping of two variables. [5].

Implemented Reduction Algorithms

This package contains many reduction algoritms. They are implemented in the djbdd.reductors package.

These reduction algorithms are implemented as children classes of djbdd.reductors.ReductionAlgorithm, so they share the same API. This API contains a execute and run method. The first one must be overriden for each particular reduction method while the second will act as a façade of execute. The run method also measures the elapsed time in the reduction method for comparing the reduction algorithms

// Some logic function used to build a BDD
String function1 = "(a && d) || (b && c)";
BDD bdd1 = new BDD(function1);

// Call to garbage collector & print the
// node table 
BDD.gc();
BDD.T.print();
        
Printer.printBDD(bdd1, "test15_bdd1_BEFORE_"+bdd1.size());

// Construct a reduction algorithm. For example SiftingReductor:
SiftingReductor reductor = new SiftingReductor();
// Start the reduction process
reductor.run();

// Call to garbage collector & print the
// node table (to compare with the first node table)
BDD.gc();
BDD.T.print();

It is important to note that these reduction methods reduce all the BDDs created in the program because they reduce the vertex mesh by swapping vertex levels.

They are listed below:

Window Permutation

Developed in the class djbdd.reductors.WindowPermutation, this algorithm was proposed by Fujita et al. & Ishiura et al. Richard L. Rudell described it and compared with its own reduction method in [7]. This implementation is based on his description.

// Window size
int windowSize = 2;
WindowPermutationReductor reductor = new WindowPermutationReductor(windowSize);
reductor.run();

Rudell's Variable Sifting

This package contains a basic implementation of the variable reordering proposed by Richard L. Rudell in [7]. This method try to find the best position for each variable keeping fixed in their position the rest.

Use example:

SiftingReductor reductor = new SiftingReductor();
reductor.run();

Random Swapper Reduction

We wanted to compare a pure random algorithm with our evolutionary algorithms to test if our results are due to randomness or because this method truly works. This reduction method is based in swapping two variables chosen at random in each iteration in the BDD tree.

int iterations = 1000;
RandomSwapperReductor reductor = new RandomSwapperReductor(iterations);
reductor.run();

Note that this algorithm, the genetic algorithm and the memetic algorithm need a random seed to be set before their execution.

Genetic Reduction

W. Lenders & C. Baier defined the genetic operators for developing a Genetic Algorithm for this BDD reduction problem in [8]. We have implemeted a version of their approach in the GeneticReductor class.

// Number of chromosomes
int populationSize = 10;
// Number of generations of the algorithm
int generations = 1000;
// % of population selected
double selectionPercentage = 10;
// Probability of mutating a gene in a chromosome
double mutationProbability = 0.1;
GeneticReductor reductor = new GeneticReductor(populationSize, generations, selectionPercentage, mutationProbability);
reductor.run();

Memetic Reduction

Based on [8], we propose another algorithm that combines the Genetic Algorithm optimizing each chromosome using the Rudell's Sifting Algorithm. Its name is MemeticReductor and its parameters are the same than the GeneticReductor.

// Number of chromosomes
int populationSize

Djbdd

Install / Use

README