Как кодировать целые числа в BDD

Question

Я реализую в Java.

В данный момент я пытаюсь использовать BDD (Binary Decision Diagramms) для хранения отношений в структуре данных.

Например, 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, не зная, сколько логических переменных я использовал для представления целого числа в двоичном виде. Например, я должен определить в начале: все мои целые числа меньше 64, поэтому они представлены 6 двоичными переменными. Если после этого я хочу добавить большее целое число, чем 64, у меня возникнет проблема, но я не хочу использовать максимальный размер целых чисел с самого начала, чтобы сэкономить время, потому что я хотел использовать BDD для сохранения работы. время, иначе есть много более простых вещей, чем BDD для простого представления кортежей.

Я использую JDD в качестве моей библиотеки BDD, поэтому в JDD BDD представлены в виде целых чисел.

Вот как я получу BDD из целочисленного кортежа:

В начале вы должны создать BDD-переменные, maxVariableCount максимальное количество двоичных переменных, представляющих целое число (объяснено в начале этого ответа):

variablesDefinition это просто число целочисленных переменных, которые я хочу представить позже в BDD. Так что в примере моего вопроса переменные Definition были бы 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.

Answer 2

Просто кодируйте целочисленные кортежи, используя алгоритм кодирования k-подмножеств, такой как lex, colex, revdoor, coolex и т. Д. Lex кодирует k-кортеж из n целых чисел в лексикографическом порядке, например, 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

Вам нужна процедура ранга (кортежа) и отмены (ранга), чтобы преобразовать кортеж в ранг и обратно.