From ae9a4407c4abf4200365faceb9d8cac0d99236b3 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 25 Apr 2013 16:02:40 -0700 Subject: Adding rollback for the other solver. --- src/sat/bsat/satSolver.c | 119 +++++++++++++++++++++++++++++++++++++++++++++- src/sat/bsat/satSolver.h | 21 ++++++++ src/sat/bsat/satSolver2.c | 4 +- 3 files changed, 141 insertions(+), 3 deletions(-) (limited to 'src/sat') diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index ab1203ea..8f3098d8 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -531,6 +531,26 @@ static void sat_solver_canceluntil(sat_solver* s, int level) { veci_resize(&s->trail_lim,level); } +static void sat_solver_canceluntil_rollback(sat_solver* s, int NewBound) { + int c, x; + + assert( sat_solver_dl(s) == 0 ); + assert( s->qtail == s->qhead ); + assert( s->qtail >= NewBound ); + + for (c = s->qtail-1; c >= NewBound; c--) + { + x = lit_var(s->trail[c]); + var_set_value(s, x, varX); + s->reasons[x] = 0; + } + + for (c = s->qhead-1; c >= NewBound; c--) + order_unassigned(s,lit_var(s->trail[c])); + + s->qhead = s->qtail = NewBound; +} + static void sat_solver_record(sat_solver* s, veci* cls) { lit* begin = veci_begin(cls); @@ -1011,6 +1031,7 @@ void sat_solver_setnvars(sat_solver* s,int n) s->activity = ABC_REALLOC(double, s->activity, s->cap); #else s->activity = ABC_REALLOC(unsigned, s->activity, s->cap); + s->activity2 = ABC_REALLOC(unsigned, s->activity2,s->cap); #endif if ( s->factors ) s->factors = ABC_REALLOC(double, s->factors, s->cap); @@ -1084,6 +1105,7 @@ void sat_solver_delete(sat_solver* s) ABC_FREE(s->polarity ); ABC_FREE(s->tags ); ABC_FREE(s->activity ); + ABC_FREE(s->activity2); ABC_FREE(s->factors ); ABC_FREE(s->orderpos ); ABC_FREE(s->reasons ); @@ -1095,7 +1117,7 @@ void sat_solver_delete(sat_solver* s) ABC_FREE(s); } -void sat_solver_rollback( sat_solver* s ) +void sat_solver_restart( sat_solver* s ) { int i; Sat_MemRestart( &s->Mem ); @@ -1160,6 +1182,8 @@ double sat_solver_memory( sat_solver* s ) Mem += s->cap * sizeof(double); // ABC_FREE(s->activity ); #else Mem += s->cap * sizeof(unsigned); // ABC_FREE(s->activity ); + if ( s->activity2 ) + Mem += s->cap * sizeof(unsigned); // ABC_FREE(s->activity2); #endif if ( s->factors ) Mem += s->cap * sizeof(double); // ABC_FREE(s->factors ); @@ -1305,6 +1329,99 @@ void sat_solver_reducedb(sat_solver* s) } } + +// reverses to the previously bookmarked point +void sat_solver_rollback( sat_solver* s ) +{ + Sat_Mem_t * pMem = &s->Mem; + int i, k, j; + static int Count = 0; + Count++; + assert( s->iVarPivot >= 0 && s->iVarPivot <= s->size ); + assert( s->iTrailPivot >= 0 && s->iTrailPivot <= s->qtail ); + // reset implication queue + sat_solver_canceluntil_rollback( s, s->iTrailPivot ); + // update order + if ( s->iVarPivot < s->size ) + { + if ( s->activity2 ) + { + s->var_inc = s->var_inc2; + memcpy( s->activity, s->activity2, sizeof(unsigned) * s->iVarPivot ); + } + veci_resize(&s->order, 0); + for ( i = 0; i < s->iVarPivot; i++ ) + { + if ( var_value(s, i) != varX ) + continue; + s->orderpos[i] = veci_size(&s->order); + veci_push(&s->order,i); + order_update(s, i); + } + } + // compact watches + for ( i = 0; i < s->iVarPivot*2; i++ ) + { + cla* pArray = veci_begin(&s->wlists[i]); + for ( j = k = 0; k < veci_size(&s->wlists[i]); k++ ) + if ( Sat_MemClauseUsed(pMem, pArray[k]) ) + pArray[j++] = pArray[k]; + veci_resize(&s->wlists[i],j); + } + // reset watcher lists + for ( i = 2*s->iVarPivot; i < 2*s->size; i++ ) + s->wlists[i].size = 0; + + // reset clause counts + s->stats.clauses = pMem->BookMarkE[0]; + s->stats.learnts = pMem->BookMarkE[1]; + // rollback clauses + Sat_MemRollBack( pMem ); + + // resize learned arrays + veci_resize(&s->act_clas, s->stats.learnts); + + // initialize other vars + s->size = s->iVarPivot; + if ( s->size == 0 ) + { + // s->size = 0; + // s->cap = 0; + s->qhead = 0; + s->qtail = 0; +#ifdef USE_FLOAT_ACTIVITY + s->var_inc = 1; + s->cla_inc = 1; + s->var_decay = (float)(1 / 0.95 ); + s->cla_decay = (float)(1 / 0.999 ); +#else + s->var_inc = (1 << 5); + s->cla_inc = (1 << 11); +#endif + s->root_level = 0; + s->random_seed = 91648253; + s->progress_estimate = 0; + s->verbosity = 0; + + s->stats.starts = 0; + s->stats.decisions = 0; + s->stats.propagations = 0; + s->stats.inspects = 0; + s->stats.conflicts = 0; + s->stats.clauses = 0; + s->stats.clauses_literals = 0; + s->stats.learnts = 0; + s->stats.learnts_literals = 0; + s->stats.tot_literals = 0; + + // initialize rollback + s->iVarPivot = 0; // the pivot for variables + s->iTrailPivot = 0; // the pivot for trail + s->hProofPivot = 1; // the pivot for proof records + } +} + + int sat_solver_addclause(sat_solver* s, lit* begin, lit* end) { lit *i,*j; diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index 56936088..acaceef9 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -47,6 +47,7 @@ extern void sat_solver_delete(sat_solver* s); extern int sat_solver_addclause(sat_solver* s, lit* begin, lit* end); extern int sat_solver_simplify(sat_solver* s); extern int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal); +extern void sat_solver_restart( sat_solver* s ); extern void sat_solver_rollback( sat_solver* s ); extern int sat_solver_nvars(sat_solver* s); @@ -101,6 +102,11 @@ struct sat_solver_t veci* wlists; // watcher lists veci act_clas; // contain clause activities + // rollback + int iVarPivot; // the pivot for variables + int iTrailPivot; // the pivot for trail + int hProofPivot; // the pivot for proof records + // activities #ifdef USE_FLOAT_ACTIVITY double var_inc; // Amount to bump next variable with. @@ -110,8 +116,10 @@ struct sat_solver_t double* activity; // A heuristic measurement of the activity of a variable. #else int var_inc; // Amount to bump next variable with. + int var_inc2; // Amount to bump next variable with. int cla_inc; // Amount to bump next clause with. unsigned* activity; // A heuristic measurement of the activity of a variable. + unsigned* activity2; // backup variable activity #endif // varinfo * vi; // variable information @@ -227,6 +235,19 @@ static int sat_solver_set_random(sat_solver* s, int fNotUseRandom) return fNotUseRandomOld; } +static inline void sat_solver_bookmark(sat_solver* s) +{ + assert( s->qhead == s->qtail ); + s->iVarPivot = s->size; + s->iTrailPivot = s->qhead; + Sat_MemBookMark( &s->Mem ); + if ( s->activity2 ) + { + s->var_inc2 = s->var_inc; + memcpy( s->activity2, s->activity, sizeof(unsigned) * s->iVarPivot ); + } +} + static inline int sat_solver_add_const( sat_solver * pSat, int iVar, int fCompl ) { lit Lits[1]; diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index 951940b3..a3dad126 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -1638,7 +1638,7 @@ void sat_solver2_rollback( sat_solver2* s ) // s->cap = 0; s->qhead = 0; s->qtail = 0; -#ifdef USE_FLOAT_ACTIVITY +#ifdef USE_FLOAT_ACTIVITY2 s->var_inc = 1; s->cla_inc = 1; s->var_decay = (float)(1 / 0.95 ); @@ -1689,7 +1689,7 @@ double sat_solver2_memory( sat_solver2* s, int fAll ) Mem += s->cap * sizeof(varinfo2); // ABC_FREE(s->vi ); Mem += s->cap * sizeof(int); // ABC_FREE(s->levels ); Mem += s->cap * sizeof(char); // ABC_FREE(s->assigns ); -#ifdef USE_FLOAT_ACTIVITY +#ifdef USE_FLOAT_ACTIVITY2 Mem += s->cap * sizeof(double); // ABC_FREE(s->activity ); #else Mem += s->cap * sizeof(unsigned); // ABC_FREE(s->activity ); -- cgit v1.2.3