这是@DCTLib 在下面的帖子中提出的建议的后续行动。
Cudd_PrintMinterm, accessing the individual minterms in the sum of products
我一直在追求建议的 (b) 部分，并将在单独的帖子中分享一些伪代码。
同时，@DCTLib 在他的 (b) 部分建议中发布了指向 https://github.com/VerifiableRobotics/slugs/blob/master/src/BFAbstractionLibrary/BFCudd.cpp 的链接。我一直在尝试阅读这个程序。 Somenzi 的经典论文 Binary Decision Diagrams 中有一个递归函数，它描述了一种计算满足分配数量的算法（下图，图 7）。我一直在尝试比较两者，蛞蝓和图 7。但很难看到任何相似之处。但是C对我来说几乎是不可思议的。你知道蛞蝓 BFCudd 是否基于 Somenze 图 7，@DCTLib？
谢谢， 桂
【问题讨论】：
标签： cudd
这不是完全相同的算法。
有两个主要区别：
首先，“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，变量排序没有影响。
【讨论】：