Crates.io | decdnnf_rs |
lib.rs | decdnnf_rs |
version | |
source | src |
created_at | 2024-07-15 14:35:46.381976 |
updated_at | 2024-07-15 14:35:46.381976 |
description | A library for Decision-DNNFs. |
homepage | https://www.cril.univ-artois.fr/software/decdnnf-rs/ |
repository | https://github.com/crillab/decdnnf_rs |
max_upload_size | |
id | 1303914 |
size | 0 |
Rust tools for Decision-DNNF formulas, including translation, model counting and model enumeration.
Decdnnf-rs is a tool for manipulating Decision-DNNFs produced by d4. It allows queries such as counting models, searching for models under assumptions, or enumeration of solutions, for which it excels. It also provides a tool for translating formulas generated by d4 into the format generated by c2d.
Decdnnf-rs requires a recent version of the Rust toolchain (>= 1.72.1). See rust-lang.org for more information on how to install Rust.
To build from source, run cargo build --release
to compile the binary. It will be set in the target/release
directory.
The decdnnf-rs tool expects a subcommand. To get the list, just invoke the command with the help flag.
decdnnf_rs -h
In the same way, you can obtain the list of expected and optional arguments by adding the help flag after the subcommand.
decdnnf_rs model-counting -h
Some options are common to most commands, like the ones dedicated to input file and logging level.
Another one of interest is --n-vars
.
Since the output format of d4 (which is the default input format of decdnnf_rs) does not provide the number of variables of the problems, this number cannot be deduced if it is more important than the highest variable index in use.
Setting --n-vars
allows to override the number of variables returned by the parser, which is set to the highest variable index.
Use the translation
command:
decdnnf_rs translation -i instance.nnf
Use the model-counting
command:
decdnnf_rs model-counting -i instance.nnf
Use the model-enumeration
command:
decdnnf_rs model-enumeration -i instance.nnf
This commands admits multiple options allowing to set the number of variables (in case it is higher than the highest index in the input formula), use a compact output or use an enumeration algorithm based on a decision tree.
Run decdnnf_rs model-enumeration -h
for more information.
Decdnnf-rs is developed at CRIL (Univ. Artois & CNRS). It is made available under the terms of the GNU GPLv3 license.