Crate decdnnf_rs 

Decdnnf-rs

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.

Compiling/installing decdnnf-rs from sources

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.

How to use

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.

By default, decdnnf_rs partially checks the correctness on the input Decision-DNNF, in particular the decomposability property of the disjunction and the determinism of the disjunction node. However, these checks may consume some time. In case you are sure of the correctness of the formula, you can skip these tests by adding the --do-not-check flag.

Translate a d4 Decision-DNNF into a c2d Decision-DNNF

Use the translation command:

decdnnf_rs translation -i instance.nnf

Count the models of a Decision-DNNF

Use the model-counting command:

decdnnf_rs model-counting -i instance.nnf

Enumerate the models of a Decision-DNNF

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.

Direct access to a model

Use the direct-access command:

decdnnf_rs direct-access --index 5 -i instance.nnf

The order of the models is determined by the structure of the formula by default, and may change with new versions of the tool. Adding the --lexicographic-order flag is an effective way to prevent this. This flag instructs the tool to sort the models according to the lexicographic order, although this approach does result in a longer processing time.

Uniform sampling

Use the sampling command:

decdnnf_rs sampling -l 5 -i instance.nnf

The indices associated with the models work in the same way as for direct access.

License

Decdnnf-rs is developed at CRIL (Univ. Artois & CNRS). It is made available under the terms of the GNU GPLv3 license.

Structs

C2dWriter

A structure used to write a Decision-DNNF using the c2d output format.

D4Reader

A structure used to read the output of the d4 compiler.

DecisionDNNF

A Decision-DNNF formula.

DecisionDNNFChecker

An algorithm used for an algorithm that checks if a Decision-DNNF is correct.

DirectAccessEngine

An object that, given an (internally computed) complete order on the models of a DecisionDNNF, allows to return the k-th model.

FreeVariables

A structure used to computes the free variables, ie. the variables that does not appear in (some) models.

Literal

A structure representing a literal.

ModelCounter

A structure used to count the models of a DecisionDNNF.

ModelEnumerator

A structure used to enumerate the models of a DecisionDNNF.

ModelFinder

A structure used to find models in a DecisionDNNF.

OrFreeVariables

A structure used to handle efficiently the free variables located at disjunction nodes.

OrderedDirectAccessEngine

An object that, given an (internally computed) complete order on the models of a DecisionDNNF, allows to return the k-th model.