Only record implied literals of the current component

[rmanhaeve]

DSHARP can emit a .nnf that is not decomposable: an AND node whose children share a variable. The formula stays logically equivalent to the input, so the search's own count is right — but decomposability is the contract of the output format, so every model counter reading the .nnf returns a wrong number, silently. Found via ML-KULeuven/problog#113, where ProbLog reported a probability of 156.13 for a model whose answer is 0.6.

Reproducer

20 variables, 26 clauses, reduced from the ProbLog instance:

p cnf 20 26
-5 -1 0
-3 4 0
-6 -3 0
-7 3 0
-9 8 0
-10 5 7 9 0
11 -2 -10 0
-11 10 0
14 -13 -3 0
-14 13 0
-14 3 0
-15 -1 14 0
8 -9 -3 0
-8 3 0
4 2 0
1 11 12 -4 0
-13 -10 0
-16 10 0
-17 -2 0
-17 15 0
-18 16 17 0
18 -16 0
-12 -18 0
-19 18 0
-12 -1 0
20 18 0

$ dsharp -Fnnf out.nnf repro.cnf | grep 'of solutions'
# of solutions:         798
$ python3 check_ddnnf.py out.nnf
non-decomposable AND at .nnf line 93
non-decomposable AND nodes: 1
models of the .nnf         : 854

798 is correct — an independent BDD over the CNF agrees. With this PR both numbers are 798 and no node is non-decomposable.

check_ddnnf.py — self-contained, no dependencies

import sys
nodes = []
with open(sys.argv[1]) as f:
    nvars = int(f.readline().split()[3])
    for line in f:
        p = line.split()
        if p[0] == 'L':   nodes.append(('L', int(p[1])))
        elif p[0] == 'A': nodes.append(('A', [int(x) for x in p[2:]]))
        elif p[0] == 'O': nodes.append(('O', [int(x) for x in p[3:]]))
varset, count, bad = [0]*len(nodes), [0]*len(nodes), 0
for i, nd in enumerate(nodes):
    if nd[0] == 'L':
        varset[i], count[i] = 1 << abs(nd[1]), 1
    elif nd[0] == 'A':                       # decomposable => children disjoint
        s, c = 0, 1
        for j in nd[1]:
            if varset[j] & s:
                bad += 1
                print('non-decomposable AND at .nnf line %d' % (i + 2))
            s |= varset[j]; c *= count[j]
        varset[i], count[i] = s, c
    else:                                    # smooth the OR on the fly
        s = 0
        for j in nd[1]: s |= varset[j]
        varset[i] = s
        count[i] = sum(count[j] << bin(s & ~varset[j]).count('1') for j in nd[1])
print('non-decomposable AND nodes: %d' % bad)
print('models of the .nnf         : %d' % (count[-1] << (nvars - bin(varset[-1]).count('1'))))

Cause

CMainSolver::BCP records every implied literal under the current decision level's AND node. That is only correct for literals of the component that level refines, and two things get past it.

Conflict clauses are excluded from the component decomposition, and that exclusion is exactly what lets them cross a component boundary: two unassigned variables sharing an unsatisfied original clause are in the same component by construction, so only a learned clause can take the first step across. Ordinary propagation then continues inside the sibling, and is recorded here too.

Both stages are visible in the reproducer. At level 3 the component being refined is {16,18,19,20} and a sibling is {3,4,5,6,7,8,11}. The learned clause (-18 ∨ 1 ∨ -2 ∨ 3) has -18 falsified at level 3, 1 and -2 falsified at level 1, and 3 free — so it implies 3, which belongs to the sibling. Then the original clauses (-3 ∨ 4) and (-6 ∨ -3) propagate 4 and -6. All three land as literal children of one AND node, beside an OR node covering {3,4,6,16,18,19,20}.

Instrumented to report every literal recorded outside the current component, and excluding implicit BCP's tentative rounds (whose recordings are detached again), every surviving crossing is initiated by a conflict clause: 2 of 2 rounds on a 53-variable reduction, 26 of 26 on the ProbLog instance. No original clause ever initiates one.

This is also the one step the paper states without proof — "the addition of conflict clauses during the solving procedure does not change the structure of the d-DNNF". True of the represented function; not of decomposability.

Why membership in the component is the right test

Let R be the component the level refines; the residual original formula splits as psi_A ∧ psi_B over disjoint variable sets.

Out-of-component literals can be dropped. If BCP implies l with var(l) ∉ R, the residual entails l, since every clause DSHARP propagates with is entailed by the input. If var(l) occurs in no unsatisfied original clause, the residual is invariant under flipping it, so it must be unsatisfiable and the branch compiles to ⊥ regardless. Otherwise var(l) lies in a sibling psi_B: fix any model of psi_A, and disjointness gives psi_B ⊨ l, so that component's own node already forces it.

In-component ones cannot. If var(l) ∈ R it is assigned, so it appears in no sub-component of R; nothing else records it and smoothing would hand it a free choice.

So the criterion is membership, not provenance — a conflict clause implying a literal over R's own variables must still be recorded. That rules out the obvious one-liner, measurably: skipping conflict-clause implications gives a wrong count on 9 of 65 instances, against 5 unpatched and 0 here, always overcounting. -noCA is sound but still running after 300 s where this takes 0.53 s. Putting conflict clauses into the decomposition would collapse the decomposition. Post-hoc DAG repair is not a local edit — 256 of 261 offending children are shared, some with 349 parents.

The change

+64/−8 in four files. CDecisionStack stamps the variables of the component the top level refines, on push, on the pop that exposes a level, and once after makeCompIdFromActGraph. varInTOSRefComp is then an O(1) comparison, permissive while no component information exists so preprocessing is unchanged. mayRecordImpliedLit guards the five recording sites in BCP and the one in implicitBCP.

The search is untouched: the guard decides only what is recorded, never what is assigned, so solution counts, heuristics, conflict analysis and the component cache are unchanged. 0.531 s against 0.534 s, and 234150 edges against 234169.

Validation

• 110 CNFs with ProbLog's own flags -smoothNNF -disableAllLits: 6 wrong unpatched, 0 patched, and no solution count changed anywhere.
• The reported instance now counts 39708868943559345451429439397652844050730171778133720697929728, matching c2d, D4 and DSHARP's own search count; 75 non-decomposable nodes become 0, and ProbLog answers 0.6.
• Equivalence checked against the CNF with a BDD for every instance under 90 variables — patched and unpatched, which is why this is invisible without a decomposability or counting check.
• ProbLog's test suite passes unchanged; exp-testing/ counts and run times unchanged, two fewer edges.

Worth noting the failure is not always out of range: sweeping the ProbLog model from 1 to 45 steps, unpatched DSHARP is wrong at 21 steps (502.16) and at 23 steps (0.95024115) — a plausible-looking probability that no sanity check catches.

Disclosure

Investigated and prepared with Claude Code (Claude Opus 5), working from ML-KULeuven/problog#113. The tracing, the reduction, the patch and the validation harness are AI-assisted work, done under my direction. Please weigh the argument rather than my word for it: the reproducer and checker above need nothing from me but the CNF, and the soundness argument is short enough to check by hand.

Fixes the compiler side of ML-KULeuven/problog#113. Happy to send a -verify flag separately — smoothing the emitted .nnf and comparing its count against the search count is one linear pass, and would have caught this immediately.