CUDD的递归方法

Question

这是以下帖子中@DCTLib建议的后续行动。

Cudd_PrintMinterm, accessing the individual minterms in the sum of products

我一直在研究这个建议的(b)部分，并将在另一篇文章中分享一些伪代码。

同时，在他的部分(b)建议中，@DCTLib发布了一个指向https://github.com/VerifiableRobotics/slugs/blob/master/src/BFAbstractionLibrary/BFCudd.cpp的链接。我一直在试着读这个节目。在经典的Somenzi论文中有一个递归函数，即二进制决策图，它描述了计算满意分配数的算法(图7)。我一直在尝试比较这两种动物，鼻涕虫和图7，但是很难看到相似之处。但对我来说，C是最难以理解的。你知道鼻涕虫BFCudd是否基于索梅泽图7 @DCTLib吗？

谢谢你，贵

​

​

Answer 1

这不是完全相同的算法。

有两个主要区别：

首先，"SatHowMany“函数在计数时不需要考虑一个变量立方体。相反，该函数考虑所有变量。"recurse_getNofSatisfyingAssignments“支持函数中显示的多维数据集，如果在BDD中找到未出现在多维数据集中的变量，则可能返回NaN (而不是数字)。其余的分歧似乎来自于这种支持。

其次，SatHowMany向节点的所有n个变量返回满意的赋值数。例如，这导致了第4行2的除法。"recurse_getNofSatisfyingAssignments“只返回要考虑的其余变量的赋值数。

这两种算法都缓存信息--在"SatHowMany“中，它称为表，在"recurse_getNofSatisfyingAssignments”中称为缓冲区。注意，在"recurse_getNofSatisfyingAssignments“的第24行中，抛出了一个常量字符串。这意味着该函数要么无法工作，要么永远无法到达代码。很可能是后者。

函数"SatHowMany“似乎假定它得到一个BDD节点--它不能是指向可补BDD节点的指针。函数"recurse_getNofSatisfyingAssignments“可以正确地处理可补节点，因为DdNode*可以存储指向可补节点的指针。

由于对多维数据集的支持，"recurse_getNofSatisfyingAssignments“支持灵活的变量排序(因此查找"cuddI”表示变量在当前BDD变量排序中的位置)。对于函数SatHowMany，变量排序没有区别。