How to encode integers in BDDs

Question

I'm implementing in Java.

At the moment I'm trying to use BDDs (Binary Decision Diagramms) in order to store relations in a datastructure.

E.g. R={(3,2),(2,0)} and the corresponding BDD:

For this reason I was looking for libraries, which have BDD functionalities in order to help me.

I found two possibilities: JavaBDD and JDD.

But in both cases, I do not understand how I can encode a simple integer to a BDD, because how or when do I give the value of my integer? Or what does it mean, if the BDD is represented by an integer?

In both cases, there are methods like:

int variable = createBDD(); //(JBDD) 

or

BDD bdd = new BDD(1000,1000);
int v1 = bdd.createVar(); // (JDD)

How can I simply create a BDD like my example?

Thank you very much!!

Answer 1

So I found a solution for this, but it is not very satisfying, as I cannot get the tuple back from the BDD without knowing, how many boolean variables I used for representing the integer in binary. So I have to define in the beginning for example: All my integers are smaller than 64, so they are represented by 6 binary variables. If I want to add a bigger integer than 64 afterwards I have a problem, but I don't want to use the maximum size of integers from the beginning, in order to save time, because I wanted to use BDDs in order to save running time, else there are a lot of easier things than BDDs for just representing tuples.

I use JDD as my BDD library, so in JDD BDDs are represented as integers.

So this is how I will get a BDD out of an integer tuple:

In the beginning you have to create the BDD-variables, the maxVariableCount is the maximum number of binary variables, which represent the integer (explained in the beginning of this answer):

variablesDefinition is just the number of integer variables I want to represent later in the BDD. So in the example of my question variablesDefinition would be 2, because each tuple has two intereger variables.

The array variables is a two dimension array, which has all BDD variables inside. So for example if our tuple has 2 elements, the BDD variables which represent the first integer variable can be found in variables[0].

BDD bddManager = new BDD(1000,100);

private int variablesDefinition;
private int[][] variables;

private void createVariables(int maxVariableCount) {
    variables = new int[variablesDefinition][maxVariableCount];
    for(int i = 0; i < variables.length; i++) {
        for(int j = 0; j < maxVariableCount; j++) {
            variables[i][j] = bddManager.createVar();
        }
    }
}

Then we can create a bdd from a given integer tuple.

private int bddFromTuple(int[] tuple) {
     int result;
     result = bddManager.ref(intAsBDD(tuple[0],variables[0]));
     for(int i = 1; i < tuple.length; i++) {
         result = bddManager.ref(bddManager.and(result, intAsBDD(tuple[i], variables[i])));
     }
     return result;
}

private int intAsBDD(int intToConvert, int[] variables) {
    return bddFromBinaryArray(intAsBinary(intToConvert, variables.length), variables);
}
private int[] intAsBinary(int intToConvert, int bitCount) {
    String binaryString =  Integer.toBinaryString(intToConvert);
    int[] returnedArray = new int[bitCount];
    for (int i = bitCount - binaryString.length(); i < returnedArray.length; i++) {
        returnedArray[i] = binaryString.charAt(i - bitCount + binaryString.length()) - DELTAConvertASCIIToInt;
    }
    return returnedArray;
}

static int DELTAConvertASCIIToInt = 48;

private int bddFromBinaryArray(int[] intAsBinary, int[] variables) {
    int f;

    int[] tmp = new int[intAsBinary.length];

    for(int i = 0; i < intAsBinary.length; i++) {
        if(intAsBinary[i] == 0) {
            if (i == 0) {
                tmp[i] = bddManager.ref(bddManager.not(variables[i]));
            }
            else {
                tmp[i] = bddManager.ref(bddManager.and(tmp[i-1], bddManager.not(variables[i])));
                bddManager.deref(tmp[i - 1]);
            }
        }
        else {
            if (i == 0) {
                tmp[i] = bddManager.ref(variables[i]);
            }
            else {
                tmp[i] = bddManager.ref(bddManager.and(tmp[i-1], variables[i]));
                bddManager.deref(tmp[i - 1]);
            }
        }

    }
    f = tmp[tmp.length-1];
    return f;
}

My first intention was to add these tuples to the BDD and afterwards being able to execute arithmetic functions in the integers in the BDD, but this is only possible after transforming the BDD back to tuples and executing the function and returning it to the BDD, which destroys all reasons why I wanted to use BDDs.

Answer 2

Simply encode integer tuples using a k-subset encoding algorithm like lex, colex, revdoor, coolex etc. Lex encodes a k-tuple out of n integers in lexicographic order, e.g. n=4, k=2 yields the (1 based) encoding

  tuple    rank
  (0,1) -> 1
  (0,2) -> 2
  (0,3) -> 3
  (1,2) -> 4
  (1,3) -> 5
  (2,3) -> 6

You need a rank(tuple) and unrank(rank) routine to transform tuple to rank and back.