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)