1

我正在使用 CUDD 包进行 BDD 操作。我想知道是否有人知道传递特定变量顺序以指示程序在构建 BDD 时使用此顺序的方法。我正在使用变量数量相对较少的布尔函数。

事实上，即使有一种方法可以将特定的输入变量传递给程序以作为 BDD 的根，这也符合我的目的。如果有人知道如何做到这一点，那么我将非常感谢您的帮助。我浏览了文档，但没有发现任何与此相关的内容。也许我错过了什么。

4

2 回答 2

1

您可以将重新排序算法设置为CUDD_REORDER_NONE

Cudd_ReduceHeap(manager, CUDD_REORDER_NONE, 0);

这样，变量的顺序由您引入它们的顺序给出。

于 2014-02-25T08:33:16.383 回答
1

CUDD 中有两个函数可以满足问题的要求：

通过在声明任何变量之前调用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。

来自Cudd_ReadReorderings的文档：

但是，甚至不启动重新排序的调用不计算在内。如果管理器中的活动节点少于 minsize，或者如果CUDD_REORDER_NONE指定为重新排序方法，则调用可能不会启动重新排序。

于 2017-10-15T21:32:09.250 回答