diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2020-11-14 22:45:23 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2020-11-14 22:45:23 -0800 |
| commit | 581f2e59721498880d20c85444c2358e6c7c97e9 (patch) | |
| tree | af3207feb533522a08b540787cde131f730c29fc /src/sat/glucose2 | |
| parent | f95476b45d8846140f02acd5f60fd1a1e654a28e (diff) | |
| download | abc-581f2e59721498880d20c85444c2358e6c7c97e9.tar.gz abc-581f2e59721498880d20c85444c2358e6c7c97e9.tar.bz2 abc-581f2e59721498880d20c85444c2358e6c7c97e9.zip | |
Improvements to the SAT solver.
Diffstat (limited to 'src/sat/glucose2')
| -rw-r--r-- | src/sat/glucose2/Glucose2.cpp | 15 | ||||
| -rw-r--r-- | src/sat/glucose2/Solver.h | 2 |
2 files changed, 12 insertions, 5 deletions
diff --git a/src/sat/glucose2/Glucose2.cpp b/src/sat/glucose2/Glucose2.cpp index f32d1210..aa3d361f 100644 --- a/src/sat/glucose2/Glucose2.cpp +++ b/src/sat/glucose2/Glucose2.cpp @@ -1153,6 +1153,13 @@ lbool Solver::search(int nof_conflicts) for (;;){ CRef confl = propagate(); + + // exact conflict limit + if ( !withinBudget() && confl != CRef_Undef ) { + lbdQueue.fastclear(); + cancelUntil(0); + return l_Undef; } + if (confl != CRef_Undef){ // CONFLICT @@ -1395,15 +1402,15 @@ printf("c ==================================[ Search Statistics (every %6d confl if (status == l_True){ - if( justUsage() && false ){ + if( justUsage() ){ assert(jheap.empty()); //JustModel.growTo(nVars()); - int i = 0; + int i = 0, j = 0; JustModel.push(toLit(0)); for (; i < trail.size(); i++) if( isRoundWatch(var(trail[i])) && !isTwoFanin(var(trail[i])) ) - JustModel.push(trail[i]); - JustModel[0] = toLit(i); + JustModel.push(trail[i]), j++; + JustModel[0] = toLit(j); } else { // Extend & copy model: model.growTo(nVars()); diff --git a/src/sat/glucose2/Solver.h b/src/sat/glucose2/Solver.h index ab73dbc5..26b3bdcb 100644 --- a/src/sat/glucose2/Solver.h +++ b/src/sat/glucose2/Solver.h @@ -546,7 +546,7 @@ inline int Solver::nClauses () const { return clauses.size(); } inline int Solver::nLearnts () const { return learnts.size(); } inline int Solver::nVars () const { return vardata.size(); } inline int Solver::nFreeVars () const { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]); } -inline int * Solver::getCex () const { return NULL; } +inline int * Solver::getCex () const { return (int*) &JustModel[0]; } inline void Solver::setPolarity (Var v, bool b) { polarity[v] = b; } inline void Solver::setDecisionVar(Var v, bool b) { |