Wrong dDNNF output with projection

[symphorien]

With this cnf formula:

p cnf 9 2
6 0
4 9 0

and projection on variable 1, d4 outputs a dDNNF equivalent to just the variable 6:

$  d4 -fpv=<(echo 1) -dDNNF -out=/dev/stdout bug.cnf 
c Benchmark Information
c Number of variables: 9
c Number of clauses: 2
c Number of literals: 3
c We are collected the projected variables ... 1  ... done
c Preproc options: 
c Integer mode 
c
c Option list 
c Caching: 1
c Reduce cache procedure level: 20
c Strategy for Reducing the cache: 0
c Cache representation: CL
c Part of the formula that is cached: NT
c Variable heuristic: VSADS
c Phase heuristic: TRUE
c Partitioning heuristic: CB + graph reduction + equivalence simplication
c
c ----------------------------------------------------------------------------------------------------------------------------------------------------------
c   #compile |       time |    #posHit |    #negHit |     #split |    Mem(MB) |     #nodes |     #edges | #equivCall | #Dec. Node | #paritioner |  limit dyn | 
c ----------------------------------------------------------------------------------------------------------------------------------------------------------
c ----------------------------------------------------------------------------------------------------------------------------------------------------------
c
c Statistics 
c Compilation Information
c Number of compiled node: 1
c Number of split formula: 0
c Number of decision node: 0
c Number of node built on domain constraints: 0
c Number of decomposable AND nodes: 0
c Number of backbone calls: 0
c Number of partitioner calls: 0
c Average number of assigned literal to obtain decomposable AND nodes: 9.00/9
c Minimum number of assigned variable where a decomposable AND appeared: 9
c 
c Graph Information
c Number of nodes: 0
c Number of edges: 0
c 
c Cache Information
c Memory used: 548 MB
c
c Number of positive hit: 0
c Number of negative hit: 1
c Number of reduceCall: 0
c
c Final time: 0.000114
c 
c unitLits 1048577 4194308 Bytes
c freeVariables 1048577
o 1 0
t 2 0
1 2 6 0
s 2

reproduced on revision f4281153c42d36089feb7d052a309100b2989eed

[symphorien]

It can even be reproduced by setting -fpv but with no priority variables: on

p cnf 3 2
1 0
2 3 0

with -fpv the result is wrong:

d4 -fpv=<(echo) -dDNNF -out=/dev/stdout /tmp/.tmpZb7ML3

but without it is correct

d4 -dDNNF -out=/dev/stdout /tmp/.tmpZb7ML3

[symphorien]

cc @jm62300 so that you receive an email (asked in https://github.com/crillab/d4/issues/2#issuecomment-793962952)

[jm62300]

Actually for projection you cannot use decomposition heuristic. Please test with the option -pv=NO.

[symphorien]

Same behavior with -pv=NO.

Actually I think the problem is that non-projected variables are never decided, and I get better results with

diff --git a/interfaces/VariableHeuristicInterface.cc b/interfaces/VariableHeuristicInterface.cc
index 3966f6b..5092512 100644
--- a/interfaces/VariableHeuristicInterface.cc
+++ b/interfaces/VariableHeuristicInterface.cc
@@ -76,12 +76,12 @@ Var VariableHeuristicInterface::selectVariable(vec<Var> &component)
   for(int i = 0 ; i<component.size() ; i++) 
     {      
       Var v = component[i];      
-      if(s.value(v) != l_Undef || !varProjected[v]) continue;
+      if(s.value(v) != l_Undef /*|| !varProjected[v]*/) continue;

       double score = sm->computeScore(v);    
       if(next == var_Undef || score > maxScore){next = v; maxScore = score;}
     }

-  assert(next == var_Undef || varProjected[next]);
+  /* assert(next == var_Undef || varProjected[next]); */
   return next;
 }// selectVariable

but then sometimes I get decisions on non-projected variables while some projection variables are not yet set, for example in

p cnf 2 1
1 2 0

(project on 2)

[jm62300]

Strange, can you give me the file you pass as parameter for the projected variables.

[symphorien]

I use shell substitution, as described above:

d4 -fpv=<(echo 2) -dDNNF -pv=NO -out=/dev/stdout thefile.cnf

[jm62300]

I just tested and I got : o 1 0 o 2 0 t 3 0 2 3 -2 1 0 2 3 2 0 1 2 0 s 2

The number of models is correct. About the dDNNF it looks OK since we want to compute the number of models projected on {2}.

v	v ---- 2 ---- T

-2 | T

Which is equivalent to: v ---- 2 ---- T	-2

T

because the root does not contain literals.

[symphorien]

did you apply the patch that I posted?

[symphorien]

Ah, maybe it's a misunderstanding:

About the dDNNF it looks OK since we want to compute the number of models projected on {2}

I thought d4 would output a dDNNF that is equivalent to the original formula, but with decisions on projected variables "above". Do you mean that it is not the case?

[jm62300]

Nope it is not the case, basic projected model counter apply a two phases process that first branch on projected variables and then only asks for satisfiability on the other variables.

I you want to first branch on a set of variables and then consider the other at the end you can simply modify the branching heuristic to do the job. If you need help I can do it.

[symphorien]

Thanks. I hacked something together that seems to work. Are you interested in having this functionality upstream? (not right now because it needs clean up and I'm not fluent in c++)