diff options
| -rw-r--r-- | src/aig/cec/cecSolve.c | 1 | ||||
| -rw-r--r-- | src/aig/ivy/ivyFraig.c | 2 | ||||
| -rw-r--r-- | src/aig/saig/saigConstr2.c | 3 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver.c | 850 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver.h | 135 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver2.c | 32 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver2.h | 2 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver_old.c | 1766 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver_old.h | 210 | ||||
| -rw-r--r-- | src/sat/bsat/satUtil.c | 4 | ||||
| -rw-r--r-- | src/sat/bsat/vecRec.h | 27 |
11 files changed, 2489 insertions, 543 deletions
diff --git a/src/aig/cec/cecSolve.c b/src/aig/cec/cecSolve.c index dc1b88eb..e86c2f35 100644 --- a/src/aig/cec/cecSolve.c +++ b/src/aig/cec/cecSolve.c @@ -376,6 +376,7 @@ void Cec_ManSatSolverRecycle( Cec_ManSat_t * p ) sat_solver_delete( p->pSat ); } p->pSat = sat_solver_new(); + p->pSat->factors = ABC_CALLOC( double, 1 ); sat_solver_setnvars( p->pSat, 1000 ); // var 0 is not used // var 1 is reserved for const0 node - add the clause diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c index b53805b4..f7c0743b 100644 --- a/src/aig/ivy/ivyFraig.c +++ b/src/aig/ivy/ivyFraig.c @@ -2113,6 +2113,7 @@ int Ivy_FraigNodesAreEquiv( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pN if ( p->pSat == NULL ) { p->pSat = sat_solver_new(); + p->pSat->factors = ABC_CALLOC( double, 1 ); p->nSatVars = 1; sat_solver_setnvars( p->pSat, 1000 ); // var 0 is reserved for const1 node - add the clause @@ -2264,6 +2265,7 @@ int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pNew ) if ( p->pSat == NULL ) { p->pSat = sat_solver_new(); + p->pSat->factors = ABC_CALLOC( double, 1 ); p->nSatVars = 1; sat_solver_setnvars( p->pSat, 1000 ); // var 0 is reserved for const1 node - add the clause diff --git a/src/aig/saig/saigConstr2.c b/src/aig/saig/saigConstr2.c index 6665d9f1..7f2eab6a 100644 --- a/src/aig/saig/saigConstr2.c +++ b/src/aig/saig/saigConstr2.c @@ -596,7 +596,8 @@ Vec_Vec_t * Ssw_ManFindDirectImplications( Aig_Man_t * p, int nFrames, int nConf pReprR = Aig_Regular(pRepr); if ( pCnf->pVarNums[Aig_ObjId(pReprR)] < 0 ) continue; - value = pSat->assigns[ pCnf->pVarNums[Aig_ObjId(pReprR)] ]; +// value = pSat->assigns[ pCnf->pVarNums[Aig_ObjId(pReprR)] ]; + value = sat_solver_get_var_value( pSat, pCnf->pVarNums[Aig_ObjId(pReprR)] ); if ( value == l_Undef ) continue; // label this node as taken diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 4d851d0f..5a05e3b0 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -29,7 +29,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA ABC_NAMESPACE_IMPL_START -//#define SAT_USE_SYSTEM_MEMORY_MANAGEMENT #define SAT_USE_ANALYZE_FINAL //================================================================================================= @@ -77,6 +76,62 @@ static inline int irand(double* seed, int size) { static void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *)); //================================================================================================= +// Variable datatype + minor functions: + +static const int var0 = 1; +static const int var1 = 0; +static const int varX = 3; + +struct varinfo_t +{ + unsigned val : 2; // variable value + unsigned pol : 1; // last polarity + unsigned tag : 1; // conflict analysis tag + unsigned lev : 28; // variable level +}; + +static inline int var_level (sat_solver* s, int v) { return s->levels[v]; } +static inline int var_value (sat_solver* s, int v) { return s->assigns[v]; } +static inline int var_polar (sat_solver* s, int v) { return s->polarity[v]; } + +static inline void var_set_level (sat_solver* s, int v, int lev) { s->levels[v] = lev; } +static inline void var_set_value (sat_solver* s, int v, int val) { s->assigns[v] = val; } +static inline void var_set_polar (sat_solver* s, int v, int pol) { s->polarity[v] = pol; } + +// variable tags +static inline int var_tag (sat_solver* s, int v) { return s->tags[v]; } +static inline void var_set_tag (sat_solver* s, int v, int tag) { + assert( tag > 0 && tag < 16 ); + if ( s->tags[v] == 0 ) + veci_push( &s->tagged, v ); + s->tags[v] = tag; +} +static inline void var_add_tag (sat_solver* s, int v, int tag) { + assert( tag > 0 && tag < 16 ); + if ( s->tags[v] == 0 ) + veci_push( &s->tagged, v ); + s->tags[v] |= tag; +} +static inline void solver2_clear_tags(sat_solver* s, int start) { + int i, * tagged = veci_begin(&s->tagged); + for (i = start; i < veci_size(&s->tagged); i++) + s->tags[tagged[i]] = 0; + veci_resize(&s->tagged,start); +} + +int sat_solver_get_var_value(sat_solver* s, int v) +{ + if ( var_value(s, v) == var0 ) + return l_False; + if ( var_value(s, v) == var1 ) + return l_True; + if ( var_value(s, v) == varX ) + return l_Undef; + assert( 0 ); + return 0; +} + +//================================================================================================= // Clause datatype + minor functions: struct clause_t @@ -85,7 +140,7 @@ struct clause_t lit lits[0]; }; -static inline int clause_size (clause* c) { return c->size_learnt >> 1; } +static inline int clause_nlits (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]); } @@ -95,23 +150,26 @@ static inline void clause_setactivity2 (clause* c, unsigned a) { *((unsigned static inline void clause_print (clause* c) { int i; printf( "{ " ); - for ( i = 0; i < clause_size(c); i++ ) + for ( i = 0; i < clause_nlits(c); i++ ) printf( "%d ", (clause_begin(c)[i] & 1)? -(clause_begin(c)[i] >> 1) : clause_begin(c)[i] >> 1 ); printf( "}\n" ); } +static inline clause* clause_read( sat_solver* s, int h ) { return (clause *)Vec_RecEntryP(&s->Mem, h); } +static inline int clause_size( int nLits, int fLearnt ) { int a = nLits + fLearnt + 1; return a + (a & 1); } + //================================================================================================= // Encode literals in clause pointers: -static inline clause* clause_from_lit (lit l) { return (clause*)((ABC_PTRUINT_T)l + (ABC_PTRUINT_T)l + 1); } -static inline int clause_is_lit (clause* c) { return ((ABC_PTRUINT_T)c & 1); } -static inline lit clause_read_lit (clause* c) { return (lit)((ABC_PTRUINT_T)c >> 1); } +static inline int clause_from_lit (lit l) { return l + l + 1; } +static inline int clause_is_lit (int h) { return (h & 1); } +static inline lit clause_read_lit (int h) { return (lit)(h >> 1); } //================================================================================================= // Simple helpers: static inline int sat_solver_dl(sat_solver* s) { return veci_size(&s->trail_lim); } -static inline vecp* sat_solver_read_wlist(sat_solver* s, lit l) { return &s->wlists[l]; } +static inline veci* sat_solver_read_wlist(sat_solver* s, lit l) { return &s->wlists[l]; } //================================================================================================= // Variable order functions: @@ -153,49 +211,31 @@ 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; - int* orderpos; - - lbool* values = s->assigns; - + int* heap = veci_begin(&s->order); + int* orderpos = s->orderpos; // Random decision: if (drand(&s->random_seed) < random_var_freq){ int next = irand(&s->random_seed,s->size); assert(next >= 0 && next < s->size); - if (values[next] == l_Undef) + if (var_value(s, next) == varX) return next; } - // Activity based decision: - - heap = veci_begin(&s->order); - orderpos = s->orderpos; - - while (veci_size(&s->order) > 0){ int next = heap[0]; int size = veci_size(&s->order)-1; int x = heap[size]; - veci_resize(&s->order,size); - orderpos[next] = -1; - if (size > 0){ - int i = 0; int child = 1; - - while (child < size){ if (child+1 < size && s->activity[heap[child]] < s->activity[heap[child+1]]) child++; - assert(child < size); - if (s->activity[x] >= s->activity[heap[child]]) break; - heap[i] = heap[child]; orderpos[heap[i]] = i; i = child; @@ -204,12 +244,9 @@ static inline int order_select(sat_solver* s, float random_var_freq) // selectv heap[i] = x; orderpos[heap[i]] = i; } - -//printf( "-%d ", next ); - if (values[next] == l_Undef) + if (var_value(s, next) == varX) return next; } - return var_Undef; } @@ -227,9 +264,9 @@ static inline void act_var_rescale(sat_solver* s) { } static inline void act_clause_rescale(sat_solver* s) { static int Total = 0; - clause** cs = (clause**)vecp_begin(&s->learnts); + clause** cs = (clause**)veci_begin(&s->learnts); int i, clk = clock(); - for (i = 0; i < vecp_size(&s->learnts); i++){ + for (i = 0; i < veci_size(&s->learnts); i++){ float a = clause_activity(cs[i]); clause_setactivity(cs[i], a * (float)1e-20); } @@ -247,6 +284,8 @@ static inline void act_var_bump(sat_solver* s, int v) { order_update(s,v); } static inline void act_var_bump_global(sat_solver* s, int v) { + if ( !s->pGlobalVars ) + return; s->activity[v] += (s->var_inc * 3.0 * s->pGlobalVars[v]); if (s->activity[v] > 1e100) act_var_rescale(s); @@ -254,6 +293,8 @@ static inline void act_var_bump_global(sat_solver* s, int v) { order_update(s,v); } static inline void act_var_bump_factor(sat_solver* s, int v) { + if ( !s->factors ) + return; s->activity[v] += (s->var_inc * s->factors[v]); if (s->activity[v] > 1e100) act_var_rescale(s); @@ -278,6 +319,7 @@ static inline void act_var_rescale(sat_solver* s) { 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); @@ -293,6 +335,7 @@ static inline void act_clause_rescale(sat_solver* s) { // 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) @@ -300,30 +343,100 @@ static inline void act_var_bump(sat_solver* s, int v) { 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_var_bump_global(sat_solver* s, int v) { + if ( !s->pGlobalVars ) + return; + s->activity[v] += (int)(s->var_inc * 3 * s->pGlobalVars[v]); + if (s->activity[v] & 0x80000000) + act_var_rescale(s); + if (s->orderpos[v] != -1) + order_update(s,v); +} +static inline void act_var_bump_factor(sat_solver* s, int v) { + if ( !s->factors ) + return; + s->activity[v] += (int)(s->var_inc * s->factors[v]); + if (s->activity[v] & 0x80000000) + act_var_rescale(s); + if (s->orderpos[v] != -1) + order_update(s,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); } +//static inline void act_clause_decay(sat_solver* s) { s->cla_inc += (s->cla_inc >> 10); } #endif //================================================================================================= +// Sorting functions (sigh): + +static inline void selectionsort(void** array, int size, int(*comp)(const void *, const void *)) +{ + int i, j, best_i; + void* tmp; + + for (i = 0; i < size-1; i++){ + best_i = i; + for (j = i+1; j < size; j++){ + if (comp(array[j], array[best_i]) < 0) + best_i = j; + } + tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp; + } +} + +static void sortrnd(void** array, int size, int(*comp)(const void *, const void *), double* seed) +{ + if (size <= 15) + selectionsort(array, size, comp); + + else{ + void* pivot = array[irand(seed, size)]; + void* tmp; + int i = -1; + int j = size; + + for(;;){ + do i++; while(comp(array[i], pivot)<0); + do j--; while(comp(pivot, array[j])<0); + + if (i >= j) break; + + tmp = array[i]; array[i] = array[j]; array[j] = tmp; + } + + sortrnd(array , i , comp, seed); + sortrnd(&array[i], size-i, comp, seed); + } +} + +void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *)) +{ +// int i; + double seed = 91648253; + sortrnd(array,size,comp,&seed); +// for ( i = 1; i < size; i++ ) +// assert(comp(array[i-1], array[i])<0); +} + +//================================================================================================= // Clause functions: /* pre: size > 1 && no variable occurs twice */ -static clause* clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt) +static int clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt) { int size; clause* c; - int i; + int h, i; assert(end - begin > 1); assert(learnt >= 0 && learnt < 2); @@ -332,23 +445,20 @@ static clause* clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt // do not allocate memory for the two-literal problem clause if ( size == 2 && !learnt ) { - vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)(clause_from_lit(begin[1]))); - vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)(clause_from_lit(begin[0]))); - return NULL; + veci_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(clause_from_lit(begin[1]))); + veci_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(clause_from_lit(begin[0]))); + return 0; } -#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT - c = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float)); -#else - c = (clause*)Sat_MmStepEntryFetch( s->pMem, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float) ); -#endif - + // create new clause + h = Vec_RecAppend( &s->Mem, clause_size(size, learnt) ); + c = clause_read( s, h ); + assert( !(h & 1) ); + if ( s->hLearnts == -1 && learnt ) + s->hLearnts = h; c->size_learnt = (size << 1) | learnt; - assert(((ABC_PTRUINT_T)c & 1) == 0); - for (i = 0; i < size; i++) c->lits[i] = begin[i]; - if (learnt) *((float*)&c->lits[size]) = 0.0; @@ -360,44 +470,35 @@ static clause* clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt assert(lit_neg(begin[0]) < s->size*2); assert(lit_neg(begin[1]) < s->size*2); - //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)c); - //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)c); - - 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]))); + //veci_push(sat_solver_read_wlist(s,lit_neg(begin[0])),c); + //veci_push(sat_solver_read_wlist(s,lit_neg(begin[1])),c); + veci_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(size > 2 ? h : clause_from_lit(begin[1]))); + veci_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(size > 2 ? h : clause_from_lit(begin[0]))); - return c; + return h; } //================================================================================================= // Minor (solver) functions: -static inline int sat_solver_enqueue(sat_solver* s, lit l, clause* from) +static inline int sat_solver_enqueue(sat_solver* s, lit l, int from) { - lbool* values = s->assigns; - int v = lit_var(l); - lbool val = values[v]; - lbool sig; + int v = lit_var(l); #ifdef VERBOSEDEBUG printf(L_IND"enqueue("L_LIT")\n", L_ind, L_lit(l)); #endif - - sig = !lit_sign(l); sig += sig - 1; - if (val != l_Undef){ - return val == sig; - }else{ - int* levels = s->levels; - clause** reasons = s->reasons; + if (var_value(s, v) != varX) + return var_value(s, v) == lit_sign(l); + else{ // New fact -- store it. #ifdef VERBOSEDEBUG printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(l)); #endif - values [v] = sig; - levels [v] = sat_solver_dl(s); - reasons[v] = from; + var_set_value(s, v, lit_sign(l)); + var_set_level(s, v, sat_solver_dl(s)); + s->reasons[v] = from; s->trail[s->qtail++] = l; - order_assigned(s, v); return true; } @@ -406,20 +507,17 @@ static inline int sat_solver_enqueue(sat_solver* s, lit l, clause* from) static inline int sat_solver_assume(sat_solver* s, lit l){ assert(s->qtail == s->qhead); - assert(s->assigns[lit_var(l)] == l_Undef); + assert(var_value(s, lit_var(l)) == varX); #ifdef VERBOSEDEBUG 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 sat_solver_enqueue(s,l,(clause*)0); + return sat_solver_enqueue(s,l,0); } static void sat_solver_canceluntil(sat_solver* s, int level) { - lit* trail; - lbool* values; - clause** reasons; int bound; int lastLev; int c; @@ -427,9 +525,6 @@ static void sat_solver_canceluntil(sat_solver* s, int level) { if (sat_solver_dl(s) <= level) return; - trail = s->trail; - values = s->assigns; - reasons = s->reasons; bound = (veci_begin(&s->trail_lim))[level]; lastLev = (veci_begin(&s->trail_lim))[veci_size(&s->trail_lim)-1]; @@ -440,15 +535,15 @@ static void sat_solver_canceluntil(sat_solver* s, int level) { //////////////////////////////////////// for (c = s->qtail-1; c >= bound; c--) { - int x = lit_var(trail[c]); - values [x] = l_Undef; - reasons[x] = (clause*)0; + int x = lit_var(s->trail[c]); + var_set_value(s, x, varX); + s->reasons[x] = 0; if ( c < lastLev ) - s->polarity[x] = !lit_sign(trail[c]); + var_set_polar( s, x, !lit_sign(s->trail[c]) ); } for (c = s->qhead-1; c >= bound; c--) - order_unassigned(s,lit_var(trail[c])); + order_unassigned(s,lit_var(s->trail[c])); s->qhead = s->qtail = bound; veci_resize(&s->trail_lim,level); @@ -458,8 +553,8 @@ static void sat_solver_record(sat_solver* s, veci* cls) { lit* begin = veci_begin(cls); lit* end = begin + veci_size(cls); - clause* c = (veci_size(cls) > 1) ? clause_create_new(s,begin,end,1) : (clause*)0; - sat_solver_enqueue(s,*begin,c); + int h = (veci_size(cls) > 1) ? clause_create_new(s,begin,end,1) : 0; + sat_solver_enqueue(s,*begin,h); /////////////////////////////////// // add clause to internal storage @@ -472,9 +567,9 @@ static void sat_solver_record(sat_solver* s, veci* cls) assert(veci_size(cls) > 0); - if (c != 0) { - vecp_push(&s->learnts,c); - act_clause_bump(s,c); + if (h != 0) { +// veci_push(&s->learnts,c); +// act_clause_bump(s,c); s->stats.learnts++; s->stats.learnts_literals += veci_size(cls); } @@ -483,82 +578,59 @@ static void sat_solver_record(sat_solver* s, veci* cls) static double sat_solver_progress(sat_solver* s) { - lbool* values = s->assigns; - int* levels = s->levels; int i; - double progress = 0; double F = 1.0 / s->size; for (i = 0; i < s->size; i++) - if (values[i] != l_Undef) - progress += pow(F, levels[i]); + if (var_value(s, i) != varX) + progress += pow(F, var_level(s, i)); return progress / s->size; } //================================================================================================= // Major methods: -static int sat_solver_lit_removable(sat_solver* s, lit l, int minl) +static int sat_solver_lit_removable(sat_solver* s, int x, int minl) { - lbool* tags = s->tags; - clause** reasons = s->reasons; - int* levels = s->levels; int top = veci_size(&s->tagged); - assert(lit_var(l) >= 0 && lit_var(l) < s->size); - assert(reasons[lit_var(l)] != 0); + assert(s->reasons[x] != 0); veci_resize(&s->stack,0); - veci_push(&s->stack,lit_var(l)); - - while (veci_size(&s->stack) > 0){ - clause* c; - int v = veci_begin(&s->stack)[veci_size(&s->stack)-1]; - assert(v >= 0 && v < s->size); - veci_resize(&s->stack,veci_size(&s->stack)-1); - assert(reasons[v] != 0); - c = reasons[v]; - - if (clause_is_lit(c)){ - int v = lit_var(clause_read_lit(c)); - if (tags[v] == l_Undef && levels[v] != 0){ - if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){ + veci_push(&s->stack,x); + + while (veci_size(&s->stack)){ + int v = veci_pop(&s->stack); + assert(s->reasons[v] != 0); + if (clause_is_lit(s->reasons[v])){ + v = lit_var(clause_read_lit(s->reasons[v])); + if (!var_tag(s,v) && var_level(s, v)){ + if (s->reasons[v] != 0 && ((1 << (var_level(s, v) & 31)) & minl)){ veci_push(&s->stack,v); - tags[v] = l_True; - veci_push(&s->tagged,v); + var_set_tag(s, v, 1); }else{ - int* tagged = veci_begin(&s->tagged); - int j; - for (j = top; j < veci_size(&s->tagged); j++) - tags[tagged[j]] = l_Undef; - veci_resize(&s->tagged,top); - return false; + solver2_clear_tags(s, top); + return 0; } } }else{ - lit* lits = clause_begin(c); - int i, j; - - for (i = 1; i < clause_size(c); i++){ + clause* c = clause_read(s, s->reasons[v]); + lit* lits = clause_begin(c); + int i; + for (i = 1; i < clause_nlits(c); i++){ int v = lit_var(lits[i]); - if (tags[v] == l_Undef && levels[v] != 0){ - if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){ - + if (!var_tag(s,v) && var_level(s, v)){ + if (s->reasons[v] != 0 && ((1 << (var_level(s, v) & 31)) & minl)){ veci_push(&s->stack,lit_var(lits[i])); - tags[v] = l_True; - veci_push(&s->tagged,v); + var_set_tag(s, v, 1); }else{ - int* tagged = veci_begin(&s->tagged); - for (j = top; j < veci_size(&s->tagged); j++) - tags[tagged[j]] = l_Undef; - veci_resize(&s->tagged,top); - return false; + solver2_clear_tags(s, top); + return 0; } } } } } - - return true; + return 1; } @@ -613,8 +685,9 @@ void Solver::analyzeFinal(Clause* confl, bool skip_first) #ifdef SAT_USE_ANALYZE_FINAL -static void sat_solver_analyze_final(sat_solver* s, clause* conf, int skip_first) +static void sat_solver_analyze_final(sat_solver* s, int hConf, int skip_first) { + clause* conf = clause_read(s, hConf); int i, j, start; veci_resize(&s->conf_final,0); if ( s->root_level == 0 ) @@ -622,110 +695,87 @@ static void sat_solver_analyze_final(sat_solver* s, clause* conf, int skip_first assert( veci_size(&s->tagged) == 0 ); // assert( s->tags[lit_var(p)] == l_Undef ); // s->tags[lit_var(p)] = l_True; - for (i = skip_first ? 1 : 0; i < clause_size(conf); i++) + for (i = skip_first ? 1 : 0; i < clause_nlits(conf); i++) { int x = lit_var(clause_begin(conf)[i]); - if (s->levels[x] > 0) - { - s->tags[x] = l_True; - veci_push(&s->tagged,x); - } + if (var_level(s, x) > 0) + var_set_tag(s, x, 1); } start = (s->root_level >= veci_size(&s->trail_lim))? s->qtail-1 : (veci_begin(&s->trail_lim))[s->root_level]; for (i = start; i >= (veci_begin(&s->trail_lim))[0]; i--){ int x = lit_var(s->trail[i]); - if (s->tags[x] == l_True){ - if (s->reasons[x] == NULL){ - assert(s->levels[x] > 0); + if (var_tag(s,x)){ + if (s->reasons[x] == 0){ + assert(var_level(s, x) > 0); veci_push(&s->conf_final,lit_neg(s->trail[i])); }else{ - clause* c = s->reasons[x]; - if (clause_is_lit(c)){ - lit q = clause_read_lit(c); + if (clause_is_lit(s->reasons[x])){ + lit q = clause_read_lit(s->reasons[x]); assert(lit_var(q) >= 0 && lit_var(q) < s->size); - if (s->levels[lit_var(q)] > 0) - { - s->tags[lit_var(q)] = l_True; - veci_push(&s->tagged,lit_var(q)); - } + if (var_level(s, lit_var(q)) > 0) + var_set_tag(s, lit_var(q), 1); } else{ + clause* c = clause_read(s, s->reasons[x]); int* lits = clause_begin(c); - for (j = 1; j < clause_size(c); j++) - if (s->levels[lit_var(lits[j])] > 0) - { - s->tags[lit_var(lits[j])] = l_True; - veci_push(&s->tagged,lit_var(lits[j])); - } + for (j = 1; j < clause_nlits(c); j++) + if (var_level(s, lit_var(lits[j])) > 0) + var_set_tag(s, lit_var(lits[j]), 1); } } } } - for (i = 0; i < veci_size(&s->tagged); i++) - s->tags[veci_begin(&s->tagged)[i]] = l_Undef; - veci_resize(&s->tagged,0); + solver2_clear_tags(s,0); } #endif -static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt) +static void sat_solver_analyze(sat_solver* s, int h, veci* learnt) { lit* trail = s->trail; - lbool* tags = s->tags; - clause** reasons = s->reasons; - int* levels = s->levels; int cnt = 0; lit p = lit_Undef; int ind = s->qtail-1; lit* lits; int i, j, minl; - int* tagged; - veci_push(learnt,lit_Undef); - do{ - assert(c != 0); - - if (clause_is_lit(c)){ - lit q = clause_read_lit(c); - assert(lit_var(q) >= 0 && lit_var(q) < s->size); - if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){ - tags[lit_var(q)] = l_True; - veci_push(&s->tagged,lit_var(q)); - act_var_bump(s,lit_var(q)); - if (levels[lit_var(q)] == sat_solver_dl(s)) + assert(h != 0); + if (clause_is_lit(h)){ + int x = lit_var(clause_read_lit(h)); + if (var_tag(s, x) == 0 && var_level(s, x) > 0){ + var_set_tag(s, x, 1); + act_var_bump(s,x); + if (var_level(s, x) == sat_solver_dl(s)) cnt++; else - veci_push(learnt,q); + veci_push(learnt,clause_read_lit(h)); } }else{ - - if (clause_learnt(c)) - act_clause_bump(s,c); - + clause* c = clause_read(s, h); +// if (clause_learnt(c)) +// act_clause_bump(s,c); lits = clause_begin(c); - //printlits(lits,lits+clause_size(c)); printf("\n"); - for (j = (p == lit_Undef ? 0 : 1); j < clause_size(c); j++){ - lit q = lits[j]; - assert(lit_var(q) >= 0 && lit_var(q) < s->size); - if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){ - tags[lit_var(q)] = l_True; - veci_push(&s->tagged,lit_var(q)); - act_var_bump(s,lit_var(q)); - if (levels[lit_var(q)] == sat_solver_dl(s)) + //printlits(lits,lits+clause_nlits(c)); printf("\n"); + for (j = (p == lit_Undef ? 0 : 1); j < clause_nlits(c); j++){ + int x = lit_var(lits[j]); + if (var_tag(s, x) == 0 && var_level(s, x) > 0){ + var_set_tag(s, x, 1); + act_var_bump(s,x); + if (var_level(s,x) == sat_solver_dl(s)) cnt++; else - veci_push(learnt,q); + veci_push(learnt,lits[j]); } } } - while (tags[lit_var(trail[ind--])] == l_Undef); + while ( !var_tag(s, lit_var(trail[ind--])) ); p = trail[ind+1]; - c = reasons[lit_var(p)]; + h = s->reasons[lit_var(p)]; cnt--; }while (cnt > 0); @@ -735,13 +785,13 @@ static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt) lits = veci_begin(learnt); minl = 0; for (i = 1; i < veci_size(learnt); i++){ - int lev = levels[lit_var(lits[i])]; + int lev = var_level(s, lit_var(lits[i])); minl |= 1 << (lev & 31); } // simplify (full) for (i = j = 1; i < veci_size(learnt); i++){ - if (reasons[lit_var(lits[i])] == 0 || !sat_solver_lit_removable(s,lits[i],minl)) + if (s->reasons[lit_var(lits[i])] == 0 || !sat_solver_lit_removable(s,lit_var(lits[i]),minl)) lits[j++] = lits[i]; } @@ -750,14 +800,11 @@ static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt) s->stats.tot_literals += j; // clear tags - tagged = veci_begin(&s->tagged); - for (i = 0; i < veci_size(&s->tagged); i++) - tags[tagged[i]] = l_Undef; - veci_resize(&s->tagged,0); + solver2_clear_tags(s,0); #ifdef DEBUG for (i = 0; i < s->size; i++) - assert(tags[i] == l_Undef); + assert(!var_tag(s, i)); #endif #ifdef VERBOSEDEBUG @@ -766,12 +813,12 @@ static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt) #endif if (veci_size(learnt) > 1){ int max_i = 1; - int max = levels[lit_var(lits[1])]; + int max = var_level(s, lit_var(lits[1])); lit tmp; for (i = 2; i < veci_size(learnt); i++) - if (levels[lit_var(lits[i])] > max){ - max = levels[lit_var(lits[i])]; + if (var_level(s, lit_var(lits[i])) > max){ + max = var_level(s, lit_var(lits[i])); max_i = i; } @@ -781,28 +828,26 @@ static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt) } #ifdef VERBOSEDEBUG { - int lev = veci_size(learnt) > 1 ? levels[lit_var(lits[1])] : 0; + int lev = veci_size(learnt) > 1 ? var_level(s, lit_var(lits[1])) : 0; printf(" } at level %d\n", lev); } #endif } -clause* sat_solver_propagate(sat_solver* s) +int sat_solver_propagate(sat_solver* s) { - lbool* values = s->assigns; - clause* confl = (clause*)0; + int hConfl = 0; lit* lits; lit false_lit; - lbool sig; //printf("sat_solver_propagate\n"); - while (confl == 0 && s->qtail - s->qhead > 0){ - lit p = s->trail[s->qhead++]; - vecp* ws = sat_solver_read_wlist(s,p); - clause **begin = (clause**)vecp_begin(ws); - clause **end = begin + vecp_size(ws); - clause **i, **j; + while (hConfl == 0 && s->qtail - s->qhead > 0){ + lit p = s->trail[s->qhead++]; + veci* ws = sat_solver_read_wlist(s,p); + int* begin = veci_begin(ws); + int* end = begin + veci_size(ws); + int*i, *j; s->stats.propagations++; s->simpdb_props--; @@ -812,24 +857,24 @@ clause* sat_solver_propagate(sat_solver* s) if (clause_is_lit(*i)){ int Lit = clause_read_lit(*i); - sig = !lit_sign(Lit); sig += sig - 1; - if (values[lit_var(Lit)] == sig){ + if (var_value(s, lit_var(Lit)) == lit_sign(Lit)){ *j++ = *i++; continue; } *j++ = *i; if (!sat_solver_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++); + hConfl = s->hBinary; + (clause_begin(s->binary))[1] = lit_neg(p); + (clause_begin(s->binary))[0] = clause_read_lit(*i++); // Copy the remaining watches: while (i < end) *j++ = *i++; } }else{ - lits = clause_begin(*i); + clause* c = clause_read(s,*i); + lits = clause_begin(c); // Make sure the false literal is data[1]: false_lit = lit_neg(p); @@ -838,29 +883,26 @@ clause* sat_solver_propagate(sat_solver* s) lits[1] = false_lit; } assert(lits[1] == false_lit); - //printf("checking clause: "); printlits(lits, lits+clause_size(*i)); printf("\n"); // If 0th watch is true, then clause is already satisfied. - sig = !lit_sign(lits[0]); sig += sig - 1; - if (values[lit_var(lits[0])] == sig){ + if (var_value(s, lit_var(lits[0])) == lit_sign(lits[0])) *j++ = *i; - }else{ + else{ // Look for new watch: - lit* stop = lits + clause_size(*i); + lit* stop = lits + clause_nlits(c); lit* k; for (k = lits + 2; k < stop; k++){ - lbool sig = lit_sign(*k); sig += sig - 1; - if (values[lit_var(*k)] != sig){ + if (var_value(s, lit_var(*k)) != !lit_sign(*k)){ lits[1] = *k; *k = false_lit; - vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i); + veci_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i); goto next; } } *j++ = *i; // Clause is unit under assignment: if (!sat_solver_enqueue(s,lits[0], *i)){ - confl = *i++; + hConfl = *i++; // Copy the remaining watches: while (i < end) *j++ = *i++; @@ -871,11 +913,11 @@ clause* sat_solver_propagate(sat_solver* s) i++; } - s->stats.inspects += j - (clause**)vecp_begin(ws); - vecp_resize(ws,j - (clause**)vecp_begin(ws)); + s->stats.inspects += j - veci_begin(ws); + veci_resize(ws,j - veci_begin(ws)); } - return confl; + return hConfl; } //================================================================================================= @@ -883,12 +925,15 @@ clause* sat_solver_propagate(sat_solver* s) sat_solver* sat_solver_new(void) { - sat_solver* s = (sat_solver*)ABC_ALLOC( char, sizeof(sat_solver)); - memset( s, 0, sizeof(sat_solver) ); + sat_solver* s = (sat_solver*)ABC_CALLOC( char, sizeof(sat_solver)); + + Vec_RecAlloc_(&s->Mem); + s->hLearnts = -1; + s->hBinary = Vec_RecAppend( &s->Mem, clause_size(2, 0) ); + s->binary = clause_read( s, s->hBinary ); + s->binary->size_learnt = (2 << 1); // initialize vectors - vecp_new(&s->clauses); - vecp_new(&s->learnts); veci_new(&s->order); veci_new(&s->trail_lim); veci_new(&s->tagged); @@ -901,15 +946,10 @@ sat_solver* sat_solver_new(void) // initialize arrays s->wlists = 0; s->activity = 0; - s->factors = 0; - s->assigns = 0; s->orderpos = 0; s->reasons = 0; - s->levels = 0; - s->tags = 0; s->trail = 0; - // initialize other vars s->size = 0; s->cap = 0; @@ -929,8 +969,8 @@ sat_solver* sat_solver_new(void) s->simpdb_props = 0; s->random_seed = 91648253; s->progress_estimate = 0; - s->binary = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit)*2); - s->binary->size_learnt = (2 << 1); +// s->binary = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit)*2); +// s->binary->size_learnt = (2 << 1); s->verbosity = 0; s->stats.starts = 0; @@ -943,12 +983,6 @@ sat_solver* sat_solver_new(void) s->stats.learnts = 0; s->stats.learnts_literals = 0; s->stats.tot_literals = 0; - -#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT - s->pMem = NULL; -#else - s->pMem = Sat_MmStepStart( 10 ); -#endif return s; } @@ -960,42 +994,46 @@ void sat_solver_setnvars(sat_solver* s,int n) int old_cap = s->cap; while (s->cap < n) s->cap = s->cap*2+1; - s->wlists = ABC_REALLOC(vecp, s->wlists, s->cap*2); + s->wlists = ABC_REALLOC(veci, s->wlists, s->cap*2); +// s->vi = ABC_REALLOC(varinfo,s->vi, s->cap); + s->levels = ABC_REALLOC(int, s->levels, s->cap); + s->assigns = ABC_REALLOC(char, s->assigns, s->cap); + s->polarity = ABC_REALLOC(char, s->polarity, s->cap); + s->tags = ABC_REALLOC(char, s->tags, s->cap); #ifdef USE_FLOAT_ACTIVITY s->activity = ABC_REALLOC(double, s->activity, s->cap); #else s->activity = ABC_REALLOC(unsigned, s->activity, s->cap); #endif + if ( s->factors ) 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->reasons = ABC_REALLOC(int, s->reasons, s->cap); s->trail = ABC_REALLOC(lit, s->trail, s->cap); - s->polarity = ABC_REALLOC(char, s->polarity, s->cap); - memset( s->wlists + 2*old_cap, 0, 2*(s->cap-old_cap)*sizeof(vecp) ); - } + memset( s->wlists + 2*old_cap, 0, 2*(s->cap-old_cap)*sizeof(veci) ); + } for (var = s->size; var < n; var++){ assert(!s->wlists[2*var].size); assert(!s->wlists[2*var+1].size); if ( s->wlists[2*var].ptr == NULL ) - vecp_new(&s->wlists[2*var]); + veci_new(&s->wlists[2*var]); if ( s->wlists[2*var+1].ptr == NULL ) - vecp_new(&s->wlists[2*var+1]); + veci_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; + if ( s->factors ) + s->factors [var] = 0; +// *((int*)s->vi + var) = 0; s->vi[var].val = varX; + s->levels [var] = 0; + s->assigns [var] = varX; + s->polarity[var] = 0; + s->tags [var] = 0; + s->orderpos[var] = veci_size(&s->order); + s->reasons [var] = 0; /* does not hold because variables enqueued at top level will not be reinserted in the heap assert(veci_size(&s->order) == var); @@ -1009,20 +1047,9 @@ void sat_solver_setnvars(sat_solver* s,int n) void sat_solver_delete(sat_solver* s) { - -#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT - int i; - for (i = 0; i < vecp_size(&s->clauses); i++) - ABC_FREE(vecp_begin(&s->clauses)[i]); - for (i = 0; i < vecp_size(&s->learnts); i++) - ABC_FREE(vecp_begin(&s->learnts)[i]); -#else - Sat_MmStepStop( s->pMem, 0 ); -#endif + Vec_RecFree_( &s->Mem ); // delete vectors - vecp_delete(&s->clauses); - vecp_delete(&s->learnts); veci_delete(&s->order); veci_delete(&s->trail_lim); veci_delete(&s->tagged); @@ -1031,23 +1058,23 @@ void sat_solver_delete(sat_solver* s) veci_delete(&s->act_vars); veci_delete(&s->temp_clause); veci_delete(&s->conf_final); - ABC_FREE(s->binary); // delete arrays - if (s->wlists != 0){ + if (s->reasons != 0){ int i; for (i = 0; i < s->cap*2; i++) - vecp_delete(&s->wlists[i]); + veci_delete(&s->wlists[i]); ABC_FREE(s->wlists ); +// ABC_FREE(s->vi ); + ABC_FREE(s->levels ); + ABC_FREE(s->assigns ); + ABC_FREE(s->polarity ); + ABC_FREE(s->tags ); ABC_FREE(s->activity ); ABC_FREE(s->factors ); - ABC_FREE(s->assigns ); ABC_FREE(s->orderpos ); ABC_FREE(s->reasons ); - ABC_FREE(s->levels ); ABC_FREE(s->trail ); - ABC_FREE(s->tags ); - ABC_FREE(s->polarity ); } sat_solver_store_free(s); @@ -1057,16 +1084,13 @@ void sat_solver_delete(sat_solver* s) void sat_solver_rollback( sat_solver* s ) { int i; -#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT - for (i = 0; i < vecp_size(&s->clauses); i++) - ABC_FREE(vecp_begin(&s->clauses)[i]); - for (i = 0; i < vecp_size(&s->learnts); i++) - ABC_FREE(vecp_begin(&s->learnts)[i]); -#else - Sat_MmStepRestart( s->pMem ); -#endif - vecp_resize(&s->clauses, 0); - vecp_resize(&s->learnts, 0); + Vec_RecRestart( &s->Mem ); + + s->hLearnts = -1; + s->hBinary = Vec_RecAppend( &s->Mem, clause_size(2, 0) ); + s->binary = clause_read( s, s->hBinary ); + s->binary->size_learnt = (2 << 1); + veci_resize(&s->trail_lim, 0); veci_resize(&s->order, 0); for ( i = 0; i < s->size*2; i++ ) @@ -1105,56 +1129,49 @@ void sat_solver_rollback( sat_solver* s ) s->stats.tot_literals = 0; } - +/* static void clause_remove(sat_solver* s, clause* c) { lit* lits = clause_begin(c); assert(lit_neg(lits[0]) < s->size*2); assert(lit_neg(lits[1]) < s->size*2); - //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)c); - //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)c); + //veci_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)c); + //veci_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)c); assert(lits[0] < s->size*2); - vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1]))); - vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0]))); + veci_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(clause_nlits(c) > 2 ? c : clause_from_lit(lits[1]))); + veci_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(clause_nlits(c) > 2 ? c : clause_from_lit(lits[0]))); if (clause_learnt(c)){ s->stats.learnts--; - s->stats.learnts_literals -= clause_size(c); + s->stats.learnts_literals -= clause_nlits(c); }else{ s->stats.clauses--; - s->stats.clauses_literals -= clause_size(c); + s->stats.clauses_literals -= clause_nlits(c); } - -#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT - ABC_FREE(c); -#else - Sat_MmStepEntryRecycle( s->pMem, (char *)c, sizeof(clause) + sizeof(lit) * clause_size(c) + clause_learnt(c) * sizeof(float) ); -#endif } static lbool clause_simplify(sat_solver* s, clause* c) { lit* lits = clause_begin(c); - lbool* values = s->assigns; int i; assert(sat_solver_dl(s) == 0); - for (i = 0; i < clause_size(c); i++){ + for (i = 0; i < clause_nlits(c); i++){ lbool sig = !lit_sign(lits[i]); sig += sig - 1; - if (values[lit_var(lits[i])] == sig) + if (s->assignss[lit_var(lits[i])] == sig) return l_True; } return l_False; } +*/ int sat_solver_simplify(sat_solver* s) { - clause** reasons; - int type; - +// clause** reasons; +// int type; assert(sat_solver_dl(s) == 0); if (sat_solver_propagate(s) != 0) @@ -1162,7 +1179,7 @@ int sat_solver_simplify(sat_solver* s) if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0) return true; - +/* reasons = s->reasons; for (type = 0; type < 2; type++){ vecp* cs = type ? &s->learnts : &s->clauses; @@ -1178,53 +1195,48 @@ int sat_solver_simplify(sat_solver* s) } vecp_resize(cs,j); } - +*/ s->simpdb_assigns = s->qhead; // (shouldn't depend on 'stats' really, but it will do for now) s->simpdb_props = (int)(s->stats.clauses_literals + s->stats.learnts_literals); - return true; } +/* static int clause_cmp (const void* x, const void* y) { - return clause_size((clause*)x) > 2 && (clause_size((clause*)y) == 2 || clause_activity((clause*)x) < clause_activity((clause*)y)) ? -1 : 1; } - + return clause_nlits((clause*)x) > 2 && (clause_nlits((clause*)y) == 2 || clause_activity((clause*)x) < clause_activity((clause*)y)) ? -1 : 1; } void sat_solver_reducedb(sat_solver* s) { int i, j; - double extra_lim = s->cla_inc / vecp_size(&s->learnts); // Remove any clause below this activity - clause** learnts = (clause**)vecp_begin(&s->learnts); + double extra_lim = s->cla_inc / veci_size(&s->learnts); // Remove any clause below this activity + clause** learnts = (clause**)veci_begin(&s->learnts); clause** reasons = s->reasons; - sat_solver_sort(vecp_begin(&s->learnts), vecp_size(&s->learnts), &clause_cmp); + sat_solver_sort(veci_begin(&s->learnts), veci_size(&s->learnts), &clause_cmp); - for (i = j = 0; i < vecp_size(&s->learnts) / 2; i++){ - if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i]) + for (i = j = 0; i < veci_size(&s->learnts) / 2; i++){ + if (clause_nlits(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i]) clause_remove(s,learnts[i]); else learnts[j++] = learnts[i]; } - for (; i < vecp_size(&s->learnts); i++){ - if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i] && clause_activity(learnts[i]) < extra_lim) + for (; i < veci_size(&s->learnts); i++){ + if (clause_nlits(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i] && clause_activity(learnts[i]) < extra_lim) clause_remove(s,learnts[i]); else learnts[j++] = learnts[i]; } - - //printf("reducedb deleted %d\n", vecp_size(&s->learnts) - j); - - - vecp_resize(&s->learnts,j); + veci_resize(&s->learnts,j); } +*/ int sat_solver_addclause(sat_solver* s, lit* begin, lit* end) { - clause * c; lit *i,*j; int maxvar; - lbool* values; lit last; + assert( begin < end ); veci_resize( &s->temp_clause, 0 ); for ( i = begin; i < end; i++ ) @@ -1232,10 +1244,6 @@ int sat_solver_addclause(sat_solver* s, lit* begin, lit* end) begin = veci_begin( &s->temp_clause ); end = begin + veci_size( &s->temp_clause ); - if (begin == end) - return false; - - //printlits(begin,end); printf("\n"); // insertion sort maxvar = lit_var(*begin); for (i = begin + 1; i < end; i++){ @@ -1246,7 +1254,6 @@ int sat_solver_addclause(sat_solver* s, lit* begin, lit* end) *j = l; } sat_solver_setnvars(s,maxvar+1); -// sat_solver_setnvars(s, lit_var(*(end-1))+1 ); /////////////////////////////////// // add clause to internal storage @@ -1257,17 +1264,13 @@ int sat_solver_addclause(sat_solver* s, lit* begin, lit* end) } /////////////////////////////////// - //printlits(begin,end); printf("\n"); - values = s->assigns; - // delete duplicates last = lit_Undef; for (i = j = begin; i < end; i++){ - //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)])); - lbool sig = !lit_sign(*i); sig += sig - 1; - if (*i == lit_neg(last) || sig == values[lit_var(*i)]) + //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -s->assignss[lit_var(*i)] : s->assignss[lit_var(*i)])); + if (*i == lit_neg(last) || var_value(s, lit_var(*i)) == lit_sign(*i)) return true; // tautology - else if (*i != last && values[lit_var(*i)] == l_Undef) + else if (*i != last && var_value(s, lit_var(*i)) == varX) last = *j++ = *i; } // j = i; @@ -1276,17 +1279,13 @@ int sat_solver_addclause(sat_solver* s, lit* begin, lit* end) return false; if (j - begin == 1) // unit clause - return sat_solver_enqueue(s,*begin,(clause*)0); + return sat_solver_enqueue(s,*begin,0); // create new clause - c = clause_create_new(s,begin,j,0); - if ( c ) - vecp_push(&s->clauses,c); - + clause_create_new(s,begin,j,0); s->stats.clauses++; s->stats.clauses_literals += j - begin; - return true; } @@ -1313,7 +1312,6 @@ void luby_test() 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; @@ -1343,8 +1341,8 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT act_var_bump_global(s, s->act_vars.ptr[i]); for (;;){ - clause* confl = sat_solver_propagate(s); - if (confl != 0){ + int hConfl = sat_solver_propagate(s); + if (hConfl != 0){ // CONFLICT int blevel; @@ -1354,24 +1352,25 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT s->stats.conflicts++; conflictC++; if (sat_solver_dl(s) == s->root_level){ #ifdef SAT_USE_ANALYZE_FINAL - sat_solver_analyze_final(s, confl, 0); + sat_solver_analyze_final(s, hConfl, 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; + sat_solver_analyze(s, hConfl, &learnt_clause); + blevel = veci_size(&learnt_clause) > 1 ? var_level(s, 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; + if ( learnt_clause.size == 1 ) + var_set_level(s, lit_var(learnt_clause.ptr[0]), 0); #endif act_var_decay(s); - act_clause_decay(s); +// act_clause_decay(s); }else{ // NO CONFLICT @@ -1385,7 +1384,6 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT 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: @@ -1399,7 +1397,7 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT // Simplify the set of problem clauses: sat_solver_simplify(s); -// if (nof_learnts >= 0 && vecp_size(&s->learnts) - s->qtail >= nof_learnts) +// if (nof_learnts >= 0 && veci_size(&s->learnts) - s->qtail >= nof_learnts) // Reduce the set of learnt clauses: // sat_solver_reducedb(s); @@ -1409,11 +1407,10 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT 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]); + veci_push( &s->model, var_value(s,i)==var1 ? l_True : l_False ); sat_solver_canceluntil(s,s->root_level); veci_delete(&learnt_clause); @@ -1428,7 +1425,7 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT return l_True; } - if ( s->polarity[next] ) // positive polarity + if ( var_polar(s, next) ) // positive polarity sat_solver_assume(s,toLit(next)); else sat_solver_assume(s,lit_neg(toLit(next))); @@ -1444,7 +1441,6 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit ABC_INT64_T nof_conflicts; ABC_INT64_T nof_learnts = sat_solver_nclauses(s) / 3; lbool status = l_Undef; - lbool* values = s->assigns; lit* i; //////////////////////////////////////////////// @@ -1478,15 +1474,16 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit //printf("solve: "); printlits(begin, end); printf("\n"); for (i = begin; i < end; i++){ - switch (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]){ - case 1: // l_True: +// switch (lit_sign(*i) ? -s->assignss[lit_var(*i)] : s->assignss[lit_var(*i)]){ + switch (var_value(s, *i)) { + case var1: // l_True: break; - case 0: // l_Undef + case varX: // l_Undef sat_solver_assume(s, *i); - if (sat_solver_propagate(s) == NULL) + if (sat_solver_propagate(s) == 0) break; // fallthrough - case -1: // l_False + case var0: // l_False sat_solver_canceluntil(s, 0); return l_False; } @@ -1535,21 +1532,18 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit lit p = *i; assert(lit_var(p) < s->size); veci_push(&s->trail_lim,s->qtail); - if (!sat_solver_enqueue(s,p,(clause*)0)) + if (!sat_solver_enqueue(s,p,0)) { - clause * r = s->reasons[lit_var(p)]; - if (r != NULL) + int h = s->reasons[lit_var(p)]; + if (h) { - clause* confl; - if (clause_is_lit(r)) + if (clause_is_lit(h)) { - confl = s->binary; - (clause_begin(confl))[1] = lit_neg(p); - (clause_begin(confl))[0] = clause_read_lit(r); + (clause_begin(s->binary))[1] = lit_neg(p); + (clause_begin(s->binary))[0] = clause_read_lit(h); + h = s->hBinary; } - else - confl = r; - sat_solver_analyze_final(s, confl, 1); + sat_solver_analyze_final(s, h, 1); veci_push(&s->conf_final, lit_neg(p)); } else @@ -1557,7 +1551,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit veci_resize(&s->conf_final,0); veci_push(&s->conf_final, lit_neg(p)); // the two lines below are a bug fix by Siert Wieringa - if (s->levels[lit_var(p)] > 0) + if (var_level(s, lit_var(p)) > 0) veci_push(&s->conf_final, p); } sat_solver_canceluntil(s, 0); @@ -1565,9 +1559,9 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit } else { - clause* confl = sat_solver_propagate(s); - if (confl != NULL){ - sat_solver_analyze_final(s, confl, 0); + int fConfl = sat_solver_propagate(s); + if (fConfl){ + sat_solver_analyze_final(s, fConfl, 0); assert(s->conf_final.size > 0); sat_solver_canceluntil(s, 0); return l_False; } @@ -1586,12 +1580,10 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit } while (status == l_Undef){ -// int nConfs = 0; double Ratio = (s->stats.learnts == 0)? 0.0 : s->stats.learnts_literals / (double)s->stats.learnts; if ( s->nRuntimeLimit && time(NULL) > s->nRuntimeLimit ) break; - if (s->verbosity >= 1) { printf("| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %6.3f %% |\n", @@ -1606,31 +1598,16 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit fflush(stdout); } nof_conflicts = (ABC_INT64_T)( 100 * luby(2, restart_iter++) ); -//printf( "%d ", (int)nof_conflicts ); -// nConfs = s->stats.conflicts; status = sat_solver_search(s, nof_conflicts, nof_learnts); -// if ( status == l_True ) -// printf( "%d ", s->stats.conflicts - nConfs ); - -// nof_conflicts = nof_conflicts * 3 / 2; //*= 1.5; nof_learnts = nof_learnts * 11 / 10; //*= 1.1; -//printf( "%d ", s->stats.conflicts ); // quit the loop if reached an external limit if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit ) - { -// printf( "Reached the limit on the number of conflicts (%d).\n", s->nConfLimit ); break; - } -// if ( s->nInsLimit && s->stats.inspects > s->nInsLimit ) if ( s->nInsLimit && s->stats.propagations > s->nInsLimit ) - { -// printf( "Reached the limit on the number of implications (%d).\n", s->nInsLimit ); break; - } if ( s->nRuntimeLimit && time(NULL) > s->nRuntimeLimit ) break; } -//printf( "\n" ); if (s->verbosity >= 1) printf("==============================================================================\n"); @@ -1655,7 +1632,7 @@ int sat_solver_nvars(sat_solver* s) int sat_solver_nclauses(sat_solver* s) { - return vecp_size(&s->clauses); + return s->stats.clauses; } @@ -1710,57 +1687,6 @@ void * sat_solver_store_release( sat_solver * s ) return pTemp; } -//================================================================================================= -// Sorting functions (sigh): - -static inline void selectionsort(void** array, int size, int(*comp)(const void *, const void *)) -{ - int i, j, best_i; - void* tmp; - - for (i = 0; i < size-1; i++){ - best_i = i; - for (j = i+1; j < size; j++){ - if (comp(array[j], array[best_i]) < 0) - best_i = j; - } - tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp; - } -} - - -static void sortrnd(void** array, int size, int(*comp)(const void *, const void *), double* seed) -{ - if (size <= 15) - selectionsort(array, size, comp); - - else{ - void* pivot = array[irand(seed, size)]; - void* tmp; - int i = -1; - int j = size; - - for(;;){ - do i++; while(comp(array[i], pivot)<0); - do j--; while(comp(pivot, array[j])<0); - - if (i >= j) break; - - tmp = array[i]; array[i] = array[j]; array[j] = tmp; - } - - sortrnd(array , i , comp, seed); - sortrnd(&array[i], size-i, comp, seed); - } -} -void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *)) -{ -// int i; - double seed = 91648253; - sortrnd(array,size,comp,&seed); -// for ( i = 1; i < size; i++ ) -// assert(comp(array[i-1], array[i])<0); -} ABC_NAMESPACE_IMPL_END diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index 4c577b1e..a0e94bfb 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -29,7 +29,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include <assert.h> #include "satVec.h" -#include "satMem.h" +#include "vecRec.h" ABC_NAMESPACE_HEADER_START @@ -54,6 +54,8 @@ 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); +extern int sat_solver_get_var_value(sat_solver* s, int v); + extern void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars ); extern void Sat_SolverPrintStats( FILE * pFile, sat_solver * p ); @@ -79,84 +81,87 @@ extern void * sat_solver_store_release( sat_solver * s ); struct clause_t; typedef struct clause_t clause; +struct varinfo_t; +typedef struct varinfo_t varinfo; + struct sat_solver_t { - int size; // nof variables - int cap; // size of varmaps - int qhead; // Head index of queue. - int qtail; // Tail index of queue. + int size; // nof variables + int cap; // size of varmaps + int qhead; // Head index of queue. + int qtail; // Tail index of queue. // clauses - vecp clauses; // List of problem constraints. (contains: clause*) - vecp learnts; // List of learnt clauses. (contains: clause*) + Vec_Rec_t Mem; + int hLearnts; // the first learnt clause + int hBinary; // the special binary clause + clause * binary; // 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. + 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. + 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; // - lbool* assigns; // Current values of variables. - int* orderpos; // Index in variable order. - clause** reasons; // - int* levels; // - lit* trail; - char* polarity; - - clause* binary; // A temporary binary clause - lbool* tags; // - veci tagged; // (contains: var) - veci stack; // (contains: var) - - veci order; // Variable order. (heap) (contains: var) - veci trail_lim; // Separator indices for different decision levels in 'trail'. (contains: int) - veci model; // If problem is solved, this vector contains the model (contains: lbool). - veci conf_final; // If problem is unsatisfiable (possibly under assumptions), - // this vector represent the final conflict clause expressed in the assumptions. - - int root_level; // Level of first proper decision. - int simpdb_assigns;// Number of top-level assignments at last 'simplifyDB()'. - 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 - - stats_t stats; - - ABC_INT64_T nConfLimit; // external limit on the number of conflicts - ABC_INT64_T nInsLimit; // external limit on the number of implications - int nRuntimeLimit; // external limit on runtime - - veci act_vars; // variables whose activity has changed - double* factors; // the activity factors - int nRestarts; // the number of local restarts - int nCalls; // the number of local restarts - int nCalls2; // the number of local restarts - - Sat_MmStep_t * pMem; - - int fSkipSimplify; // set to one to skip simplification of the clause database - int fNotUseRandom; // do not allow random decisions with a fixed probability - - int * pGlobalVars; // for experiments with global vars during interpolation + veci* wlists; // +// varinfo * vi; // variable information + int* levels; // + char* assigns; // Current values of variables. + char* polarity; // + char* tags; // + + int* orderpos; // Index in variable order. + int* reasons; // + lit* trail; + veci tagged; // (contains: var) + veci stack; // (contains: var) + + veci order; // Variable order. (heap) (contains: var) + veci trail_lim; // Separator indices for different decision levels in 'trail'. (contains: int) + veci model; // If problem is solved, this vector contains the model (contains: lbool). + veci conf_final; // If problem is unsatisfiable (possibly under assumptions), + // this vector represent the final conflict clause expressed in the assumptions. + + int root_level; // Level of first proper decision. + int simpdb_assigns;// Number of top-level assignments at last 'simplifyDB()'. + 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 + + stats_t stats; + + ABC_INT64_T nConfLimit; // external limit on the number of conflicts + ABC_INT64_T nInsLimit; // external limit on the number of implications + int nRuntimeLimit; // external limit on runtime + + veci act_vars; // variables whose activity has changed + double* factors; // the activity factors + int nRestarts; // the number of local restarts + int nCalls; // the number of local restarts + int nCalls2; // the number of local restarts + + int fSkipSimplify; // set to one to skip simplification of the clause database + int fNotUseRandom; // do not allow random decisions with a fixed probability + + int * pGlobalVars; // for experiments with global vars during interpolation // clause store - void * pStore; - int fSolved; + void * pStore; + int fSolved; // trace recording - FILE * pFile; - int nClauses; - int nRoots; + FILE * pFile; + int nClauses; + int nRoots; - veci temp_clause; // temporary storage for a CNF clause + veci temp_clause; // temporary storage for a CNF clause }; static int sat_solver_var_value( sat_solver* s, int v ) diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index 5eb65132..0cda3295 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -65,14 +65,6 @@ static inline double drand(double* seed) { static inline int irand(double* seed, int size) { return (int)(drand(seed) * size); } -static inline int sat_float2int( float Val ) { union { int x; float y; } v; v.y = Val; return v.x; } -static inline float sat_int2float( int Num ) { union { int x; float y; } v; v.x = Num; return v.y; } - -//================================================================================================= -// Predeclarations: - -static void solver2_sort(void** array, int size, int(*comp)(const void *, const void *)); - //================================================================================================= // Variable datatype + minor functions: @@ -82,23 +74,27 @@ static const int varX = 3; struct varinfo_t { - unsigned val : 2; // variable value +// unsigned val : 2; // variable value unsigned pol : 1; // last polarity unsigned partA : 1; // partA variable unsigned tag : 4; // conflict analysis tags - unsigned lev : 24; // variable level +// unsigned lev : 24; // variable level }; int var_is_partA (sat_solver2* s, int v) { return s->vi[v].partA; } void var_set_partA(sat_solver2* s, int v, int partA) { s->vi[v].partA = partA; } -static inline int var_value (sat_solver2* s, int v) { return s->vi[v].val; } +//static inline int var_level (sat_solver2* s, int v) { return s->vi[v].lev; } +static inline int var_level (sat_solver2* s, int v) { return s->levels[v]; } +//static inline int var_value (sat_solver2* s, int v) { return s->vi[v].val; } +static inline int var_value (sat_solver2* s, int v) { return s->assigns[v]; } static inline int var_polar (sat_solver2* s, int v) { return s->vi[v].pol; } -static inline int var_level (sat_solver2* s, int v) { return s->vi[v].lev; } -static inline void var_set_value (sat_solver2* s, int v, int val) { s->vi[v].val = val; } +//static inline void var_set_level (sat_solver2* s, int v, int lev) { s->vi[v].lev = lev; } +static inline void var_set_level (sat_solver2* s, int v, int lev) { s->levels[v] = lev; } +//static inline void var_set_value (sat_solver2* s, int v, int val) { s->vi[v].val = val; } +static inline void var_set_value (sat_solver2* s, int v, int val) { s->assigns[v] = val; } static inline void var_set_polar (sat_solver2* s, int v, int pol) { s->vi[v].pol = pol; } -static inline void var_set_level (sat_solver2* s, int v, int lev) { s->vi[v].lev = lev; } // variable tags static inline int var_tag (sat_solver2* s, int v) { return s->vi[v].tag; } @@ -1268,6 +1264,8 @@ void sat_solver2_setnvars(sat_solver2* s,int n) s->wlists = ABC_REALLOC(veci, s->wlists, s->cap*2); s->vi = ABC_REALLOC(varinfo, s->vi, s->cap); + s->levels = ABC_REALLOC(int, s->levels, s->cap); + s->assigns = ABC_REALLOC(char, s->assigns, s->cap); s->trail = ABC_REALLOC(lit, s->trail, s->cap); s->orderpos = ABC_REALLOC(int, s->orderpos, s->cap); s->reasons = ABC_REALLOC(cla, s->reasons, s->cap); @@ -1288,7 +1286,9 @@ void sat_solver2_setnvars(sat_solver2* s,int n) veci_new(&s->wlists[2*var]); if ( s->wlists[2*var+1].ptr == NULL ) veci_new(&s->wlists[2*var+1]); - *((int*)s->vi + var) = 0; s->vi[var].val = varX; + *((int*)s->vi + var) = 0; //s->vi[var].val = varX; + s->levels [var] = 0; + s->assigns [var] = varX; s->orderpos[var] = veci_size(&s->order); s->reasons [var] = 0; if ( s->fProofLogging ) @@ -1346,6 +1346,8 @@ void sat_solver2_delete(sat_solver2* s) veci_delete(&s->wlists[i]); ABC_FREE(s->wlists ); ABC_FREE(s->vi ); + ABC_FREE(s->levels ); + ABC_FREE(s->assigns ); ABC_FREE(s->trail ); ABC_FREE(s->orderpos ); ABC_FREE(s->reasons ); diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h index 0c08ac1e..21dc3b21 100644 --- a/src/sat/bsat/satSolver2.h +++ b/src/sat/bsat/satSolver2.h @@ -126,6 +126,8 @@ struct sat_solver2_t // internal state varinfo * vi; // variable information + int* levels; // + char* assigns; // lit* trail; // sequence of assignment and implications int* orderpos; // Index in variable order. cla* reasons; // reason clauses diff --git a/src/sat/bsat/satSolver_old.c b/src/sat/bsat/satSolver_old.c new file mode 100644 index 00000000..4d851d0f --- /dev/null +++ b/src/sat/bsat/satSolver_old.c @@ -0,0 +1,1766 @@ +/************************************************************************************************** +MiniSat -- Copyright (c) 2005, Niklas Sorensson +http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/ + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ +// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko + +#include <stdio.h> +#include <assert.h> +#include <string.h> +#include <math.h> + +#include "satSolver.h" +#include "satStore.h" + +ABC_NAMESPACE_IMPL_START + +//#define SAT_USE_SYSTEM_MEMORY_MANAGEMENT +#define SAT_USE_ANALYZE_FINAL + +//================================================================================================= +// Debug: + +//#define VERBOSEDEBUG + +// For derivation output (verbosity level 2) +#define L_IND "%-*d" +#define L_ind sat_solver_dl(s)*2+2,sat_solver_dl(s) +#define L_LIT "%sx%d" +#define L_lit(p) lit_sign(p)?"~":"", (lit_var(p)) + +// Just like 'assert()' but expression will be evaluated in the release version as well. +static inline void check(int expr) { assert(expr); } + +static void printlits(lit* begin, lit* end) +{ + int i; + for (i = 0; i < end - begin; i++) + printf(L_LIT" ",L_lit(begin[i])); +} + +//================================================================================================= +// Random numbers: + + +// Returns a random float 0 <= x < 1. Seed must never be 0. +static inline double drand(double* seed) { + int q; + *seed *= 1389796; + q = (int)(*seed / 2147483647); + *seed -= (double)q * 2147483647; + return *seed / 2147483647; } + + +// Returns a random integer 0 <= x < size. Seed must never be 0. +static inline int irand(double* seed, int size) { + return (int)(drand(seed) * size); } + + +//================================================================================================= +// Predeclarations: + +static void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *)); + +//================================================================================================= +// Clause datatype + minor functions: + +struct clause_t +{ + int size_learnt; + 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 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: + +static inline clause* clause_from_lit (lit l) { return (clause*)((ABC_PTRUINT_T)l + (ABC_PTRUINT_T)l + 1); } +static inline int clause_is_lit (clause* c) { return ((ABC_PTRUINT_T)c & 1); } +static inline lit clause_read_lit (clause* c) { return (lit)((ABC_PTRUINT_T)c >> 1); } + +//================================================================================================= +// Simple helpers: + +static inline int sat_solver_dl(sat_solver* s) { return veci_size(&s->trail_lim); } +static inline vecp* sat_solver_read_wlist(sat_solver* s, lit l) { return &s->wlists[l]; } + +//================================================================================================= +// Variable order functions: + +static inline void order_update(sat_solver* s, int v) // updateorder +{ + int* orderpos = s->orderpos; + int* heap = veci_begin(&s->order); + int i = orderpos[v]; + int x = heap[i]; + int parent = (i - 1) / 2; + + assert(s->orderpos[v] != -1); + + while (i != 0 && s->activity[x] > s->activity[heap[parent]]){ + heap[i] = heap[parent]; + orderpos[heap[i]] = i; + i = parent; + parent = (i - 1) / 2; + } + heap[i] = x; + orderpos[x] = i; +} + +static inline void order_assigned(sat_solver* s, int v) +{ +} + +static inline void order_unassigned(sat_solver* s, int v) // undoorder +{ + int* orderpos = s->orderpos; + if (orderpos[v] == -1){ + orderpos[v] = veci_size(&s->order); + veci_push(&s->order,v); + order_update(s,v); +//printf( "+%d ", v ); + } +} + +static inline int order_select(sat_solver* s, float random_var_freq) // selectvar +{ + int* heap; + int* orderpos; + + lbool* values = s->assigns; + + // Random decision: + if (drand(&s->random_seed) < random_var_freq){ + int next = irand(&s->random_seed,s->size); + assert(next >= 0 && next < s->size); + if (values[next] == l_Undef) + return next; + } + + // Activity based decision: + + heap = veci_begin(&s->order); + orderpos = s->orderpos; + + + while (veci_size(&s->order) > 0){ + int next = heap[0]; + int size = veci_size(&s->order)-1; + int x = heap[size]; + + veci_resize(&s->order,size); + + orderpos[next] = -1; + + if (size > 0){ + + int i = 0; + int child = 1; + + + while (child < size){ + if (child+1 < size && s->activity[heap[child]] < s->activity[heap[child+1]]) + child++; + + assert(child < size); + + if (s->activity[x] >= s->activity[heap[child]]) + break; + + heap[i] = heap[child]; + orderpos[heap[i]] = i; + i = child; + child = 2 * child + 1; + } + heap[i] = x; + orderpos[heap[i]] = i; + } + +//printf( "-%d ", next ); + if (values[next] == l_Undef) + return next; + } + + return var_Undef; +} + +//================================================================================================= +// Activity functions: + +#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; + if (s->activity[v] > 1e100) + 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) { + s->activity[v] += (s->var_inc * 3.0 * s->pGlobalVars[v]); + if (s->activity[v] > 1e100) + act_var_rescale(s); + 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]); + if (s->activity[v] > 1e100) + act_var_rescale(s); + 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; } + +#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, clk = clock(); + for (i = 0; i < vecp_size(&s->learnts); i++){ + unsigned a = clause_activity2(cs[i]); + clause_setactivity2(cs[i], a >> 14); + } + s->cla_inc >>= 14; + s->cla_inc = Abc_MaxInt( s->cla_inc, (1<<10) ); + +// 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 + + +//================================================================================================= +// Clause functions: + +/* pre: size > 1 && no variable occurs twice + */ +static clause* clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt) +{ + int size; + clause* c; + int i; + + assert(end - begin > 1); + assert(learnt >= 0 && learnt < 2); + size = end - begin; + + // do not allocate memory for the two-literal problem clause + if ( size == 2 && !learnt ) + { + vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)(clause_from_lit(begin[1]))); + vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)(clause_from_lit(begin[0]))); + return NULL; + } + +#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT + c = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float)); +#else + c = (clause*)Sat_MmStepEntryFetch( s->pMem, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float) ); +#endif + + c->size_learnt = (size << 1) | learnt; + assert(((ABC_PTRUINT_T)c & 1) == 0); + + for (i = 0; i < size; i++) + c->lits[i] = begin[i]; + + if (learnt) + *((float*)&c->lits[size]) = 0.0; + + assert(begin[0] >= 0); + assert(begin[0] < s->size*2); + assert(begin[1] >= 0); + assert(begin[1] < s->size*2); + + assert(lit_neg(begin[0]) < s->size*2); + assert(lit_neg(begin[1]) < s->size*2); + + //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)c); + //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)c); + + 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]))); + + return c; +} + + +//================================================================================================= +// Minor (solver) functions: + +static inline int sat_solver_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 + + 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 + values [v] = sig; + levels [v] = sat_solver_dl(s); + reasons[v] = from; + s->trail[s->qtail++] = l; + + order_assigned(s, v); + return true; + } +} + + +static inline int sat_solver_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") ", L_ind, L_lit(l)); + printf( "act = %.20f\n", s->activity[lit_var(l)] ); +#endif + veci_push(&s->trail_lim,s->qtail); + return sat_solver_enqueue(s,l,(clause*)0); +} + + +static void sat_solver_canceluntil(sat_solver* s, int level) { + lit* trail; + lbool* values; + clause** reasons; + int bound; + int lastLev; + int c; + + if (sat_solver_dl(s) <= level) + return; + + trail = s->trail; + values = s->assigns; + reasons = s->reasons; + bound = (veci_begin(&s->trail_lim))[level]; + lastLev = (veci_begin(&s->trail_lim))[veci_size(&s->trail_lim)-1]; + + //////////////////////////////////////// + // added to cancel all assignments +// if ( level == -1 ) +// bound = 0; + //////////////////////////////////////// + + for (c = s->qtail-1; c >= bound; c--) { + int x = lit_var(trail[c]); + values [x] = l_Undef; + reasons[x] = (clause*)0; + if ( c < lastLev ) + s->polarity[x] = !lit_sign(trail[c]); + } + + for (c = s->qhead-1; c >= bound; c--) + order_unassigned(s,lit_var(trail[c])); + + s->qhead = s->qtail = bound; + veci_resize(&s->trail_lim,level); +} + +static void sat_solver_record(sat_solver* s, veci* cls) +{ + lit* begin = veci_begin(cls); + lit* end = begin + veci_size(cls); + clause* c = (veci_size(cls) > 1) ? clause_create_new(s,begin,end,1) : (clause*)0; + sat_solver_enqueue(s,*begin,c); + + /////////////////////////////////// + // add clause to internal storage + if ( s->pStore ) + { + int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, begin, end ); + assert( RetValue ); + } + /////////////////////////////////// + + assert(veci_size(cls) > 0); + + if (c != 0) { + vecp_push(&s->learnts,c); + act_clause_bump(s,c); + s->stats.learnts++; + s->stats.learnts_literals += veci_size(cls); + } +} + + +static double sat_solver_progress(sat_solver* s) +{ + lbool* values = s->assigns; + int* levels = s->levels; + int i; + + double progress = 0; + double F = 1.0 / s->size; + for (i = 0; i < s->size; i++) + if (values[i] != l_Undef) + progress += pow(F, levels[i]); + return progress / s->size; +} + +//================================================================================================= +// Major methods: + +static int sat_solver_lit_removable(sat_solver* s, lit l, int minl) +{ + lbool* tags = s->tags; + clause** reasons = s->reasons; + int* levels = s->levels; + int top = veci_size(&s->tagged); + + assert(lit_var(l) >= 0 && lit_var(l) < s->size); + assert(reasons[lit_var(l)] != 0); + veci_resize(&s->stack,0); + veci_push(&s->stack,lit_var(l)); + + while (veci_size(&s->stack) > 0){ + clause* c; + int v = veci_begin(&s->stack)[veci_size(&s->stack)-1]; + assert(v >= 0 && v < s->size); + veci_resize(&s->stack,veci_size(&s->stack)-1); + assert(reasons[v] != 0); + c = reasons[v]; + + if (clause_is_lit(c)){ + int v = lit_var(clause_read_lit(c)); + if (tags[v] == l_Undef && levels[v] != 0){ + if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){ + veci_push(&s->stack,v); + tags[v] = l_True; + veci_push(&s->tagged,v); + }else{ + int* tagged = veci_begin(&s->tagged); + int j; + for (j = top; j < veci_size(&s->tagged); j++) + tags[tagged[j]] = l_Undef; + veci_resize(&s->tagged,top); + return false; + } + } + }else{ + lit* lits = clause_begin(c); + int i, j; + + for (i = 1; i < clause_size(c); i++){ + int v = lit_var(lits[i]); + if (tags[v] == l_Undef && levels[v] != 0){ + if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){ + + veci_push(&s->stack,lit_var(lits[i])); + tags[v] = l_True; + veci_push(&s->tagged,v); + }else{ + int* tagged = veci_begin(&s->tagged); + for (j = top; j < veci_size(&s->tagged); j++) + tags[tagged[j]] = l_Undef; + veci_resize(&s->tagged,top); + return false; + } + } + } + } + } + + return true; +} + + +/*_________________________________________________________________________________________________ +| +| analyzeFinal : (p : Lit) -> [void] +| +| Description: +| Specialized analysis procedure to express the final conflict in terms of assumptions. +| Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and +| stores the result in 'out_conflict'. +|________________________________________________________________________________________________@*/ +/* +void Solver::analyzeFinal(Clause* confl, bool skip_first) +{ + // -- NOTE! This code is relatively untested. Please report bugs! + conflict.clear(); + if (root_level == 0) return; + + vec<char>& seen = analyze_seen; + for (int i = skip_first ? 1 : 0; i < confl->size(); i++){ + Var x = var((*confl)[i]); + if (level[x] > 0) + seen[x] = 1; + } + + int start = (root_level >= trail_lim.size()) ? trail.size()-1 : trail_lim[root_level]; + for (int i = start; i >= trail_lim[0]; i--){ + Var x = var(trail[i]); + if (seen[x]){ + GClause r = reason[x]; + if (r == GClause_NULL){ + assert(level[x] > 0); + conflict.push(~trail[i]); + }else{ + if (r.isLit()){ + Lit p = r.lit(); + if (level[var(p)] > 0) + seen[var(p)] = 1; + }else{ + Clause& c = *r.clause(); + for (int j = 1; j < c.size(); j++) + if (level[var(c[j])] > 0) + seen[var(c[j])] = 1; + } + } + seen[x] = 0; + } + } +} +*/ + +#ifdef SAT_USE_ANALYZE_FINAL + +static void sat_solver_analyze_final(sat_solver* s, clause* conf, int skip_first) +{ + int i, j, start; + veci_resize(&s->conf_final,0); + if ( s->root_level == 0 ) + return; + assert( veci_size(&s->tagged) == 0 ); +// assert( s->tags[lit_var(p)] == l_Undef ); +// s->tags[lit_var(p)] = l_True; + for (i = skip_first ? 1 : 0; i < clause_size(conf); i++) + { + int x = lit_var(clause_begin(conf)[i]); + if (s->levels[x] > 0) + { + s->tags[x] = l_True; + veci_push(&s->tagged,x); + } + } + + start = (s->root_level >= veci_size(&s->trail_lim))? s->qtail-1 : (veci_begin(&s->trail_lim))[s->root_level]; + for (i = start; i >= (veci_begin(&s->trail_lim))[0]; i--){ + int x = lit_var(s->trail[i]); + if (s->tags[x] == l_True){ + if (s->reasons[x] == NULL){ + assert(s->levels[x] > 0); + veci_push(&s->conf_final,lit_neg(s->trail[i])); + }else{ + clause* c = s->reasons[x]; + if (clause_is_lit(c)){ + lit q = clause_read_lit(c); + assert(lit_var(q) >= 0 && lit_var(q) < s->size); + if (s->levels[lit_var(q)] > 0) + { + s->tags[lit_var(q)] = l_True; + veci_push(&s->tagged,lit_var(q)); + } + } + else{ + int* lits = clause_begin(c); + for (j = 1; j < clause_size(c); j++) + if (s->levels[lit_var(lits[j])] > 0) + { + s->tags[lit_var(lits[j])] = l_True; + veci_push(&s->tagged,lit_var(lits[j])); + } + } + } + } + } + for (i = 0; i < veci_size(&s->tagged); i++) + s->tags[veci_begin(&s->tagged)[i]] = l_Undef; + veci_resize(&s->tagged,0); +} + +#endif + + +static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt) +{ + lit* trail = s->trail; + lbool* tags = s->tags; + clause** reasons = s->reasons; + int* levels = s->levels; + int cnt = 0; + lit p = lit_Undef; + int ind = s->qtail-1; + lit* lits; + int i, j, minl; + int* tagged; + + veci_push(learnt,lit_Undef); + + do{ + assert(c != 0); + + if (clause_is_lit(c)){ + lit q = clause_read_lit(c); + assert(lit_var(q) >= 0 && lit_var(q) < s->size); + if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){ + tags[lit_var(q)] = l_True; + veci_push(&s->tagged,lit_var(q)); + act_var_bump(s,lit_var(q)); + if (levels[lit_var(q)] == sat_solver_dl(s)) + cnt++; + else + veci_push(learnt,q); + } + }else{ + + if (clause_learnt(c)) + act_clause_bump(s,c); + + lits = clause_begin(c); + //printlits(lits,lits+clause_size(c)); printf("\n"); + for (j = (p == lit_Undef ? 0 : 1); j < clause_size(c); j++){ + lit q = lits[j]; + assert(lit_var(q) >= 0 && lit_var(q) < s->size); + if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){ + tags[lit_var(q)] = l_True; + veci_push(&s->tagged,lit_var(q)); + act_var_bump(s,lit_var(q)); + if (levels[lit_var(q)] == sat_solver_dl(s)) + cnt++; + else + veci_push(learnt,q); + } + } + } + + while (tags[lit_var(trail[ind--])] == l_Undef); + + p = trail[ind+1]; + c = reasons[lit_var(p)]; + cnt--; + + }while (cnt > 0); + + *veci_begin(learnt) = lit_neg(p); + + lits = veci_begin(learnt); + minl = 0; + for (i = 1; i < veci_size(learnt); i++){ + int lev = levels[lit_var(lits[i])]; + minl |= 1 << (lev & 31); + } + + // simplify (full) + for (i = j = 1; i < veci_size(learnt); i++){ + if (reasons[lit_var(lits[i])] == 0 || !sat_solver_lit_removable(s,lits[i],minl)) + lits[j++] = lits[i]; + } + + // update size of learnt + statistics + veci_resize(learnt,j); + s->stats.tot_literals += j; + + // clear tags + tagged = veci_begin(&s->tagged); + for (i = 0; i < veci_size(&s->tagged); i++) + tags[tagged[i]] = l_Undef; + veci_resize(&s->tagged,0); + +#ifdef DEBUG + for (i = 0; i < s->size; i++) + assert(tags[i] == l_Undef); +#endif + +#ifdef VERBOSEDEBUG + printf(L_IND"Learnt {", L_ind); + for (i = 0; i < veci_size(learnt); i++) printf(" "L_LIT, L_lit(lits[i])); +#endif + if (veci_size(learnt) > 1){ + int max_i = 1; + int max = levels[lit_var(lits[1])]; + lit tmp; + + for (i = 2; i < veci_size(learnt); i++) + if (levels[lit_var(lits[i])] > max){ + max = levels[lit_var(lits[i])]; + max_i = i; + } + + tmp = lits[1]; + lits[1] = lits[max_i]; + lits[max_i] = tmp; + } +#ifdef VERBOSEDEBUG + { + int lev = veci_size(learnt) > 1 ? levels[lit_var(lits[1])] : 0; + printf(" } at level %d\n", lev); + } +#endif +} + + +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){ + lit p = s->trail[s->qhead++]; + vecp* ws = sat_solver_read_wlist(s,p); + clause **begin = (clause**)vecp_begin(ws); + clause **end = begin + vecp_size(ws); + clause **i, **j; + + s->stats.propagations++; + s->simpdb_props--; + + //printf("checking lit %d: "L_LIT"\n", veci_size(ws), L_lit(p)); + for (i = j = begin; i < end; ){ + if (clause_is_lit(*i)){ + + 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 (!sat_solver_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: + while (i < end) + *j++ = *i++; + } + }else{ + + lits = clause_begin(*i); + + // Make sure the false literal is data[1]: + false_lit = lit_neg(p); + if (lits[0] == false_lit){ + lits[0] = lits[1]; + lits[1] = false_lit; + } + assert(lits[1] == false_lit); + //printf("checking clause: "); printlits(lits, lits+clause_size(*i)); printf("\n"); + + // If 0th watch is true, then clause is already satisfied. + sig = !lit_sign(lits[0]); sig += sig - 1; + if (values[lit_var(lits[0])] == sig){ + *j++ = *i; + }else{ + // Look for new watch: + lit* stop = lits + clause_size(*i); + lit* k; + for (k = lits + 2; k < stop; k++){ + lbool sig = lit_sign(*k); sig += sig - 1; + if (values[lit_var(*k)] != sig){ + lits[1] = *k; + *k = false_lit; + vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i); + goto next; } + } + + *j++ = *i; + // Clause is unit under assignment: + if (!sat_solver_enqueue(s,lits[0], *i)){ + confl = *i++; + // Copy the remaining watches: + while (i < end) + *j++ = *i++; + } + } + } + next: + i++; + } + + s->stats.inspects += j - (clause**)vecp_begin(ws); + vecp_resize(ws,j - (clause**)vecp_begin(ws)); + } + + return confl; +} + +//================================================================================================= +// External solver functions: + +sat_solver* sat_solver_new(void) +{ + sat_solver* s = (sat_solver*)ABC_ALLOC( char, sizeof(sat_solver)); + memset( s, 0, sizeof(sat_solver) ); + + // initialize vectors + vecp_new(&s->clauses); + vecp_new(&s->learnts); + veci_new(&s->order); + veci_new(&s->trail_lim); + veci_new(&s->tagged); + veci_new(&s->stack); + veci_new(&s->model); + veci_new(&s->act_vars); + veci_new(&s->temp_clause); + veci_new(&s->conf_final); + + // initialize arrays + s->wlists = 0; + s->activity = 0; + s->factors = 0; + s->assigns = 0; + s->orderpos = 0; + s->reasons = 0; + s->levels = 0; + s->tags = 0; + s->trail = 0; + + + // initialize other vars + 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->simpdb_assigns = 0; + s->simpdb_props = 0; + s->random_seed = 91648253; + s->progress_estimate = 0; + s->binary = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit)*2); + s->binary->size_learnt = (2 << 1); + 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; + +#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT + s->pMem = NULL; +#else + s->pMem = Sat_MmStepStart( 10 ); +#endif + return s; +} + +void sat_solver_setnvars(sat_solver* s,int n) +{ + int var; + + if (s->cap < n){ + int old_cap = s->cap; + 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); + memset( s->wlists + 2*old_cap, 0, 2*(s->cap-old_cap)*sizeof(vecp) ); + } + + for (var = s->size; var < n; var++){ + assert(!s->wlists[2*var].size); + assert(!s->wlists[2*var+1].size); + if ( s->wlists[2*var].ptr == NULL ) + vecp_new(&s->wlists[2*var]); + if ( s->wlists[2*var+1].ptr == NULL ) + 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) +{ + +#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT + int i; + for (i = 0; i < vecp_size(&s->clauses); i++) + ABC_FREE(vecp_begin(&s->clauses)[i]); + for (i = 0; i < vecp_size(&s->learnts); i++) + ABC_FREE(vecp_begin(&s->learnts)[i]); +#else + Sat_MmStepStop( s->pMem, 0 ); +#endif + + // delete vectors + vecp_delete(&s->clauses); + vecp_delete(&s->learnts); + veci_delete(&s->order); + veci_delete(&s->trail_lim); + veci_delete(&s->tagged); + veci_delete(&s->stack); + veci_delete(&s->model); + veci_delete(&s->act_vars); + veci_delete(&s->temp_clause); + veci_delete(&s->conf_final); + ABC_FREE(s->binary); + + // delete arrays + if (s->wlists != 0){ + int i; + for (i = 0; i < s->cap*2; i++) + vecp_delete(&s->wlists[i]); + ABC_FREE(s->wlists ); + ABC_FREE(s->activity ); + ABC_FREE(s->factors ); + ABC_FREE(s->assigns ); + ABC_FREE(s->orderpos ); + ABC_FREE(s->reasons ); + ABC_FREE(s->levels ); + ABC_FREE(s->trail ); + ABC_FREE(s->tags ); + ABC_FREE(s->polarity ); + } + + sat_solver_store_free(s); + ABC_FREE(s); +} + +void sat_solver_rollback( sat_solver* s ) +{ + int i; +#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT + for (i = 0; i < vecp_size(&s->clauses); i++) + ABC_FREE(vecp_begin(&s->clauses)[i]); + for (i = 0; i < vecp_size(&s->learnts); i++) + ABC_FREE(vecp_begin(&s->learnts)[i]); +#else + Sat_MmStepRestart( s->pMem ); +#endif + vecp_resize(&s->clauses, 0); + vecp_resize(&s->learnts, 0); + veci_resize(&s->trail_lim, 0); + veci_resize(&s->order, 0); + for ( i = 0; i < s->size*2; i++ ) + s->wlists[i].size = 0; + + // initialize other vars + 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->simpdb_assigns = 0; + s->simpdb_props = 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; +} + + +static void clause_remove(sat_solver* s, clause* c) +{ + lit* lits = clause_begin(c); + assert(lit_neg(lits[0]) < s->size*2); + assert(lit_neg(lits[1]) < s->size*2); + + //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)c); + //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)c); + + assert(lits[0] < s->size*2); + vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1]))); + vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0]))); + + if (clause_learnt(c)){ + s->stats.learnts--; + s->stats.learnts_literals -= clause_size(c); + }else{ + s->stats.clauses--; + s->stats.clauses_literals -= clause_size(c); + } + +#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT + ABC_FREE(c); +#else + Sat_MmStepEntryRecycle( s->pMem, (char *)c, sizeof(clause) + sizeof(lit) * clause_size(c) + clause_learnt(c) * sizeof(float) ); +#endif +} + +static lbool clause_simplify(sat_solver* s, clause* c) +{ + lit* lits = clause_begin(c); + lbool* values = s->assigns; + int i; + + assert(sat_solver_dl(s) == 0); + + for (i = 0; i < clause_size(c); i++){ + lbool sig = !lit_sign(lits[i]); sig += sig - 1; + if (values[lit_var(lits[i])] == sig) + return l_True; + } + return l_False; +} + +int sat_solver_simplify(sat_solver* s) +{ + clause** reasons; + int type; + + assert(sat_solver_dl(s) == 0); + + if (sat_solver_propagate(s) != 0) + return false; + + if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0) + return true; + + reasons = s->reasons; + for (type = 0; type < 2; type++){ + vecp* cs = type ? &s->learnts : &s->clauses; + clause** cls = (clause**)vecp_begin(cs); + + int i, j; + for (j = i = 0; i < vecp_size(cs); i++){ + if (reasons[lit_var(*clause_begin(cls[i]))] != cls[i] && + clause_simplify(s,cls[i]) == l_True) + clause_remove(s,cls[i]); + else + cls[j++] = cls[i]; + } + vecp_resize(cs,j); + } + + s->simpdb_assigns = s->qhead; + // (shouldn't depend on 'stats' really, but it will do for now) + s->simpdb_props = (int)(s->stats.clauses_literals + s->stats.learnts_literals); + + return true; +} + + +static int clause_cmp (const void* x, const void* y) { + return clause_size((clause*)x) > 2 && (clause_size((clause*)y) == 2 || clause_activity((clause*)x) < clause_activity((clause*)y)) ? -1 : 1; } + +void sat_solver_reducedb(sat_solver* s) +{ + int i, j; + double extra_lim = s->cla_inc / vecp_size(&s->learnts); // Remove any clause below this activity + clause** learnts = (clause**)vecp_begin(&s->learnts); + clause** reasons = s->reasons; + + sat_solver_sort(vecp_begin(&s->learnts), vecp_size(&s->learnts), &clause_cmp); + + for (i = j = 0; i < vecp_size(&s->learnts) / 2; i++){ + if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i]) + clause_remove(s,learnts[i]); + else + learnts[j++] = learnts[i]; + } + for (; i < vecp_size(&s->learnts); i++){ + if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i] && clause_activity(learnts[i]) < extra_lim) + clause_remove(s,learnts[i]); + else + learnts[j++] = learnts[i]; + } + + //printf("reducedb deleted %d\n", vecp_size(&s->learnts) - j); + + + vecp_resize(&s->learnts,j); +} + +int sat_solver_addclause(sat_solver* s, lit* begin, lit* end) +{ + clause * c; + lit *i,*j; + int maxvar; + lbool* values; + lit last; + + veci_resize( &s->temp_clause, 0 ); + for ( i = begin; i < end; i++ ) + veci_push( &s->temp_clause, *i ); + begin = veci_begin( &s->temp_clause ); + end = begin + veci_size( &s->temp_clause ); + + if (begin == end) + return false; + + //printlits(begin,end); printf("\n"); + // insertion sort + maxvar = lit_var(*begin); + for (i = begin + 1; i < end; i++){ + lit l = *i; + maxvar = lit_var(l) > maxvar ? lit_var(l) : maxvar; + for (j = i; j > begin && *(j-1) > l; j--) + *j = *(j-1); + *j = l; + } + sat_solver_setnvars(s,maxvar+1); +// sat_solver_setnvars(s, lit_var(*(end-1))+1 ); + + /////////////////////////////////// + // add clause to internal storage + if ( s->pStore ) + { + int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, begin, end ); + assert( RetValue ); + } + /////////////////////////////////// + + //printlits(begin,end); printf("\n"); + values = s->assigns; + + // delete duplicates + last = lit_Undef; + for (i = j = begin; i < end; i++){ + //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)])); + lbool sig = !lit_sign(*i); sig += sig - 1; + if (*i == lit_neg(last) || sig == values[lit_var(*i)]) + return true; // tautology + else if (*i != last && values[lit_var(*i)] == l_Undef) + last = *j++ = *i; + } +// j = i; + + if (j == begin) // empty clause + return false; + + if (j - begin == 1) // unit clause + return sat_solver_enqueue(s,*begin,(clause*)0); + + // create new clause + c = clause_create_new(s,begin,j,0); + if ( c ) + vecp_push(&s->clauses,c); + + + s->stats.clauses++; + s->stats.clauses_literals += j - begin; + + return true; +} + + +double luby(double y, int x) +{ + int size, seq; + for (size = 1, seq = 0; size < x+1; seq++, size = 2*size + 1); + while (size-1 != x){ + size = (size-1) >> 1; + seq--; + x = x % size; + } + return pow(y, (double)seq); +} + +void luby_test() +{ + int i; + for ( i = 0; i < 20; i++ ) + printf( "%d ", (int)luby(2,i) ); + 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_dl(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_dl(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_dl(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 + sat_solver_assume(s,toLit(next)); + else + sat_solver_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; + ABC_INT64_T nof_conflicts; + ABC_INT64_T nof_learnts = sat_solver_nclauses(s) / 3; + lbool status = l_Undef; + lbool* values = s->assigns; + lit* i; + + //////////////////////////////////////////////// + if ( s->fSolved ) + { + if ( s->pStore ) + { + int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, NULL, NULL ); + assert( RetValue ); + } + return l_False; + } + //////////////////////////////////////////////// + + // set the external limits + s->nCalls++; + s->nRestarts = 0; + s->nConfLimit = 0; + s->nInsLimit = 0; + if ( nConfLimit ) + s->nConfLimit = s->stats.conflicts + nConfLimit; + if ( nInsLimit ) +// s->nInsLimit = s->stats.inspects + nInsLimit; + s->nInsLimit = s->stats.propagations + nInsLimit; + if ( nConfLimitGlobal && (s->nConfLimit == 0 || s->nConfLimit > nConfLimitGlobal) ) + s->nConfLimit = nConfLimitGlobal; + if ( nInsLimitGlobal && (s->nInsLimit == 0 || s->nInsLimit > nInsLimitGlobal) ) + s->nInsLimit = nInsLimitGlobal; + +#ifndef SAT_USE_ANALYZE_FINAL + + //printf("solve: "); printlits(begin, end); printf("\n"); + for (i = begin; i < end; i++){ + switch (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]){ + case 1: // l_True: + break; + case 0: // l_Undef + sat_solver_assume(s, *i); + if (sat_solver_propagate(s) == NULL) + break; + // fallthrough + case -1: // l_False + sat_solver_canceluntil(s, 0); + return l_False; + } + } + s->root_level = sat_solver_dl(s); + +#endif + +/* + // Perform assumptions: + root_level = assumps.size(); + for (int i = 0; i < assumps.size(); i++){ + Lit p = assumps[i]; + assert(var(p) < nVars()); + if (!sat_solver_assume(p)){ + GClause r = reason[var(p)]; + if (r != GClause_NULL){ + Clause* confl; + if (r.isLit()){ + confl = propagate_tmpbin; + (*confl)[1] = ~p; + (*confl)[0] = r.lit(); + }else + confl = r.clause(); + analyzeFinal(confl, true); + conflict.push(~p); + }else + conflict.clear(), + conflict.push(~p); + cancelUntil(0); + return false; } + Clause* confl = propagate(); + if (confl != NULL){ + analyzeFinal(confl), assert(conflict.size() > 0); + cancelUntil(0); + return false; } + } + assert(root_level == decisionLevel()); +*/ + +#ifdef SAT_USE_ANALYZE_FINAL + // Perform assumptions: + s->root_level = end - begin; + for ( i = begin; i < end; i++ ) + { + lit p = *i; + assert(lit_var(p) < s->size); + veci_push(&s->trail_lim,s->qtail); + if (!sat_solver_enqueue(s,p,(clause*)0)) + { + clause * r = s->reasons[lit_var(p)]; + if (r != NULL) + { + clause* confl; + if (clause_is_lit(r)) + { + confl = s->binary; + (clause_begin(confl))[1] = lit_neg(p); + (clause_begin(confl))[0] = clause_read_lit(r); + } + else + confl = r; + sat_solver_analyze_final(s, confl, 1); + veci_push(&s->conf_final, lit_neg(p)); + } + else + { + veci_resize(&s->conf_final,0); + veci_push(&s->conf_final, lit_neg(p)); + // the two lines below are a bug fix by Siert Wieringa + if (s->levels[lit_var(p)] > 0) + veci_push(&s->conf_final, p); + } + sat_solver_canceluntil(s, 0); + return l_False; + } + else + { + clause* confl = sat_solver_propagate(s); + if (confl != NULL){ + sat_solver_analyze_final(s, confl, 0); + assert(s->conf_final.size > 0); + sat_solver_canceluntil(s, 0); + return l_False; } + } + } + assert(s->root_level == sat_solver_dl(s)); +#endif + + s->nCalls2++; + + if (s->verbosity >= 1){ + printf("==================================[MINISAT]===================================\n"); + printf("| Conflicts | ORIGINAL | LEARNT | Progress |\n"); + printf("| | Clauses Literals | Limit Clauses Literals Lit/Cl | |\n"); + printf("==============================================================================\n"); + } + + while (status == l_Undef){ +// int nConfs = 0; + double Ratio = (s->stats.learnts == 0)? 0.0 : + s->stats.learnts_literals / (double)s->stats.learnts; + if ( s->nRuntimeLimit && time(NULL) > s->nRuntimeLimit ) + break; + + if (s->verbosity >= 1) + { + printf("| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %6.3f %% |\n", + (double)s->stats.conflicts, + (double)s->stats.clauses, + (double)s->stats.clauses_literals, + (double)nof_learnts, + (double)s->stats.learnts, + (double)s->stats.learnts_literals, + Ratio, + s->progress_estimate*100); + fflush(stdout); + } + nof_conflicts = (ABC_INT64_T)( 100 * luby(2, restart_iter++) ); +//printf( "%d ", (int)nof_conflicts ); +// nConfs = s->stats.conflicts; + status = sat_solver_search(s, nof_conflicts, nof_learnts); +// if ( status == l_True ) +// printf( "%d ", s->stats.conflicts - nConfs ); + +// nof_conflicts = nof_conflicts * 3 / 2; //*= 1.5; + nof_learnts = nof_learnts * 11 / 10; //*= 1.1; +//printf( "%d ", s->stats.conflicts ); + // quit the loop if reached an external limit + if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit ) + { +// printf( "Reached the limit on the number of conflicts (%d).\n", s->nConfLimit ); + break; + } +// if ( s->nInsLimit && s->stats.inspects > s->nInsLimit ) + if ( s->nInsLimit && s->stats.propagations > s->nInsLimit ) + { +// printf( "Reached the limit on the number of implications (%d).\n", s->nInsLimit ); + break; + } + if ( s->nRuntimeLimit && time(NULL) > s->nRuntimeLimit ) + break; + } +//printf( "\n" ); + if (s->verbosity >= 1) + printf("==============================================================================\n"); + + sat_solver_canceluntil(s,0); + + //////////////////////////////////////////////// + if ( status == l_False && s->pStore ) + { + int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, NULL, NULL ); + assert( RetValue ); + } + //////////////////////////////////////////////// + return status; +} + + +int sat_solver_nvars(sat_solver* s) +{ + return s->size; +} + + +int sat_solver_nclauses(sat_solver* s) +{ + return vecp_size(&s->clauses); +} + + +int sat_solver_nconflicts(sat_solver* s) +{ + return (int)s->stats.conflicts; +} + +//================================================================================================= +// Clause storage functions: + +void sat_solver_store_alloc( sat_solver * s ) +{ + assert( s->pStore == NULL ); + s->pStore = Sto_ManAlloc(); +} + +void sat_solver_store_write( sat_solver * s, char * pFileName ) +{ + if ( s->pStore ) Sto_ManDumpClauses( (Sto_Man_t *)s->pStore, pFileName ); +} + +void sat_solver_store_free( sat_solver * s ) +{ + if ( s->pStore ) Sto_ManFree( (Sto_Man_t *)s->pStore ); + s->pStore = NULL; +} + +int sat_solver_store_change_last( sat_solver * s ) +{ + if ( s->pStore ) return Sto_ManChangeLastClause( (Sto_Man_t *)s->pStore ); + return -1; +} + +void sat_solver_store_mark_roots( sat_solver * s ) +{ + if ( s->pStore ) Sto_ManMarkRoots( (Sto_Man_t *)s->pStore ); +} + +void sat_solver_store_mark_clauses_a( sat_solver * s ) +{ + if ( s->pStore ) Sto_ManMarkClausesA( (Sto_Man_t *)s->pStore ); +} + +void * sat_solver_store_release( sat_solver * s ) +{ + void * pTemp; + if ( s->pStore == NULL ) + return NULL; + pTemp = s->pStore; + s->pStore = NULL; + return pTemp; +} + +//================================================================================================= +// Sorting functions (sigh): + +static inline void selectionsort(void** array, int size, int(*comp)(const void *, const void *)) +{ + int i, j, best_i; + void* tmp; + + for (i = 0; i < size-1; i++){ + best_i = i; + for (j = i+1; j < size; j++){ + if (comp(array[j], array[best_i]) < 0) + best_i = j; + } + tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp; + } +} + + +static void sortrnd(void** array, int size, int(*comp)(const void *, const void *), double* seed) +{ + if (size <= 15) + selectionsort(array, size, comp); + + else{ + void* pivot = array[irand(seed, size)]; + void* tmp; + int i = -1; + int j = size; + + for(;;){ + do i++; while(comp(array[i], pivot)<0); + do j--; while(comp(pivot, array[j])<0); + + if (i >= j) break; + + tmp = array[i]; array[i] = array[j]; array[j] = tmp; + } + + sortrnd(array , i , comp, seed); + sortrnd(&array[i], size-i, comp, seed); + } +} + +void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *)) +{ +// int i; + double seed = 91648253; + sortrnd(array,size,comp,&seed); +// for ( i = 1; i < size; i++ ) +// assert(comp(array[i-1], array[i])<0); +} +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/bsat/satSolver_old.h b/src/sat/bsat/satSolver_old.h new file mode 100644 index 00000000..4c577b1e --- /dev/null +++ b/src/sat/bsat/satSolver_old.h @@ -0,0 +1,210 @@ +/************************************************************************************************** +MiniSat -- Copyright (c) 2005, Niklas Sorensson +http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/ + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ +// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko + +#ifndef satSolver_h +#define satSolver_h + + +#include <stdio.h> +#include <stdlib.h> +#include <string.h> +#include <assert.h> + +#include "satVec.h" +#include "satMem.h" + +ABC_NAMESPACE_HEADER_START + +//#define USE_FLOAT_ACTIVITY + +//================================================================================================= +// Public interface: + +struct sat_solver_t; +typedef struct sat_solver_t sat_solver; + +extern sat_solver* sat_solver_new(void); +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_rollback( sat_solver* s ); + +extern int sat_solver_nvars(sat_solver* s); +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); + +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 ); +extern void Sat_SolverDoubleClauses( sat_solver * p, int iVar ); + +// trace recording +extern void Sat_SolverTraceStart( sat_solver * pSat, char * pName ); +extern void Sat_SolverTraceStop( sat_solver * pSat ); +extern void Sat_SolverTraceWrite( sat_solver * pSat, int * pBeg, int * pEnd, int fRoot ); + +// clause storage +extern void sat_solver_store_alloc( sat_solver * s ); +extern void sat_solver_store_write( sat_solver * s, char * pFileName ); +extern void sat_solver_store_free( sat_solver * s ); +extern void sat_solver_store_mark_roots( sat_solver * s ); +extern void sat_solver_store_mark_clauses_a( sat_solver * s ); +extern void * sat_solver_store_release( sat_solver * s ); + +//================================================================================================= +// Solver representation: + +struct clause_t; +typedef struct clause_t clause; + +struct sat_solver_t +{ + int size; // nof variables + int cap; // size of varmaps + int qhead; // Head index of queue. + int qtail; // Tail index of queue. + + // clauses + vecp clauses; // List of problem constraints. (contains: clause*) + 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; // + lbool* assigns; // Current values of variables. + int* orderpos; // Index in variable order. + clause** reasons; // + int* levels; // + lit* trail; + char* polarity; + + clause* binary; // A temporary binary clause + lbool* tags; // + veci tagged; // (contains: var) + veci stack; // (contains: var) + + veci order; // Variable order. (heap) (contains: var) + veci trail_lim; // Separator indices for different decision levels in 'trail'. (contains: int) + veci model; // If problem is solved, this vector contains the model (contains: lbool). + veci conf_final; // If problem is unsatisfiable (possibly under assumptions), + // this vector represent the final conflict clause expressed in the assumptions. + + int root_level; // Level of first proper decision. + int simpdb_assigns;// Number of top-level assignments at last 'simplifyDB()'. + 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 + + stats_t stats; + + ABC_INT64_T nConfLimit; // external limit on the number of conflicts + ABC_INT64_T nInsLimit; // external limit on the number of implications + int nRuntimeLimit; // external limit on runtime + + veci act_vars; // variables whose activity has changed + double* factors; // the activity factors + int nRestarts; // the number of local restarts + int nCalls; // the number of local restarts + int nCalls2; // the number of local restarts + + Sat_MmStep_t * pMem; + + int fSkipSimplify; // set to one to skip simplification of the clause database + int fNotUseRandom; // do not allow random decisions with a fixed probability + + int * pGlobalVars; // for experiments with global vars during interpolation + // clause store + void * pStore; + int fSolved; + + // trace recording + FILE * pFile; + int nClauses; + int nRoots; + + veci temp_clause; // temporary storage for a CNF clause +}; + +static int sat_solver_var_value( sat_solver* s, int v ) +{ + assert( s->model.ptr != NULL && v < s->size ); + return (int)(s->model.ptr[v] == l_True); +} +static int sat_solver_var_literal( sat_solver* s, int v ) +{ + assert( s->model.ptr != NULL && v < s->size ); + return toLitCond( v, s->model.ptr[v] != l_True ); +} +static void sat_solver_act_var_clear(sat_solver* s) +{ + int i; + for (i = 0; i < s->size; i++) + s->activity[i] = 0.0; + s->var_inc = 1.0; +} +static void sat_solver_compress(sat_solver* s) +{ + if ( s->qtail != s->qhead ) + { + int RetValue = sat_solver_simplify(s); + assert( RetValue != 0 ); + } +} + +static int sat_solver_final(sat_solver* s, int ** ppArray) +{ + *ppArray = s->conf_final.ptr; + return s->conf_final.size; +} + +static int sat_solver_set_runtime_limit(sat_solver* s, int Limit) +{ + int nRuntimeLimit = s->nRuntimeLimit; + s->nRuntimeLimit = Limit; + return nRuntimeLimit; +} + +static int sat_solver_set_random(sat_solver* s, int fNotUseRandom) +{ + int fNotUseRandomOld = s->fNotUseRandom; + s->fNotUseRandom = fNotUseRandom; + return fNotUseRandomOld; +} + +ABC_NAMESPACE_HEADER_END + +#endif diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c index 17a9ba4a..5e809172 100644 --- a/src/sat/bsat/satUtil.c +++ b/src/sat/bsat/satUtil.c @@ -58,6 +58,7 @@ static void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, int fIncreme ***********************************************************************/ void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars ) { +/* FILE * pFile; void ** pClauses; int nClauses, i; @@ -110,6 +111,7 @@ void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBe fprintf( pFile, "\n" ); fclose( pFile ); +*/ } /**Function************************************************************* @@ -273,6 +275,7 @@ int * Sat_Solver2GetModel( sat_solver2 * p, int * pVars, int nVars ) ***********************************************************************/ void Sat_SolverDoubleClauses( sat_solver * p, int iVar ) { +/* clause * pClause; lit Lit, * pLits; int RetValue, nClauses, nVarsOld, nLitsOld, nLits, c, v; @@ -305,6 +308,7 @@ void Sat_SolverDoubleClauses( sat_solver * p, int iVar ) for ( v = 0; v < nLits; v++ ) pLits[v] -= nLitsOld; } +*/ } diff --git a/src/sat/bsat/vecRec.h b/src/sat/bsat/vecRec.h index d81cc631..fd0cc242 100644 --- a/src/sat/bsat/vecRec.h +++ b/src/sat/bsat/vecRec.h @@ -66,6 +66,9 @@ struct Vec_Rec_t_ for ( c = 1; c <= p->nChunks; c++ ) \ for ( s = 0; p->pChunks[c][s] && ((Handle) = (((c)<<16)|(s))); s += Size, assert(s < p->Mask) ) +#define Vec_RecForEachEntryStart( p, Size, Handle, c, s, hStart ) \ + for ( c = Vec_RecChunk(hStart), s = Vec_RecShift(hStart); c <= p->nChunks; c++, s = 0 ) \ + for ( ; p->pChunks[c][s] && ((Handle) = (((c)<<16)|(s))); s += Size, assert(s < p->Mask) ) //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -97,6 +100,22 @@ static inline Vec_Rec_t * Vec_RecAlloc() p->pChunks[1][0] = 0; return p; } +static inline void Vec_RecAlloc_( Vec_Rec_t * p ) +{ +// Vec_Rec_t * p; +// p = ABC_CALLOC( Vec_Rec_t, 1 ); + memset( p, 0, sizeof(Vec_Rec_t) ); + p->LogSize = 15; // chunk size = 2^15 ints = 128 Kb + p->Mask = (1 << p->LogSize) - 1; + p->hCurrent = (1 << 16); + p->nChunks = 1; + p->nChunksAlloc = 16; + p->pChunks = ABC_CALLOC( int *, p->nChunksAlloc ); + p->pChunks[0] = NULL; + p->pChunks[1] = ABC_ALLOC( int, (1 << 16) ); + p->pChunks[1][0] = 0; +// return p; +} /**Function************************************************************* @@ -239,6 +258,14 @@ static inline void Vec_RecFree( Vec_Rec_t * p ) ABC_FREE( p->pChunks ); ABC_FREE( p ); } +static inline void Vec_RecFree_( Vec_Rec_t * p ) +{ + int i; + for ( i = 0; i < p->nChunksAlloc; i++ ) + ABC_FREE( p->pChunks[i] ); + ABC_FREE( p->pChunks ); +// ABC_FREE( p ); +} /**Function************************************************************* |