OxiDD

OxiDD是一个高度模块化的决策图框架，使用Rust编写。决策图最显著的例子是由（减少有序的）二进制决策图（BDD）提供的，它们是布尔函数𝔹ⁿ → 𝔹的简洁表示。这种BDD表示是规范的，因此，决定布尔函数的等价性（通常是一个co-NP完全问题）可以在常数时间内完成。此外，两个BDD f,g 上的许多布尔运算可以在 𝒪(|f|·|g|)（其中|f|表示f中的节点数）时间内完成。OxiDD旨在成为一个框架，用于实现各种决策图的高性能实现，而无需付出太多努力。

特性

• 已实现多种（减少有序的）决策图
  • 二进制决策图（BDD）
  • 带补边BDD（BCDD）
  • 零抑制BDD（ZBDD，即ZDD/ZSDD）
  • 多终端BDD（MTBDD，即ADD）
  • 三值决策图（TDD）
• 可扩展性：由于OxiDD的模块化设计，可以无需重新实现核心数据结构即可实现新的决策图类型。
• 并发性：表示DD的函数可以安全地在多线程环境中使用。此外，应用算法可以并行地在多个CPU核心上执行。
• 性能：与其他流行的BDD库（例如BuDDy、CUDD和Sylvan）相比，OxiDD已经具有竞争力，甚至超越了它们。
• 支持重新排序：OxiDD可以将决策图重新排序到给定的变量顺序。支持动态重新排序，例如通过筛选，即将到来。

入门

构建公式(x₁ ∧ x₂) ∨ x₃的BDD如下

// Create a manager for up to 2048 nodes, up to 1024 apply cache entries, and
// use 8 threads for the apply algorithms. In practice, you would choose higher
// capacities depending on the system resources.
let manager_ref = oxidd::bdd::new_manager(2048, 1024, 8);
let (x1, x2, x3) = manager_ref.with_manager_exclusive(|manager| {(
      BDDFunction::new_var(manager).unwrap(),
      BDDFunction::new_var(manager).unwrap(),
      BDDFunction::new_var(manager).unwrap(),
)});
// The APIs are designed such that out-of-memory situations can be handled
// gracefully. This is the reason for the `?` operator.
let res = x1.and(&x2)?.or(&x3)?;
println!("{}", res.satisfiable());

（我们将在未来添加更详细的指南。）

项目结构

主代码位于 crates 目录中。该框架围绕一组核心特性构建，这些特性位于 oxidd-core crate 中。这些特性是抽象的，使得可以轻松地用另一个组件替换一个组件，如下面的依赖关系图所示。DD 节点存储的数据结构主要由 oxidd-manager-index crate 定义。还有一个 oxidd-manager-pointer crate，其中包含一个替代实现（在这里，边由指针而不是 32 位索引表示）。apply 缓存的实现可以在 oxidd-cache crate 中找到。各种 DD 类型的简化规则和主要算法在 oxidd-rules-* crate 中实现。所有组件的“连接”方式有多种。oxidd crate 为最终用户提供了合理的默认实例化。还有一些其他的crate，但上述的才是最重要的。

除了 Rust 代码外，在 bindings 目录中还有 C/C++ 和 Python 的绑定。OxiDD 有一个位于 oxidd-ffi crate 的外国函数接口 (FFI)。它不公开整个可以从 Rust 中使用的 API，但它足以创建 BDD 并在它们上应用各种逻辑运算符。原则上，你可以使用任何可以调用 C 函数的语言来使用 FFI。然而，还有更方便的 C++ 绑定，它是建立在 C FFI 之上的。你可以直接使用 CMake 包含此存储库。要从 Python 使用 OxiDD，最简单的方法是使用 PyPI 上的包（即将发布）。

常见问题解答

问题：关于 X 语言绑定怎么办？

如上所述，OxiDD 已经支持 C/C++ 和 Python。C# 和 Java 绑定可能在今年稍后出现。如果您想从不同的语言中使用 OxiDD，请与我们联系。我们真的希望支持您和您的用例。

问题：关于动态/自动重新排序怎么办？

OxiDD 已经支持建立给定变量顺序的重新排序。在不向应用算子的算法中引入不安全代码、添加相对昂贵的同步机制或完全禁用并发的情况下实现这一点是一个更大的努力。更多细节可以在我们的论文中找到。但是，现在添加诸如筛选之类的重新排序启发式方法是低垂的果实。接下来，我们还将致力于动态重新排序（即中止操作进行重新排序，然后再次启动它们）和自动重新排序（即识别动态重新排序有利的时刻的启发式方法）。

许可协议

OxiDD 根据您的意见，可以许可为 MIT 或 Apache 2.0。

除非您明确声明，否则根据 Apache 2.0 许可证定义的，您有意提交以包含在此项目中的任何贡献，将如上所述双重许可，没有其他条款或条件。

出版物

介绍 OxiDD 的开创性论文已发表在 TACAS'24 上。如果您使用 OxiDD，请引用我们如下

Nils Husung, Clemens Dubslaff, Holger Hermanns, 和 Maximilian A. Köhl: 《OxiDD：一个安全、并发、模块化和性能卓越的 Rust 决策图框架》。在：《第 30 届国际工具和算法构建与系统分析会议（TACAS’24）论文集》（2024年接受发表）

@inproceedings{oxidd24,
  author        = {Husung, Nils and Dubslaff, Clemens and Hermanns, Holger and K{\"o}hl, Maximilian A.},
  booktitle     = {Proceedings of the 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'24)},
  title         = {{OxiDD}: A Safe, Concurrent, Modular, and Performant Decision Diagram Framework in {Rust}},
  year          = {2024},
  doi           = {10.1007/978-3-031-57256-2_13}
}

致谢

这项工作部分得到德国研究基金会（DFG）的资助，项目 TRR 248（见https://perspicuous-computing.science，项目 ID 389792660）和 EXC 2050/1（CeTI，项目 ID 390696704，作为德国卓越战略的一部分）。