OxiDD

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

特性

• 已实现多种类型的（有序）决策图
  • 二值决策图 (BDDs)
  • 带补边 BDDs (BCDDs)
  • 零抑制 BDDs (ZBDDs，又称 ZDDs/ZSDDs)
  • 多终端 BDDs (MTBDDs，又称 ADDs)
  • 三值决策图 (TDDs)
• 可扩展性：由于 OxiDD 的模块化设计，可以实现新的决策图类型，而无需重新实现核心数据结构。
• 并发：表示为 DD 的函数可以在多线程环境中安全使用。此外，可应用算法可以在多个 CPU 核心上并行执行。
• 性能：与 BuDDy、CUDD 和 Sylvan 等其他流行 BDD 库相比，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目录中。[https://github.com/oxidd/oxidd/blob/a31cd9f22ea46a79f34a5ecd61f86354e60ebe76/crates/oxidd-rules-tdd/crates](https://github.com/oxidd/oxidd/blob/a31cd9f22ea46a79f34a5ecd61f86354e60ebe76/crates/oxidd-rules-tdd/crates "crates")。该框架围绕一组核心特质构建，这些特质位于oxidd-core目录中。这些特质是抽象化的，使得可以轻松地替换一个组件为另一个，如下面的依赖图所示。DD节点存储的数据结构主要是由oxidd-manager-index目录定义的。还有oxidd-manager-pointer目录，它包含了一种替代实现（在这里，边由指针而不是32位索引表示）。apply缓存的实现可以在oxidd-cache目录中找到。不同DD类型的主要规则和算法实现于oxidd-rules-*目录中。所有组件的“连接”方式有很多种。oxidd目录为最终用户提供了合理的默认实例。还有更多crates，但上述的是最重要的。

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

常见问题解答

问题：关于语言X的绑定呢？

如上所述，OxiDD已经支持C/C++和Python。C#和Java绑定可能在今年晚些时候跟进。如果您想从不同的语言中使用OxiDD，请与我们联系。我们非常乐意支持您和您的使用场景。

问题：关于动态/自动重排序呢？

OxiDD已经支持了建立给定变量顺序意义上的重排序。在不引入不安全代码到应用运算符的算法中、添加相对昂贵的同步机制或完全禁用并发的情况下实现这一点是一个较大的工作量。更多细节可以在[我们的论文](https://doi.org/10.1007/978-3-031-57256-2_13 "我们的论文")中找到。但是，现在，添加如sifting这样的重排序启发式方法是一个低垂的果实。接下来，我们还将致力于动态重排序（即中止操作以进行重排序，然后重新启动它们）和自动重排序（即识别动态重排序有益的时间点的启发式方法）。

许可

OxiDD的许可根据您的选择可以是[MIT](https://github.com/oxidd/oxidd/blob/a31cd9f22ea46a79f34a5ecd61f86354e60ebe76/crates/oxidd-rules-tdd/LICENSE-MIT "MIT")或[Apache 2.0](https://github.com/oxidd/oxidd/blob/a31cd9f22ea46a79f34a5ecd61f86354e60ebe76/crates/oxidd-rules-tdd/LICENSE-APACHE "Apache 2.0")。

除非您明确声明，否则，根据Apache 2.0许可定义的，您有意提交给本项目包含的任何贡献，都将按照上述方式双重许可，不附加任何额外条款或条件。

出版物

介绍OxiDD的开创性论文在TACAS'24上发表。[https://doi.org/10.1007/978-3-031-57256-2_13](https://doi.org/10.1007/978-3-031-57256-2_13 "seminal paper")如果您使用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，作为德国卓越战略的一部分）。