Wrong nnf file produced with right model count on formulas

symphorien commented 3 years ago

I think there are situations where dsharp outputs the correct model count but an incorrect nnf. A possible trigger is a large number of useless variables, in the sense that they don't appear in the formula at all.

Reproducer: formula.cnf:

p cnf 400 25
23 -34 -287 0
-23 -288  0
 292 287  -298 0
-292 -298 0
24 288 0
-24 -299 0
303 298  306 0
-306 -309 0
-303 -309 0
299 -310   0
309  8 0
310 -321 0
-321 325 8 0
325 331 0
321 -332 0
331 339 342 0
-339 342 0
332 -343 0
48 -34 0
 343 29  354 0
-29 355 0
-354 355 357 0
34 -357   399 0
3 399 0
399  400 0

Steps to reproduce:

dsharp -Fnnf formula.nnf formula.cnf

outputs

#SAT (full):        1003423649010231476228717449425288172853483301587463560042403927001189267086150888397612820568126355100717618571509760

and c2d agrees:

c2d -count -in formula.cnf
[...]
Counting...[1003423649010231476228717449425288172853483301587463560042403927001189267086150888397612820568126355100717618571509760] models / 0.000s

However, the model count of the corresponding nnf is not the same. For the bug report I use query-dnnf from https://www.cril.univ-artois.fr/kc/d-DNNF-reasoner.html, but I confirmed this with my own tool computing the model count from the nnf.

query-dnnf <<EOF
load formula.nnf
mc
EOF
> I will parse a graph of 400 variables and 175 nodes...
Done, returning item now...
> 1007463893786228957007320280685556805128418235790001520882379093805335556916236051595072291229027640395917516949422080
> %

but the file returned by c2d has the right model count:

query-dnnf <<EOF
load formula.cnf.nnf
mc
EOF
> I will parse a graph of 400 variables and 143 nodes...
Done, returning item now...
> 1003423649010231476228717449425288172853483301587463560042403927001189267086150888397612820568126355100717618571509760
> %

The bug is actually due to the fact that the file has 400 variables but 372 of them are just useless. If I replace the variables in the cnf by consecutive ones (1, 2, 3...) I get the right count: script to do this: reduce_cnf.py

#!/usr/bin/env python3

import sys

vars = {}
nvars = 0
lines = 0
with open(sys.argv[1]) as f:
    next(f)
    for line in f:
        if not line:
            continue
        lines += 1
        for word in line.strip().split(" "):
            if not word:
                continue
            lit = int(word)
            if lit == 0:
                print(lit)
            else:
                var = abs(lit)
                if var not in vars:
                    nvars += 1
                    vars[var] = nvars
                print(lit//var*vars[var], end=" ")

print(f"p cnf {nvars} {lines}")

./reduce_cnf.py formula.cnf | tac > reduced.cnf
dsharp reduced.cnf
#SAT (full):        104310

and this is the right count because log2(1003423649010231476228717449425288172853483301587463560042403927001189267086150888397612820568126355100717618571509760 / 104310) = 372 However if I do the same transformation to the nnf, I get a different result: script reduce_dnnf.py

#!/usr/bin/env python3

import sys

vars = {}
nvars = 0
lines = 0
with open(sys.argv[1]) as f:
    for line in f:
        if line.startswith("L"):
            var = abs(int(line.strip().split(" ")[1]))
            if var not in vars:
                nvars += 1
                vars[var] = nvars

with open(sys.argv[1]) as f:
    for line in f:
        if line.startswith("nnf"):
            _, v, e, _ = line.strip(" ").split(" ")
            print(f"nnf {v} {e} {nvars}")
        elif line.startswith("L"):
            lit = int(line.strip().split(" ")[1])
            var = abs(lit)
            new_lit = lit//var*vars[var]
            print(f"L {new_lit}")
        elif line.startswith("O"):
            _, opposing, rest = line.strip().split(" ", 2)
            print(f"O {vars[int(opposing)]} {rest}")
        else:
            print(line.strip())

./reduce_dnnf.py formula.nnf > reduced.nnf
query-dnnf <<EOF
load reduced.nnf
mc
EOF
> I will parse a graph of 28 variables and 175 nodes...
Done, returning item now...
> 104730
> %

which is wrong. This also support the hypothesis that the model count originally printed by dsharp is correct, but not the nnf produced.

I tried to reduce this example as much as possible (with creduce) but now I think I investigated all I could think of. I can't use the validations scripts in src/extra because they use kr which is a python module I could not find.

haz commented 3 years ago

Ya, the krtoolkit's been largely deprecated.

Typically, when you generate, you just want to work with the aspects of the theory that make sense. If you want direct counts on the original theory vocabulary, then you need to be careful about how you count. This means accounting for variables that don't appear in the d-DNNF or making sure that all variables appear.

Can you try with the -smoothNNF option included? This should hopefully include that extra context.

symphorien commented 3 years ago

Even with -smoothNNF dsharp returns a nnf with 1007463893786228957007320280685556805128418235790001520882379093805335556916236051595072291229027640395917516949422080 models while it prints 1003423649010231476228717449425288172853483301587463560042403927001189267086150888397612820568126355100717618571509760 models.

I know that if I have n extra variables I must take into account a factor or 2^n, the bug I report here is different. The reproducer, with 372 extra variables, makes dsharp output a nnf with 104730*2^372 instead of 104310*2^372.

The extra variables come from bitblasting, and removing them would incur yet another layer of variable translation I'd like not to have to write...

haz commented 3 years ago

Hrmz...I very much suspect the variable ordering (gaps in the CNF) being the culprit. Two quick followups:

Can you confirm if your original reduce works/doesn't on the generated nnf count? I.e., the one independently verified (and not just what dsharp reports).
Can you tack on trivial clauses for all 400 variables and see if it comes out fine? I.e., something like...
```
for i in range(1,401):
print(f'{i} -{i} 0')
```

I've tried putting things through the d4 reasoner, but am getting unsat for the generated nnf (not sure what's going on there with that software).

