#diagram #decision #bdd #order #oxi-dd #variables #file-format

oxidd-parser

逻辑文件格式的解析器

5 个不稳定版本

0.3.1 2024年7月15日
0.3.0 2024年7月14日
0.2.1 2024年6月6日
0.2.0 2024年6月5日
0.1.0 2024年4月11日

#414 in 解析器实现

Download history 7/week @ 2024-05-20 302/week @ 2024-06-03 9/week @ 2024-06-10 4/week @ 2024-06-17 74/week @ 2024-07-08 162/week @ 2024-07-15 43/week @ 2024-07-29

279 每月下载次数
用于 oxidd-cli

MIT/Apache

110KB
2.5K SLoC

OxiDD

Matrix

OxiDD 是一个用 Rust 编写的非常模块化的决策图框架。决策图最显著的实例是 (减少排序的)二进制决策图(BDDs),它们是布尔函数 𝔹n → 𝔹 的简洁表示。这种 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 crate 中。这些特性是实现组件之间轻松互换的抽象,如下面的依赖关系图所示。DD 节点存储的数据结构主要由 oxidd-manager-index crate 定义。还有一个名为 oxidd-manager-pointer 的 crate,它包含一个替代实现(在这里,边由指针而不是 32 位索引表示)。apply 缓存的实现可以在 oxidd-cache crate 中找到。不同类型 DD 的化简规则和主要算法在 oxidd-rules-* crate 中实现。所有组件可以以不同的方式“连接”在一起。oxidd crate 为最终用户提供了合理的默认实例化。还有一些其他的 crate,但上述的是最重要的。

Crate Dependency Graph

除了 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 根据您的意见,受 MITApache 2.0 许可协议的许可。

除非您明确声明,否则根据 Apache 2.0 许可证定义,您有意提交给本项目的任何贡献,都将根据上述协议双重许可,而无需任何附加条款或条件。

出版物

介绍 OxiDD 的开创性论文在 TACAS'24 上发表。如果您使用 OxiDD,请引用我们如下:

Nils Husung, Clemens Dubslaff, Holger Hermanns, 和 Maximilian A. Köhl: OxiDD:一个安全、并发、模块化和高效的 Rust 决策图框架。 在:30th 国际会议关于构建和分析系统(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,作为德国卓越战略的一部分)。

依赖项

~3–10MB
~108K SLoC