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

Question

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

На данный момент я пытаюсь использовать BDD (Двоичные схемы принятия решений) для хранения отношений в структуре данных.

E.g. 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. Таким образом, в примере моего вопроса variablesDefinition будет 2, потому что каждый кортеж имеет две переменные intereger.

Массив 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 и т. Д. Лекс кодирует k-кортеж из n целых чисел в лексикографическом порядке, например. п = 4, к = 2 дает (1) кодирования на основе

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

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