Compile! Project - CRIL-CNRS & Univ. Artois

cnf2eadt is a compiler associating with an input CNF formula an equivalent representation from the language EADT of (extended) affine decision trees. An extended affine decision tree simply is a tree with affine decision nodes and some specific decomposable conjunction or disjunction nodes. Unlike standard decision trees, the decision nodes of an EADT formula are not labeled by variables but by affine clauses. Interestingly, the models of an EADT representation can be counted efficiently.

We study EADT, and several subsets of it along the lines of the knowledge compilation map. We also describe a compiler and present some experimental results. Those results show that the EADT compilation-based approach is competitive with (and in some cases is able to outperform) the model counter Cachet and the d-DNNF compilation-based approach to model counting based on the C2D compiler.

For more details, see the paper:

F. Koriche, J.-M. Lagniez, P. Marquis and S. Thomas. "Affine Decision Trees for Model Counting". Proceedings of IJCAI'13, pages 947-953. (pdf)

The cnf2eadt compiler (v1.0)

The runtime code ./cnf2eadt can be launched on any computer with a 64-bit architecture, under Linux OS. [EADT compiler] [Benchmarks]

To run the compiler on a given CNF instance, use ./cnf2eadt instance.cnf. The instance must conform to the standard DIMACS format.

The corresponding output gives successively:

• the number of variables of the input CNF instance
• the number of clauses of the input CNF instance
• the number of OR nodes in the resulting compiled representation
• the number of AND nodes in the resulting compiled representation
• the number of True leaves in the resulting compiled representation
• the number of False leaves in the resulting compiled representation
• the compilation time (in seconds)
• the time needed to count the models of the instance from the compiled representation
• the number of models of the CNF instance

In order to count the number of models of the instance instance.cnf once conditioned successively by some queries (terms), put a instance.queries file in the same folder as the one used for instance.cnf.

Every .queries file must conform to the following format:

• the first line ("queries NQ NV NT") gives the numbers of queries in the file (NQ), the numbers of variables in the instance (NV) and the (constant) number of variables per term (NT)
• the next lines are the queries themselves (one term per line).Each term q is represented by a sequence of NT+1 signed integers, the last one being a 0; the others integers corresponds to literals (positive ones for positive integers, negated otherwise). Thus if (for instance) NQ == 1000, the file must contain 1001 lines

The command is ./cnf2eadt instance.cnf -queries

The corresponding output gives successively:

• the number of variables of the input CNF instance
• the number of clauses of the input CNF instance
• the number of OR nodes in the resulting compiled representation
• the number of AND nodes in the resulting compiled representation
• the number of True leaves in the resulting compiled representation
• the number of False leaves in the resulting compiled representation
• the compilation time (in seconds)
• the cumulated time needed to count for each query q the models of the compiled representation conditioned by q, from the compiled representation
• and for each query q:
  • the query q itself
  • the number of models of the input CNF instance conditioned by q

Finally, the option -uq=n can be used in conjunction with -queries to make precise a specific query (the one of rank n in the instance.queries file), on which one wants to focus.