Пакет 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
указан как метод переупорядочения.