The d-DNNF reasoner

Queries and transformations on d-DNNF representations

d-DNNF-reasoner is a tool for reasoning on d-DNNF representations. This tool implements some useful queries and transformations on compiled forms, including conditioning, satisfiability checking and model counting (CD, CO and CT operations as defined in the knowledge compilation map).

Ressources for the d-DNNF reasoner

How to build the d-DNNF reasoner

How to use d-DNNF-reasoner

d-DNNF-reasoner commands

Note that d-DNNF-reasoner performs some reductions of the current d-DNNF representation. This explains some behaviors that may be odd; for example, loading a file and storing it without any transformation may result in getting an output file that is different from the input one (although the two d-DNNF representations are equivalent).

Input/output format:

d-DNNF-reasoner is able to read commands from the standard input or from a file. d-DNNF loading is achieved by running a command which reads a d-DNNF representation encoded using the format used by the c2d compiler. According to the compiler language specification, a d-DNNF representation is encoded as follows:

A leaf node is specified by an expression L [-]j, where j (resp. -j) denotes the positive (resp. negative) literal of the j th variable (with j in [1,...,n]). One can build Boolean constant nodes using special cases of and-nodes and or-nodes (defined below): A 0 stands for true, while O 0 0 stands for false.

An and-node is declared using a statement A c i1 ... ic where c is the number of children the and-node admits, and i1 ... ic are the indexes of these children. An or-node is declared using a statement O j c i1 ... ic where c i1 ... ic give the node children and j defines the variable on which the children conflicts if it is different from 0. Note that as we consider d-DNNF representations, the two following patterns are the only ones which are allowed:

Encoding of a d-DNNF representation
The d-DNNF representation:
  AND( -1,4,

is encoded by:

nnf 13 15 4
L -1
L 1
L -2
L 2
L -3
L 3
L -4
L 4
A 2 2 5
A 2 3 4
O 2 2 8 9
A 3 7 0 10
A 4 1 2 4 6
O 1 2 11 12

d-DNNF-reasoner also provides the weighted model counting query. Weights are associated with literals using a dedicated file composed of lines following the pattern [-]j w; [-]j is a literal and w is a (float) weight where the decimal separator is a dot. Literals unassigned in the weights file are given a weight of 1.

Associating weights with literals
The following file, when loaded, associates the weights 2, 3, 0.5 with the literals -1, 1 and 2.

-1 2
1 3
2 0.5

Finally, objective functions are specified using the same formalism as weight files, except that the weights associated with literals are integer values.

Objective functions
The following file describes the objective function 2.¬a + 3.a + 2.b, where a is variable 1 and b is variable 2.

-1 2
1 3
2 1