OxiDD

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

特性

• 已实现几种（简化排序的）决策图
  • 二进制决策图 (BDDs)
  • 带有补边 (BCDDs) 的 BDDs
  • 零抑制 BDDs (ZBDDs，也称为 ZDDs/ZSDDs)
  • 多终端 BDDs (MTBDDs，也称为 ADDs)
  • 三元决策图 (TDDs)
• 可扩展性：由于 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 包中。这些特性是抽象化，使得可以轻松地用一个组件替换另一个组件，如下面的依赖图所示。存储 DD 节点的数据结构主要是由 oxidd-manager-index 包定义的。还有一个 oxidd-manager-pointer 包，它包含一个替代实现（在这里，边由指针而不是 32 位索引表示）。apply 缓存的实现可以在 oxidd-cache 包中找到。各种 DD 类型的简化规则和主要算法在 oxidd-rules-* 包中得到实现。所有组件可以通过不同的方式“连接”在一起。oxidd 包为最终用户提供了合理的默认实例化。还有一些其他包，但上述的是最重要的。

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

常见问题解答

Q: 关于 X 语言有绑定吗？

如上所述，OxiDD 已支持 C/C++ 和 Python。C# 和 Java 绑定可能会在下半年推出。如果您想从其他语言使用 OxiDD，请与我们联系。我们非常希望支持您和您的用例。

Q: 关于动态/自动重新排序怎么办？

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

许可

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，作为德国卓越战略的一部分）。