Пакет CUDD: способ передачи определенного переменного порядка?

Я работаю с пакетом CUDD для выполнения манипуляций с BDD. Мне было интересно, если кто-нибудь знает способ передать конкретный порядок переменных, чтобы указать программе использовать этот порядок при создании BDD. Я работаю с булевыми функциями, которые имеют относительно небольшое количество переменных.

На самом деле, даже если есть способ передать в программу определенную входную переменную для корня BDD, это также послужит моей цели. Если кто-нибудь знает, как это сделать, то я был бы очень признателен за помощь. Я просмотрел документацию и ничего подобного не нашел. Может быть, я что-то пропустил.

2 ответа

Решение

Вы можете установить алгоритм переупорядочения на CUDD_REORDER_NONE

Cudd_ReduceHeap(manager, CUDD_REORDER_NONE, 0);

Таким образом, порядок переменных определяется порядком их введения.

В CUDD есть две функции, которые делают то, что задает вопрос:

  • Cudd_AutodynDisable(manager): "Отключает автоматическое динамическое изменение порядка."
  • Cudd_ShuffleHeap(manager, permutation): "Переупорядочивает переменные в соответствии с заданной перестановкой."

По телефону Cudd_AutodynDisable перед объявлением каких-либо переменных уровни переменных будут инициализированы и останутся в порядке объявления переменных.

Чтобы обратиться к более общему случаю получения некоторого желаемого переменного порядка в произвольное позднее время, сначала вызовите Cudd_AutodynDisable и затем передайте требуемый порядок переменных Cudd_ShuffleHeap,

Примеры вызова этих функций можно найти в методе dd.cudd.BDD.configure и в функции dd.cudd.reorder пакета Python dd в частности, в привязках Cython к CUDD.

Порядок переменных можно изменить и изменить порядок, используя dd.cudd следующее:

from dd import cudd

bdd = cudd.BDD()
vrs = ['x', 'y', 'z']
bdd.declare(*vrs)
levels = {var: bdd.level_of_var(var) for var in vrs}
>>> levels
{'x': 0, 'y': 1, 'z': 2}
# change the levels
desired_levels = dict(x=2, y=0, z=1)
cudd.reorder(bdd, desired_levels)
# confirm that variables are now where desired
new_levels = {var: bdd.level_of_var(var) for var in vrs}
>>> new_levels
{'x': 2, 'y': 0, 'z': 1}
# dynamic reordering is initially turned on
>>> bdd.configure()
{'garbage_collection': True,
 'loose_up_to': 6710886,
 'max_cache_hard': 4294967295,
 'max_cache_soft': 4096,
 'max_growth': 1.2,
 'max_memory': 18446744073709551615,
 'max_swaps': 2000000,
 'max_vars': 1000,
 'min_hit': 30,
 'reordering': True}
# turn off dynamic reordering
bdd.configure(reordering=False)
# confirm dynamic reordering is now off
>>> bdd.configure()
{'garbage_collection': True,
 ...
 'reordering': False}  # here it is

Cudd_ReduceHeap вызывает переупорядочение, за исключением особого случая, когда выбор CUDD_REORDER_NONE дано.

От Cudd_ReadReorderings Документация:

Однако вызовы, которые даже не инициируют переупорядочение, не учитываются. Вызов может не инициировать переупорядочение, если в менеджере меньше живых узлов меньшего размера, или если CUDD_REORDER_NONE указан как метод переупорядочения.

Другие вопросы по тегам