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