From 8a7ffbebf9d57691a6f434cf984bf27b9c7e51c8 Mon Sep 17 00:00:00 2001 From: Robin Manhaeve Date: Tue, 8 Sep 2026 08:38:23 +0200 Subject: [PATCH] Only record implied literals of the current component The compiled d-DNNF could be non-decomposable: some AND nodes had children whose variable sets overlap. The written formula stays logically equivalent to the input CNF, so the search's own model count is unaffected, but any consumer that relies on decomposability -- i.e. any (weighted) model counter reading the .nnf -- silently returns a wrong result. ProbLog reported a probability of 156.13 for a model whose answer is 0.6 (ML-KULeuven/problog#113). Cause: BCP records every implied literal as a child of the current decision level's AND node. Conflict clauses are deliberately left out of the component decomposition, which makes them the only clauses whose unit propagation can take the first step across a component boundary (two unassigned variables sharing an unsatisfied original clause are in the same component by construction). Once a sibling component's variable has been assigned that way, ordinary propagation continues inside the sibling and everything it implies is recorded in this branch as well. An implied literal is now only recorded when its variable belongs to the component the current decision level is refining. Out-of-component implied literals may be dropped: the components are variable-disjoint, so such a literal is entailed by the sibling component on its own and that component records it; if the current branch is unsatisfiable it compiles to bottom regardless. Literals implied by a conflict clause over the current component's own variables are still recorded, since nothing else constrains them -- skipping those instead loses information and overcounts. Membership is tested with a stamp per decision level, marked when the level is pushed or exposed by a pop, so the test is O(1) and the added marking is proportional to work the component analysis already does. The search itself is untouched: the guard only decides what is recorded, never what is assigned, so solution counts, heuristics, learning and the component cache are unchanged. On a 20 variable, 26 clause reduction of the reported instance dsharp reports 798 solutions while its own .nnf has 854 models; with this change both are 798. On the reported instance the .nnf now counts 39708868943559345451429439397652844050730171778133720697929728 models, matching c2d and D4. Across 109 CNFs run with ProbLog's flags (-smoothNNF -disableAllLits) no output is non-decomposable any more, every .nnf model count agrees with the search count, and run time and representation size are unchanged. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01WwfmE52z7BJmmaewvNzaVY --- src/src_sharpSAT/MainSolver/DecisionStack.cpp | 7 ++++ src/src_sharpSAT/MainSolver/DecisionStack.h | 38 ++++++++++++++++++- src/src_sharpSAT/MainSolver/MainSolver.cpp | 14 ++++--- src/src_sharpSAT/MainSolver/MainSolver.h | 13 +++++++ 4 files changed, 64 insertions(+), 8 deletions(-) diff --git a/src/src_sharpSAT/MainSolver/DecisionStack.cpp b/src/src_sharpSAT/MainSolver/DecisionStack.cpp index 4418399..53c7701 100755 --- a/src/src_sharpSAT/MainSolver/DecisionStack.cpp +++ b/src/src_sharpSAT/MainSolver/DecisionStack.cpp @@ -58,6 +58,7 @@ bool CDecisionStack::pop() (end()-2)->includeSol(top().getOverallSols()); pop_back(); + stampTOSRefComp(); return true; } @@ -72,6 +73,8 @@ void CDecisionStack::push(DTNode * other) top().iImpLitOfs = allImpliedLits.size(); top().iRemCompOfs = allComponentsStack.size(); top().iEndRemComps = allComponentsStack.size(); + + stampTOSRefComp(); } @@ -85,6 +88,10 @@ void CDecisionStack::init(unsigned int resSize) allComponentsStack.reserve(theClPool.countAllVars()); allComponentsStack.push_back(new CComponentId()); + varCompStamp.clear(); + varCompStamp.resize(theClPool.countAllVars() + 2, 0); + stampCounter = 0; + // initialize the stack to contain at least level zero DTNode * dummyLeft = new DTNode(DT_NodeType::kDTAnd, 2); DTNode * dummyRight = new DTNode(DT_NodeType::kDTAnd, 1); diff --git a/src/src_sharpSAT/MainSolver/DecisionStack.h b/src/src_sharpSAT/MainSolver/DecisionStack.h index d02b0dd..3f01372 100755 --- a/src/src_sharpSAT/MainSolver/DecisionStack.h +++ b/src/src_sharpSAT/MainSolver/DecisionStack.h @@ -37,6 +37,10 @@ class CDecision // Solutioncount CRealNum rnNumSols[2]; + + /// identifies the stamp that marks the variables of refComp in + /// CDecisionStack::varCompStamp (0 means "not stamped yet") + unsigned int compStamp; //////////////////// /// decision tree node @@ -82,7 +86,8 @@ class CDecision iImpLitOfs = (unsigned int) -1; iRemCompOfs = (unsigned int) -1; iEndRemComps = (unsigned int) -1; - + compStamp = 0; + flipNode = other; } @@ -133,7 +138,15 @@ class CDecisionStack : vector vector allImpliedLits; vector allComponentsStack; - + + /// varCompStamp[v] == top().compStamp <=> v belongs to the component + /// that the current decision level is refining. Used to decide whether an + /// implied literal may be recorded in the decision tree: literals implied + /// through conflict clauses can lie outside that component, and recording + /// them there would break decomposability of the compiled d-DNNF. + vector varCompStamp; + unsigned int stampCounter; + void reactivateTOS(); // store each cacheEntry where the children of top().refComp are stored @@ -159,6 +172,27 @@ class CDecisionStack : vector CDecisionStack(CInstanceGraph &pool):theClPool(pool) { addToDecLev = 0; + stampCounter = 0; + } + + /// (re)mark the variables of the component that the top decision level + /// refines. Has to be called whenever top() changes. + void stampTOSRefComp() + { + CComponentId &rComp = *allComponentsStack[top().refCompId]; + // countVars() is theVars.size()-1 and underflows on an empty component, + // so test empty() -- an empty component has no varsSENTINEL to stop at. + if (rComp.empty()) return; // not initialized yet: allow all + top().compStamp = ++stampCounter; + for (vector::const_iterator it = rComp.varsBegin(); *it != varsSENTINEL; it++) + varCompStamp[*it] = top().compStamp; + } + + /// is theVar part of the component refined by the current decision level? + bool varInTOSRefComp(VarIdT theVar) + { + if (top().compStamp == 0) return true; // no component information (yet) + return varCompStamp[theVar] == top().compStamp; } ~CDecisionStack() {} diff --git a/src/src_sharpSAT/MainSolver/MainSolver.cpp b/src/src_sharpSAT/MainSolver/MainSolver.cpp index dc76df3..00456cb 100755 --- a/src/src_sharpSAT/MainSolver/MainSolver.cpp +++ b/src/src_sharpSAT/MainSolver/MainSolver.cpp @@ -89,6 +89,7 @@ void CMainSolver::solve(const char *lpstrFileName) lastTimeCClDeleted = CStepTime::getTime(); lastCClCleanUp = CStepTime::getTime(); makeCompIdFromActGraph(decStack.TOSRefComp()); + decStack.stampTOSRefComp(); bcpImplQueue.clear(); bcpImplQueue.reserve(countAllVars()); @@ -847,7 +848,7 @@ bool CMainSolver::BCP(vector &thePairsOfImpl) decStack.TOS_addImpliedLit(satLit); #ifdef FULL_DDNNF - if (enable_DT_recording) + if (enable_DT_recording && mayRecordImpliedLit(satLit)) { DTNode * satLitDTNode = get_lit_node(satLit.toSignedInt()); satLitDTNode->addParent(decStack.top().getCurrentDTNode(), true); @@ -868,7 +869,7 @@ bool CMainSolver::BCP(vector &thePairsOfImpl) thePairsOfImpl.push_back(AntAndLit(unLit, *bt)); #ifdef FULL_DDNNF - if (enable_DT_recording) + if (enable_DT_recording && mayRecordImpliedLit(*bt)) { DTNode * ccLit = get_lit_node((*bt).toSignedInt()); ccLit->addParent(decStack.top().getCurrentDTNode(), true); @@ -891,7 +892,7 @@ bool CMainSolver::BCP(vector &thePairsOfImpl) { thePairsOfImpl.push_back(AntAndLit(unLit, *bt)); - if (enable_DT_recording) + if (enable_DT_recording && mayRecordImpliedLit(*bt)) { // Add the implied literal due to a conflict clause DTNode * ccLit = get_lit_node((*bt).toSignedInt()); @@ -954,7 +955,7 @@ bool CMainSolver::BCP(vector &thePairsOfImpl) if (pCl->isCC()) { #endif - if (enable_DT_recording) + if (enable_DT_recording && mayRecordImpliedLit(pCl->idLitA())) { DTNode * ccLit = get_lit_node( pCl->idLitA().toSignedInt()); @@ -981,7 +982,7 @@ bool CMainSolver::BCP(vector &thePairsOfImpl) if (pCl->isCC()) { #endif - if (enable_DT_recording) + if (enable_DT_recording && mayRecordImpliedLit(pCl->idLitB())) { DTNode * ccLit = get_lit_node( pCl->idLitB().toSignedInt()); @@ -1177,7 +1178,8 @@ bool CMainSolver::implicitBCP() // Add the successful ibcp lit to the graph DTNode * ibcpLit = get_lit_node( theLit.oppositeLit().toSignedInt()); - ibcpLit->addParent(decStack.top().getCurrentDTNode(), true); + if (mayRecordImpliedLit(theLit.oppositeLit())) + ibcpLit->addParent(decStack.top().getCurrentDTNode(), true); implPairs.clear(); } diff --git a/src/src_sharpSAT/MainSolver/MainSolver.h b/src/src_sharpSAT/MainSolver/MainSolver.h index e62fc2e..a44e5fd 100644 --- a/src/src_sharpSAT/MainSolver/MainSolver.h +++ b/src/src_sharpSAT/MainSolver/MainSolver.h @@ -235,6 +235,19 @@ class CMainSolver: public CInstanceGraph public: + /// An implied literal may only be recorded in the decision tree when its + /// variable belongs to the component that the current decision level is + /// refining. Unit propagation over conflict clauses can imply literals of + /// *sibling* components (conflict clauses are deliberately ignored when the + /// residual formula is decomposed), and recording those here would put the + /// same variable both in this branch and in the sibling's sub-d-DNNF, + /// i.e. make the compiled formula non-decomposable. Such literals are + /// entailed by the sibling component alone, so leaving them out is safe. + bool mayRecordImpliedLit(const LiteralIdT &lit) + { + return decStack.varInTOSRefComp(lit.toVarIdx()); + } + DTNode * get_lit_node(int lit) { if (lit < 0)