source: vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/MainSolver.cpp

#include "MainSolver.h" // class's header file

// class constructor
CMainSolver::CMainSolver():decStack(*this)
{
   stopWatch.setTimeBound(CSolverConf::secsTimeBound);  
   remPoll = 0;
}

// class destructor
CMainSolver::~CMainSolver()
{ 
   toDEBUGOUT("removed. Poll: "<<remPoll<<endl);
}



bool CMainSolver::performPreProcessing()
{    
   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;
}

void CMainSolver::solve(const char *lpstrFileName)
{
  SOLVER_StateT exSt;
  
  stopWatch.markStartTime();  

  createfromFile(lpstrFileName);  
   
  decStack.init(countAllVars());
  
  CStepTime::makeStart(); 
  
  xFormulaCache.init();   
  
  toSTDOUT("#Vars:"<<countAllVars()<<endl); 
  toSTDOUT("#Clauses:"<<countAllClauses()<<endl);  
  toSTDOUT("#bin Cls:"<<countBinClauses()<<endl); 
   
  bool needToCount = performPreProcessing(); 

  if (needToCount && !(CSolverConf::count)) {
        theRunAn.setExitState(SUCCESS);
        theRunAn.setSatCount(1.0);
        stopWatch.markStopTime();
        theRunAn.setElapsedTime(stopWatch.getElapsedTime());
        xFormulaCache.printStatistics(theRunAn);
        return;
  }

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


SOLVER_StateT CMainSolver::countSAT()
{   
   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;   
      }      
   }
}



bool CMainSolver::findVSADSDecVar(LiteralIdT &theLit, const CComponentId & superComp)
{   
    vector<VarIdT>::const_iterator it;
      
    int score = -1;         
    int bo;
    PVARV 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(pVV == NULL) return false;
        
    bool pol = pVV->scoreDLIS[true] + pVV->scoreVSIDS[true] > pVV->scoreDLIS[false] + pVV->scoreVSIDS[false];
    
    theLit = pVV->getLitIdT(pol);
    
    return true;
}


bool CMainSolver::decide()
{   
   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().includeSol(cacheVal);       
       theRunAn.addValue(SOLUTION,decStack.getDL());          
       decStack.TOS_popRemComp();       
       return false;   
     }   
   /////////////////////////////   
   decStack.push();   
   bcpImplQueue.clear();
   bcpImplQueue.push_back(AntAndLit(NOT_A_CLAUSE,theLit));   
   
       theRunAn.addValue(DECISION,decStack.getDL());  
   
   
   if(theRunAn.getData().nDecisions % 255 == 0)
   {   
      doVSIDSScoreDiv();    
   }
       
   return true;
}

void CMainSolver::removeAllCachePollutions()
{
   // 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());    
   
}

retStateT CMainSolver::backTrack()
{   
    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());
       }  
           
    } while(decStack.pop());
    
    return EXIT;
}



bool CMainSolver::bcp()
{   
    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;
}


retStateT CMainSolver::resolveConflict()
{   
   int backtrackDecLev;          
   
   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();
       }
      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;   
}



/////////////////////////////////////////////////////
// BEGIN component analysis
/////////////////////////////////////////////////////



bool CMainSolver::recordRemainingComps()
{
  // 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; 
  
  for(vt = refSupComp.varsBegin(); *vt != varsSENTINEL; vt++)
   if(lookUpVars[*vt] == IN_SUP_COMP)
   {
     decStack.TOS_addRemComp();
    
     getComp(*vt, decStack.TOSRefComp(), lookUpCls, lookUpVars);    
   }  
  
 
  decStack.TOS_sortRemComps();
  return true;
}




bool CMainSolver::getComp(const VarIdT &theVar, 
                            const CComponentId &superComp,
                            viewStateT lookUpCls[], 
                            viewStateT lookUpVars[])
{  
  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);          
  
  /////////////////////////////////////////////////
  // 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);  
  decStack.lastComp().setTrueClauseCount(nClausesSeen + nBinClsSeen);
  
  return true;
}



