我正在使用 CUDD 包进行 BDD 操作。我想知道是否有人知道传递特定变量顺序以指示程序在构建 BDD 时使用此顺序的方法。我正在使用变量数量相对较少的布尔函数。
事实上，即使有一种方法可以将特定的输入变量传递给程序以作为 BDD 的根，这也符合我的目的。如果有人知道如何做到这一点，那么我将非常感谢您的帮助。我浏览了文档，但没有发现任何与此相关的内容。也许我错过了什么。
问问题
722 次
2 回答
1
您可以将重新排序算法设置为CUDD_REORDER_NONE
Cudd_ReduceHeap(manager, CUDD_REORDER_NONE, 0);
这样，变量的顺序由您引入它们的顺序给出。
于 2014-02-25T08:33:16.383 回答
1
CUDD 中有两个函数可以满足问题的要求：
Cudd_AutodynDisable(manager)：“禁用自动动态重新排序。”Cudd_ShuffleHeap(manager, permutation)：“根据给定的排列重新排序变量。”
通过在声明任何变量之前调用Cudd_AutodynDisable，变量级别将被初始化并保持变量声明的顺序。
为了解决在任意稍后时间获得某些所需变量顺序的更一般情况，首先调用Cudd_AutodynDisable，然后将所需变量顺序传递给Cudd_ShuffleHeap。
调用这些函数的示例可以在Python包dd.cudd.BDD.configure的方法和函数中找到，特别是在其与 CUDD 的 Cython 绑定中。dd.cudd.reorderdd
可以使用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。
但是，甚至不启动重新排序的调用不计算在内。如果管理器中的活动节点少于 minsize，或者如果
CUDD_REORDER_NONE指定为重新排序方法，则调用可能不会启动重新排序。
于 2017-10-15T21:32:09.250 回答