4

我正在用Java实现。

目前，我正在尝试使用 BDD（二进制决策图）将关系存储在数据结构中。

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

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

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

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

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

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

或者

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

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

非常感谢！！

4

2 回答 2

0

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

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

所以这就是我如何从一个整数元组中得到一个 BDD：

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

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

该数组variables是一个二维数组，其中包含所有 BDD 变量。因此，例如，如果我们的元组有 2 个元素，则代表第一个整数变量的 BDD 变量可以在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();
        }
    }
}

然后我们可以从给定的整数元组创建一个 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 的所有原因。

于 2014-04-03T16:37:49.767 回答
0

只需使用 k 子集编码算法（如 lex、colex、revdoor、coolex 等）对整数元组进行编码。Lex 按字典顺序从 n 个整数中编码一个 k 元组，例如 n=4，k=2 产生（基于 1）编码

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

您需要一个 rank(tuple) 和 unrank(rank) 例程来将 tuple 转换为 rank 和返回。

于 2016-02-25T17:55:32.587 回答