From f67c0c173d1cfd9b9f732471950124128fa7b317 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 9 Dec 2011 23:49:30 -0800 Subject: Changes to the main SAT solver: fixing performance bug (resetting decay params after each restart), making the SAT solver platform- and runtime-independent (by using interger-based activity). --- src/aig/fra/fraCec.c | 2 +- src/sat/bsat/satSolver.c | 528 +++++++++++++++++++++++++--------------------- src/sat/bsat/satSolver.h | 50 +---- src/sat/bsat/satSolver2.c | 40 ++-- src/sat/bsat/satSolver2.h | 27 +-- 5 files changed, 331 insertions(+), 316 deletions(-) (limited to 'src') diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c index 6e655590..38bf73d9 100644 --- a/src/aig/fra/fraCec.c +++ b/src/aig/fra/fraCec.c @@ -253,7 +253,7 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi pMan->pData = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize ); } // free the sat_solver - if ( fVerbose ) +// if ( fVerbose ) Sat_SolverPrintStats( stdout, pSat ); //sat_solver_store_write( pSat, "trace.cnf" ); //sat_solver_store_free( pSat ); diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index c448d8c3..97213e0d 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -29,23 +29,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA ABC_NAMESPACE_IMPL_START -#define SAT_USE_ANALYZE_FINAL - -/* -extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd ); -extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd ); -extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd ); -extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd ); -extern void * Sto_ManAlloc(); -extern void Sto_ManDumpClauses( void * p, char * pFileName ); -extern void Sto_ManFree( void * p ); -extern int Sto_ManChangeLastClause( void * p ); -extern void Sto_ManMarkRoots( void * p ); -extern void Sto_ManMarkClausesA( void * p ); -*/ - //#define SAT_USE_SYSTEM_MEMORY_MANAGEMENT - +#define SAT_USE_ANALYZE_FINAL //================================================================================================= // Debug: @@ -54,7 +39,7 @@ extern void Sto_ManMarkClausesA( void * p ); // For derivation output (verbosity level 2) #define L_IND "%-*d" -#define L_ind sat_solver_dlevel(s)*3+3,sat_solver_dlevel(s) +#define L_ind sat_solver_dlevel(s)*2+2,sat_solver_dlevel(s) #define L_LIT "%sx%d" #define L_lit(p) lit_sign(p)?"~":"", (lit_var(p)) @@ -100,11 +85,20 @@ struct clause_t lit lits[0]; }; -static inline int clause_size (clause* c) { return c->size_learnt >> 1; } -static inline lit* clause_begin (clause* c) { return c->lits; } -static inline int clause_learnt (clause* c) { return c->size_learnt & 1; } -static inline float clause_activity (clause* c) { return *((float*)&c->lits[c->size_learnt>>1]); } -static inline void clause_setactivity(clause* c, float a) { *((float*)&c->lits[c->size_learnt>>1]) = a; } +static inline int clause_size (clause* c) { return c->size_learnt >> 1; } +static inline lit* clause_begin (clause* c) { return c->lits; } +static inline int clause_learnt (clause* c) { return c->size_learnt & 1; } +static inline float clause_activity (clause* c) { return *((float*)&c->lits[c->size_learnt>>1]); } +static inline unsigned clause_activity2 (clause* c) { return *((unsigned*)&c->lits[c->size_learnt>>1]); } +static inline void clause_setactivity (clause* c, float a) { *((float*)&c->lits[c->size_learnt>>1]) = a; } +static inline void clause_setactivity2 (clause* c, unsigned a) { *((unsigned*)&c->lits[c->size_learnt>>1]) = a; } +static inline void clause_print (clause* c) { + int i; + printf( "{ " ); + for ( i = 0; i < clause_size(c); i++ ) + printf( "%d ", (clause_begin(c)[i] & 1)? -(clause_begin(c)[i] >> 1) : clause_begin(c)[i] >> 1 ); + printf( "}\n" ); +} //================================================================================================= // Encode literals in clause pointers: @@ -125,7 +119,6 @@ static inline vecp* sat_solver_read_wlist(sat_solver* s, lit l) { return &s->w static inline void order_update(sat_solver* s, int v) // updateorder { int* orderpos = s->orderpos; - double* activity = s->activity; int* heap = veci_begin(&s->order); int i = orderpos[v]; int x = heap[i]; @@ -133,7 +126,7 @@ static inline void order_update(sat_solver* s, int v) // updateorder assert(s->orderpos[v] != -1); - while (i != 0 && activity[x] > activity[heap[parent]]){ + while (i != 0 && s->activity[x] > s->activity[heap[parent]]){ heap[i] = heap[parent]; orderpos[heap[i]] = i; i = parent; @@ -161,7 +154,6 @@ static inline void order_unassigned(sat_solver* s, int v) // undoorder static inline int order_select(sat_solver* s, float random_var_freq) // selectvar { int* heap; - double* activity; int* orderpos; lbool* values = s->assigns; @@ -177,7 +169,6 @@ static inline int order_select(sat_solver* s, float random_var_freq) // selectv // Activity based decision: heap = veci_begin(&s->order); - activity = s->activity; orderpos = s->orderpos; @@ -191,19 +182,18 @@ static inline int order_select(sat_solver* s, float random_var_freq) // selectv orderpos[next] = -1; if (size > 0){ - double act = activity[x]; int i = 0; int child = 1; while (child < size){ - if (child+1 < size && activity[heap[child]] < activity[heap[child+1]]) + if (child+1 < size && s->activity[heap[child]] < s->activity[heap[child+1]]) child++; assert(child < size); - if (act >= activity[heap[child]]) + if (s->activity[x] >= s->activity[heap[child]]) break; heap[i] = heap[child]; @@ -226,62 +216,103 @@ static inline int order_select(sat_solver* s, float random_var_freq) // selectv //================================================================================================= // Activity functions: -static inline void act_var_rescale(sat_solver* s) { +#ifdef USE_FLOAT_ACTIVITY + +static inline void act_var_rescale(sat_solver* s) { double* activity = s->activity; int i; for (i = 0; i < s->size; i++) activity[i] *= 1e-100; s->var_inc *= 1e-100; } +static inline void act_clause_rescale(sat_solver* s) { + static int Total = 0; + clause** cs = (clause**)vecp_begin(&s->learnts); + int i, clk = clock(); + for (i = 0; i < vecp_size(&s->learnts); i++){ + float a = clause_activity(cs[i]); + clause_setactivity(cs[i], a * (float)1e-20); + } + s->cla_inc *= (float)1e-20; + Total += clock() - clk; + printf( "Rescaling... Cla inc = %10.3f Conf = %10d ", s->cla_inc, s->stats.conflicts ); + Abc_PrintTime( 1, "Time", Total ); +} static inline void act_var_bump(sat_solver* s, int v) { -// s->activity[v] += s->var_inc; - s->activity[v] += (s->pGlobalVars? 3.0 : 1.0) * s->var_inc; + s->activity[v] += s->var_inc; if (s->activity[v] > 1e100) act_var_rescale(s); - //printf("bump %d %f\n", v-1, activity[v]); if (s->orderpos[v] != -1) order_update(s,v); } - -static inline void act_var_bump_factor(sat_solver* s, int v) { - s->activity[v] += (s->var_inc * s->factors[v]); +static inline void act_var_bump_global(sat_solver* s, int v) { + s->activity[v] += (s->var_inc * 3.0 * s->pGlobalVars[v]); if (s->activity[v] > 1e100) act_var_rescale(s); - //printf("bump %d %f\n", v-1, activity[v]); if (s->orderpos[v] != -1) order_update(s,v); } - -static inline void act_var_bump_global(sat_solver* s, int v) { - s->activity[v] += (s->var_inc * 3.0 * s->pGlobalVars[v]); +static inline void act_var_bump_factor(sat_solver* s, int v) { + s->activity[v] += (s->var_inc * s->factors[v]); if (s->activity[v] > 1e100) act_var_rescale(s); - //printf("bump %d %f\n", v-1, activity[v]); if (s->orderpos[v] != -1) order_update(s,v); } +static inline void act_clause_bump(sat_solver* s, clause *c) { + float a = clause_activity(c) + s->cla_inc; + clause_setactivity(c,a); + if (a > 1e20) act_clause_rescale(s); +} +static inline void act_var_decay(sat_solver* s) { s->var_inc *= s->var_decay; } +static inline void act_clause_decay(sat_solver* s) { s->cla_inc *= s->cla_decay; } -static inline void act_var_decay(sat_solver* s) { s->var_inc *= s->var_decay; } +#else +static inline void act_var_rescale(sat_solver* s) { + unsigned* activity = s->activity; + int i; + for (i = 0; i < s->size; i++) + activity[i] >>= 19; + s->var_inc >>= 19; + s->var_inc = Abc_MaxInt( s->var_inc, (1<<4) ); +} static inline void act_clause_rescale(sat_solver* s) { + static int Total = 0; clause** cs = (clause**)vecp_begin(&s->learnts); - int i; + int i, clk = clock(); for (i = 0; i < vecp_size(&s->learnts); i++){ - float a = clause_activity(cs[i]); - clause_setactivity(cs[i], a * (float)1e-20); + unsigned a = clause_activity2(cs[i]); + clause_setactivity2(cs[i], a >> 14); } - s->cla_inc *= (float)1e-20; -} - + s->cla_inc >>= 14; + s->cla_inc = Abc_MaxInt( s->cla_inc, (1<<10) ); -static inline void act_clause_bump(sat_solver* s, clause *c) { - float a = clause_activity(c) + s->cla_inc; - clause_setactivity(c,a); - if (a > 1e20) act_clause_rescale(s); +// Total += clock() - clk; +// printf( "Rescaling... Cla inc = %5d Conf = %10d ", s->cla_inc, s->stats.conflicts ); +// Abc_PrintTime( 1, "Time", Total ); } +static inline void act_var_bump(sat_solver* s, int v) { + s->activity[v] += s->var_inc; + if (s->activity[v] & 0x80000000) + act_var_rescale(s); + if (s->orderpos[v] != -1) + order_update(s,v); +} +static inline void act_var_bump_global(sat_solver* s, int v) {} +static inline void act_var_bump_factor(sat_solver* s, int v) {} +static inline void act_clause_bump(sat_solver* s, clause*c) { + unsigned a = clause_activity2(c) + s->cla_inc; + clause_setactivity2(c,a); + if (a & 0x80000000) + act_clause_rescale(s); +} +static inline void act_var_decay(sat_solver* s) { s->var_inc += (s->var_inc >> 4); } +static inline void act_clause_decay(sat_solver* s) { s->cla_inc += (s->cla_inc >> 10); } + +#endif -static inline void act_clause_decay(sat_solver* s) { s->cla_inc *= s->cla_decay; } //================================================================================================= // Clause functions: @@ -306,7 +337,6 @@ static clause* clause_new(sat_solver* s, lit* begin, lit* end, int learnt) return NULL; } -// c = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float)); #ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT c = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float)); #else @@ -336,8 +366,6 @@ static clause* clause_new(sat_solver* s, lit* begin, lit* end, int learnt) vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)(size > 2 ? c : clause_from_lit(begin[1]))); vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)(size > 2 ? c : clause_from_lit(begin[0]))); -// if ( learnt ) -// printf( "%d ", size ); return c; } @@ -390,69 +418,26 @@ static lbool clause_simplify(sat_solver* s, clause* c) //================================================================================================= // Minor (solver) functions: -void sat_solver_setnvars(sat_solver* s,int n) -{ - int var; - - if (s->cap < n){ - - while (s->cap < n) s->cap = s->cap*2+1; - - s->wlists = ABC_REALLOC(vecp, s->wlists, s->cap*2); - s->activity = ABC_REALLOC(double, s->activity, s->cap); - s->factors = ABC_REALLOC(double, s->factors, s->cap); - s->assigns = ABC_REALLOC(lbool, s->assigns, s->cap); - s->orderpos = ABC_REALLOC(int, s->orderpos, s->cap); - s->reasons = ABC_REALLOC(clause*,s->reasons, s->cap); - s->levels = ABC_REALLOC(int, s->levels, s->cap); - s->tags = ABC_REALLOC(lbool, s->tags, s->cap); - s->trail = ABC_REALLOC(lit, s->trail, s->cap); - s->polarity = ABC_REALLOC(char, s->polarity, s->cap); - } - - for (var = s->size; var < n; var++){ - vecp_new(&s->wlists[2*var]); - vecp_new(&s->wlists[2*var+1]); - s->activity [var] = 0; - s->factors [var] = 0; - s->assigns [var] = l_Undef; - s->orderpos [var] = veci_size(&s->order); - s->reasons [var] = (clause*)0; - s->levels [var] = 0; - s->tags [var] = l_Undef; - s->polarity [var] = 0; - - /* does not hold because variables enqueued at top level will not be reinserted in the heap - assert(veci_size(&s->order) == var); - */ - veci_push(&s->order,var); - order_update(s, var); - } - - s->size = n > s->size ? n : s->size; -} - - static inline int enqueue(sat_solver* s, lit l, clause* from) { lbool* values = s->assigns; int v = lit_var(l); lbool val = values[v]; + lbool sig; #ifdef VERBOSEDEBUG printf(L_IND"enqueue("L_LIT")\n", L_ind, L_lit(l)); #endif - lbool sig = !lit_sign(l); sig += sig - 1; + sig = !lit_sign(l); sig += sig - 1; if (val != l_Undef){ return val == sig; }else{ + int* levels = s->levels; + clause** reasons = s->reasons; // New fact -- store it. #ifdef VERBOSEDEBUG printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(l)); #endif - int* levels = s->levels; - clause** reasons = s->reasons; - values [v] = sig; levels [v] = sat_solver_dlevel(s); reasons[v] = from; @@ -468,7 +453,8 @@ static inline int assume(sat_solver* s, lit l){ assert(s->qtail == s->qhead); assert(s->assigns[lit_var(l)] == l_Undef); #ifdef VERBOSEDEBUG - printf(L_IND"assume("L_LIT")\n", L_ind, L_lit(l)); + printf(L_IND"assume("L_LIT") ", L_ind, L_lit(l)); + printf( "act = %.20f\n", s->activity[lit_var(l)] ); #endif veci_push(&s->trail_lim,s->qtail); return enqueue(s,l,(clause*)0); @@ -852,6 +838,8 @@ clause* sat_solver_propagate(sat_solver* s) lbool* values = s->assigns; clause* confl = (clause*)0; lit* lits; + lit false_lit; + lbool sig; //printf("sat_solver_propagate\n"); while (confl == 0 && s->qtail - s->qhead > 0){ @@ -867,20 +855,24 @@ clause* sat_solver_propagate(sat_solver* s) //printf("checking lit %d: "L_LIT"\n", veci_size(ws), L_lit(p)); for (i = j = begin; i < end; ){ if (clause_is_lit(*i)){ -// s->stats.inspects2++; + + int Lit = clause_read_lit(*i); + sig = !lit_sign(Lit); sig += sig - 1; + if (values[lit_var(Lit)] == sig){ + *j++ = *i++; + continue; + } + *j++ = *i; if (!enqueue(s,clause_read_lit(*i),clause_from_lit(p))){ confl = s->binary; (clause_begin(confl))[1] = lit_neg(p); (clause_begin(confl))[0] = clause_read_lit(*i++); // Copy the remaining watches: -// s->stats.inspects2 += end - i; while (i < end) *j++ = *i++; } }else{ - lit false_lit; - lbool sig; lits = clause_begin(*i); @@ -915,7 +907,6 @@ clause* sat_solver_propagate(sat_solver* s) if (!enqueue(s,lits[0], *i)){ confl = *i++; // Copy the remaining watches: -// s->stats.inspects2 += end - i; while (i < end) *j++ = *i++; } @@ -963,133 +954,6 @@ void sat_solver_reducedb(sat_solver* s) vecp_resize(&s->learnts,j); } -static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT64_T nof_learnts) -{ - int* levels = s->levels; - double var_decay = 0.95; - double clause_decay = 0.999; - double random_var_freq = s->fNotUseRandom ? 0.0 : 0.02; - - ABC_INT64_T conflictC = 0; - veci learnt_clause; - int i; - - assert(s->root_level == sat_solver_dlevel(s)); - - s->nRestarts++; - s->stats.starts++; - s->var_decay = (float)(1 / var_decay ); - s->cla_decay = (float)(1 / clause_decay); - veci_resize(&s->model,0); - veci_new(&learnt_clause); - - // use activity factors in every even restart - if ( (s->nRestarts & 1) && veci_size(&s->act_vars) > 0 ) -// if ( veci_size(&s->act_vars) > 0 ) - for ( i = 0; i < s->act_vars.size; i++ ) - act_var_bump_factor(s, s->act_vars.ptr[i]); - - // use activity factors in every restart - if ( s->pGlobalVars && veci_size(&s->act_vars) > 0 ) - for ( i = 0; i < s->act_vars.size; i++ ) - act_var_bump_global(s, s->act_vars.ptr[i]); - - for (;;){ - clause* confl = sat_solver_propagate(s); - if (confl != 0){ - // CONFLICT - int blevel; - -#ifdef VERBOSEDEBUG - printf(L_IND"**CONFLICT**\n", L_ind); -#endif - s->stats.conflicts++; conflictC++; - if (sat_solver_dlevel(s) == s->root_level){ -#ifdef SAT_USE_ANALYZE_FINAL - sat_solver_analyze_final(s, confl, 0); -#endif - veci_delete(&learnt_clause); - return l_False; - } - - veci_resize(&learnt_clause,0); - sat_solver_analyze(s, confl, &learnt_clause); - blevel = veci_size(&learnt_clause) > 1 ? levels[lit_var(veci_begin(&learnt_clause)[1])] : s->root_level; - blevel = s->root_level > blevel ? s->root_level : blevel; - sat_solver_canceluntil(s,blevel); - sat_solver_record(s,&learnt_clause); -#ifdef SAT_USE_ANALYZE_FINAL -// if (learnt_clause.size() == 1) level[var(learnt_clause[0])] = 0; // (this is ugly (but needed for 'analyzeFinal()') -- in future versions, we will backtrack past the 'root_level' and redo the assumptions) - if ( learnt_clause.size == 1 ) s->levels[lit_var(learnt_clause.ptr[0])] = 0; -#endif - act_var_decay(s); - act_clause_decay(s); - - }else{ - // NO CONFLICT - int next; - - if (nof_conflicts >= 0 && conflictC >= nof_conflicts){ - // Reached bound on number of conflicts: - s->progress_estimate = sat_solver_progress(s); - sat_solver_canceluntil(s,s->root_level); - veci_delete(&learnt_clause); - return l_Undef; } - - if ( (s->nConfLimit && s->stats.conflicts > s->nConfLimit) || -// (s->nInsLimit && s->stats.inspects > s->nInsLimit) ) - (s->nInsLimit && s->stats.propagations > s->nInsLimit) ) - { - // Reached bound on number of conflicts: - s->progress_estimate = sat_solver_progress(s); - sat_solver_canceluntil(s,s->root_level); - veci_delete(&learnt_clause); - return l_Undef; - } - - if (sat_solver_dlevel(s) == 0 && !s->fSkipSimplify) - // Simplify the set of problem clauses: - sat_solver_simplify(s); - - if (nof_learnts >= 0 && vecp_size(&s->learnts) - s->qtail >= nof_learnts) - // Reduce the set of learnt clauses: - sat_solver_reducedb(s); - - // New variable decision: - s->stats.decisions++; - next = order_select(s,(float)random_var_freq); - - if (next == var_Undef){ - // Model found: - lbool* values = s->assigns; - int i; - veci_resize(&s->model, 0); - for (i = 0; i < s->size; i++) - veci_push(&s->model,(int)values[i]); - sat_solver_canceluntil(s,s->root_level); - veci_delete(&learnt_clause); - - /* - veci apa; veci_new(&apa); - for (i = 0; i < s->size; i++) - veci_push(&apa,(int)(s->model.ptr[i] == l_True ? toLit(i) : lit_neg(toLit(i)))); - printf("model: "); printlits((lit*)apa.ptr, (lit*)apa.ptr + veci_size(&apa)); printf("\n"); - veci_delete(&apa); - */ - - return l_True; - } - - if ( s->polarity[next] ) // positive polarity - assume(s,toLit(next)); - else - assume(s,lit_neg(toLit(next))); - } - } - - return l_Undef; // cannot happen -} - //================================================================================================= // External solver functions: @@ -1127,10 +991,17 @@ sat_solver* sat_solver_new(void) s->cap = 0; s->qhead = 0; s->qtail = 0; - s->cla_inc = 1; - s->cla_decay = 1; +#ifdef USE_FLOAT_ACTIVITY s->var_inc = 1; - s->var_decay = 1; + s->cla_inc = 1; +// s->var_decay = 1; +// s->cla_decay = 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->simpdb_assigns = 0; s->simpdb_props = 0; @@ -1159,6 +1030,55 @@ sat_solver* sat_solver_new(void) return s; } +void sat_solver_setnvars(sat_solver* s,int n) +{ + int var; + + if (s->cap < n){ + + while (s->cap < n) s->cap = s->cap*2+1; + + s->wlists = ABC_REALLOC(vecp, s->wlists, s->cap*2); +#ifdef USE_FLOAT_ACTIVITY + s->activity = ABC_REALLOC(double, s->activity, s->cap); +#else + s->activity = ABC_REALLOC(unsigned, s->activity, s->cap); +#endif + s->factors = ABC_REALLOC(double, s->factors, s->cap); + s->assigns = ABC_REALLOC(lbool, s->assigns, s->cap); + s->orderpos = ABC_REALLOC(int, s->orderpos, s->cap); + s->reasons = ABC_REALLOC(clause*,s->reasons, s->cap); + s->levels = ABC_REALLOC(int, s->levels, s->cap); + s->tags = ABC_REALLOC(lbool, s->tags, s->cap); + s->trail = ABC_REALLOC(lit, s->trail, s->cap); + s->polarity = ABC_REALLOC(char, s->polarity, s->cap); + } + + for (var = s->size; var < n; var++){ + vecp_new(&s->wlists[2*var]); + vecp_new(&s->wlists[2*var+1]); +#ifdef USE_FLOAT_ACTIVITY + s->activity[var] = 0; +#else + s->activity[var] = (1<<10); +#endif + s->factors [var] = 0; + s->assigns [var] = l_Undef; + s->orderpos [var] = veci_size(&s->order); + s->reasons [var] = (clause*)0; + s->levels [var] = 0; + s->tags [var] = l_Undef; + s->polarity [var] = 0; + + /* does not hold because variables enqueued at top level will not be reinserted in the heap + assert(veci_size(&s->order) == var); + */ + veci_push(&s->order,var); + order_update(s, var); + } + + s->size = n > s->size ? n : s->size; +} void sat_solver_delete(sat_solver* s) { @@ -1262,8 +1182,7 @@ int sat_solver_addclause(sat_solver* s, lit* begin, lit* end) else if (*i != last && values[lit_var(*i)] == l_Undef) last = *j++ = *i; } - - //printf("final: "); printlits(begin,j); printf("\n"); +// j = i; if (j == begin) // empty clause return false; @@ -1340,6 +1259,133 @@ void luby_test() printf( "\n" ); } +static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT64_T nof_learnts) +{ + int* levels = s->levels; + double var_decay = 0.95; + double clause_decay = 0.999; + double random_var_freq = s->fNotUseRandom ? 0.0 : 0.02; + + ABC_INT64_T conflictC = 0; + veci learnt_clause; + int i; + + assert(s->root_level == sat_solver_dlevel(s)); + + s->nRestarts++; + s->stats.starts++; +// s->var_decay = (float)(1 / var_decay ); // move this to sat_solver_new() +// s->cla_decay = (float)(1 / clause_decay); // move this to sat_solver_new() + veci_resize(&s->model,0); + veci_new(&learnt_clause); + + // use activity factors in every even restart + if ( (s->nRestarts & 1) && veci_size(&s->act_vars) > 0 ) +// if ( veci_size(&s->act_vars) > 0 ) + for ( i = 0; i < s->act_vars.size; i++ ) + act_var_bump_factor(s, s->act_vars.ptr[i]); + + // use activity factors in every restart + if ( s->pGlobalVars && veci_size(&s->act_vars) > 0 ) + for ( i = 0; i < s->act_vars.size; i++ ) + act_var_bump_global(s, s->act_vars.ptr[i]); + + for (;;){ + clause* confl = sat_solver_propagate(s); + if (confl != 0){ + // CONFLICT + int blevel; + +#ifdef VERBOSEDEBUG + printf(L_IND"**CONFLICT**\n", L_ind); +#endif + s->stats.conflicts++; conflictC++; + if (sat_solver_dlevel(s) == s->root_level){ +#ifdef SAT_USE_ANALYZE_FINAL + sat_solver_analyze_final(s, confl, 0); +#endif + veci_delete(&learnt_clause); + return l_False; + } + + veci_resize(&learnt_clause,0); + sat_solver_analyze(s, confl, &learnt_clause); + blevel = veci_size(&learnt_clause) > 1 ? levels[lit_var(veci_begin(&learnt_clause)[1])] : s->root_level; + blevel = s->root_level > blevel ? s->root_level : blevel; + sat_solver_canceluntil(s,blevel); + sat_solver_record(s,&learnt_clause); +#ifdef SAT_USE_ANALYZE_FINAL +// if (learnt_clause.size() == 1) level[var(learnt_clause[0])] = 0; // (this is ugly (but needed for 'analyzeFinal()') -- in future versions, we will backtrack past the 'root_level' and redo the assumptions) + if ( learnt_clause.size == 1 ) s->levels[lit_var(learnt_clause.ptr[0])] = 0; +#endif + act_var_decay(s); + act_clause_decay(s); + + }else{ + // NO CONFLICT + int next; + + if (nof_conflicts >= 0 && conflictC >= nof_conflicts){ + // Reached bound on number of conflicts: + s->progress_estimate = sat_solver_progress(s); + sat_solver_canceluntil(s,s->root_level); + veci_delete(&learnt_clause); + return l_Undef; } + + if ( (s->nConfLimit && s->stats.conflicts > s->nConfLimit) || +// (s->nInsLimit && s->stats.inspects > s->nInsLimit) ) + (s->nInsLimit && s->stats.propagations > s->nInsLimit) ) + { + // Reached bound on number of conflicts: + s->progress_estimate = sat_solver_progress(s); + sat_solver_canceluntil(s,s->root_level); + veci_delete(&learnt_clause); + return l_Undef; + } + + if (sat_solver_dlevel(s) == 0 && !s->fSkipSimplify) + // Simplify the set of problem clauses: + sat_solver_simplify(s); + + if (nof_learnts >= 0 && vecp_size(&s->learnts) - s->qtail >= nof_learnts) + // Reduce the set of learnt clauses: + sat_solver_reducedb(s); + + // New variable decision: + s->stats.decisions++; + next = order_select(s,(float)random_var_freq); + + if (next == var_Undef){ + // Model found: + lbool* values = s->assigns; + int i; + veci_resize(&s->model, 0); + for (i = 0; i < s->size; i++) + veci_push(&s->model,(int)values[i]); + sat_solver_canceluntil(s,s->root_level); + veci_delete(&learnt_clause); + + /* + veci apa; veci_new(&apa); + for (i = 0; i < s->size; i++) + veci_push(&apa,(int)(s->model.ptr[i] == l_True ? toLit(i) : lit_neg(toLit(i)))); + printf("model: "); printlits((lit*)apa.ptr, (lit*)apa.ptr + veci_size(&apa)); printf("\n"); + veci_delete(&apa); + */ + + return l_True; + } + + if ( s->polarity[next] ) // positive polarity + assume(s,toLit(next)); + else + assume(s,lit_neg(toLit(next))); + } + } + + return l_Undef; // cannot happen +} + 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) { int restart_iter = 0; diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index f500b46b..ac85300a 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -33,38 +33,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA ABC_NAMESPACE_HEADER_START - -//================================================================================================= -// Simple types: -/* -#ifndef __cplusplus -#ifndef false -# define false 0 -#endif -#ifndef true -# define true 1 -#endif -#endif - -typedef int lit; -typedef char lbool; - -static const int var_Undef = -1; -static const lit lit_Undef = -2; - -static const lbool l_Undef = 0; -static const lbool l_True = 1; -static const lbool l_False = -1; - -static inline lit toLit (int v) { return v + v; } -static inline lit toLitCond(int v, int c) { return v + v + (c != 0); } -static inline lit lit_neg (lit l) { return l ^ 1; } -static inline int lit_var (lit l) { return l >> 1; } -static inline int lit_sign (lit l) { return l & 1; } -static inline int lit_print(lit l) { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; } -static inline lit lit_read (int s) { return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); } -static inline int lit_check(lit l, int n) { return l >= 0 && lit_var(l) < n; } -*/ +//#define USE_FLOAT_ACTIVITY //================================================================================================= // Public interface: @@ -84,14 +53,7 @@ extern int sat_solver_nclauses(sat_solver* s); extern int sat_solver_nconflicts(sat_solver* s); extern void sat_solver_setnvars(sat_solver* s,int n); -/* -struct stats_t -{ - ABC_INT64_T starts, decisions, propagations, inspects, conflicts; - ABC_INT64_T clauses, clauses_literals, learnts, learnts_literals, max_literals, tot_literals; -}; -typedef struct stats_t stats_t; -*/ + extern void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars ); extern void Sat_SolverPrintStats( FILE * pFile, sat_solver * p ); extern int * Sat_SolverGetModel( sat_solver * p, int * pVars, int nVars ); @@ -128,13 +90,19 @@ struct sat_solver_t vecp learnts; // List of learnt clauses. (contains: clause*) // activities +#ifdef USE_FLOAT_ACTIVITY double var_inc; // Amount to bump next variable with. double var_decay; // INVERSE decay factor for variable activity: stores 1/decay. float cla_inc; // Amount to bump next clause with. float cla_decay; // INVERSE decay factor for clause activity: stores 1/decay. + double* activity; // A heuristic measurement of the activity of a variable. +#else + int var_inc; // 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. +#endif vecp* wlists; // - double* activity; // A heuristic measurement of the activity of a variable. lbool* assigns; // Current values of variables. int* orderpos; // Index in variable order. clause** reasons; // diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index fab5e7da..bf616a10 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -38,7 +38,7 @@ ABC_NAMESPACE_IMPL_START // For derivation output (verbosity level 2) #define L_IND "%-*d" -#define L_ind solver2_dlevel(s)*3+3,solver2_dlevel(s) +#define L_ind solver2_dlevel(s)*2+2,solver2_dlevel(s) #define L_LIT "%sx%d" #define L_lit(p) lit_sign(p)?"~":"", (lit_var(p)) static void printlits(lit* begin, lit* end) @@ -285,7 +285,7 @@ static inline int order_select(sat_solver2* s, float random_var_freq) // select //================================================================================================= // Activity functions: -#ifdef USE_FLOAT_ACTIVITY +#ifdef USE_FLOAT_ACTIVITY2 static inline void act_var_rescale(sat_solver2* s) { double* activity = s->activity; @@ -303,8 +303,8 @@ static inline void act_clause_rescale(sat_solver2* s) { s->cla_inc *= (float)1e-20; Total += clock() - clk; -// printf( "Rescaling... Cla inc = %10.3f Conf = %10d ", s->cla_inc, s->stats.conflicts ); -// Abc_PrintTime( 1, "Time", Total ); + printf( "Rescaling... Cla inc = %10.3f Conf = %10d ", s->cla_inc, s->stats.conflicts ); + Abc_PrintTime( 1, "Time", Total ); } static inline void act_var_bump(sat_solver2* s, int v) { s->activity[v] += s->var_inc; @@ -342,7 +342,7 @@ static inline void act_clause_rescale(sat_solver2* s) { s->cla_inc >>= 14; s->cla_inc = Abc_MaxInt( s->cla_inc, (1<<10) ); - Total += clock() - clk; +// Total += clock() - clk; // printf( "Rescaling... Cla inc = %5d Conf = %10d ", s->cla_inc, s->stats.conflicts ); // Abc_PrintTime( 1, "Time", Total ); } @@ -443,7 +443,7 @@ static inline int solver2_enqueue(sat_solver2* s, lit l, int from) { int v = lit_var(l); #ifdef VERBOSEDEBUG - printf(L_IND"solver2_enqueue("L_LIT")\n", L_ind, L_lit(l)); + printf(L_IND"enqueue("L_LIT")\n", L_ind, L_lit(l)); #endif if (var_value(s, v) != varX) return var_value(s, v) == lit_sign(l); @@ -454,15 +454,6 @@ static inline int solver2_enqueue(sat_solver2* s, lit l, int from) #endif var_set_value( s, v, lit_sign(l) ); var_set_level( s, v, solver2_dlevel(s) ); -/* - if ( s->units && s->units[v] != 0 ) - { - assert( solver2_dlevel(s) == 0 ); -// assert( from == 0 ); - if ( from ) - printf( "." ); - } -*/ s->reasons[v] = from; // = from << 1; s->trail[s->qtail++] = l; order_assigned(s, v); @@ -475,7 +466,8 @@ static inline int solver2_assume(sat_solver2* s, lit l) assert(s->qtail == s->qhead); assert(var_value(s, lit_var(l)) == varX); #ifdef VERBOSEDEBUG - printf(L_IND"solver2_assume("L_LIT")\n", L_ind, L_lit(l)); + printf(L_IND"assume("L_LIT") ", L_ind, L_lit(l)); + printf( "act = %.20f\n", s->activity[lit_var(l)] ); #endif veci_push(&s->trail_lim,s->qtail); return solver2_enqueue(s,l,0); @@ -664,8 +656,6 @@ static int solver2_lit_removable_rec(sat_solver2* s, int v) } } } -// if (pfl && visit[p0] & 1){ -// result.push(p0); } if ( s->fProofLogging && (var_tag(s,v) & 1) ) veci_push(&s->min_lit_order, v ); var_add_tag(s,v,6); @@ -1075,6 +1065,8 @@ Abc_PrintTime( 1, "Time", clock() - clk ); static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts) { +// double var_decay = 0.95; +// double clause_decay = 0.999; double random_var_freq = s->fNotUseRandom ? 0.0 : 0.02; ABC_INT64_T conflictC = 0; @@ -1084,6 +1076,8 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts) assert(s->root_level == solver2_dlevel(s)); s->stats.starts++; +// s->var_decay = (float)(1 / var_decay ); +// s->cla_decay = (float)(1 / clause_decay); veci_resize(&s->model,0); veci_new(&learnt_clause); @@ -1208,11 +1202,13 @@ sat_solver2* sat_solver2_new(void) // initialize other s->hLearntFirst = -1; // the first learnt clause s->hLearntLast = -1; // the last learnt clause -#ifdef USE_FLOAT_ACTIVITY +#ifdef USE_FLOAT_ACTIVITY2 s->var_inc = 1; s->cla_inc = 1; s->var_decay = (float)(1 / 0.95 ); s->cla_decay = (float)(1 / 0.999 ); +// s->cla_decay = 1; +// s->var_decay = 1; #else s->var_inc = (1 << 5); s->cla_inc = (1 << 11); @@ -1250,7 +1246,7 @@ void sat_solver2_setnvars(sat_solver2* s,int n) s->reasons = ABC_REALLOC(cla, s->reasons, s->cap); if ( s->fProofLogging ) s->units = ABC_REALLOC(cla, s->units, s->cap); -#ifdef USE_FLOAT_ACTIVITY +#ifdef USE_FLOAT_ACTIVITY2 s->activity = ABC_REALLOC(double, s->activity, s->cap); #else s->activity = ABC_REALLOC(unsigned, s->activity, s->cap); @@ -1265,7 +1261,11 @@ void sat_solver2_setnvars(sat_solver2* s,int n) s->reasons [var] = 0; if ( s->fProofLogging ) s->units [var] = 0; +#ifdef USE_FLOAT_ACTIVITY2 + s->activity[var] = 0; +#else s->activity[var] = (1<<10); +#endif // does not hold because variables enqueued at top level will not be reinserted in the heap // assert(veci_size(&s->order) == var); veci_push(&s->order,var); diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h index 137f1968..8738abdf 100644 --- a/src/sat/bsat/satSolver2.h +++ b/src/sat/bsat/satSolver2.h @@ -32,7 +32,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA ABC_NAMESPACE_HEADER_START -#define USE_FLOAT_ACTIVITY +//#define USE_FLOAT_ACTIVITY2 //================================================================================================= // Public interface: @@ -92,19 +92,9 @@ struct sat_solver2_t int simpdb_props; // Number of propagations before next 'simplifyDB()'. double random_seed; double progress_estimate; - int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything - int fNotUseRandom; // do not allow random decisions with a fixed probability -// int fSkipSimplify; // set to one to skip simplification of the clause database - int fProofLogging; // enable proof-logging - - // clauses - veci clauses; // clause memory - veci* wlists; // watcher lists (for each literal) - int hLearntFirst; // the first learnt clause - int hLearntLast; // in proof-logging mode, the ID of the final conflict clause (conf_final) + int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything // activities - // activities -#ifdef USE_FLOAT_ACTIVITY +#ifdef USE_FLOAT_ACTIVITY2 double var_inc; // Amount to bump next variable with. double var_decay; // INVERSE decay factor for variable activity: stores 1/decay. float cla_inc; // Amount to bump next clause with. @@ -115,6 +105,17 @@ struct sat_solver2_t int cla_inc; // Amount to bump next clause with. unsigned* activity; // A heuristic measurement of the activity of a variable. #endif + + int fNotUseRandom; // do not allow random decisions with a fixed probability +// int fSkipSimplify; // set to one to skip simplification of the clause database + int fProofLogging; // enable proof-logging + + // clauses + veci clauses; // clause memory + veci* wlists; // watcher lists (for each literal) + int hLearntFirst; // the first learnt clause + int hLearntLast; // in proof-logging mode, the ID of the final conflict clause (conf_final) + veci claActs; // clause activities veci claProofs; // clause proofs -- cgit v1.2.3