/d-dnnf-reasoner

Primary LanguageRustGNU Lesser General Public License v3.0LGPL-3.0

ddnnife a d-dnnf-reasoner

ddnnife takes a smooth d-DNNF as input following the standard format specified by c2d or a d-DNNF conforming the d4 standard, which is an extension of the c2d standard. After parsing and storing the d-DNNF, ddnnife can be used to compute the cardinality of single features, all features, or partial configurations. Additionally, via the stream API, ddnnife is able to compute SAT queries, core/dead features, atomic sets, enumerate complete valid configurations, and produce uniform random samples.

Table of contents

  1. Building
  2. Usage

Building

In the following, we describe the process to compile ddnnife. As an alternative, we offer binaries of the major releases on the main branch.

Requirements for Building

First, if not done already, you have to install rust. The recommended way is the following, using curl and rustup:

curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh

After that, we recommend entering "1" to proceed with installation (without customizations).

Additionally, we use rug for the computations. Make sure to install everything mentioned on rugs crates.io page to use rug and our software. There it says:

Rug [...] depends on the GMP, MPFR and MPC libraries through the low-level FFI bindings in the gmp-mpfr-sys crate, which needs some setup to build; the gmp-mpfr-sys documentation has some details on usage under [different os][...].

To build on GNU/Linux, make sure you have diffutils, ggc, m4 and make installed on your system. For example on Ubuntu:

sudo apt-get update && apt-get install diffutils gcc m4 make

Build the Binaries

Make sure that the current working directory is the one including the Cargo.toml file.

Both 

cargo build --release

ddnnife 

cargo build --release --bin ddnnife

dhone (dsharp preprocessor) 

cargo build --release --bin dhone

Usage

Binary on the Command Line

Simply execute the binaries with the -h, --help flag or no parameter at all to get an overview over all possible paramters and how to use them.

Note: In this and the following code examples, we added the ./target/release/ directories as prefix because that's where the binaries are placed when building. They are built according to the previous chapter and the working directory is not switched.

Help for dhone

./target/release/dhone -h

and ddnnife

./target/release/ddnnife -h

Examples

Preprocesses the d-DNNF: berkeleydb_dsharp.dimacs.nnf which may need preprocessing because it was created with dsharp (in this case it is actually necessary) and save the resulting d-DNNF as berkeleydb_prepo.dimacs.nnf

./target/release/dhone example_input/berkeleydb_dsharp.dimacs.nnf -s example_input/berkeleydb_prepo.dimacs.nnf

Compute the cardinality of a feature model for automotive01.

./target/release/ddnnife example_input/automotive01.dimacs.nnf

Compute the cardinality of features for busybox-1.18.0.dimacs.nnf with 2 threads and save the result as busybox-features.csv in the current working directory.

./target/release/ddnnife example_input/busybox-1.18.0.dimacs.nnf -c busybox -j 2

Compute the cardinality of features for automotive01 when compiled with d4. Here we need the -o Option that allows us to specify the total number of features. That information is needed but not contained in d-DNNFs using the d4 standard. Furthermore, the parsing takes more time because we have to smooth the d-DNNF. The results will be saved as auto1_d4-features.csv.

./target/release/ddnnife example_input/auto1_d4.nnf -o 2513 -c

An alternative to the above, using the possibility to load a model via stdin.

cat example_input/auto1_d4.nnf | ./target/release/ddnnife -p -o 2513 -c

Compute the cardinality of partial configurations for X264.dimacs.nnf with 4 threads (default) and save the result as X264.dimacs-queries.txt"(default) in the current working directory (default).

./target/release/ddnnife example_input/X264.dimacs.nnf -q example_input/X264.config

Stream API

With the --stream flag, we introduce the possibility to interact with ddnnife via stdin and stdout. The user can choose between different kinds of queries that can be further adjusted with additional parameters. The idea behind the stream API is to interact with ddnnife with another program, but for testing purposes one can use the stdin and stdout of a terminal to test the API.

