Decdnnf-rs

决策-DNNF 公式的 Rust 工具，包括翻译、模型计数和模型枚举。

Decdnnf-rs 是一个用于操作由 d4 生成的决策-DNNF 的工具。它允许查询，如计数模型、在假设下搜索模型或枚举解，在这些方面表现出色。它还提供了一个工具，将 d4 生成的公式翻译成由 c2d 生成的格式。

从源代码编译/安装 decdnnf-rs

Decdnnf-rs 需要 Rust 工具链的最新版本（>= 1.72.1）。有关如何安装 Rust 的更多信息，请参阅 rust-lang.org。

要从源代码构建，请运行 cargo build --release 编译二进制文件。它将在 target/release 目录中设置。

如何使用

decdnnf-rs 工具期望一个子命令。要获取列表，只需使用帮助标志调用命令。

decdnnf_rs -h

同样，您可以在子命令后添加帮助标志来获取预期和可选参数的列表。

decdnnf_rs model-counting -h

一些选项是大多数命令共有的，例如针对输入文件和日志级别的选项。另一个有趣的选项是 --n-vars。由于 d4 的输出格式（这是 decdnnf_rs 的默认输入格式）不提供问题的变量数，因此如果这个数字比使用的最高变量索引更重要，就无法推断出来。设置 --n-vars 允许覆盖解析器返回的变量数，该数字设置为最高变量索引。

将 d4 决策-DNNF 翻译成 c2d 决策-DNNF

使用 translation 命令

decdnnf_rs translation -i instance.nnf

计数决策-DNNF 的模型

使用 model-counting 命令

decdnnf_rs model-counting -i instance.nnf

枚举决策-DNNF 的模型

使用 model-enumeration 命令

decdnnf_rs model-enumeration -i instance.nnf

此命令接受多个选项，允许设置变量的数量（如果它高于输入公式的最高索引），使用紧凑的输出或使用基于决策树的枚举算法。运行 decdnnf_rs model-enumeration -h 获取更多信息。

许可证

Decdnnf-rs 由 CRIL（Artois 大学 & CNRS）开发。它根据 GNU GPLv3 许可证条款提供。