symphorien commented 3 years ago

the original example huge.zip exhibits the same symptoms: it has all variables from 1 to 48188 and then only 143266. dsharp reports modelcount 4461995750531416167540069333363359924424694844431198083614111931159519762806178444657066927051203674112 but query-ddnnf reports 229444603521703015523348419735591225287785768516636831980854151762282508413039418176192678584186287876044585538449466338760687935865724455832173718382393266989432832

adding all variables in useless clauses as you suggest does not remove the bug. I can reproduce with

p cnf 400 425
23 -34 -287 0
-23 -288  0
292 287  -298 0
-292 -298 0
24 288 0
-24 -299 0
303 298  306 0
-306 -309 0
-303 -309 0
299 -310   0
309  8 0
310 -321 0
-321 325 8 0
325 331 0
321 -332 0
331 339 342 0
-339 342 0
332 -343 0
48 -34 0
343 29  354 0
-29 355 0
-354 355 357 0
34 -357   399 0
3 399 0
399  400 0
1 -1 0
2 -2 0
3 -3 0
4 -4 0
5 -5 0
6 -6 0
7 -7 0
8 -8 0
9 -9 0
10 -10 0
11 -11 0
12 -12 0
13 -13 0
14 -14 0
15 -15 0
16 -16 0
17 -17 0
18 -18 0
19 -19 0
20 -20 0
21 -21 0
22 -22 0
23 -23 0
24 -24 0
25 -25 0
26 -26 0
27 -27 0
28 -28 0
29 -29 0
30 -30 0
31 -31 0
32 -32 0
33 -33 0
34 -34 0
35 -35 0
36 -36 0
37 -37 0
38 -38 0
39 -39 0
40 -40 0
41 -41 0
42 -42 0
43 -43 0
44 -44 0
45 -45 0
46 -46 0
47 -47 0
48 -48 0
49 -49 0
50 -50 0
51 -51 0
52 -52 0
53 -53 0
54 -54 0
55 -55 0
56 -56 0
57 -57 0
58 -58 0
59 -59 0
60 -60 0
61 -61 0
62 -62 0
63 -63 0
64 -64 0
65 -65 0
66 -66 0
67 -67 0
68 -68 0
69 -69 0
70 -70 0
71 -71 0
72 -72 0
73 -73 0
74 -74 0
75 -75 0
76 -76 0
77 -77 0
78 -78 0
79 -79 0
80 -80 0
81 -81 0
82 -82 0
83 -83 0
84 -84 0
85 -85 0
86 -86 0
87 -87 0
88 -88 0
89 -89 0
90 -90 0
91 -91 0
92 -92 0
93 -93 0
94 -94 0
95 -95 0
96 -96 0
97 -97 0
98 -98 0
99 -99 0
100 -100 0
101 -101 0
102 -102 0
103 -103 0
104 -104 0
105 -105 0
106 -106 0
107 -107 0
108 -108 0
109 -109 0
110 -110 0
111 -111 0
112 -112 0
113 -113 0
114 -114 0
115 -115 0
116 -116 0
117 -117 0
118 -118 0
119 -119 0
120 -120 0
121 -121 0
122 -122 0
123 -123 0
124 -124 0
125 -125 0
126 -126 0
127 -127 0
128 -128 0
129 -129 0
130 -130 0
131 -131 0
132 -132 0
133 -133 0
134 -134 0
135 -135 0
136 -136 0
137 -137 0
138 -138 0
139 -139 0
140 -140 0
141 -141 0
142 -142 0
143 -143 0
144 -144 0
145 -145 0
146 -146 0
147 -147 0
148 -148 0
149 -149 0
150 -150 0
151 -151 0
152 -152 0
153 -153 0
154 -154 0
155 -155 0
156 -156 0
157 -157 0
158 -158 0
159 -159 0
160 -160 0
161 -161 0
162 -162 0
163 -163 0
164 -164 0
165 -165 0
166 -166 0
167 -167 0
168 -168 0
169 -169 0
170 -170 0
171 -171 0
172 -172 0
173 -173 0
174 -174 0
175 -175 0
176 -176 0
177 -177 0
178 -178 0
179 -179 0
180 -180 0
181 -181 0
182 -182 0
183 -183 0
184 -184 0
185 -185 0
186 -186 0
187 -187 0
188 -188 0
189 -189 0
190 -190 0
191 -191 0
192 -192 0
193 -193 0
194 -194 0
195 -195 0
196 -196 0
197 -197 0
198 -198 0
199 -199 0
200 -200 0
201 -201 0
202 -202 0
203 -203 0
204 -204 0
205 -205 0
206 -206 0
207 -207 0
208 -208 0
209 -209 0
210 -210 0
211 -211 0
212 -212 0
213 -213 0
214 -214 0
215 -215 0
216 -216 0
217 -217 0
218 -218 0
219 -219 0
220 -220 0
221 -221 0
222 -222 0
223 -223 0
224 -224 0
225 -225 0
226 -226 0
227 -227 0
228 -228 0
229 -229 0
230 -230 0
231 -231 0
232 -232 0
233 -233 0
234 -234 0
235 -235 0
236 -236 0
237 -237 0
238 -238 0
239 -239 0
240 -240 0
241 -241 0
242 -242 0
243 -243 0
244 -244 0
245 -245 0
246 -246 0
247 -247 0
248 -248 0
249 -249 0
250 -250 0
251 -251 0
252 -252 0
253 -253 0
254 -254 0
255 -255 0
256 -256 0
257 -257 0
258 -258 0
259 -259 0
260 -260 0
261 -261 0
262 -262 0
263 -263 0
264 -264 0
265 -265 0
266 -266 0
267 -267 0
268 -268 0
269 -269 0
270 -270 0
271 -271 0
272 -272 0
273 -273 0
274 -274 0
275 -275 0
276 -276 0
277 -277 0
278 -278 0
279 -279 0
280 -280 0
281 -281 0
282 -282 0
283 -283 0
284 -284 0
285 -285 0
286 -286 0
287 -287 0
288 -288 0
289 -289 0
290 -290 0
291 -291 0
292 -292 0
293 -293 0
294 -294 0
295 -295 0
296 -296 0
297 -297 0
298 -298 0
299 -299 0
300 -300 0
301 -301 0
302 -302 0
303 -303 0
304 -304 0
305 -305 0
306 -306 0
307 -307 0
308 -308 0
309 -309 0
310 -310 0
311 -311 0
312 -312 0
313 -313 0
314 -314 0
315 -315 0
316 -316 0
317 -317 0
318 -318 0
319 -319 0
320 -320 0
321 -321 0
322 -322 0
323 -323 0
324 -324 0
325 -325 0
326 -326 0
327 -327 0
328 -328 0
329 -329 0
330 -330 0
331 -331 0
332 -332 0
333 -333 0
334 -334 0
335 -335 0
336 -336 0
337 -337 0
338 -338 0
339 -339 0
340 -340 0
341 -341 0
342 -342 0
343 -343 0
344 -344 0
345 -345 0
346 -346 0
347 -347 0
348 -348 0
349 -349 0
350 -350 0
351 -351 0
352 -352 0
353 -353 0
354 -354 0
355 -355 0
356 -356 0
357 -357 0
358 -358 0
359 -359 0
360 -360 0
361 -361 0
362 -362 0
363 -363 0
364 -364 0
365 -365 0
366 -366 0
367 -367 0
368 -368 0
369 -369 0
370 -370 0
371 -371 0
372 -372 0
373 -373 0
374 -374 0
375 -375 0
376 -376 0
377 -377 0
378 -378 0
379 -379 0
380 -380 0
381 -381 0
382 -382 0
383 -383 0
384 -384 0
385 -385 0
386 -386 0
387 -387 0
388 -388 0
389 -389 0
390 -390 0
391 -391 0
392 -392 0
393 -393 0
394 -394 0
395 -395 0
396 -396 0
397 -397 0
398 -398 0
399 -399 0
400 -400 0

