java - 如何在 BDD 中编码整数

Question

我正在用 Java 实现。

目前我正在尝试使用 BDD(二元决策图)来将关系存储在数据结构中。

例如R={(3,2),(2,0)} 和相应的 BDD:

出于这个原因，我一直在寻找具有 BDD 功能的库来帮助我。

我发现了两种可能性:JavaBDD 和 JDD。

但在这两种情况下，我都不明白如何将一个简单的整数编码为 BDD，因为我如何或何时给出整数的值？或者，如果 BDD 由整数表示，这意味着什么？

在这两种情况下，都有如下方法:

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

或

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

我怎样才能像我的示例一样简单地创建 BDD？

非常感谢!!

Answer 1

所以我找到了一个解决方案，但它不是很令人满意，因为我无法从 BDD 取回元组，而不知道我使用了多少个 boolean 变量来表示二进制整数。所以我必须在开始时定义例如:我所有的整数都小于 64，所以它们由 6 个二进制变量表示。如果我想在之后添加一个大于 64 的整数，我会遇到问题，但我不想从一开始就使用整数的最大大小，以节省时间，因为我想使用 BDD 来节省运行时间时间，否则有很多比 BDD 更简单的东西来表示元组。

我使用 JDD 作为我的 BDD 库，因此在 JDD 中 BDD 表示为整数。

这就是我从整数元组中获取 BDD 的方法:

一开始你必须创建 BDD 变量，maxVariableCount 是二进制变量的最大数量，它代表整数(在这个答案的开头解释):

variablesDefinition 只是我稍后要在 BDD 中表示的整数变量的数量。所以在我的问题的例子中，variablesDefinition 将是 2，因为每个元组都有两个整数变量。

variables 数组是一个二维数组，其中包含所有 BDD 变量。因此，例如，如果我们的元组有 2 个元素，则可以在 variables[0] 中找到表示第一个整数变量的 BDD 变量。

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

然后我们可以从给定的整数元组创建一个 bdd。

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;
}

我的第一个意图是将这些元组添加到 BDD 中，然后能够在 BDD 中的整数中执行算术函数，但这只有在将 BDD 转换回元组并执行函数并将其返回给BDD，它破坏了我想使用 BDD 的所有原因。