Compile! Project - CRIL-CNRS & Univ. Artois

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

• source files in ZIP format

How to build the d-DNNF reasoner

• This software requires a C++ compiler supporting C++14, GNU Make, and the GNU MP library to be built.
• Decompress the archive, and enter the commands ./configure and make in the software directory to build the program.
• The program is built in the current directory under the name query-dnnf.

How to use d-DNNF-reasoner

• d-DNNF-reasoner: launches d-DNNF-reasoner and runs a shell to execute some commands
• d-DNNF-reasoner -cmd commands.txt: launches d-DNNF-reasoner, executes the commands reported in file "commands.txt", and exits
• cat commands.txt | d-DNNF-reasoner: same as above

d-DNNF-reasoner commands

• general commands
  
  • h: displays help (list of commands)
  • q: quits the program
• input/output commands
  
  • load filename: loads a d-DNNF representation from the file "filename"
  • w filename: loads a file containing weights associated with the literals
  • p: prints the current d-DNNF representation to the standard output
  • store filename: stores the current d-DNNF representation to the file "filename"
• queries/transformations
  
  • cond i₁ ... i_n: conditions the d-DNNF representation by i₁, ..., and i_n
  • model [i₁ ... i_n]: computes and prints to the standard output a model of the current d-DNNF representation containing the literals i₁, ..., and i_n; prints "UNSAT" if none
  • mc [i₁ ... i_n]: computes and prints to the standard output the number of models of the current d-DNNF representation containing the literals i₁, ..., and i_n; prints the weighted model count when weights have been associated with the literals
  • min filename: computes and prints to the standard output a model of the current d-DNNF representation which minimizes the objective function described in "filename"
  • mintr filename: transforms the current d-DNNF representation to remove the models which do not minimize the objective function described in "filename"
• current formula statistics
  
  • vars: displays the number of variables of the current d-DNNF representation (including free ones) to the standard output
  • nodes: displays the number of nodes of the current d-DNNF representation to the standard output

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:

• first, a preamble line nnf v e n where
  
  • v is the number of nodes,
  • e is the number of edges,
  • n is the number of Boolean variables under consideration;
• then, a sequence of leaf-nodes (one per line), and-nodes and or-nodes, appearing according to the topological order (children must be described before their parents); note that every node is implicitly indexed by an integer from 0 to v-1, such that the induced order respects the order of declaration.

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 i₁ ... i_c are the indexes of these children. An or-node is declared using a statement O j c i1 ... ic where c i₁ ... i_c 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:

• O j 2 i1 i2 for a decision node,
• O 0 0 for the false node.

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.

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