symphorien commented 3 years ago

Ok I can reproduce this bug without useless variables, it is only a question of the order of clauses: reproducer:

p cnf 28 25
1 -2 -3 0
-1 -4 0
5 3 -6 0
-5 -6 0
7 4 0
-7 -8 0
9 6 10 0
-10 -11 0
-9 -11 0
8 -12 0
11 13 0
12 -14 0
-14 15 13 0
15 16 0
14 -17 0
16 18 19 0
-18 19 0
17 -20 0
21 -2 0
20 22 23 0
-22 24 0
-23 24 25 0
2 -25 26 0
27 26 0
26 28 0

If I reverse the order of clauses, then the symptoms disappear.

haz commented 3 years ago

I fear this issue is pretty deep. Banged my head against it for a while, and the best I could narrow down is that it involves conflict analysis, and most likely the pollutants infrastructure (something set up by sharpSAT in order to cache things quicker).

As a temporary solution, using the --noCA option would resolve the issue.

symphorien commented 3 years ago

Thanks for invistigating this bug!

I just tried --noCA on the reproducer of https://github.com/QuMuLab/dsharp/issues/12#issuecomment-853124845 but it does not circumvent the problem:

$  dsharp --noCA -Fnnf repro.nnf repro.cnf
#SAT (full):        104310
$  query-dnnf <<EOF                       
load repro.nnf
mc
EOF
> I will parse a graph of 28 variables and 175 nodes...
Done, returning item now...
> 104730
> %

