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核心上执行。
• 性能：与其他流行的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-* crates中实现的。所有组件可以“连接”在一起的方式有很多种。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上的包（即将发布）。

常见问题解答

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