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

Last change on this file since 70 was 9, checked in by cecile, 15 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.