Changes to the main SAT solver: fixing performance bug (resetting decay params after each restart), making the SAT solver platform- and runtime-independent (by using interger-based activity).

4 files changed, 330 insertions, 315 deletions

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