/////////////////////////////////////////////////////
// END component analysis
/////////////////////////////////////////////////////


void CMainSolver::makeCompIdFromActGraph(CComponentId& rComp)
{
   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()); 
}


void CMainSolver::printComponent(const CComponentId& rComp)
{
  vector<ClauseIdT>::const_iterator it;  
  for(it = rComp.clsBegin(); *it != clsSENTINEL;it++)
  {
    printActiveClause(*it);
  }
}




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

bool CMainSolver::BCP(vector<AntAndLit> &thePairsOfImpl)
{
   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);
       
       pUnWatchCls = &getVar(unLit).getWatchClauses(unLit.polarity());
       
       //BEGIN Propagate Bin Clauses
       for(bt = getVar(unLit).getBinLinks(unLit.polarity()).begin(); *bt != SENTINEL_LIT;bt++)          
       {
          if(getVar(*bt).isActive()) thePairsOfImpl.push_back(AntAndLit(unLit,*bt));
          else if(!isSatisfied(*bt))
          {
             getConflicted().push_back(unLit);
             getConflicted().push_back(*bt);
             return false;
          }
       }
       for(bt = bt+1; *bt != SENTINEL_LIT;bt++)
       {
          if(getVar(*bt).isActive()) thePairsOfImpl.push_back(AntAndLit(unLit,*bt));
          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();
             }
          }
          else
          {
             pCl->setTouched();
             if(getVar(pCl->idLitB()).isActive()) //IMPLIES_LITB;
                thePairsOfImpl.push_back(AntAndLit(actCl,pCl->idLitB()));
             else  //provided that SATISFIED has been tested                   
             {
                getConflicted().push_back(actCl);
                return false;
             }
         }
      }
    }   
    return true; 
}


bool CMainSolver::createAntClauseFor(const LiteralIdT &Lit)
{
        const vector<LiteralIdT> &actCCl = caGetPrevLastUIPCCl();
   
        bool created = createLastUIPCCl();  
  
        if(!created && actCCl.size() != 2) return false;  
  
        if(actCCl.size() == 1) 
        {
          getVar(Lit).adjustAntecedent(NOT_A_CLAUSE);
          return true; // theLit has become a unit clause: nothing to be done
        } 
        if(actCCl.size() == 2)
        {
                #ifdef DEBUG
                assert(actCCl.front() != Lit.oppositeLit());
                assert(actCCl.back() != Lit.oppositeLit());
                #endif
                
                if(actCCl.front() == Lit)
                        getVar(Lit).adjustAntecedent(AntecedentT(actCCl.back()));                
                else if(actCCl.back() == Lit)    
                        getVar(Lit).adjustAntecedent(AntecedentT(actCCl.front()));    
    
                return true;
        }
        setCClImplyingLit(getLastClauseId(),Lit);       
        getVar(Lit).adjustAntecedent(AntecedentT(getLastClauseId()));   
        return true;
}

