The d4 compiler

d4 is a compiler associating with an input CNF formula an equivalent representation from the language Decision-DNNF. Decision-DNNF is the language consisting of the Boolean circuits with a single output (its root), where each input is a literal or a Boolean constant, and each internal gate is either a decomposable ∧ gate of the form N = ∧(N1, . . . , Nk) (”decomposable” means here that for each i, j ∈ {1, . . . , k} with i ≠ j the subcircuits of N rooted at Ni and Nj do not share any common variable) or decision gates of the form N = ite(x, N1, N2). x is the decision variable at gate N, it does not occur in the subcircuits N1, N2, and ite is a ternary connective whose semantics is given by ite(X, Y, Z) = (¬X ∧ Y ) ∨ (X ∧ Z) (”ite” means ”if ... then ... else ...: if X then Z else Y ).

For more details, see the paper:

J.-M. Lagniez and P. Marquis. "An Improved Decision-DNNF Compiler". Proceedings of IJCAI'17, pages 667-673. (pdf)

Source code

The source code can be found on Github.

Resources for the d4 compiler (V 1.0)

How to use d4

The runtime code ./d4 can be launched on any computer with a 64-bit architecture, under Linux OS.

Example of DIMACS CNF formula
p cnf 3 3
1 2 3 0
-1 -2 0
-2 -3 0

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

Example of invocation $ ./d4 test.cnf -out="compiledForm.nnf"

c WARNING: for repeatability, setting FPU to use double precision
c Problem Statistics:
c
c Benchmark Information
c Number of variables: 3
c Number of clauses: 3
c Number of literals: 7
c Parse time: 0.00
c
c d-DNNF Information
c Number of nodes: 2
c Number of edges: 4
c
c Final time: 0.008000
c
s 4

The output generated by the compiler d4 is the number of models of the input, starting with "s". For the input test.cnf, the output is 4, which means that test.cnf has 4 models.

The number of internal nodes (decomposable AND nodes and decision nodes) and the number of edges of the resulting Decision-DNNF representation is displayed, as well as the overall compilation time ("Final time"); this time includes the parsing time, which is also reported.

For the test.cnf instance, the compiled form (as a Decision-DNNF representation) has 2 internal nodes (which are decision nodes) and 4 edges. The compilation time is equal to 0.008 second.

If the option -out="fileName.nnf" is used, a d-DNNF representation equivalent to the Decision-DNNF representation computed by d4 is generated and stored in file fileName.nnf. The d-DNNF representation which is stored follows the same format as those produced by the C2D compiler.

Here are the contents of the output file compiledForm.nnf for the test.cnf instance: nnf 15 4 3
O 0 0
A 0
L -1
L 3
A 3 3 2 1
L 1
A 2 5 1
O 1 2 6 4
L -2
A 2 8 7
L -1
L 2
L -3
A 4 12 11 10 1
O 2 2 13 9