Wrong nnf file produced with right model count on formulas#12
Description
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 becauselog2(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.