bool CMainSolver::implicitBCP()
{
   vector<LiteralIdT>::iterator jt;
   vector<LiteralIdT>::const_iterator it,lt;   
   vector<ClauseIdT>::const_iterator ct;    

   static vector<AntAndLit> implPairs;    
   implPairs.clear();
   vector<LiteralIdT> nextStep; 
   bool viewedLits[(countAllVars()+1)*2 +1];    
   LiteralIdT newLit;
   AntecedentT theAnt, nant;
   LiteralIdT theLit,nlit;
   implPairs.reserve(decStack.TOSRefComp().countVars());        
   nextStep.reserve(decStack.TOSRefComp().countVars());
   int allFound = 0;
   bool bsat;
   
   int impOfs = 0;  
   int step;
   do{ 
      if(decStack.TOS_countImplLits() - impOfs > 0) 
      {
         memset(viewedLits,false,sizeof(bool)*((countAllVars()+1)*2 +1));
         nextStep.clear();
         for(it = decStack.TOS_ImpliedLits_begin()+ impOfs; it != decStack.TOS_ImpliedLits_end(); it++)
         {  
            step = var_InClsStep(!it->polarity());            
            for(ct = var_InClsStart(it->toVarIdx(),!it->polarity()); *ct != SENTINEL_CL; ct+= step)
            {
               bsat = false;
               for(lt = begin(getClause(*ct));*lt != ClauseEnd(); lt++)
                {
                  if(isSatisfied(*lt)) { bsat = true; break; }                    
                }
               
               if(bsat) continue;
               for(lt = begin(getClause(*ct));*lt != ClauseEnd(); lt++)
                if(getVar(*lt).isActive() && !viewedLits[lt->toUInt()])
                {
                   nextStep.push_back(*lt);
                   viewedLits[lt->toUInt()] = true;
                }
            }           
         }
      }
      impOfs = decStack.TOS_countImplLits();
      
      for(jt = nextStep.begin(); jt != nextStep.end(); jt++)
       if(getVar(*jt).isActive())
       {
         implPairs.push_back(AntAndLit(NOT_A_CLAUSE,jt->oppositeLit()));        
         // BEGIN BCPROPAGATIONNI
         unsigned int sz = decStack.countAllImplLits();
         
         // we increase the decLev artificially
         // s.t. after the tentative BCP call, we can learn a conflict clause
         // relative to the assignment of *jt
         decStack.beginTentative();
         
         bool bSucceeded = BCP(implPairs);       
         
         
         decStack.shrinkImplLitsTo(sz);
         theAnt = NOT_A_CLAUSE;
         theLit = implPairs[0].getLit();
                 
         if(!bSucceeded && CSolverConf::analyzeConflicts
            && !getConflicted().empty())
         {
            
            caGetCauses_lastUIP(getConflicted());    
            
            createAntClauseFor(theLit.oppositeLit());           
            //createLastUIPCCl(); 
            
            theRunAn.addValue(IBCPIMPL,decStack.getDL(),1);
            theAnt = getVar(theLit).getAntecedent();
            
         }
         decStack.endTentative();
         
         for(vector<AntAndLit>::iterator at = implPairs.begin(); at != implPairs.end(); at++)
            getVar(at->theLit).unsetVal(); 
         implPairs.clear();
    
         if(!bSucceeded)
         {
            implPairs.push_back(AntAndLit(theAnt,theLit.oppositeLit()));          
                    
            if(!BCP(implPairs))
            {
             implPairs.clear();
             return false;
            } 
          
            implPairs.clear();          
         }    
      // END BCPROPAGATIONNI
      }      
      allFound += decStack.TOS_countImplLits() - impOfs;  
     
   }while(decStack.TOS_countImplLits() - impOfs > 0);   
   return true;   
}

///////////////////////////////////////////////////////////////////////////////////////////////
// BEGIN module conflictAnalyzer
///////////////////////////////////////////////////////////////////////////////////////////////


void CMainSolver::caIncludeCauses(LiteralIdT theLit, bool viewedVars[])
{ 
        vector<LiteralIdT>::const_iterator it; 
        
        ClauseIdT implCl;

        if(!getVar(theLit).getAntecedent().isAClause())
        {
                LiteralIdT hlit;   
                hlit = getVar(theLit).getAntecedent().toLit();   
                caIncorporateLit(hlit,viewedVars); 
                #ifdef DEBUG
                assert(hlit != NOT_A_LIT);  
                #endif
                return;
        }
 
        implCl = getVar(theLit).getAntecedent().toCl();
 
        if(implCl == NOT_A_CLAUSE) 
        // theLit has not been implied, in fact this means that
        // either theLit is the decided variable, a unit clause or
        // a variable that has been tentatively assigned by ImplicitBCP
        // other cases may not occur !
        {   
                caAddtoCauses(theLit,viewedVars);        
                return;
        }
 
        for(it = begin(getClause(implCl)); *it != ClauseEnd(); it ++)
        {   
                caIncorporateLit(*it,viewedVars);
        }
}
///////////////////////////////////////////////////////////////////
//
//  BEGIN public
//
///////////////////////////////////////////////////////////////////

