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: BDD corresponding to R={(3,2),(2,0)}

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!!

What is your problem actually? You don't know how to represent relation on integers as a truth table or you don't know how to make BDD from a truth table? — max taldykin, Apr 02 '14 at 11:33
I don't know how to execute arithmetic functions on integers represented in BDDs, without transforming the BDD to integers executing the function and transforming it back to BDD with Java. I heard this works for other libraries in other programming languages, but I think this doesn't exist in these java libraries. — tralala, Apr 03 '14 at 11:35
There is nothing about arithmetic functions in your question. — max taldykin, Apr 03 '14 at 11:58
Yes, I'm sorry, I was in hurry before. So my initial question was, if there is a simple possibility to take an integer tuple and create a BDD out of it. But I don't think that it is possible, like I wanted. For this, I have to convert the integers to it's binary representations and add these as simple variables to the BDD. I will add an answer to this question now, how I think it is the best possibility, but this version is not really satisfying.. — tralala, Apr 03 '14 at 16:03

score 0 · Accepted Answer · answered Apr 03 '14 at 16:37

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.

score 0 · Answer 2 · answered Feb 25 '16 at 17:55

0

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.

answered Feb 25 '16 at 17:55

Carsten

1

Another, better solution: use ZDDs to encode tuples. That's more efficient than BDDs. ZDD stores subsets of sets – Carsten Feb 25 '16 at 18:00

How to encode integers in BDDs

2 Answers2