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目录中。这些特性是实现组件之间轻松替换的抽象，如下面的依赖关系图所示。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++绑定，它建立在C FFI之上。您只需使用CMake包含此存储库。要从Python使用OxiDD，最简单的方法是使用PyPI上的包（即将发布）。

常见问题解答

问：X语言的绑定怎么办？

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

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

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