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

Last change on this file since 88 was 9, checked in by cecile, 13 years ago

add sharpSat
File size: 35.0 KB
Line 
1#include "MainSolver.h" // class's header file
2
3// class constructor
4CMainSolver::CMainSolver():decStack(*this)
5{
6   stopWatch.setTimeBound(CSolverConf::secsTimeBound); 
7   remPoll = 0;
8}
9
10// class destructor
11CMainSolver::~CMainSolver()
12{ 
13   toDEBUGOUT("removed. Poll: "<<remPoll<<endl);
14}
15
16
17
18bool CMainSolver::performPreProcessing()
19{   
20   if(!prepBCP())
21   {
22      theRunAn.setExitState(SUCCESS);
23      stopWatch.markStopTime();
24      return false;
25   }   
26   if(CSolverConf::allowPreProcessing)
27   {   
28      toSTDOUT("BEGIN preprocessing"<<endl);                 
29      if(!prepFindHiddenBackBoneLits()) 
30      {
31        theRunAn.setExitState(SUCCESS);
32        toSTDOUT("ERR: UNSAT Formula"<<endl); 
33        stopWatch.markStopTime();
34        return false;
35      }             
36      toSTDOUT(endl<<"END preprocessing"<<endl); 
37   }
38     
39   prep_CleanUpPool();     
40 
41   toSTDOUT("#Vars remaining:"<<countAllVars()<<endl); 
42   toSTDOUT("#Clauses remaining:"<<countAllClauses()<<endl); 
43   toSTDOUT("#bin Cls remaining:"<<countBinClauses()<<endl);   
44
45   return true;
46}
47
48void CMainSolver::solve(const char *lpstrFileName)
49{
50  SOLVER_StateT exSt;
51 
52  stopWatch.markStartTime(); 
53
54  createfromFile(lpstrFileName); 
55   
56  decStack.init(countAllVars());
57 
58  CStepTime::makeStart(); 
59 
60  xFormulaCache.init();   
61 
62  toSTDOUT("#Vars:"<<countAllVars()<<endl); 
63  toSTDOUT("#Clauses:"<<countAllClauses()<<endl); 
64  toSTDOUT("#bin Cls:"<<countBinClauses()<<endl); 
65   
66  bool needToCount = performPreProcessing(); 
67
68  if (needToCount && !(CSolverConf::count)) {
69        theRunAn.setExitState(SUCCESS);
70        theRunAn.setSatCount(1.0);
71        stopWatch.markStopTime();
72        theRunAn.setElapsedTime(stopWatch.getElapsedTime());
73        xFormulaCache.printStatistics(theRunAn);
74        return;
75  }
76
77  theRunAn.setRemovedClauses(theRunAn.getData().nRemovedClauses +  theRunAn.getData().nOriginalClauses - getMaxOriginalClIdx() + 1 -countBinClauses());
78 
79  if(needToCount)
80  {
81     // the following call only correct if bin clauses not used for caching
82     CCacheEntry::adjustPackSize(countAllVars(), getMaxOriginalClIdx());
83 
84     lastTimeCClDeleted = CStepTime::getTime();
85     lastCClCleanUp = CStepTime::getTime();
86     makeCompIdFromActGraph(decStack.TOSRefComp());
87     bcpImplQueue.clear();
88     bcpImplQueue.reserve(countAllVars());
89     
90     // the size of componentSearchStack has to be reserved, otherwise getComp(...) might
91     // become erroneous due to realloc
92     componentSearchStack.reserve(countAllVars()+2);
93     
94     exSt = countSAT();       
95 
96     theRunAn.setExitState(exSt);
97     theRunAn.setSatCount(decStack.top().getOverallSols());
98  }
99  else{
100   
101    theRunAn.setExitState(SUCCESS);
102    theRunAn.setSatCount(0.0);
103  } 
104 
105  stopWatch.markStopTime();
106 
107  theRunAn.setElapsedTime(stopWatch.getElapsedTime());
108 
109  xFormulaCache.printStatistics(theRunAn);
110}
111
112
113SOLVER_StateT CMainSolver::countSAT()
114{   
115   retStateT res;   
116   
117   while(true)
118   {     
119      while(decide())
120      {
121         if(stopWatch.timeBoundBroken()) return TIMEOUT;   
122 
123         while(!bcp())
124         {
125            res = resolveConflict();
126            if (res == EXIT) return SUCCESS;   
127            if (res == PROCESS_COMPONENT) break; //force calling decide()   
128         } 
129      }     
130     
131      res = backTrack(); 
132      if(res == EXIT) return SUCCESS; 
133     
134      while(res != PROCESS_COMPONENT && !bcp())
135      { 
136         res = resolveConflict();
137         if(res == EXIT) return SUCCESS;   
138      }     
139   }
140}
141
142
143
144bool CMainSolver::findVSADSDecVar(LiteralIdT &theLit, const CComponentId & superComp)
145{   
146    vector<VarIdT>::const_iterator it;
147     
148    int score = -1;         
149    int bo;
150    PVARV pVV = NULL;
151       
152    for(it = superComp.varsBegin(); *it != varsSENTINEL; it++)
153      if(getVar(*it).isActive())
154      { 
155         bo = (int) getVar(*it).getVSIDSScore() + getVar(*it).getDLCSScore() ; 
156         
157         if(bo > score)
158         {
159              score = bo;             
160              pVV = &getVar(*it);
161         }
162      }
163   
164    if(pVV == NULL) return false;
165       
166    bool pol = pVV->scoreDLIS[true] + pVV->scoreVSIDS[true] > pVV->scoreDLIS[false] + pVV->scoreVSIDS[false];
167   
168    theLit = pVV->getLitIdT(pol);
169   
170    return true;
171}
172
173
174bool CMainSolver::decide()
175{   
176   LiteralIdT theLit(NOT_A_LIT);
177   
178   CStepTime::stepTime(); // Solver-Zeit   
179   
180   
181   if(CStepTime::getTime() - xFormulaCache.getLastDivTime() > xFormulaCache.getScoresDivTime())
182   {   
183      xFormulaCache.divCacheScores();   
184      xFormulaCache.setLastDivTime(CStepTime::getTime());
185   }
186       
187     
188   if(!bcpImplQueue.empty()) return true;
189     
190   if(!decStack.TOS_hasAnyRemComp())
191   { 
192     recordRemainingComps();     
193     if(decStack.TOS_countRemComps() == 0)
194     {   
195       handleSolution();
196       return false;
197     }
198   }
199   
200
201   if(!findVSADSDecVar(theLit, decStack.TOS_NextComp())   
202     || decStack.TOS_NextComp().getClauseCount() == 0) // i.e. component satisfied
203   {   
204    handleSolution();   
205    decStack.TOS_popRemComp();
206    return false;             
207   }   
208     
209   //checkCachedCompVal:
210   static CRealNum cacheVal;   
211   
212   decStack.TOS_NextComp();
213   
214   if(CSolverConf::allowComponentCaching
215     && 
216     xFormulaCache.extract(decStack.TOS_NextComp(),cacheVal))
217     {   
218       decStack.top().includeSol(cacheVal);       
219       theRunAn.addValue(SOLUTION,decStack.getDL());         
220       decStack.TOS_popRemComp();       
221       return false;   
222     }   
223   /////////////////////////////   
224   decStack.push();   
225   bcpImplQueue.clear();
226   bcpImplQueue.push_back(AntAndLit(NOT_A_CLAUSE,theLit));   
227   
228       theRunAn.addValue(DECISION,decStack.getDL()); 
229   
230   
231   if(theRunAn.getData().nDecisions % 255 == 0)
232   {   
233      doVSIDSScoreDiv();   
234   }
235       
236   return true;
237}
238
239void CMainSolver::removeAllCachePollutions()
240{
241   // check if one sibling has modelcount 0
242   // if so, the other siblings may have polluted the cache --> remove pollutions
243   // cout << decStack.getDL()<<" "<<endl;
244   for(vector<CComponentId *>::iterator it = decStack.TOSRemComps_begin();
245         it != decStack.getAllCompStack().end(); it++)
246      // if component *it is cached remove it and all of its descendants
247      if((*it)->cachedAs != 0)
248      { 
249               remPoll += xFormulaCache.removePollutedEntries((*it)->cachedAs);
250               (*it)->cachedAs = 0;
251               (*it)->cachedChildren.clear();         
252      }
253      // it might occur that *it is not yet cached, but has descedants that are cached
254      // thus we have to delete them
255      else if(!(*it)->cachedChildren.empty())
256      {
257        for(vector<unsigned int>::iterator ct = (*it)->cachedChildren.begin();
258             ct != (*it)->cachedChildren.end(); ct++)
259         {   
260           remPoll += xFormulaCache.removePollutedEntries(*ct);
261         }     
262      }                 
263      xFormulaCache.revalidateCacheLinksIn(decStack.getAllCompStack());   
264   
265}
266
267retStateT CMainSolver::backTrack()
268{   
269    unsigned int refTime = theRunAn.getData().nAddedClauses;
270    LiteralIdT aLit;
271
272    if(refTime - lastTimeCClDeleted > 1000
273       && countCCls() > 3000)
274    {     
275      deleteConflictCls();
276      lastTimeCClDeleted = refTime;
277    }
278   
279    if(refTime - lastCClCleanUp > 35000 )
280    {
281      cleanUp_deletedCCls();
282      toSTDOUT("cleaned:"); printCClstats();   
283      lastCClCleanUp = refTime;
284    }
285   
286    //component cache delete old entries
287    if(CSolverConf::allowComponentCaching)
288      xFormulaCache.deleteEntries(decStack);
289     
290    do{   
291       if(decStack.top().getBranchSols() == 0.0)
292                removeAllCachePollutions(); 
293       
294       if(decStack.top().anotherCompProcessible())
295       { 
296         return PROCESS_COMPONENT;
297       }
298             
299       if(!decStack.top().isFlipped())
300       {             
301         aLit = decStack.TOS_decLit();
302         decStack.flipTOS();
303         bcpImplQueue.push_back(AntAndLit(NOT_A_CLAUSE,aLit.oppositeLit()));
304         return RESOLVED;   
305       }
306   
307       //include the component value of the current component into the Cache
308       if(CSolverConf::allowComponentCaching)
309       {   
310         xFormulaCache.include(decStack.TOSRefComp(), decStack.top().getOverallSols());
311       } 
312           
313    } while(decStack.pop());
314   
315    return EXIT;
316}
317
318
319
320bool CMainSolver::bcp()
321{   
322    bool bSucceeded;   
323       
324    vector<LiteralIdT>::iterator it;             
325   
326    //BEGIN process unit clauses
327    for(it = theUnitClauses.begin(); it != theUnitClauses.end(); it++)
328    {     
329     if(getVar(*it).isActive())           
330        bcpImplQueue.push_back(AntAndLit(NOT_A_CLAUSE, *it));             
331     
332     if(isUnitCl(it->oppositeLit()))
333     {       
334       // dealing with opposing unit clauses is handed over to
335       // resolveConflict
336       return false; 
337     }         
338    }   
339    //END process unit clauses
340   
341    bSucceeded = BCP(bcpImplQueue);
342    bcpImplQueue.clear();
343   
344    if(CSolverConf::allowImplicitBCP
345        && bSucceeded )
346      {         
347         bSucceeded = implicitBCP();                     
348      }
349   
350    theRunAn.addValue(IMPLICATION, decStack.getDL(),
351                      decStack.TOS_countImplLits());   
352   
353   
354    return bSucceeded;
355}
356
357
358retStateT CMainSolver::resolveConflict()
359{   
360   int backtrackDecLev;         
361   
362   for(vector<LiteralIdT>::iterator it = theUnitClauses.begin(); it != theUnitClauses.end(); it++)
363    {   
364     if(isUnitCl(it->oppositeLit()))
365     {
366       toSTDOUT("\nOPPOSING UNIT CLAUSES - INSTANCE UNSAT\n");
367       return EXIT; 
368     }         
369    }
370       
371   theRunAn.addValue(CONFLICT,  decStack.getDL(), 1);
372           
373   #ifdef DEBUG
374    assert(!getConflicted().empty());
375   #endif
376   
377   if(!CSolverConf::analyzeConflicts || getConflicted().empty())
378          return backTrack(); 
379           
380   caGetCauses_firstUIP(getConflicted());       
381   backtrackDecLev = getMaxDecLevFromAnalysis();       
382   
383   
384     
385   if(ca_1UIPClause.size() < ca_lastUIPClause.size()) 
386      create1UIPCCl(); 
387   //BEGIN Backtracking
388     
389    if(backtrackDecLev < decStack.getDL())
390    {     
391      if(CSolverConf::doNonChronBackTracking) 
392       while(decStack.getDL() > backtrackDecLev)
393       {         
394         /// check for polluted cache Entries
395         removeAllCachePollutions();         
396         ///         
397         decStack.pop();
398       }
399      return backTrack();
400       
401    } 
402     
403    // maybe the other branch had some solutions
404    if(decStack.top().isFlipped()) 
405    {       
406       return backTrack();     
407    } 
408   
409    // now: if the other branch has to be visited:
410   
411    createAntClauseFor(decStack.TOS_decLit().oppositeLit());
412     
413    LiteralIdT aLit = decStack.TOS_decLit();
414    AntecedentT ant = getVar(aLit).getAntecedent();
415    decStack.flipTOS();   
416   
417    bcpImplQueue.push_back(AntAndLit(ant,aLit.oppositeLit()));             
418    //END Backtracking
419    return RESOLVED;   
420}
421
422
423
424/////////////////////////////////////////////////////
425// BEGIN component analysis
426/////////////////////////////////////////////////////
427
428
429
430bool CMainSolver::recordRemainingComps()
431{
432  // the refComp has to be copied!! because in case that the vector
433  // containing it has to realloc (which might happen here)
434  // copying the refcomp is not necessary anymore, as the allCompsStack is a vector
435  // of pointers - realloc does not invalidate these
436  CComponentId & refSupComp = decStack.TOSRefComp(); 
437 
438  viewStateT lookUpCls[getMaxOriginalClIdx()+2];         
439  viewStateT lookUpVars[countAllVars()+2];       
440 
441  memset(lookUpCls,NIL,sizeof(viewStateT)*(getMaxOriginalClIdx()+2)); 
442  memset(lookUpVars,NIL,sizeof(viewStateT)*(countAllVars()+2));
443 
444  vector<VarIdT>::const_iterator vt; 
445  vector<ClauseIdT>::const_iterator itCl;
446 
447  for(itCl = refSupComp.clsBegin(); *itCl != clsSENTINEL; itCl++)
448  {   
449     lookUpCls[*itCl] = IN_SUP_COMP;     
450  }
451   
452  for(vt = refSupComp.varsBegin(); *vt != varsSENTINEL; vt++)
453  {
454    if(getVar(*vt).isActive())
455    {
456     lookUpVars[*vt] = IN_SUP_COMP;
457     getVar(*vt).scoreDLIS[true] = 0;
458     getVar(*vt).scoreDLIS[false] = 0;
459    }
460  }
461 
462  vector<LiteralIdT>::const_iterator itL; 
463 
464  for(vt = refSupComp.varsBegin(); *vt != varsSENTINEL; vt++)
465   if(lookUpVars[*vt] == IN_SUP_COMP)
466   {
467     decStack.TOS_addRemComp();
468   
469     getComp(*vt, decStack.TOSRefComp(), lookUpCls, lookUpVars);   
470   } 
471 
472 
473  decStack.TOS_sortRemComps();
474  return true;
475}
476
477
478
479
480bool CMainSolver::getComp(const VarIdT &theVar, 
481                            const CComponentId &superComp,
482                            viewStateT lookUpCls[], 
483                            viewStateT lookUpVars[])
484{ 
485  componentSearchStack.clear();         
486     
487  lookUpVars[theVar] = SEEN; 
488  componentSearchStack.push_back(theVar); 
489  vector<VarIdT>::const_iterator vt,itVEnd; 
490     
491  vector<LiteralIdT>::const_iterator itL;
492  vector<ClauseIdT>::const_iterator itCl;         
493 
494  CVariableVertex * pActVar;
495 
496  unsigned int nClausesSeen = 0, nBinClsSeen = 0; 
497 
498  for(vt = componentSearchStack.begin(); vt !=componentSearchStack.end();vt++)
499  // the for-loop is applicable here because componentSearchStack.capacity() == countAllVars()
500  {   
501    pActVar = &getVar(*vt);   
502   //BEGIN traverse binary clauses
503   for(itL =pActVar->getBinLinks(true).begin();*itL != SENTINEL_LIT;itL++)
504    if(lookUpVars[itL->toVarIdx()] == IN_SUP_COMP)
505    {
506       nBinClsSeen++;
507       lookUpVars[itL->toVarIdx()] = SEEN;
508       componentSearchStack.push_back(itL->toVarIdx());
509       getVar(*itL).scoreDLIS[itL->polarity()]++;
510       pActVar->scoreDLIS[true]++; 
511    }
512   for(itL =pActVar->getBinLinks(false).begin();*itL != SENTINEL_LIT;itL++)
513    if(lookUpVars[itL->toVarIdx()] == IN_SUP_COMP)
514    {
515       nBinClsSeen++;
516       lookUpVars[itL->toVarIdx()] = SEEN;
517       componentSearchStack.push_back(itL->toVarIdx());
518       getVar(*itL).scoreDLIS[itL->polarity()]++;
519       pActVar->scoreDLIS[false]++; 
520    }
521   //END traverse binary clauses
522   
523   
524   for(itCl = var_InClsBegin(*pActVar); *itCl != SENTINEL_CL; itCl++)   
525    if(lookUpCls[*itCl] == IN_SUP_COMP)
526    {   
527       itVEnd = componentSearchStack.end();
528       for(itL = begin(getClause(*itCl)); *itL != ClauseEnd(); itL++)       
529         if(lookUpVars[itL->toVarIdx()] == NIL) //i.e. the var is not active
530         {   
531            if(!isSatisfied(*itL)) continue;     
532            //BEGIN accidentally entered a satisfied clause: undo the search process
533            while(componentSearchStack.end() != itVEnd)
534            {
535               lookUpVars[componentSearchStack.back()] = IN_SUP_COMP;
536               componentSearchStack.pop_back();
537            }
538            lookUpCls[*itCl] = NIL;
539            for(vector<LiteralIdT>::iterator itX = begin(getClause(*itCl));itX != itL; itX++)
540            {
541             if(getVar(*itX).scoreDLIS[itX->polarity()] > 0) getVar(*itX).scoreDLIS[itX->polarity()]--; 
542            }
543            //END accidentally entered a satisfied clause: undo the search process
544            break;
545             
546         }else{
547         
548          getVar(*itL).scoreDLIS[itL->polarity()]++; 
549          if(lookUpVars[itL->toVarIdx()] == IN_SUP_COMP)
550           {         
551              lookUpVars[itL->toVarIdx()] = SEEN;           
552              componentSearchStack.push_back(itL->toVarIdx());
553           }
554           }
555         
556           
557      if(lookUpCls[*itCl] == NIL) continue;
558      nClausesSeen++; 
559      lookUpCls[*itCl] = SEEN;         
560    }       
561  }
562   
563  /////////////////////////////////////////////////
564  // BEGIN store variables in resComp
565  /////////////////////////////////////////////////
566 
567  decStack.lastComp().reserveSpace(componentSearchStack.size(), nClausesSeen); 
568 
569  for(vt = superComp.varsBegin(); *vt != varsSENTINEL; vt++)
570   if(lookUpVars[*vt] == SEEN) //we have to put a var into our component
571    {
572        decStack.lastComp().addVar(*vt);       
573        lookUpVars[*vt] = IN_OTHER_COMP;
574    } 
575 
576  decStack.lastComp().addVar(varsSENTINEL);         
577 
578  /////////////////////////////////////////////////
579  // END store variables in resComp
580  /////////////////////////////////////////////////
581 
582  for(itCl = superComp.clsBegin(); *itCl != clsSENTINEL; itCl++)
583    if(lookUpCls[*itCl] == SEEN)
584    {
585       decStack.lastComp().addCl(*itCl);             
586       lookUpCls[*itCl] = IN_OTHER_COMP;
587    }
588  decStack.lastComp().addCl(clsSENTINEL); 
589  decStack.lastComp().setTrueClauseCount(nClausesSeen + nBinClsSeen);
590 
591  return true;
592}
593
594
595
596/////////////////////////////////////////////////////
597// END component analysis
598/////////////////////////////////////////////////////
599
600
601void CMainSolver::makeCompIdFromActGraph(CComponentId& rComp)
602{
603   DepositOfClauses::iterator it;
604   DepositOfVars::iterator jt;
605   
606   rComp.clear();
607   unsigned int nBinClauses = 0;
608   unsigned int idx = 1;
609   for(it = beginOfClauses(); it != endOfClauses(); it++, idx++)
610   {
611      #ifdef DEBUG
612      assert(!it->isDeleted()); // deleted Cls should be cleaned by prepCleanPool
613      #endif
614      rComp.addCl(ClauseIdT(idx));       
615   }
616   rComp.addCl(clsSENTINEL);
617   idx = 1; 
618   for(jt = beginOfVars(); jt != endOfVars();jt++, idx++)
619   {   
620     #ifdef DEBUG
621     assert(jt->isActive()); // deleted Vars should be cleaned by prepCleanPool
622     #endif
623     rComp.addVar(idx);     
624     nBinClauses += countActiveBinLinks(idx);
625   
626   }
627   rComp.addVar(varsSENTINEL);
628   
629   nBinClauses >>=1; 
630   rComp.setTrueClauseCount(nBinClauses + rComp.countCls()); 
631}
632
633
634void CMainSolver::printComponent(const CComponentId& rComp)
635{
636  vector<ClauseIdT>::const_iterator it; 
637  for(it = rComp.clsBegin(); *it != clsSENTINEL;it++)
638  {
639    printActiveClause(*it);
640  }
641}
642
643
644
645
646///////////////////////////////////////////////
647
648bool CMainSolver::BCP(vector<AntAndLit> &thePairsOfImpl)
649{
650   extd_vector<ClauseIdT>* pUnWatchCls;
651   extd_vector<ClauseIdT>::iterator it;
652   bool retV;
653   ClauseIdT actCl;
654   PCLV pCl;
655   vector<LiteralIdT>::const_iterator bt;
656   vector<LiteralIdT>::iterator itL;
657   LiteralIdT satLit,unLit;
658   
659   getConflicted().clear();
660   
661   for(unsigned int i = 0; i < thePairsOfImpl.size();i++)
662    if(assignVal(thePairsOfImpl[i].getLit(),thePairsOfImpl[i].getAnt()))
663    {     
664       satLit = thePairsOfImpl[i].getLit();
665       unLit = thePairsOfImpl[i].getLit().oppositeLit();
666       decStack.TOS_addImpliedLit(satLit);
667       
668       pUnWatchCls = &getVar(unLit).getWatchClauses(unLit.polarity());
669       
670       //BEGIN Propagate Bin Clauses
671       for(bt = getVar(unLit).getBinLinks(unLit.polarity()).begin(); *bt != SENTINEL_LIT;bt++)         
672       {
673          if(getVar(*bt).isActive()) thePairsOfImpl.push_back(AntAndLit(unLit,*bt));
674          else if(!isSatisfied(*bt))
675          {
676             getConflicted().push_back(unLit);
677             getConflicted().push_back(*bt);
678             return false;
679          }
680       }
681       for(bt = bt+1; *bt != SENTINEL_LIT;bt++)
682       {
683          if(getVar(*bt).isActive()) thePairsOfImpl.push_back(AntAndLit(unLit,*bt));
684          else if(!isSatisfied(*bt))
685          {
686             getConflicted().push_back(unLit);
687             getConflicted().push_back(*bt);
688             return false;
689          }
690       }
691       //END Propagate Bin Clauses
692       
693       for(it = pUnWatchCls->end()-1; *it != SENTINEL_CL; it--)
694       {
695          actCl = *it;
696          pCl = &getClause(actCl);   
697          // all clauses treated as conflict clauses, because no subsumption
698          // is being performed
699          if(isSatisfied(pCl->idLitA()) || isSatisfied(pCl->idLitB())) continue;
700          ///////////////////////////////////////
701          //BEGIN update watched Lits
702          ///////////////////////////////////////
703          retV = false;
704          for(itL = begin(*pCl); *itL != ClauseEnd(); itL++)
705          if(getVar(*itL).isActive() || isSatisfied(*itL))
706          {
707             if(*itL == pCl->idLitA() || *itL == pCl->idLitB()) continue;
708             retV = isSatisfied(*itL);
709             getVar(*itL).addWatchClause(actCl,itL->polarity());
710             if(pCl->idLitA() == unLit)
711                pCl->setLitA(*itL);
712             else
713                pCl->setLitB(*itL);
714             pUnWatchCls->quickErase(it);
715             break;
716          }     
717          if(retV) continue; // i.e. clause satisfied           
718          ///////////////////////////////////////
719          //END update watched Lits
720          ///////////////////////////////////////     
721         
722          if(getVar(pCl->idLitA()).isActive())
723          {
724             if(!getVar(pCl->idLitB()).isActive()) //IMPLIES_LITA;
725             {
726                thePairsOfImpl.push_back(AntAndLit(actCl,pCl->idLitA()));
727                pCl->setTouched();
728             }
729          }
730          else
731          {
732             pCl->setTouched();
733             if(getVar(pCl->idLitB()).isActive()) //IMPLIES_LITB;
734                thePairsOfImpl.push_back(AntAndLit(actCl,pCl->idLitB()));
735             else  //provided that SATISFIED has been tested                   
736             {
737                getConflicted().push_back(actCl);
738                return false;
739             }
740         }
741      }
742    }   
743    return true; 
744}
745
746
747bool CMainSolver::createAntClauseFor(const LiteralIdT &Lit)
748{
749        const vector<LiteralIdT> &actCCl = caGetPrevLastUIPCCl();
750   
751        bool created = createLastUIPCCl(); 
752 
753        if(!created && actCCl.size() != 2) return false; 
754 
755        if(actCCl.size() == 1) 
756        {
757          getVar(Lit).adjustAntecedent(NOT_A_CLAUSE);
758          return true; // theLit has become a unit clause: nothing to be done
759        } 
760        if(actCCl.size() == 2)
761        {
762                #ifdef DEBUG
763                assert(actCCl.front() != Lit.oppositeLit());
764                assert(actCCl.back() != Lit.oppositeLit());
765                #endif
766               
767                if(actCCl.front() == Lit)
768                        getVar(Lit).adjustAntecedent(AntecedentT(actCCl.back()));               
769                else if(actCCl.back() == Lit)   
770                        getVar(Lit).adjustAntecedent(AntecedentT(actCCl.front()));   
771   
772                return true;
773        }
774        setCClImplyingLit(getLastClauseId(),Lit);       
775        getVar(Lit).adjustAntecedent(AntecedentT(getLastClauseId()));   
776        return true;
777}
778
779bool CMainSolver::implicitBCP()
780{
781   vector<LiteralIdT>::iterator jt;
782   vector<LiteralIdT>::const_iterator it,lt;   
783   vector<ClauseIdT>::const_iterator ct;   
784
785   static vector<AntAndLit> implPairs;   
786   implPairs.clear();
787   vector<LiteralIdT> nextStep; 
788   bool viewedLits[(countAllVars()+1)*2 +1];   
789   LiteralIdT newLit;
790   AntecedentT theAnt, nant;
791   LiteralIdT theLit,nlit;
792   implPairs.reserve(decStack.TOSRefComp().countVars());       
793   nextStep.reserve(decStack.TOSRefComp().countVars());
794   int allFound = 0;
795   bool bsat;
796   
797   int impOfs = 0; 
798   int step;
799   do{ 
800      if(decStack.TOS_countImplLits() - impOfs > 0) 
801      {
802         memset(viewedLits,false,sizeof(bool)*((countAllVars()+1)*2 +1));
803         nextStep.clear();
804         for(it = decStack.TOS_ImpliedLits_begin()+ impOfs; it != decStack.TOS_ImpliedLits_end(); it++)
805         { 
806            step = var_InClsStep(!it->polarity());           
807            for(ct = var_InClsStart(it->toVarIdx(),!it->polarity()); *ct != SENTINEL_CL; ct+= step)
808            {
809               bsat = false;
810               for(lt = begin(getClause(*ct));*lt != ClauseEnd(); lt++)
811                {
812                  if(isSatisfied(*lt)) { bsat = true; break; }                   
813                }
814               
815               if(bsat) continue;
816               for(lt = begin(getClause(*ct));*lt != ClauseEnd(); lt++)
817                if(getVar(*lt).isActive() && !viewedLits[lt->toUInt()])
818                {
819                   nextStep.push_back(*lt);
820                   viewedLits[lt->toUInt()] = true;
821                }
822            }           
823         }
824      }
825      impOfs = decStack.TOS_countImplLits();
826     
827      for(jt = nextStep.begin(); jt != nextStep.end(); jt++)
828       if(getVar(*jt).isActive())
829       {
830         implPairs.push_back(AntAndLit(NOT_A_CLAUSE,jt->oppositeLit()));       
831         // BEGIN BCPROPAGATIONNI
832         unsigned int sz = decStack.countAllImplLits();
833         
834         // we increase the decLev artificially
835         // s.t. after the tentative BCP call, we can learn a conflict clause
836         // relative to the assignment of *jt
837         decStack.beginTentative();
838         
839         bool bSucceeded = BCP(implPairs);       
840         
841         
842         decStack.shrinkImplLitsTo(sz);
843         theAnt = NOT_A_CLAUSE;
844         theLit = implPairs[0].getLit();
845                 
846         if(!bSucceeded && CSolverConf::analyzeConflicts
847            && !getConflicted().empty())
848         {
849           
850            caGetCauses_lastUIP(getConflicted());   
851           
852            createAntClauseFor(theLit.oppositeLit());           
853            //createLastUIPCCl();
854           
855            theRunAn.addValue(IBCPIMPL,decStack.getDL(),1);
856            theAnt = getVar(theLit).getAntecedent();
857           
858         }
859         decStack.endTentative();
860         
861         for(vector<AntAndLit>::iterator at = implPairs.begin(); at != implPairs.end(); at++)
862            getVar(at->theLit).unsetVal(); 
863         implPairs.clear();
864   
865         if(!bSucceeded)
866         {
867            implPairs.push_back(AntAndLit(theAnt,theLit.oppositeLit()));         
868                   
869            if(!BCP(implPairs))
870            {
871             implPairs.clear();
872             return false;
873            } 
874         
875            implPairs.clear();         
876         }   
877      // END BCPROPAGATIONNI
878      }     
879      allFound += decStack.TOS_countImplLits() - impOfs; 
880     
881   }while(decStack.TOS_countImplLits() - impOfs > 0);   
882   return true;   
883}
884
885///////////////////////////////////////////////////////////////////////////////////////////////
886// BEGIN module conflictAnalyzer
887///////////////////////////////////////////////////////////////////////////////////////////////
888
889
890void CMainSolver::caIncludeCauses(LiteralIdT theLit, bool viewedVars[])
891{ 
892        vector<LiteralIdT>::const_iterator it; 
893       
894        ClauseIdT implCl;
895
896        if(!getVar(theLit).getAntecedent().isAClause())
897        {
898                LiteralIdT hlit;   
899                hlit = getVar(theLit).getAntecedent().toLit();   
900                caIncorporateLit(hlit,viewedVars); 
901                #ifdef DEBUG
902                assert(hlit != NOT_A_LIT); 
903                #endif
904                return;
905        }
906 
907        implCl = getVar(theLit).getAntecedent().toCl();
908 
909        if(implCl == NOT_A_CLAUSE) 
910        // theLit has not been implied, in fact this means that
911        // either theLit is the decided variable, a unit clause or
912        // a variable that has been tentatively assigned by ImplicitBCP
913        // other cases may not occur !
914        {   
915                caAddtoCauses(theLit,viewedVars);       
916                return;
917        }
918 
919        for(it = begin(getClause(implCl)); *it != ClauseEnd(); it ++)
920        {   
921                caIncorporateLit(*it,viewedVars);
922        }
923}
924///////////////////////////////////////////////////////////////////
925//
926//  BEGIN public
927//
928///////////////////////////////////////////////////////////////////
929
930void CMainSolver::caAddtoCauses(LiteralIdT theLit, bool viewedVars[])
931{   
932        viewedVars[theLit.toVarIdx()] = true; 
933     
934        ca_lastUIPClause.push_back(theLit.oppositeLit());
935   
936        if(getVar(theLit).getDLOD() > imaxDecLev) imaxDecLev = getVar(theLit).getDLOD();
937}
938
939void CMainSolver::caIncorporateLit(const LiteralIdT &Lit, bool viewedVars[])
940{   
941        if(Lit == NOT_A_LIT) return;
942       
943        if(!viewedVars[Lit.toVarIdx()])
944        {       
945                viewedVars[Lit.toVarIdx()] = true;
946                ////
947                getVar(Lit).scoreVSIDS[Lit.polarity()]++;
948                getVar(Lit).scoreVSIDS[Lit.oppositeLit().polarity()]++;
949                ////
950                if(getVar(Lit).getDLOD() == decStack.getDL())
951                {         
952                        theQueue.push_back(Lit.oppositeLit());   
953                }       
954                else caAddtoCauses(Lit.oppositeLit(),viewedVars); 
955        }
956}
957
958bool CMainSolver::caInit(vector<AntecedentT> & theConflicted, bool viewedVars[])
959{
960        vector<LiteralIdT>::const_iterator it;
961   
962        imaxDecLev = -1;
963     
964        ca_1UIPClause.clear();
965        ca_lastUIPClause.clear();
966   
967        theQueue.clear();       
968        theQueue.reserve(countAllVars()+1);
969   
970        ClauseIdT idConflCl;
971        LiteralIdT idConflLit;
972   
973        if(theConflicted[0].isAClause())
974        {
975                idConflCl = theConflicted[0].toCl();     
976               
977                for(it = begin(getClause(idConflCl)); *it != ClauseEnd(); it ++)
978                {   
979                        caIncorporateLit(*it,viewedVars);
980                }
981        }
982        else
983        {
984                if(theConflicted.size() < 2)
985                {
986                        toSTDOUT("error in getcauses bincl"<<endl);
987                        return false;     
988                }
989     
990                idConflLit = theConflicted[0].toLit();     
991                caIncorporateLit(idConflLit,viewedVars);
992                idConflLit = theConflicted[1].toLit();
993                caIncorporateLit(idConflLit,viewedVars);
994        }
995   
996        return true;
997}
998
999bool CMainSolver::caGetCauses_lastUIP(vector<AntecedentT> & theConflicted)
1000{
1001        vector<LiteralIdT>::const_iterator it;
1002        bool viewedVars[countAllVars()+1]; 
1003   
1004        memset(viewedVars,false,sizeof(bool)*(countAllVars()+1));     
1005   
1006        if(!caInit(theConflicted,viewedVars)) return false;
1007   
1008        for(unsigned int i = 0; i < theQueue.size();i++)
1009        {
1010                viewedVars[theQueue[i].toVarIdx()] = true;
1011                caIncludeCauses(theQueue[i], viewedVars);
1012        }
1013   
1014        // analyzer data
1015        theRunAn.addValue(CCL_lastUIP, decStack.getDL(),ca_lastUIPClause.size());
1016        return true;
1017}
1018
1019
1020bool CMainSolver::caGetCauses_firstUIP(vector<AntecedentT> & theConflicted)
1021{
1022        vector<LiteralIdT>::const_iterator it;
1023        bool viewedVars[countAllVars()+1];
1024   
1025        memset(viewedVars,false,sizeof(bool)*(countAllVars()+1)); 
1026   
1027        if(!caInit(theConflicted,viewedVars)) return false;
1028   
1029        bool pastfirstUIP = false;
1030   
1031        for(unsigned int i = 0; i < theQueue.size();i++)       
1032        { 
1033               
1034                if(i == theQueue.size()-1 && pastfirstUIP == false)
1035                {
1036                        pastfirstUIP = true;
1037       
1038                        ca_1UIPClause = ca_lastUIPClause;
1039       
1040                        ca_1UIPClause.push_back(theQueue.back().oppositeLit());             
1041                } 
1042                viewedVars[theQueue[i].toVarIdx()] = true;
1043                caIncludeCauses(theQueue[i], viewedVars);
1044        }   
1045        // analyzer data
1046        theRunAn.addValue(CCL_1stUIP, decStack.getDL(), ca_1UIPClause.size());       
1047        theRunAn.addValue(CCL_lastUIP, decStack.getDL(),ca_lastUIPClause.size());
1048   
1049        return true;
1050}
1051
1052///////////////////////////////////////////////////////////////////////////////////////////////
1053// END module conflictAnalyzer
1054///////////////////////////////////////////////////////////////////////////////////////////////
1055
1056
1057
1058////////////////////////////////////////////////////////////////////////
1059//
1060//  BEGIN Methods for Preprocessing
1061//
1062///////////////////////////////////////////////////////////////////////
1063
1064bool CMainSolver::prep_IBCP(vector<AntAndLit> &impls)
1065{   
1066        bool bSucceeded = false;   
1067   
1068        getConflicted().clear();
1069   
1070        unsigned int sz = decStack.countAllImplLits();
1071   
1072        bSucceeded = BCP(impls);
1073        decStack.shrinkImplLitsTo(sz);   
1074   
1075        vector<AntAndLit>::iterator it;
1076 
1077        for(it = impls.begin(); it != impls.end(); it++)
1078        {
1079                getVar(it->theLit).unsetVal();
1080        }
1081   
1082        impls.clear();   
1083        return bSucceeded;
1084}
1085
1086bool CMainSolver::prepFindHiddenBackBoneLits()
1087{
1088   DepositOfVars::iterator jt;                           
1089   vector<AntAndLit> implPairs;
1090   implPairs.reserve(countAllVars());   
1091   
1092   int foundInLoop = 0;
1093   int allFound = 0;
1094   
1095   do{
1096      foundInLoop = 0;
1097     
1098      for(jt = beginOfVars(); jt != endOfVars(); jt++)
1099       if(jt->isActive() && jt->countBinLinks() > 0)
1100       {
1101          if(jt->countBinLinks(false)>0) implPairs.push_back(AntAndLit(NOT_A_CLAUSE,jt->getLitIdT(true)));
1102          if((jt->countBinLinks(false)>0) && !prep_IBCP(implPairs))
1103          {
1104             foundInLoop++;
1105             if(!prepBCP(jt->getLitIdT(false))) return false;
1106          }
1107          else if(jt->countBinLinks(true)>0)
1108          {
1109             implPairs.push_back(AntAndLit(NOT_A_CLAUSE,jt->getLitIdT(false)));
1110             if(!prep_IBCP(implPairs))
1111             {
1112                foundInLoop++;
1113                if(!prepBCP(jt->getLitIdT(true))) return false;
1114             }
1115          }
1116       }             
1117       allFound += foundInLoop;       
1118       
1119   }while(foundInLoop != 0);   
1120   if(allFound != 0) toSTDOUT("found UCCL"<<allFound << endl);
1121   return true;   
1122}
1123
1124bool CMainSolver::prepBCP(LiteralIdT firstLit)
1125{
1126   vector<LiteralIdT> impls;   
1127   int step = 0;
1128   LiteralIdT unLit, satLit;
1129   
1130   impls.reserve(countAllVars());
1131   
1132   if(firstLit != NOT_A_LIT) impls.push_back(firstLit);   
1133   
1134   // prepare UnitClauses for BCP
1135   if(!theUnitClauses.empty())
1136   {
1137      impls.insert(impls.end(),theUnitClauses.begin(),theUnitClauses.end());   
1138      theUnitClauses.clear(); 
1139      theUClLookUp.clear();
1140   }
1141   
1142   vector<ClauseIdT>::iterator it;
1143   vector<ClauseIdT>::iterator itBegin;
1144   vector<LiteralIdT>::iterator lt;
1145   CVariableVertex *pV;   
1146   
1147   for(unsigned int i = 0; i < impls.size();i++)
1148    if(getVar(impls[i]).setVal(impls[i].polarity(), 0))
1149    {   
1150      unLit = impls[i].oppositeLit();
1151      satLit = impls[i];
1152      pV = &getVar(satLit);     
1153               
1154      // BEGIN propagation             
1155      for(lt = pV->getBinLinks(unLit.polarity()).begin(); *lt != SENTINEL_LIT;lt++)             
1156      {
1157         if(getVar(*lt).isActive()) impls.push_back(*lt);       
1158           else
1159            if(getVar(*lt).getboolVal() != lt->polarity()) return false;     
1160      }
1161      CClauseVertex *pCl;
1162     
1163      itBegin = var_InClsStart(unLit.toVarIdx(),unLit.polarity());
1164      step = var_InClsStep(unLit.polarity());
1165     
1166      for(it = itBegin; *it != SENTINEL_CL; it+= step)
1167       if(!getClause(*it).isDeleted()) 
1168       {
1169          pCl = &getClause(*it); 
1170          eraseLiteralFromCl(*it,unLit);       
1171          switch(getClause(*it).length())
1172          {
1173             case 0: return false;
1174             case 1: impls.push_back(*begin(*pCl));
1175                     break;
1176             case 2:
1177                     createBinCl((*begin(*pCl)),*(begin(*pCl)+1));                     
1178                     /// mark clause *it as deleted                     
1179                     
1180                     getVar(pCl->idLitB()).eraseWatchClause(*it, pCl->idLitB().polarity());
1181                     getVar(pCl->idLitA()).eraseWatchClause(*it, pCl->idLitA().polarity()); 
1182                     
1183                     for(vector<LiteralIdT>::iterator litt = begin(*pCl); *litt != ClauseEnd();litt++)
1184                     { 
1185                       if(*litt != unLit)                       
1186                       var_EraseClsLink(litt->toVarIdx(), litt->polarity(),*it); 
1187                       *litt = NOT_A_LIT;
1188                     } 
1189 
1190                     pCl->setDeleted();
1191                     
1192                     ///
1193                     break;
1194             default: break;
1195          };
1196       }
1197       //END propagation
1198       
1199       //BEGIN subsumption
1200       for(lt = pV->getBinLinks(satLit.polarity()).begin(); *lt != SENTINEL_LIT;lt++)
1201           getVar(*lt).eraseBinLinkTo(satLit,lt->polarity());       
1202       
1203      itBegin = var_InClsStart(satLit.toVarIdx(),satLit.polarity());
1204      step = var_InClsStep(satLit.polarity());
1205     
1206       for(it = itBegin; *it != SENTINEL_CL;it+= step)
1207       
1208         if(!getClause(*it).isDeleted())
1209         {
1210          pCl = &getClause(*it); 
1211          /// mark clause *it as deleted
1212                   
1213          getVar(pCl->idLitB()).eraseWatchClause(*it, pCl->idLitB().polarity());
1214          getVar(pCl->idLitA()).eraseWatchClause(*it, pCl->idLitA().polarity()); 
1215                 
1216          vector<LiteralIdT>::iterator litt; 
1217          for(litt = begin(*pCl); *litt != ClauseEnd();litt++)
1218          { 
1219             if(*litt != satLit) 
1220             // deleting ClauseEdges from satLit would be erroneous as it affects satPCl
1221                var_EraseClsLink(litt->toVarIdx(), litt->polarity(),*it); 
1222             *litt = NOT_A_LIT;
1223          } 
1224 
1225          pCl->setDeleted();                     
1226          ///
1227         } 
1228       // END subsumption
1229       
1230       for(it = var_InClsBegin(unLit.toVarIdx(),false);*it != SENTINEL_CL;it++)
1231       {
1232         *it = SENTINEL_CL;
1233       }
1234       
1235       pV->eraseAllEdges();           
1236   }     
1237   return true; 
1238}
1239
1240
1241////////////////////////////////////////////////////////////////////////
1242//
1243//  END Methods for Preprocessing
1244//
1245///////////////////////////////////////////////////////////////////////
1246
1247
1248bool CMainSolver::printUnitClauses()
1249{   
1250        vector<LiteralIdT>::iterator it,jt;     
1251   
1252        toSTDOUT("UCCL:\n");
1253        for(it = theUnitClauses.begin(); it != theUnitClauses.end(); it++)
1254        {     
1255                toSTDOUT((it->polarity()?" ":"-")<<getVar(*it).getVarNum()<< " 0\n");     
1256        }
1257        toSTDOUT(endl);   
1258             
1259        return true;
1260}
Note: See TracBrowser for help on using the repository browser.