We start ddnnife in stream mode for the automotive01 model via

./target/release/ddnnife example_input/auto1_d4.nnf -o 2513 --stream

From here on, we can use the following types of queries:

  • count: computes the cardinality of a partial configuration
  • core: lists core and dead features
  • sat: computes if a partial configuration is satisfiable
  • enum: lists complete satisfiable configurations
  • random: gives uniform random samples (which are complete and satisfiable)
  • atomic: computes atomic sets
  • save: saves the d-DNNF for future use
  • exit: leaves the stream mode

Furthermore, where sensible, the types of queries can be combined with the parameters:

  • v variables: the features we are interested in
  • a assumptions: assignments of features to true or false
  • l limit: the number of solutions
  • s seed: seeding for random operations
  • p path: the absolute path, we want to save the d-DNNF

The table below depicts the possible combinations of a query type with the parameters. The order of parameters has no influence on the result and if two or more paramters are valid, then every possible combination of those is also valid.

query type / parameter variables assumptions limit seed path
count ✔ ✔ ✘ ✘ ✘
core ✔ ✔ ✘ ✘ ✘
sat ✔ ✔ ✘ ✘ ✘
enum ✘ ✔ ✔ ✔ ✘
random ✘ ✔ ✔ ✔ ✘
atomic ✔ ✔ ✘ ✘ ✘
save ✘ ✘ ✘ ✘ ✔
exit ✘ ✘ ✘ ✘ ✘

Sub solutions (like multiple uniform random samples) will be separated by a ";". Intern a solution, the feature numbers are separated by a space. The end of an answer is indicated by a new line.

Syntactically wrong queries will result in an error message with error code. The different error codes are:

  • E1 Operation is not yet supported
  • E2 Operation does not exist. Neither now nor in the future
  • E3 Parse error
  • E4 Syntax error
  • E5 Operation was not able to be done, because of wrong input
  • E6 File or path error

Examples

After entering the stream API, the following examples are conceivable.

Check whether the features 10, 100, and 1000 are either core or dead under the assumption that feature 1 is deselected.

core a -1 v 10 100 1000

Compute the cardinality of partial configuration for the configurations: [1, -4, -5, -6], [2, -4, -5, -6], and [3, -4, -5, -6].

count v 1 2 3 a -4 -5 -6

Similarly to count, we compute whether the partial configuration is satisfiable: [1, -4, -5, -6], [2, -4, -5, -6], and [3, -4, -5, -6].

sat v 1 2 3 a -4 -5 -6

Lists all possible complete and valid configurations, with feature 1 selected and feature 2 deselected, as long as there are some left. Each following call will result in configurations that were not yet computed as results. After all configurations were returned as result, we start again at the beginning.

enum l 10 a 1 -2

Creates 10 uniform random samples with the seed 42. If neither l nor s is set, one uniform random sample will be created.

random l 1 s 42

Computes all atomic sets for the candidates v under the assumptions a. If no candidates are supplied, all features of the d-DNNF will be the candidates.

atomic v 1 2 3 4 5 6 7 8 9 10 a 1

Saves the nnf as smooth d-DNNF in the c2d format. The parameter p or path has to be set, and the path must be absolute.

save p /home/user/Documents/d-DNNFs/auto1.nnf

Exit the stream mode and terminate the ddnnife instance.

exit

Create Documentation

Genrates a Html file of the documentation and opens it in the default browser.

cargo doc --open

Besides the generated documentation, there are further comments in the code itself.

Run Tests

We highly encourage also running test cases with the release build, because the debug build is very slow in comparison.

cargo test --release

Test Coverage

Test coverage can be determined with llvm-cov. llvm-cov is not included in rustup. Make sure to execute the following commands in the folder that also contains the Cargo.toml file.

usage:

  1. Install llvm-cov
  2. Run tests. The results will be displayed in your default browser if the --open flag is set. Alternatively, the report will be printed to the console.
cargo +stable install cargo-llvm-cov
cargo llvm-cov --release --open