xDd -各种二进制决策图

此Crate包含以下实现

• BDD -二进制决策图
• ZDD -零抑制二进制决策图
• MBDD -多重集合二进制决策图（用于表示多重集合而不是集合）
• MZDD -多重集合零抑制二进制决策图
• πDD -基于交换的排列决策图，后端使用ZDD或MZDD
• Rot-πDD -基于旋转的排列决策图，后端使用ZDD或MZDD

这一切都是通过大量的泛型参数实现的。

这与其他决策图Crate相比如何

xDd实现了许多不同类型的决策图，并且专注于组合数学问题中使用xDd，而不是等价性。

如果您有一个组合数学问题，这可能是一个适合您的Crate。如果您正在做集成电路设计，可能就不适合了。

在覆盖决策图类型方面，它目前非常完整，远远超过我所知的其他任何Crate，但它只包含更常见的算法（如并集、交集、非、基数）。

什么是BDD或ZDD？

BDD是二进制决策图，是一种表示布尔函数f(v0,v1,..vn)（布尔变量）的方法。在许多现实世界情况下，它表现出紧凑性。ZDD是一种变体，在大多数情况下f(v0,v1,..vn)为真且大多数变量为假时，通常更有效。

它们被Donald Knuth在《计算机程序设计艺术》第4卷第1分册中有很好的描述。

tests/chessboard_coverings.rs展示了BDD或ZDD如何被用来高效地计算棋盘被多米诺骨牌覆盖的方案数量，正如Knuth的书中第119页和120页所描述的。

tests/directed_animals.rs 展示了使用 BDD 或 ZDD 在正方形格子上枚举有向动物的一个例子，这是一个它可以完成但效率不是特别高的任务（但是一个很好的示例和集成测试）。

MBDD 或 MZDD 是什么？

BDD 通常被认为是从布尔变量集到布尔变量的函数 f(v0,v1,..vn)。另一种思考方式是，它是一个集合 S，其中元组 (v0,v1,..vn) 是 S 的一个元素，当且仅当 f(v0,v1,..vn) 为真。

多重集类似于集合，但元素可以多次出现在集合中。每个元素都有一个重复次数，即它在集合中出现的次数。如果 A 和 B 是集合，则 A 并 B 中元素的重复次数是该元素在 A 中的重复次数加上在 B 中的重复次数。集合交集的运算与乘法相同。请注意，在其他应用中存在其他多重集并集和交集的定义。

MBDD 是一种扩展，它以这种方式表示多重集。

或者，可以将其视为一个函数 f(v0,v1,..vn) 从布尔变量集到非负整数，使得 (f∪g)(v0,v1,..vn) = f(v0,v1,..vn)+g(v0,v1,..vn)，且 (f∩g)(v0,v1,..vn) = f(v0,v1,..vn)*g(v0,v1,..vn)。

MZDD 与之类似，但基于 ZDD 而不是 BDD。

一个示例应用在 examples/pap.rs 中，该程序计算长度为 n 的排列中包含给定模式 p 恰好 k 次的所有 k。

πDD 或 Rot-πDD 是什么？

这些排列决策图是两种使用 BDD 或 ZDD 或 MBDD 或 MZDD 作为后端来编码排列集的方法。

πDD 由 Shin-ichi Minato 提出：πDD：用于排列空间高效问题解决的新的决策图。在理论和方法论应用 - 满足性测试 - SAT 2011 - 第 14 届国际会议，SAT 2011，美国密歇根州安阿伯，2011 年 6 月 19-22 日。会议论文集，第 6695 卷计算机科学讲义，第 90-104 页。Springer，柏林，海德堡，2011

Rot-πDD 是一个类似的数据结构，在许多情况下表现更好，Yuma Inoue，基于决策图的多排列集操作研究，信息科学博士论文，北海道大学，（2017）。

这些通常由 ZDD 支持，但也可以用 MZDD 有用，如在 examples/pap.rs 中。

使用此库的通用思路

要创建一个图，您将使用一个工厂，然后特定的图将是该工厂表中一行的一个引用。这与 Knuth 中的方法类似。这允许构建越来越复杂的组合对象。

这些工厂实现了 [DecisionDiagramFactory] 特性。

对于 BDD 或 MBDD，使用 BDDFactory。对于 ZDD 或 MZDD 使用 ZDDFactory。这两个工厂都由两个泛型参数化

