OxiDD

OxiDD 是一个高度模块化的决策图框架，用 Rust 编写。最显著的决策图实例是由 (减少顺序的) 二值决策图 (BDD) 提供，它们是布尔函数 𝔹ⁿ → 𝔹 的简洁表示。这种 BDD 表示法是规范的，因此，判断布尔函数的等价性——在一般情况下是一个 co-NP-完全问题——可以在常数时间内完成。此外，许多布尔运算可以在两个 BDD f,g 之间以 𝒪(|f| · |g|) (其中 |f| 表示 f 中的节点数) 的时间复杂度进行。OxiDD 致力于成为框架，以实现各种决策图的高性能实现，同时降低实现难度。

// 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 上的软件包（即将发布）。

常见问题解答（FAQ）

Q：关于 X 语言绑定呢？

如上所述，OxiDD 已经支持 C/C++ 和 Python。C# 和 Java 绑定可能在今年稍后出现。如果你希望从不同的语言使用 OxiDD，请与我们联系。我们非常愿意支持你和你使用的情况。

Q：关于动态/自动重新排序呢？

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

许可

OxiDD 根据 MIT 或 Apache 2.0 许可证之一许可，具体取决于您的意见。

除非您明确表示，否则，您根据 Apache 2.0 许可证定义的任何有意提交以包含在此项目中的贡献，将按上述方式双重许可，而不附加任何额外条款或条件。

出版物

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

尼尔斯·胡松，克莱门斯·杜布斯拉夫，霍格尔·赫尔曼斯，以及马克西米利安·A·科赫：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，作为德国卓越战略的一部分）。