void CMainSolver::caAddtoCauses(LiteralIdT theLit, bool viewedVars[])
{   
        viewedVars[theLit.toVarIdx()] = true; 
      
        ca_lastUIPClause.push_back(theLit.oppositeLit());
   
        if(getVar(theLit).getDLOD() > imaxDecLev) imaxDecLev = getVar(theLit).getDLOD();
}

void CMainSolver::caIncorporateLit(const LiteralIdT &Lit, bool viewedVars[])
{    
        if(Lit == NOT_A_LIT) return;
        
        if(!viewedVars[Lit.toVarIdx()])
        {       
                viewedVars[Lit.toVarIdx()] = true;
                ////
                getVar(Lit).scoreVSIDS[Lit.polarity()]++;
                getVar(Lit).scoreVSIDS[Lit.oppositeLit().polarity()]++;
                ////
                if(getVar(Lit).getDLOD() == decStack.getDL())
                {         
                        theQueue.push_back(Lit.oppositeLit());   
                }       
                else caAddtoCauses(Lit.oppositeLit(),viewedVars);  
        }
}

bool CMainSolver::caInit(vector<AntecedentT> & theConflicted, bool viewedVars[])
{
        vector<LiteralIdT>::const_iterator it;
   
        imaxDecLev = -1;
     
        ca_1UIPClause.clear();
        ca_lastUIPClause.clear();
   
        theQueue.clear();       
        theQueue.reserve(countAllVars()+1);
   
        ClauseIdT idConflCl;
        LiteralIdT idConflLit;
   
        if(theConflicted[0].isAClause())
        {
                idConflCl = theConflicted[0].toCl();     
                
                for(it = begin(getClause(idConflCl)); *it != ClauseEnd(); it ++)
                {   
                        caIncorporateLit(*it,viewedVars);
                }
        }
        else
        {
                if(theConflicted.size() < 2)
                {
                        toSTDOUT("error in getcauses bincl"<<endl);
                        return false;     
                }
     
                idConflLit = theConflicted[0].toLit();     
                caIncorporateLit(idConflLit,viewedVars);
                idConflLit = theConflicted[1].toLit();
                caIncorporateLit(idConflLit,viewedVars);
        }
   
        return true;
}

bool CMainSolver::caGetCauses_lastUIP(vector<AntecedentT> & theConflicted)
{
        vector<LiteralIdT>::const_iterator it;
        bool viewedVars[countAllVars()+1]; 
    
        memset(viewedVars,false,sizeof(bool)*(countAllVars()+1));     
   
        if(!caInit(theConflicted,viewedVars)) return false;
   
        for(unsigned int i = 0; i < theQueue.size();i++)
        {
                viewedVars[theQueue[i].toVarIdx()] = true;
                caIncludeCauses(theQueue[i], viewedVars);
        }
   
        // analyzer data
        theRunAn.addValue(CCL_lastUIP, decStack.getDL(),ca_lastUIPClause.size());
        return true;
}


