[Compile! Project] Issue with some of the ddnnf generated

[jdusart]

Hi,

I am working on a Java API to manipulate a DDNNF and I am getting errors when I check that the AND gates are decomposable on some of the DDNNF that I generate using d4, not all of them. Some of the problematic CNF:
https://github.com/diverse-project/samplingfm/blob/master/Benchmarks/FeatureModels/pati.cnf
https://github.com/diverse-project/samplingfm/blob/master/Benchmarks/FeatureModels/cerf.cnf
https://github.com/diverse-project/samplingfm/blob/master/Benchmarks/FeatureModels/olpch2294.cnf

I don't think the problem is in my algorithm, since it's a very simple one and the subroutine are also used in a counting algorithm that give me the same results as d4.

(Note: I am the research engineer recruited on the COMMODE project)

[jdusart]

I have investigated a bit more and I am now sure that there is at least one bug in d4. I have run a test of compiling with d4 and then count the number of model with query-dnnf and the two program disagree but not always. I am attaching the trace of an execution. My implementation and query-dnnf agree on the count.

jeremie@jeremie-TUF-GAMING-FX504GM-FX80GM $ ./d4 ../mastermind_06_08_03.net.cnf -out=tmp.ddnnf
c WARNING: for repeatability, setting FPU to use double precision
c Problem Statistics:
c
c Benchmark Information
c Number of variables: 3979
c Number of clauses: 8833
c Number of literals: 19324
c Parse time: 0.00
c
c d-DNNF Information
c Number of nodes: 78645
c Number of edges: 159111
c
c Final time: 14.242140
c
s 107786116268245684913533484187099217586754687657495695953688460210254593858480474423296
jeremie@jeremie-TUF-GAMING-FX504GM-FX80GM $ ./query-dnnf tmp.ddnnf
load tmp.ddnnf
I will parse a graph of 3979 variables and 7736926 nodes...
Parsed 2 million nodes yet...
Parsed 4 million nodes yet...
Parsed 6 million nodes yet...
Done, returning item now...
mc
107786116268245684913533484187099217586754687657495695953688460210254593858480474423296
^C
jeremie@jeremie-TUF-GAMING-FX504GM-FX80GM $ java -cp jDDNNF.jar spirals.ddnnf.mains.CountingMain tmp.ddnnf
tmp.ddnnf
Count: 107786116268245684913533484187099217586754687657495695953688460210254593858480474423296
jeremie@jeremie-TUF-GAMING-FX504GM-FX80GM $ java -cp jDDNNF.jar spirals.ddnnf.mains.CheckDDNNF tmp.ddnnf
Not a ddnnf! id: 7736925
jeremie@jeremie-TUF-GAMING-FX504GM-FX80GM $ rm tmp.ddnnf
jeremie@jeremie-TUF-GAMING-FX504GM-FX80GM $ ./d4 ../mastermind_06_08_03.net.cnf -out=tmp.ddnnf
c WARNING: for repeatability, setting FPU to use double precision
c Problem Statistics:
c
c Benchmark Information
c Number of variables: 3979
c Number of clauses: 8833
c Number of literals: 19324
c Parse time: 0.00
c
c d-DNNF Information
c Number of nodes: 78694
c Number of edges: 159190
c
c Final time: 17.456699
c
s 107786116268245684913533484187099217586754687657495695953688460210254593858480474423296
jeremie@jeremie-TUF-GAMING-FX504GM-FX80GM $ java -cp jDDNNF.jar spirals.ddnnf.mains.CountingMain tmp.ddnnf
tmp.ddnnf
Count: 166683025214157941492941029847354226054685717626431828808944885126688881800181907881840889944866816
jeremie@jeremie-TUF-GAMING-FX504GM-FX80GM $ ./query-dnnf
load tmp.ddnnf
I will parse a graph of 3979 variables and 7634840 nodes...
Parsed 2 million nodes yet...
Parsed 4 million nodes yet...
Parsed 6 million nodes yet...
Done, returning item now...
mc
166683025214157941492941029847354226054685717626431828808944885126688881800181907881840889944866816

[elonca]

Got a bug for a small instance, maybe related to the issue.
In the following example, the root And node is not decomposable :

lonca@pc-lens-141-245:~/Téléchargements/tmp$ cat DDNNF-124.cnf 
p cnf 3 3
1 -1 0
-2 -3 0
3 -2 0