• 第一个是用于在 BDD 表中持有行索引的类型（Knuth 术语中的 HI 和 LO 指针）。对于 2022 年代的内存大小，这通常是 u32 - 每个条目都需要很多字节：一些用于表条目，更多用于用于保持唯一性的哈希表。但对于某些大型内存系统，可能需要使用更长的整数。
• 第二个是应用于存储此 MBDD 或 MZDD 的重复次数的类型。对于 MBDD 或 MZDD，这通常是 u32 或 u64；对于 BDD 或 ZDD，则为特殊零内存使用 NoMultiplicity。

速查表

• 对于 BDD，使用 BDDFactory＜u32,NoMultiplicity＞
• 对于 ZDD，使用 ZDDFactory＜u32,NoMultiplicity＞
• 对于 MBDD，使用 BDDFactory＜u32,u32＞
• 对于 MZDD，使用 ZDDFactory＜u32,u32＞

没有BDD是否会导致MBDD成为特殊情况而降低效率？实际上并非如此。只有一些非常微小的、略微更长的代码路径，其范围微不足道；这类似于rust标准库中将HashSet作为HashMap的零长度键的特殊情况的实现。

πDD或Rot-πDD由PermutationDecisionDiagramFactory表示，该Factory通过三个泛型参数进行参数化

• 旋转的单位类型（对于πDD是Swap，对于Rot-πDD是LeftRotation）
• 用于存储行索引的类型（见上文）
• 用于存储多重性的类型（见上文）

速查表

• 对于在上述参考中由Minato使用的πDD，请使用PermutationDecisionDiagramFactory::<Swap,u32,NoMultiplicity>
• 对于在上述参考中由Inoue使用的Rot-πDD，请使用PermutationDecisionDiagramFactory::<LeftRotation,u32,NoMultiplicity>
• 对于在examples/pap.rs中使用的具有多重性的Rot-πDD，请使用PermutationDecisionDiagramFactory::<LeftRotation,u32,u32>。

基数/解的数量/生成函数。

获取xDG的解的数量在组合数学问题中是一个常见需求。在最简单的情况下，这只是一个整数解的数量，正如Knuth描述中的算法C所产生的那样。

代码可能如下所示

fn enumate() {
    let num_variables : u16 = 4; // the number of variables in the BDD
    let mut factory = BDDFactory::<u32,NoMultiplicity>::new(num_variables); // create the factory
    let node = set_up_combinatorics_problem(&mut factory); // whatever your problem is
    let num_solutions : u128 = factory.number_solutions(node);
    println!("Answer is {}",num_solutions);
}

number_solutions函数以一种非常通用的方式实现了算法C，参数化结果类型。当泛型参数是u64或u128（未来版本可能还会添加更多）时，结果是简单的整数解的数量。

然而，有各种各样的项目可能希望从一个xDG中提取，它们使用与算法C非常相似的算法。

如果泛型参数是SingleVariableGeneratingFunction<u64>（或其他整数参数），则结果是给出解图中每个变量为真的数量下解的数量数组的数组。这是Knuth参考书中第74页上描述的生成函数。

如果泛型参数是SingleVariableGeneratingFunctionFixedLength<10>或类似，则结果类似于SingleVariableGeneratingFunction<u64>，除了结果数组被截断到长度10。

如果泛型参数是GeneratingFunctionSplitByMultiplicity<u64>或类似，则结果是给出按多重性划分的解的数量的数组。这在examples/pap.rs中使用。

其他各种事情都是可能的；您可以通过实现GeneratingFunctionWithMultiplicity特质来定义自己的。

可视化图

您可以使用make_dot_file函数生成适合Graphviz的dot格式的文件。

我创建的一个示例图像，用于调试排列组合

梯形是起始节点；椭圆形是决策点，矩形是终端。每个椭圆形左上角的数字是节点索引。如果涉及多重性，边将标记多重性。如果给定变量为假，则使用虚线；如果变量为真，则使用实线。

未来

当前变量的数量是一个u16类型。我考虑过将其通用化，尽管已经有很多通用参数了，我不希望为新手增加复杂性。如果有人真的需要这个功能，请通过github联系我。

对于其他期望的功能，也请通过github联系我。不保证一定能实现，但我愿意听取需求。

许可证

版权所有 2022 Andrew Conway。

根据以下任一许可证授权：

• Apache License 2.0（《LICENSE-APACHE》或http://www.apache.org/licenses/LICENSE-2.0）
• MIT许可证（《LICENSE-MIT》或http://opensource.org/licenses/MIT）

任您选择。

贡献

除非您明确表示否则，根据Apache-2.0许可证定义的，您有意提交以包含在作品中的任何贡献，将根据上述许可证双授权，不附加任何额外条款或条件。