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 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.