lonca@pc-lens-141-245:~/Téléchargements/tmp$ ./d4 DDNNF-124.cnf -out=/dev/stdout
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: 2
c Number of literals: 4
c Parse time: 0.00
c
c d-DNNF Information
c Number of nodes: 1
c Number of edges: 2
c 
c Final time: 0.001846
c 
s 4
nnf 8 2 3
O 0 0
A 0
L -2
A 2 2 1
A 1 0
O 2 2 4 3
L -2
A 2 6 5

[jm62300]

It is strange ... actually I changed the output format.
I compiled and test, and I got:
o 1 1 0
o 2 0
t 3 0
f 4 0
2 3 -2 0
2 4 2 0
1 2 0

[jm62300]

I am a bit busy, but I will add a description of the format soon.

[jm62300]

Here is an example:
o 2 0
f 3 0
o 4 0
t 5 0
o 6 0
6 5 -5 -3 0
6 5 5 3 0
4 5 -4 -1 3 5 0
4 6 4 1 0
2 3 -2 0
2 4 2 0
1 2 6 0

The format is more suited for decision-DNNF.
We have different kind of nodes with some information:

• o, for a decision node
• f, for a false leaf
• t, for a true leaf
• a, for an and node (not present in this example)
  The second argument just after the type of node is the index.
  To sum up, in our example we have 3 or nodes (2, 4 and 6), 1 false (3) node and 1 true node (5).

Then, we have edges that link all these nodes together.
Each edge also gives the unit literals between the two nodes (a decision node at least contains a literal).
For example, 2 3 -2 0 means the node or with the index 2 is linked to the false node because we branch with the literal -2.

We have a special index 1 which represents the root.
1 (6) ------- 2 (-2) --------- F
|(2)
---------- 4 (-4 -1 3 5) -------- T (5)
| (4 1)
------------------ 6 (-5 -3) ------- T (5)
| (5 3)
T (5)

[symphorien]

In your example, when trying to reason locally on the root node:

1 (6) ------- ...
|(2)
...

do I have the guarantee that the root node is a decision node on 2 and 6 which means that the bottom branch entails 2 and -6, and that the right branch entails 6 and -2 ?

[symphorien]

Also what does it mean when an or node has 2 non zero associated integers ?

o 1 1 0

[jm62300]

o is actually about deterministic or node.
When we have: o 1 1 0 it is because the other branch is false and then we simplified the formula by only considering one branch.
Tomorrow I will update the README with a formal definition of the output format.

[jdusart]

My problem is solved with the last version of d4.
Thanks

[symphorien]

When we have: o 1 1 0 it is because the other branch is false and then we simplified the formula by only considering one branch.

I don't really understand...

[jm62300]

Yesterday I update the README in order to describe the format.
Please have a look.

[symphorien]

Yes I saw that but it does not explain the semantics of o followed by several non zero integers: all mentions of nodes are:

When a line represents a node it starts with a node type and is followed by its index.
The second argument just after the type of node is its index.

which only explains cases where the node type is followed by a single non zero integer.

[jm62300]

Actually I fixed that, and now you only have the index.
Initially the second value was the number of branches, but this value is irrelevant then I removed it and update the source code accordingly.

/!\ The readme is in progress and the description for the certified part is in construction.

[symphorien]

oh ok

[symphorien]

with current master 021fad8
and cnf file:

p cnf 6 3
-2 -1 0
5 4 0
6 4 0

I still get o 1 1 0:

o 1 1 0
a 2 2 0
o 3 0
t 4 0
3 4 -1 0
3 4 1 -2 0
2 3 0
o 5 0
5 4 -4 5 6 0
5 4 4 0
2 5 0
1 2 0

[jm62300]

Strange, I will have a look. Maybe I missed something when I modified the source code.

[jm62300]

I fixed the problem, it comes from the Root node.
I also removed the number of children for the And nodes.
I did not do it for the certified version, actually I still need time for finishing the README about this part and add the certifier.

[symphorien]

Awesome, thanks!
My only remaining question is #1 (comment) .

[jm62300]

Actually the root node is generally not a decision node.
It is here to store the unit literals.

[symphorien]

Well if there is a unit literal it's a decision between False and whatever goes next, right ?

[symphorien]

Oh that's exactly what the example is... I see your point now.
But does this mean that for all non-root or nodes there will always be a variable n such that one outgoing edge is labelled with n and one other with -n ?