Only record implied literals of the current component

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);

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<CDecision>
     vector<LiteralIdT> allImpliedLits;
 
     vector<CComponentId *> 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<unsigned int> varCompStamp;
+    unsigned int stampCounter;
+
     void reactivateTOS();
 
     // store each cacheEntry where the children of top().refComp are stored
@@ -159,6 +172,27 @@ class CDecisionStack : vector<CDecision>
     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<VarIdT>::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() {}

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<AntAndLit> &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<AntAndLit> &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<AntAndLit> &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<AntAndLit> &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<AntAndLit> &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();
 				}

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)