bool CMainSolver::caGetCauses_firstUIP(vector<AntecedentT> & theConflicted)
{
        vector<LiteralIdT>::const_iterator it;
        bool viewedVars[countAllVars()+1];
   
        memset(viewedVars,false,sizeof(bool)*(countAllVars()+1));  
   
        if(!caInit(theConflicted,viewedVars)) return false;
   
        bool pastfirstUIP = false;
   
        for(unsigned int i = 0; i < theQueue.size();i++)        
        { 
                
                if(i == theQueue.size()-1 && pastfirstUIP == false)
                {
                        pastfirstUIP = true;
       
                        ca_1UIPClause = ca_lastUIPClause;
       
                        ca_1UIPClause.push_back(theQueue.back().oppositeLit());              
                } 
                viewedVars[theQueue[i].toVarIdx()] = true;
                caIncludeCauses(theQueue[i], viewedVars);
        }   
        // analyzer data
        theRunAn.addValue(CCL_1stUIP, decStack.getDL(), ca_1UIPClause.size());       
        theRunAn.addValue(CCL_lastUIP, decStack.getDL(),ca_lastUIPClause.size());
   
        return true;
}

///////////////////////////////////////////////////////////////////////////////////////////////
// END module conflictAnalyzer
///////////////////////////////////////////////////////////////////////////////////////////////



////////////////////////////////////////////////////////////////////////
//
//  BEGIN Methods for Preprocessing
//
///////////////////////////////////////////////////////////////////////

bool CMainSolver::prep_IBCP(vector<AntAndLit> &impls)
{   
        bool bSucceeded = false;   
    
        getConflicted().clear();
    
        unsigned int sz = decStack.countAllImplLits();
    
        bSucceeded = BCP(impls);
        decStack.shrinkImplLitsTo(sz);    
    
        vector<AntAndLit>::iterator it;
 
        for(it = impls.begin(); it != impls.end(); it++)
        {
                getVar(it->theLit).unsetVal();
        }
    
        impls.clear();    
        return bSucceeded;
}

bool CMainSolver::prepFindHiddenBackBoneLits()
{
   DepositOfVars::iterator jt;                            
   vector<AntAndLit> implPairs;
   implPairs.reserve(countAllVars());    
   
   int foundInLoop = 0;
   int allFound = 0;
   
   do{
      foundInLoop = 0;
      
      for(jt = beginOfVars(); jt != endOfVars(); jt++)
       if(jt->isActive() && jt->countBinLinks() > 0)
       {
          if(jt->countBinLinks(false)>0) implPairs.push_back(AntAndLit(NOT_A_CLAUSE,jt->getLitIdT(true)));
          if((jt->countBinLinks(false)>0) && !prep_IBCP(implPairs))
          {
             foundInLoop++;
             if(!prepBCP(jt->getLitIdT(false))) return false;
          }
          else if(jt->countBinLinks(true)>0)
          {
             implPairs.push_back(AntAndLit(NOT_A_CLAUSE,jt->getLitIdT(false)));
             if(!prep_IBCP(implPairs))
             {
                foundInLoop++;
                if(!prepBCP(jt->getLitIdT(true))) return false;
             }
          }
       }              
       allFound += foundInLoop;       
       
   }while(foundInLoop != 0);    
   if(allFound != 0) toSTDOUT("found UCCL"<<allFound << endl);
   return true;   
}

