decStack(*this)

{

stopWatch.setTimeBound(CSolverConf::secsTimeBound);

remPoll = 0;

{

if (!prepBCP())

{

theRunAn.setExitState(SUCCESS);

stopWatch.markStopTime();

return false;

}

if (CSolverConf::allowPreProcessing)

{

toSTDOUT("BEGIN preprocessing" << endl);

if (!prepFindHiddenBackBoneLits())

{

theRunAn.setExitState(SUCCESS);

toSTDOUT("ERR: UNSAT Formula" << endl);

stopWatch.markStopTime();

return false;

}

toSTDOUT(endl << "END preprocessing" << endl);

}

prep_CleanUpPool();

toSTDOUT("#Vars remaining:" << countAllVars() << endl);

toSTDOUT("#Clauses remaining:" << countAllClauses() << endl);

toSTDOUT("#bin Cls remaining:" << countBinClauses() << endl);

return true;

{

SOLVER_StateT exSt;

stopWatch.markStartTime();

num_Nodes = 3;

enable_DT_recording = true;

createfromFile(lpstrFileName);

decStack.init(countAllVars());

CStepTime::makeStart();

xFormulaCache.init();

bdg_var_count = originalVarCount;

// Create the initial LIT nodes for quick caching

for (int i = 0; i <= originalVarCount; ++i)

{

//Original:

litNodes.push_back(new DTNode(i, true, num_Nodes++));

litNodes.push_back(new DTNode(-1 * i, true, num_Nodes++));

}

toSTDOUT("#Vars:" << countAllVars() << endl);

toSTDOUT("#Clauses:" << countAllClauses() << endl);

toSTDOUT("#bin Cls:" << countBinClauses() << endl);

bool needToCount = performPreProcessing();

theRunAn.setRemovedClauses(theRunAn.getData().nRemovedClauses

+ theRunAn.getData().nOriginalClauses - getMaxOriginalClIdx() + 1

- countBinClauses());

if (needToCount)

{

// the following call only correct if bin clauses not used for caching

CCacheEntry::adjustPackSize(countAllVars(), getMaxOriginalClIdx());

lastTimeCClDeleted = CStepTime::getTime();

lastCClCleanUp = CStepTime::getTime();

makeCompIdFromActGraph(decStack.TOSRefComp());

bcpImplQueue.clear();

bcpImplQueue.reserve(countAllVars());

// the size of componentSearchStack has to be reserved, otherwise getComp(...) might

// become erroneous due to realloc

componentSearchStack.reserve(countAllVars() + 2);

exSt = countSAT();

theRunAn.setExitState(exSt);

theRunAn.setSatCount(decStack.top().getOverallSols());

}

else

{

theRunAn.setExitState(SUCCESS);

theRunAn.setSatCount(0.0);

}

stopWatch.markStopTime();

theRunAn.setElapsedTime(stopWatch.getElapsedTime());

xFormulaCache.printStatistics(theRunAn);

// There may have been some translation done during the preprocessing

// phase, so we translate the bdg literals back.

decStack.top().getDTNode()->uncheck(1);

translateLiterals(getVarTranslation());

// We also need to add all of the backbones found in preprocessing, but

// we only do this if there are solutions.

if (decStack.top().getOverallSols() != 0)

{

vector<LiteralIdT>::iterator bbit;

for (bbit = backbones.begin(); bbit != backbones.end(); bbit++)

{

// Check to make sure that the node hasn't been altered

if (bbit->toSignedInt() == get_lit_node(bbit->toSignedInt())->getVal())

decStack.top().getCurrentDTNode()->addChild(get_lit_node(bbit->toSignedInt()), true);

else

decStack.top().getCurrentDTNode()->addChild(get_lit_node_full(bbit->toSignedInt()), true);

}

}

// We compress the tree now that the search is finished

decStack.top().getDTNode()->uncheck(2);

std::cout << "Uncompressed Edges: " << decStack.top().getDTNode()->count(true) << endl;

decStack.top().getDTNode()->uncheck(3);

decStack.top().getDTNode()->compressNode();

decStack.top().getDTNode()->uncheck(4);

bdg_edge_count = decStack.top().getDTNode()->count(true);

std::cout << "Compressed Edges: " << bdg_edge_count << endl;

// There may have been some translation done during the file parsing

// phase, so we translate the bdg literals back.

decStack.top().getDTNode()->uncheck(5);

// We may have litnodes that aren't used yet (but will after smoothing).

// Thus, we need to make sure that all litnodes are unchecked.

for (int i = 0; i < litNodes.size(); i++)

litNodes[i]->uncheck(5);

translateLiterals(getOrigTranslation());

if (CSolverConf::smoothNNF) {

// Smooth the d-DNNF (note: this may cause AND-AND parent-children)

set<int> literals;

decStack.top().getDTNode()->uncheck(6);

decStack.top().getDTNode()->smooth(num_Nodes, *this, literals);

// See if we've got every literal in the d-DNNF

if (2 * originalVarCount == literals.size())

return;

// TODO: Fix an AND node to the top

if (DT_NodeType::kDTAnd != decStack.top().getDTNode()->getType())

toSTDOUT("Error: The top node wasn't an AND node.");

// Make sure that every literal appears some place

DTNode* botNode = new DTNode(DT_NodeType::kDTAnd, num_Nodes++);

botNode->botIfy();

for (int i = 1; i <= originalVarCount; ++i) {

// Check if neither exist

if ((literals.find(i) == literals.end()) &&

(literals.find(-1 * i) == literals.end())) {

// Add an arbitrary choice between the two

DTNode* newOr = new DTNode(DT_NodeType::kDTOr, num_Nodes++);

newOr->choiceVar = (unsigned) i;

decStack.top().getDTNode()->addChild(newOr, true);

newOr->addChild(new DTNode(i, true, num_Nodes++), true);

newOr->addChild(new DTNode((-1 * i), true, num_Nodes++), true);

} else if ((literals.find(i) == literals.end()) && CSolverConf::ensureAllLits) {

DTNode* newOr = new DTNode(DT_NodeType::kDTOr, num_Nodes++);

DTNode* newAnd = new DTNode(DT_NodeType::kDTAnd, num_Nodes++);

get_lit_node_full(-1 * i)->sub_parents(newOr);

newOr->addChild(get_lit_node_full(-1 * i), true);

newOr->addChild(newAnd, true);

newOr->choiceVar = (unsigned) i;

newAnd->addChild(new DTNode(i, true, num_Nodes++), true);

newAnd->addChild(botNode, true);

} else if ((literals.find(-1 * i) == literals.end()) && CSolverConf::ensureAllLits) {

DTNode* newOr = new DTNode(DT_NodeType::kDTOr, num_Nodes++);

DTNode* newAnd = new DTNode(DT_NodeType::kDTAnd, num_Nodes++);

get_lit_node_full(i)->sub_parents(newOr);

newOr->addChild(get_lit_node_full(i), true);

newOr->addChild(newAnd, true);

newOr->choiceVar = (unsigned) i;

newAnd->addChild(new DTNode((-1 * i), true, num_Nodes++), true);

newAnd->addChild(botNode, true);

}

}

}

{

retStateT res;

while (true)

{

while (decide())

{

if (stopWatch.timeBoundBroken())

return TIMEOUT;

while (!bcp())

{

res = resolveConflict();

if (res == EXIT)

return SUCCESS;

if (res == PROCESS_COMPONENT)

break; //force calling decide()

}

}

res = backTrack();

if (res == EXIT)

return SUCCESS;

while (res != PROCESS_COMPONENT && !bcp())

{

res = resolveConflict();

if (res == EXIT)

return SUCCESS;

}

}

const CComponentId & superComp)

{

vector<VarIdT>::const_iterator it;

int score = -1;

int pr_score = -1;

int bo;

PVARV pVV = NULL;

PVARV pr_pVV = NULL;

for (it = superComp.varsBegin(); *it != varsSENTINEL; it++)

if (getVar(*it).isActive())

{

bo = (int) getVar(*it).getVSIDSScore() + getVar(*it).getDLCSScore();

if (bo > score)

{

score = bo;

pVV = &getVar(*it);

}

if (0 != priorityVars.count(getVar(*it).getVarNum()))

{

if (bo > pr_score)

{

pr_score = bo;

pr_pVV = &getVar(*it);

}

}

}

// If we have a priority variable remaining, then take the best one as a decision

if (-1 != pr_score) {

score = pr_score;

pVV = pr_pVV;

}

if (pVV == NULL)

return false;

bool pol = pVV->scoreDLIS[true] + pVV->scoreVSIDS[true]

> pVV->scoreDLIS[false] + pVV->scoreVSIDS[false];

theLit = pVV->getLitIdT(pol);

return true;

{

LiteralIdT theLit(NOT_A_LIT);

CStepTime::stepTime(); // Solver-Zeit

if (CStepTime::getTime() - xFormulaCache.getLastDivTime()

> xFormulaCache.getScoresDivTime())

{

xFormulaCache.divCacheScores();

xFormulaCache.setLastDivTime(CStepTime::getTime());

}

if (!bcpImplQueue.empty())

return true;

if (!decStack.TOS_hasAnyRemComp())

{

recordRemainingComps();

if (decStack.TOS_countRemComps() == 0)

{

handleSolution();

return false;

}

}

if (!findVSADSDecVar(theLit, decStack.TOS_NextComp())

|| decStack.TOS_NextComp().getClauseCount() == 0) // i.e. component satisfied

{

handleSolution();

decStack.TOS_popRemComp();

return false;

}

//checkCachedCompVal:

static CRealNum cacheVal;

//decStack.TOS_NextComp();

if (CSolverConf::allowComponentCaching && xFormulaCache.extract(

decStack.TOS_NextComp(), cacheVal,

decStack.top().getCurrentDTNode()))

{

decStack.top().includeSol(cacheVal);

theRunAn.addValue(SOLUTION, decStack.getDL());

decStack.TOS_popRemComp();

return false;

}

/////////////////////////////

// Create the nodes

DTNode * newNode = new DTNode(DT_NodeType::kDTOr, num_Nodes++);

DTNode * left = new DTNode(DT_NodeType::kDTAnd, num_Nodes++);

DTNode * right = new DTNode(DT_NodeType::kDTAnd, num_Nodes++);

DTNode * leftLit = get_lit_node(theLit.toSignedInt());

DTNode * rightLit = get_lit_node(-1 * theLit.toSignedInt());

newNode->choiceVar = theLit.toVarIdx();

// Set the parents

left->addParent(newNode, true);

leftLit->addParent(left, true);

right->addParent(newNode, true);

rightLit->addParent(right, true);

newNode->addParent(decStack.top().getCurrentDTNode(), true);

decStack.push(newNode);

bcpImplQueue.clear();

bcpImplQueue.push_back(AntAndLit(NOT_A_CLAUSE, theLit));

theRunAn.addValue(DECISION, decStack.getDL());

if (theRunAn.getData().nDecisions % 255 == 0)

{

doVSIDSScoreDiv();

}

return true;

{

// We are removing the pollutions because a conflict was found, so the

// current decision level must be reset to only contain the literal.

// TODO: Confirm that this is not required for the graph

//decStack.top().getCurrentDTNode()->reset();

// check if one sibling has modelcount 0

// if so, the other siblings may have polluted the cache --> remove pollutions

// cout << decStack.getDL()<<" "<<endl;

for (vector<CComponentId *>::iterator it = decStack.TOSRemComps_begin(); it

!= decStack.getAllCompStack().end(); it++)

// if component *it is cached remove it and all of its descendants

if ((*it)->cachedAs != 0)

{

remPoll += xFormulaCache.removePollutedEntries((*it)->cachedAs);

(*it)->cachedAs = 0;

(*it)->cachedChildren.clear();

}

// it might occur that *it is not yet cached, but has descedants that are cached

// thus we have to delete them

else if (!(*it)->cachedChildren.empty())

{

for (vector<unsigned int>::iterator ct =

(*it)->cachedChildren.begin(); ct

!= (*it)->cachedChildren.end(); ct++)

{

remPoll += xFormulaCache.removePollutedEntries(*ct);

}

}

xFormulaCache.revalidateCacheLinksIn(decStack.getAllCompStack());

{

unsigned int refTime = theRunAn.getData().nAddedClauses;

LiteralIdT aLit;

if (refTime - lastTimeCClDeleted > 1000 && countCCls() > 3000)

{

deleteConflictCls();

lastTimeCClDeleted = refTime;

}

if (refTime - lastCClCleanUp > 35000)

{

cleanUp_deletedCCls();

toSTDOUT("cleaned:");

printCClstats();

lastCClCleanUp = refTime;

}

//component cache delete old entries

if (CSolverConf::allowComponentCaching)

xFormulaCache.deleteEntries(decStack);

do

{

if (decStack.top().getBranchSols() == 0.0)

{

removeAllCachePollutions();

}

if (decStack.top().anotherCompProcessible())

{

return PROCESS_COMPONENT;

}

if (!decStack.top().isFlipped())

{

aLit = decStack.TOS_decLit();

decStack.flipTOS();

bcpImplQueue.push_back(AntAndLit(NOT_A_CLAUSE, aLit.oppositeLit()));

return RESOLVED;

}

//include the component value of the current component into the Cache

if (CSolverConf::allowComponentCaching)

{

xFormulaCache.include(decStack.TOSRefComp(),

decStack.top().getOverallSols(),

decStack.top().getOrDTNode());

}

} while (decStack.pop());

return EXIT;

{

bool bSucceeded;

vector<LiteralIdT>::iterator it;

//BEGIN process unit clauses

for (it = theUnitClauses.begin(); it != theUnitClauses.end(); it++)

{

if (getVar(*it).isActive())

bcpImplQueue.push_back(AntAndLit(NOT_A_CLAUSE, *it));

if (isUnitCl(it->oppositeLit()))

{

// dealing with opposing unit clauses is handed over to

// resolveConflict

return false;

}

}

//END process unit clauses

bSucceeded = BCP(bcpImplQueue);

bcpImplQueue.clear();

if (CSolverConf::allowImplicitBCP && bSucceeded)

{

bSucceeded = implicitBCP();

}

theRunAn.addValue(IMPLICATION, decStack.getDL(),

decStack.TOS_countImplLits());

return bSucceeded;

{

int backtrackDecLev;

// Since we have a conflict, we should add a bottom to the current DTNode

DTNode * newBot = new DTNode(DT_NodeType::kDTBottom, num_Nodes++);

newBot->addParent(decStack.top().getCurrentDTNode(), true);

for (vector<LiteralIdT>::iterator it = theUnitClauses.begin(); it

!= theUnitClauses.end(); it++)

{

if (isUnitCl(it->oppositeLit()))

{

toSTDOUT("\nOPPOSING UNIT CLAUSES - INSTANCE UNSAT\n");

return EXIT;

}

}

theRunAn.addValue(CONFLICT, decStack.getDL(), 1);

#ifdef DEBUG

assert(!getConflicted().empty());

#endif

if (!CSolverConf::analyzeConflicts || getConflicted().empty())

return backTrack();

caGetCauses_firstUIP(getConflicted());

backtrackDecLev = getMaxDecLevFromAnalysis();

if (ca_1UIPClause.size() < ca_lastUIPClause.size())

create1UIPCCl();

//BEGIN Backtracking

if (backtrackDecLev < decStack.getDL())

{

if (CSolverConf::doNonChronBackTracking)

while (decStack.getDL() > backtrackDecLev)

{

/// check for polluted cache Entries

removeAllCachePollutions();

decStack.pop();

newBot = new DTNode(DT_NodeType::kDTBottom, num_Nodes++);

newBot->addParent(decStack.top().getCurrentDTNode(), true);

}

return backTrack();

}

// maybe the other branch had some solutions

if (decStack.top().isFlipped())

{

return backTrack();

}

// now: if the other branch has to be visited:

createAntClauseFor(decStack.TOS_decLit().oppositeLit());

LiteralIdT aLit = decStack.TOS_decLit();

AntecedentT ant = getVar(aLit).getAntecedent();

decStack.flipTOS();

bcpImplQueue.push_back(AntAndLit(ant, aLit.oppositeLit()));

//END Backtracking

return RESOLVED;

{

// the refComp has to be copied!! because in case that the vector

// containing it has to realloc (which might happen here)

// copying the refcomp is not necessary anymore, as the allCompsStack is a vector

// of pointers - realloc does not invalidate these

CComponentId & refSupComp = decStack.TOSRefComp();

viewStateT lookUpCls[getMaxOriginalClIdx() + 2];

viewStateT lookUpVars[countAllVars() + 2];

memset(lookUpCls, NIL, sizeof(viewStateT) * (getMaxOriginalClIdx() + 2));

memset(lookUpVars, NIL, sizeof(viewStateT) * (countAllVars() + 2));

vector<VarIdT>::const_iterator vt;

vector<ClauseIdT>::const_iterator itCl;

for (itCl = refSupComp.clsBegin(); *itCl != clsSENTINEL; itCl++)

{

lookUpCls[*itCl] = IN_SUP_COMP;

}

for (vt = refSupComp.varsBegin(); *vt != varsSENTINEL; vt++)

{

if (getVar(*vt).isActive())

{

lookUpVars[*vt] = IN_SUP_COMP;

getVar(*vt).scoreDLIS[true] = 0;

getVar(*vt).scoreDLIS[false] = 0;

}

}

vector<LiteralIdT>::const_iterator itL;

componentSearchStack.clear();

if (CSolverConf::disableDynamicDecomp)

{

decStack.TOS_addRemComp();

decStack.lastComp().setTrueClauseCount(0);

for (vt = refSupComp.varsBegin(); *vt != varsSENTINEL; vt++)

if (lookUpVars[*vt] == IN_SUP_COMP)

{

lookUpVars[*vt] = SEEN;

componentSearchStack.push_back(*vt);

getComp(*vt, decStack.TOSRefComp(), lookUpCls, lookUpVars);

}

decStack.lastComp().addVar(varsSENTINEL);

decStack.lastComp().addCl(clsSENTINEL);

}

else

{

for (vt = refSupComp.varsBegin(); *vt != varsSENTINEL; vt++)

if (lookUpVars[*vt] == IN_SUP_COMP)

{

decStack.TOS_addRemComp();

decStack.lastComp().setTrueClauseCount(0);

lookUpVars[*vt] = SEEN;

componentSearchStack.push_back(*vt);

getComp(*vt, decStack.TOSRefComp(), lookUpCls, lookUpVars);

decStack.lastComp().addVar(varsSENTINEL);

decStack.lastComp().addCl(clsSENTINEL);

}

}

decStack.TOS_sortRemComps();

return true;

viewStateT lookUpCls[], viewStateT lookUpVars[])

{

/* Moved to above */

//componentSearchStack.clear();

//lookUpVars[theVar] = SEEN;

//componentSearchStack.push_back(theVar);

vector<VarIdT>::const_iterator vt, itVEnd;

vector<LiteralIdT>::const_iterator itL;

vector<ClauseIdT>::const_iterator itCl;

CVariableVertex * pActVar;

unsigned int nClausesSeen = 0, nBinClsSeen = 0;

for (vt = componentSearchStack.begin(); vt != componentSearchStack.end(); vt++)

// the for-loop is applicable here because componentSearchStack.capacity() == countAllVars()

{

pActVar = &getVar(*vt);

//BEGIN traverse binary clauses

for (itL = pActVar->getBinLinks(true).begin(); *itL != SENTINEL_LIT; itL++)

if (lookUpVars[itL->toVarIdx()] == IN_SUP_COMP)

{

nBinClsSeen++;

lookUpVars[itL->toVarIdx()] = SEEN;

componentSearchStack.push_back(itL->toVarIdx());

getVar(*itL).scoreDLIS[itL->polarity()]++;

pActVar->scoreDLIS[true]++;

}

for (itL = pActVar->getBinLinks(false).begin(); *itL != SENTINEL_LIT; itL++)

if (lookUpVars[itL->toVarIdx()] == IN_SUP_COMP)

{

nBinClsSeen++;

lookUpVars[itL->toVarIdx()] = SEEN;

componentSearchStack.push_back(itL->toVarIdx());

getVar(*itL).scoreDLIS[itL->polarity()]++;

pActVar->scoreDLIS[false]++;

}

//END traverse binary clauses

for (itCl = var_InClsBegin(*pActVar); *itCl != SENTINEL_CL; itCl++)

if (lookUpCls[*itCl] == IN_SUP_COMP)

{

itVEnd = componentSearchStack.end();

for (itL = begin(getClause(*itCl)); *itL != ClauseEnd(); itL++)

if (lookUpVars[itL->toVarIdx()] == NIL) //i.e. the var is not active

{

if (!isSatisfied(*itL))

continue;

//BEGIN accidentally entered a satisfied clause: undo the search process

while (componentSearchStack.end() != itVEnd)

{

lookUpVars[componentSearchStack.back()]

= IN_SUP_COMP;

componentSearchStack.pop_back();

}

lookUpCls[*itCl] = NIL;

for (vector<LiteralIdT>::iterator itX = begin(

getClause(*itCl)); itX != itL; itX++)

{

if (getVar(*itX).scoreDLIS[itX->polarity()] > 0)

getVar(*itX).scoreDLIS[itX->polarity()]--;

}

//END accidentally entered a satisfied clause: undo the search process

break;

}

else

{

getVar(*itL).scoreDLIS[itL->polarity()]++;

if (lookUpVars[itL->toVarIdx()] == IN_SUP_COMP)

{

lookUpVars[itL->toVarIdx()] = SEEN;

componentSearchStack.push_back(itL->toVarIdx());

}

}

if (lookUpCls[*itCl] == NIL)

continue;

nClausesSeen++;

lookUpCls[*itCl] = SEEN;

}

}

/////////////////////////////////////////////////

// BEGIN store variables in resComp

/////////////////////////////////////////////////

decStack.lastComp().reserveSpace(componentSearchStack.size(), nClausesSeen);

for (vt = superComp.varsBegin(); *vt != varsSENTINEL; vt++)

if (lookUpVars[*vt] == SEEN) //we have to put a var into our component

{

decStack.lastComp().addVar(*vt);

lookUpVars[*vt] = IN_OTHER_COMP;

}

//decStack.lastComp().addVar(varsSENTINEL); // Moved to above

/////////////////////////////////////////////////

// END store variables in resComp

/////////////////////////////////////////////////

for (itCl = superComp.clsBegin(); *itCl != clsSENTINEL; itCl++)

if (lookUpCls[*itCl] == SEEN)

{

decStack.lastComp().addCl(*itCl);

lookUpCls[*itCl] = IN_OTHER_COMP;

}

//decStack.lastComp().addCl(clsSENTINEL); // Moved to above

decStack.lastComp().addTrueClauseCount(nClausesSeen + nBinClsSeen);

return true;

{

DepositOfClauses::iterator it;

DepositOfVars::iterator jt;

rComp.clear();

unsigned int nBinClauses = 0;

unsigned int idx = 1;

for (it = beginOfClauses(); it != endOfClauses(); it++, idx++)

{

#ifdef DEBUG

assert(!it->isDeleted()); // deleted Cls should be cleaned by prepCleanPool

#endif

rComp.addCl(ClauseIdT(idx));

}

rComp.addCl(clsSENTINEL);

idx = 1;

for (jt = beginOfVars(); jt != endOfVars(); jt++, idx++)

{

#ifdef DEBUG

assert(jt->isActive()); // deleted Vars should be cleaned by prepCleanPool

#endif

rComp.addVar(idx);

nBinClauses += countActiveBinLinks(idx);

}

rComp.addVar(varsSENTINEL);

nBinClauses >>= 1;

rComp.setTrueClauseCount(nBinClauses + rComp.countCls());

{

vector<ClauseIdT>::const_iterator it;

for (it = rComp.clsBegin(); *it != clsSENTINEL; it++)

{

printActiveClause(*it);

}

{

extd_vector<ClauseIdT>* pUnWatchCls;

extd_vector<ClauseIdT>::iterator it;

bool retV;

ClauseIdT actCl;

PCLV pCl;

vector<LiteralIdT>::const_iterator bt;

vector<LiteralIdT>::iterator itL;

LiteralIdT satLit, unLit;

getConflicted().clear();

for (unsigned int i = 0; i < thePairsOfImpl.size(); i++)

if (assignVal(thePairsOfImpl[i].getLit(), thePairsOfImpl[i].getAnt()))

{

satLit = thePairsOfImpl[i].getLit();

unLit = thePairsOfImpl[i].getLit().oppositeLit();

decStack.TOS_addImpliedLit(satLit);

#ifdef FULL_DDNNF

if (enable_DT_recording)

{

DTNode * satLitDTNode = get_lit_node(satLit.toSignedInt());

satLitDTNode->addParent(decStack.top().getCurrentDTNode(), true);

dirtyLitNodes.push_back(pair<DTNode *, DTNode *> (

decStack.top().getCurrentDTNode(), satLitDTNode));

}

#endif

pUnWatchCls = &getVar(unLit).getWatchClauses(unLit.polarity());

//BEGIN Propagate Bin Clauses

/* First propagate the original binary clauses */

for (bt = getVar(unLit).getBinLinks(unLit.polarity()).begin(); *bt

!= SENTINEL_LIT; bt++)

{

if (getVar(*bt).isActive())

{

thePairsOfImpl.push_back(AntAndLit(unLit, *bt));

#ifdef FULL_DDNNF

if (enable_DT_recording)

{

DTNode * ccLit = get_lit_node((*bt).toSignedInt());

ccLit->addParent(decStack.top().getCurrentDTNode(), true);

dirtyLitNodes.push_back(pair<DTNode *, DTNode*> (

decStack.top().getCurrentDTNode(), ccLit));

}

#endif

}

else if (!isSatisfied(*bt))

{

getConflicted().push_back(unLit);

getConflicted().push_back(*bt);

return false;

}

}

/* Next propagate the conflict generated binary clauses */

for (bt = bt + 1; *bt != SENTINEL_LIT; bt++)

{

if (getVar(*bt).isActive())

{

thePairsOfImpl.push_back(AntAndLit(unLit, *bt));

if (enable_DT_recording)

{

// Add the implied literal due to a conflict clause

DTNode * ccLit = get_lit_node((*bt).toSignedInt());

ccLit->addParent(decStack.top().getCurrentDTNode(), true);

dirtyLitNodes.push_back(pair<DTNode *, DTNode*> (

decStack.top().getCurrentDTNode(), ccLit));

}

}

else if (!isSatisfied(*bt))

{

getConflicted().push_back(unLit);

getConflicted().push_back(*bt);

return false;

}

}

//END Propagate Bin Clauses

for (it = pUnWatchCls->end() - 1; *it != SENTINEL_CL; it--)

{

actCl = *it;

pCl = &getClause(actCl);

// all clauses treated as conflict clauses, because no subsumption

// is being performed

if (isSatisfied(pCl->idLitA()) || isSatisfied(pCl->idLitB()))

continue;

///////////////////////////////////////

//BEGIN update watched Lits

///////////////////////////////////////

retV = false;

for (itL = begin(*pCl); *itL != ClauseEnd(); itL++)

if (getVar(*itL).isActive() || isSatisfied(*itL))

{

if (*itL == pCl->idLitA() || *itL == pCl->idLitB())

continue;

retV = isSatisfied(*itL);

getVar(*itL).addWatchClause(actCl, itL->polarity());

if (pCl->idLitA() == unLit)

pCl->setLitA(*itL);

else

pCl->setLitB(*itL);

pUnWatchCls->quickErase(it);

break;

}

if (retV)

continue; // i.e. clause satisfied

///////////////////////////////////////

//END update watched Lits

///////////////////////////////////////

if (getVar(pCl->idLitA()).isActive())

{

if (!getVar(pCl->idLitB()).isActive()) //IMPLIES_LITA;

{

thePairsOfImpl.push_back(

AntAndLit(actCl, pCl->idLitA()));

pCl->setTouched();

// Add the implied literal due to a conflict clause

#ifndef FULL_DDNNF

if (pCl->isCC())

{

#endif

if (enable_DT_recording)

{

DTNode * ccLit = get_lit_node(

pCl->idLitA().toSignedInt());

ccLit->addParent(decStack.top().getCurrentDTNode(),

true);

dirtyLitNodes.push_back(pair<DTNode *, DTNode*> (

decStack.top().getCurrentDTNode(), ccLit));

}

#ifndef FULL_DDNNF

}

#endif

}

}

else

{

pCl->setTouched();

if (getVar(pCl->idLitB()).isActive())

{ //IMPLIES_LITB;

thePairsOfImpl.push_back(

AntAndLit(actCl, pCl->idLitB()));

// Add the implied literal due to a conflict clause

#ifndef FULL_DDNNF

if (pCl->isCC())

{

#endif

if (enable_DT_recording)

{

DTNode * ccLit = get_lit_node(

pCl->idLitB().toSignedInt());

ccLit->addParent(decStack.top().getCurrentDTNode(),

true);

dirtyLitNodes.push_back(pair<DTNode *, DTNode*> (

decStack.top().getCurrentDTNode(), ccLit));

}

#ifndef FULL_DDNNF

}

#endif

}

else //provided that SATISFIED has been tested

{

getConflicted().push_back(actCl);

return false;