VincentDerk commented 2 months ago

I realise this is an old issue but this might relate to an issue that I am observing. Since my CNF is a lot larger, I took a look at #12 (comment), hoping it will solve my issue too.

So far I found the following when running dsharp without any extra flags, just the nnf and cnf paths.

The produced nnf is not actually a d-DNNF. I discovered the logical formula of the nnf is semantically equivalent to the CNF. The model count of the nnf is reported erroneously to be 104730 because query-dnnf computes the model count assuming it is a ddnnf, which it is not.
There is one AND node in the nnf that is violating the decomposability property, having two children sharing variable 13.
```
The AND node on nnf line 168 has children 1, 164, 167, who have the following variable scopes:
    1:{6}
    164:{9, 10, 11, 13}
    167:{1, 3, 4, 7, 8, 12, 13, 14, 17, 20, 22, 23, 24, 25}
```
Observe that variable 13 is used in both, violating decomposability. Manually checking the CNF, 13 should not be present in 167. By conditioning on 2, -16, -6, we infer 15 which removes the clause connecting 13 to 14 and 15.

During compilation, the AND node on line 168 corresponds to getID() == 271, which might help with using breakpoints to figure out why down the line variable 13 ends up in 167. Furthermore, I believe 167 corresponds to getID()==279, and 164 corresponds to getID==274.

That is as far as I got right now. I might revisit this later, but I could use some pointers as to where in the codebase we best proceed debugging.

QuMuLab / dsharp

Wrong nnf file produced with right model count on formulas #12