bool CMainSolver::prepBCP(LiteralIdT firstLit)
{
   vector<LiteralIdT> impls;   
   int step = 0;
   LiteralIdT unLit, satLit;
    
   impls.reserve(countAllVars());
    
   if(firstLit != NOT_A_LIT) impls.push_back(firstLit);    
   
   // prepare UnitClauses for BCP
   if(!theUnitClauses.empty())
   {
      impls.insert(impls.end(),theUnitClauses.begin(),theUnitClauses.end());    
      theUnitClauses.clear();  
      theUClLookUp.clear();
   }
    
   vector<ClauseIdT>::iterator it;
   vector<ClauseIdT>::iterator itBegin;
   vector<LiteralIdT>::iterator lt;
   CVariableVertex *pV;    
    
   for(unsigned int i = 0; i < impls.size();i++)
    if(getVar(impls[i]).setVal(impls[i].polarity(), 0))
    {   
      unLit = impls[i].oppositeLit();
      satLit = impls[i];
      pV = &getVar(satLit);      
                
      // BEGIN propagation              
      for(lt = pV->getBinLinks(unLit.polarity()).begin(); *lt != SENTINEL_LIT;lt++)             
      {
         if(getVar(*lt).isActive()) impls.push_back(*lt);       
           else
            if(getVar(*lt).getboolVal() != lt->polarity()) return false;     
      }
      CClauseVertex *pCl;
      
      itBegin = var_InClsStart(unLit.toVarIdx(),unLit.polarity());
      step = var_InClsStep(unLit.polarity());
      
      for(it = itBegin; *it != SENTINEL_CL; it+= step)
       if(!getClause(*it).isDeleted()) 
       {
          pCl = &getClause(*it); 
          eraseLiteralFromCl(*it,unLit);       
          switch(getClause(*it).length())
          {
             case 0: return false;
             case 1: impls.push_back(*begin(*pCl));
                     break;
             case 2:
                     createBinCl((*begin(*pCl)),*(begin(*pCl)+1));                     
                     /// mark clause *it as deleted                     
                     
                     getVar(pCl->idLitB()).eraseWatchClause(*it, pCl->idLitB().polarity());
                     getVar(pCl->idLitA()).eraseWatchClause(*it, pCl->idLitA().polarity());  
                     
                     for(vector<LiteralIdT>::iterator litt = begin(*pCl); *litt != ClauseEnd();litt++)
                     {  
                       if(*litt != unLit)                        
                       var_EraseClsLink(litt->toVarIdx(), litt->polarity(),*it); 
                       *litt = NOT_A_LIT;
                     }  
  
                     pCl->setDeleted();
                     
                     ///
                     break;
             default: break;
          };
       }
       //END propagation
       
       //BEGIN subsumption 
       for(lt = pV->getBinLinks(satLit.polarity()).begin(); *lt != SENTINEL_LIT;lt++)
           getVar(*lt).eraseBinLinkTo(satLit,lt->polarity());       
        
      itBegin = var_InClsStart(satLit.toVarIdx(),satLit.polarity());
      step = var_InClsStep(satLit.polarity());
      
       for(it = itBegin; *it != SENTINEL_CL;it+= step)
       
         if(!getClause(*it).isDeleted())
         {
          pCl = &getClause(*it); 
          /// mark clause *it as deleted
                    
          getVar(pCl->idLitB()).eraseWatchClause(*it, pCl->idLitB().polarity());
          getVar(pCl->idLitA()).eraseWatchClause(*it, pCl->idLitA().polarity());  
                  
          vector<LiteralIdT>::iterator litt;  
          for(litt = begin(*pCl); *litt != ClauseEnd();litt++)
          {  
             if(*litt != satLit) 
             // deleting ClauseEdges from satLit would be erroneous as it affects satPCl
                var_EraseClsLink(litt->toVarIdx(), litt->polarity(),*it); 
             *litt = NOT_A_LIT;
          }  
  
          pCl->setDeleted();                     
          ///
         } 
       // END subsumption
       
       for(it = var_InClsBegin(unLit.toVarIdx(),false);*it != SENTINEL_CL;it++)
       {
         *it = SENTINEL_CL;
       }
       
       pV->eraseAllEdges();            
   }      
   return true;  
}


////////////////////////////////////////////////////////////////////////
//
//  END Methods for Preprocessing
//
///////////////////////////////////////////////////////////////////////


bool CMainSolver::printUnitClauses()
{   
        vector<LiteralIdT>::iterator it,jt;     
    
        toSTDOUT("UCCL:\n");
        for(it = theUnitClauses.begin(); it != theUnitClauses.end(); it++)
        {     
                toSTDOUT((it->polarity()?" ":"-")<<getVar(*it).getVarNum()<< " 0\n");     
        }
        toSTDOUT(endl);   
             
        return true;
}