Re-introducing floating-point activity in the SAT solver.

2 files changed, 171 insertions, 39 deletions

diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 3295fc6f..73d0cf36 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -145,12 +145,22 @@ static inline void order_update(sat_solver* s, int v) // updateorder
 
     assert(s->orderpos[v] != -1);
 
+#ifdef USE_FLOAT_ACTIVITY_NEW
+    while (i != 0 && xSat_LessThan(s->activity[heap[parent]], s->activity[x]) ){
+        heap[i]           = heap[parent];
+        orderpos[heap[i]] = i;
+        i                 = parent;
+        parent            = (i - 1) / 2;
+    }
+#else
     while (i != 0 && s->activity[x] > s->activity[heap[parent]]){
         heap[i]           = heap[parent];
         orderpos[heap[i]] = i;
         i                 = parent;
         parent            = (i - 1) / 2;
     }
+#endif
+
     heap[i]     = x;
     orderpos[x] = i;
 }
@@ -192,11 +202,21 @@ static inline int  order_select(sat_solver* s, float random_var_freq) // selectv
             int    i     = 0;
             int    child = 1;
             while (child < size){
+
+#ifdef USE_FLOAT_ACTIVITY_NEW
+                if (child+1 < size && xSat_LessThan(s->activity[heap[child]], s->activity[heap[child+1]]) )
+                    child++;
+                assert(child < size);
+                if ( !xSat_LessThan(s->activity[x], s->activity[heap[child]]) )
+                    break;
+#else
                 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;
+#endif
+
                 heap[i]           = heap[child];
                 orderpos[heap[i]] = i;
                 i                 = child;
@@ -213,6 +233,7 @@ static inline int  order_select(sat_solver* s, float random_var_freq) // selectv
 
 void sat_solver_set_var_activity(sat_solver* s, int * pVars, int nVars) 
 {
+#ifndef USE_FLOAT_ACTIVITY_NEW
     int i;
     for (i = 0; i < s->size; i++)
         s->activity[i] = 0;
@@ -223,6 +244,7 @@ void sat_solver_set_var_activity(sat_solver* s, int * pVars, int nVars)
         s->activity[iVar] = nVars-i;
         order_update( s, iVar );
     }
+#endif
 }
 
 //=================================================================================================
@@ -230,6 +252,46 @@ void sat_solver_set_var_activity(sat_solver* s, int * pVars, int nVars)
 
 #ifdef USE_FLOAT_ACTIVITY
 
+#ifdef USE_FLOAT_ACTIVITY_NEW
+
+static inline void act_var_rescale(sat_solver* s)  {
+    xFloat_t * activity = s->activity;
+    int i;
+    for (i = 0; i < s->size; i++)
+        activity[i] = xSat_FloatDiv( activity[i], 1<<10 ); // activity[i] / 2^1024
+    s->var_inc = xSat_FloatDiv( s->var_inc, 1<<10 ); 
+}
+static inline void act_clause_rescale(sat_solver* s) {
+    xFloat_t* activity = (xFloat_t *)veci_begin(&s->act_clas);
+    int i;
+    for (i = 0; i < veci_size(&s->act_clas); i++)
+        activity[i] = xSat_FloatDiv( activity[i], 1<<10 ); // activity[i] / 2^1024
+    s->cla_inc = xSat_FloatDiv( s->cla_inc, 1<<10 );
+}
+static inline void act_var_bump(sat_solver* s, int v) {
+    s->activity[v] = xSat_FloatAdd( s->activity[v], s->var_inc );
+    if ( xSat_LessThan(xSat_FloatCreate(1 << 12, 1 << 15), s->activity[v]) ) // 2^4096 < s->activity[v]
+        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) {
+    assert(0);
+}
+static inline void act_var_bump_factor(sat_solver* s, int v) {
+    assert(0);
+}
+static inline void act_clause_bump(sat_solver* s, clause *c) {
+    xFloat_t* act = (xFloat_t *)veci_begin(&s->act_clas) + c->lits[c->size];
+    *act = xSat_FloatAdd( *act, s->cla_inc );
+    if ( xSat_LessThan(xSat_FloatCreate(1 << 12, 1 << 15), *act) )  // 2^4096 < *act
+        act_clause_rescale(s);
+}
+static inline void act_var_decay(sat_solver* s)    { s->var_inc = xSat_FloatMul(s->var_inc, s->var_decay); }
+static inline void act_clause_decay(sat_solver* s) { s->cla_inc = xSat_FloatMul(s->cla_inc, s->cla_decay); }
+
+#else
+
 static inline void act_var_rescale(sat_solver* s)  {
     double* activity = s->activity;
     int i;
@@ -238,18 +300,11 @@ static inline void act_var_rescale(sat_solver* s)  {
     s->var_inc *= 1e-100;
 }
 static inline void act_clause_rescale(sat_solver* s) {
-//    static abctime Total = 0;
-    clause** cs = (clause**)veci_begin(&s->learnts);
-    int i;//, clk = Abc_Clock();
-    for (i = 0; i < veci_size(&s->learnts); i++){
-        float a = clause_activity(cs[i]);
-        clause_setactivity(cs[i], a * (float)1e-20);
-    }
+    float* activity = (float *)veci_begin(&s->act_clas);
+    int i;
+    for (i = 0; i < veci_size(&s->act_clas); i++)
+        activity[i] *= (float)1e-20;
     s->cla_inc *= (float)1e-20;
-
-    Total += Abc_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;
@@ -259,31 +314,22 @@ 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);
-    if (s->orderpos[v] != -1)
-        order_update(s,v);
+    assert(0);
 }
 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);
-    if (s->orderpos[v] != -1)
-        order_update(s,v);
+    assert(0);
 }
 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);
+    float* act = (float *)veci_begin(&s->act_clas) + c->lits[c->size];
+    *act += s->cla_inc;
+    if (*act > 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; }
 
+#endif
+
 #else
 
 static inline void act_var_rescale(sat_solver* s) {
@@ -296,17 +342,12 @@ static inline void act_var_rescale(sat_solver* s) {
 }
 
 static inline void act_clause_rescale(sat_solver* s) {
-    static abctime Total = 0;
-    abctime clk = Abc_Clock();
     unsigned* activity = (unsigned *)veci_begin(&s->act_clas);
     int i;
     for (i = 0; i < veci_size(&s->act_clas); i++)
         activity[i] >>= 14;
     s->cla_inc >>= 14;
     s->cla_inc = Abc_MaxInt( s->cla_inc, (1<<10) );
-    Total += Abc_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) {
@@ -447,7 +488,15 @@ int sat_solver_clause_new(sat_solver* s, lit* begin, lit* end, int learnt)
         assert( clause_id(c) == veci_size(&s->act_clas) );
 //        veci_push(&s->learned, h);
 //        act_clause_bump(s,clause_read(s, h));
+#ifdef USE_FLOAT_ACTIVITY
+#ifdef USE_FLOAT_ACTIVITY_NEW
+        veci_push(&s->act_clas, xSat_Float2Uint(xSat_FloatCreateConst1()));
+#else
+        veci_push(&s->act_clas, 0);
+#endif
+#else
         veci_push(&s->act_clas, (1<<10));
+#endif
         s->stats.learnts++;
         s->stats.learnts_literals += size;
     }
@@ -1055,10 +1104,17 @@ sat_solver* sat_solver_new(void)
     s->qhead                  = 0;
     s->qtail                  = 0;
 #ifdef USE_FLOAT_ACTIVITY
+#ifdef USE_FLOAT_ACTIVITY_NEW
+    s->var_inc                = xSat_FloatCreateConst1();
+    s->cla_inc                = xSat_FloatCreateConst1();
+    s->var_decay              = xSat_FloatFromFloat( (float)(1 / 0.95) );
+    s->cla_decay              = xSat_FloatFromFloat( (float)(1 / 0.999) );
+#else
     s->var_inc                = 1;
     s->cla_inc                = 1;
     s->var_decay              = (float)(1 / 0.95 );
     s->cla_decay              = (float)(1 / 0.999);
+#endif
 #else
     s->var_inc                = (1 <<  5);
     s->cla_inc                = (1 << 11);
@@ -1126,10 +1182,17 @@ sat_solver* zsat_solver_new_seed(double seed)
     s->qhead                  = 0;
     s->qtail                  = 0;
 #ifdef USE_FLOAT_ACTIVITY
+#ifdef USE_FLOAT_ACTIVITY_NEW
+    s->var_inc                = xSat_FloatCreateConst1();
+    s->cla_inc                = xSat_FloatCreateConst1();
+    s->var_decay              = xSat_FloatFromFloat( (float)(1 / 0.95) );
+    s->cla_decay              = xSat_FloatFromFloat( (float)(1 / 0.999) );
+#else
     s->var_inc                = 1;
     s->cla_inc                = 1;
     s->var_decay              = (float)(1 / 0.95 );
     s->cla_decay              = (float)(1 / 0.999);
+#endif
 #else
     s->var_inc                = (1 <<  5);
     s->cla_inc                = (1 << 11);
@@ -1174,7 +1237,11 @@ void sat_solver_setnvars(sat_solver* s,int n)
         s->tags      = ABC_REALLOC(char,   s->tags,     s->cap);
         s->loads     = ABC_REALLOC(char,   s->loads,    s->cap);
 #ifdef USE_FLOAT_ACTIVITY
+#ifdef USE_FLOAT_ACTIVITY_NEW
+        s->activity  = ABC_REALLOC(xFloat_t,   s->activity, s->cap);
+#else
         s->activity  = ABC_REALLOC(double,   s->activity, s->cap);
+#endif
 #else
         s->activity  = ABC_REALLOC(unsigned, s->activity, s->cap);
         s->activity2 = ABC_REALLOC(unsigned, s->activity2,s->cap);
@@ -1198,7 +1265,11 @@ void sat_solver_setnvars(sat_solver* s,int n)
         if ( s->wlists[2*var+1].ptr == NULL )
             veci_new(&s->wlists[2*var+1]);
 #ifdef USE_FLOAT_ACTIVITY
+#ifdef USE_FLOAT_ACTIVITY_NEW
+        s->activity[var] = xSat_FloatCreateConst1();
+#else
         s->activity[var] = 0;
+#endif
 #else
         s->activity[var] = (1<<10);
 #endif
@@ -1292,10 +1363,17 @@ void sat_solver_restart( sat_solver* s )
     s->qhead                  = 0;
     s->qtail                  = 0;
 #ifdef USE_FLOAT_ACTIVITY
+#ifdef USE_FLOAT_ACTIVITY_NEW
+    s->var_inc                = xSat_FloatCreateConst1();
+    s->cla_inc                = xSat_FloatCreateConst1();
+    s->var_decay              = xSat_FloatFromFloat( (float)(1 / 0.95) );
+    s->cla_decay              = xSat_FloatFromFloat( (float)(1 / 0.999) );
+#else
     s->var_inc                = 1;
     s->cla_inc                = 1;
-    s->var_decay              = (float)(1 / 0.95  );
-    s->cla_decay              = (float)(1 / 0.999 );
+    s->var_decay              = (float)(1 / 0.95 );
+    s->cla_decay              = (float)(1 / 0.999);
+#endif
 #else
     s->var_inc                = (1 <<  5);
     s->cla_inc                = (1 << 11);
@@ -1341,10 +1419,17 @@ void zsat_solver_restart_seed( sat_solver* s, double seed )
     s->qhead                  = 0;
     s->qtail                  = 0;
 #ifdef USE_FLOAT_ACTIVITY
+#ifdef USE_FLOAT_ACTIVITY_NEW
+    s->var_inc                = xSat_FloatCreateConst1();
+    s->cla_inc                = xSat_FloatCreateConst1();
+    s->var_decay              = xSat_FloatFromFloat( (float)(1 / 0.95) );
+    s->cla_decay              = xSat_FloatFromFloat( (float)(1 / 0.999) );
+#else
     s->var_inc                = 1;
     s->cla_inc                = 1;
-    s->var_decay              = (float)(1 / 0.95  );
-    s->cla_decay              = (float)(1 / 0.999 );
+    s->var_decay              = (float)(1 / 0.95 );
+    s->cla_decay              = (float)(1 / 0.999);
+#endif
 #else
     s->var_inc                = (1 <<  5);
     s->cla_inc                = (1 << 11);
@@ -1382,7 +1467,11 @@ double sat_solver_memory( sat_solver* s )
     Mem += s->cap * sizeof(char);     // ABC_FREE(s->tags     );
     Mem += s->cap * sizeof(char);     // ABC_FREE(s->loads    );
 #ifdef USE_FLOAT_ACTIVITY
+#ifdef USE_FLOAT_ACTIVITY_NEW
+    Mem += s->cap * sizeof(xFloat_t);   // ABC_FREE(s->activity );
+#else
     Mem += s->cap * sizeof(double);   // ABC_FREE(s->activity );
+#endif
 #else
     Mem += s->cap * sizeof(unsigned); // ABC_FREE(s->activity );
     if ( s->activity2 )
@@ -1600,10 +1689,17 @@ void sat_solver_rollback( sat_solver* s )
         s->qhead                  = 0;
         s->qtail                  = 0;
 #ifdef USE_FLOAT_ACTIVITY
+#ifdef USE_FLOAT_ACTIVITY_NEW
+        s->var_inc                = xSat_FloatCreateConst1();
+        s->cla_inc                = xSat_FloatCreateConst1();
+        s->var_decay              = xSat_FloatFromFloat( (float)(1 / 0.95) );
+        s->cla_decay              = xSat_FloatFromFloat( (float)(1 / 0.999) );
+#else
         s->var_inc                = 1;
         s->cla_inc                = 1;
-        s->var_decay              = (float)(1 / 0.95  );
-        s->cla_decay              = (float)(1 / 0.999 );
+        s->var_decay              = (float)(1 / 0.95 );
+        s->cla_decay              = (float)(1 / 0.999);
+#endif
 #else
         s->var_inc                = (1 <<  5);
         s->cla_inc                = (1 << 11);
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index 6ed611e1..226d8c7a 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -30,10 +30,12 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "satVec.h"
 #include "satClause.h"
+#include "sat/xsat/xsatFloat.h"
 
 ABC_NAMESPACE_HEADER_START
 
 //#define USE_FLOAT_ACTIVITY
+//#define USE_FLOAT_ACTIVITY_NEW
 
 //=================================================================================================
 // Public interface:
@@ -117,11 +119,23 @@ struct sat_solver_t
 
     // activities
 #ifdef USE_FLOAT_ACTIVITY
+#ifdef USE_FLOAT_ACTIVITY_NEW
+    xFloat_t    var_inc;       // Amount to bump next variable with.
+    xFloat_t    var_inc2;      // Amount to bump next variable with.
+    xFloat_t    var_decay;     // INVERSE decay factor for variable activity: stores 1/decay. 
+    xFloat_t    cla_inc;       // Amount to bump next clause with.
+    xFloat_t    cla_decay;     // INVERSE decay factor for clause activity: stores 1/decay.
+    xFloat_t*   activity;      // A heuristic measurement of the activity of a variable.
+    xFloat_t*   activity2;     // backup variable activity
+#else
     double      var_inc;       // Amount to bump next variable with.
+    double      var_inc2;      // 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*     activity2;     // A heuristic measurement of the activity of a variable.
+#endif
 #else
     int         var_inc;       // Amount to bump next variable with.
     int         var_inc2;      // Amount to bump next variable with.
@@ -218,9 +232,21 @@ static int sat_solver_var_literal( sat_solver* s, int v )
 static void sat_solver_act_var_clear(sat_solver* s) 
 {
     int i;
+#ifdef USE_FLOAT_ACTIVITY
+#ifdef USE_FLOAT_ACTIVITY_NEW
+    for (i = 0; i < s->size; i++)
+        s->activity[i] = xSat_FloatCreateConst1();
+    s->var_inc = xSat_FloatCreateConst1();
+#else
     for (i = 0; i < s->size; i++)
         s->activity[i] = 0;
     s->var_inc = 1;
+#endif
+#else
+    for (i = 0; i < s->size; i++)
+        s->activity[i] = 0;
+    s->var_inc = (1 <<  5);
+#endif
 }
 static void sat_solver_compress(sat_solver* s) 
 {
@@ -286,8 +312,18 @@ static inline void sat_solver_bookmark(sat_solver* s)
     Sat_MemBookMark( &s->Mem );
     if ( s->activity2 )
     {
+#ifdef USE_FLOAT_ACTIVITY
+#ifdef USE_FLOAT_ACTIVITY_NEW
+        s->var_inc2 = s->var_inc;
+        memcpy( s->activity2, s->activity, sizeof(xFloat_t) * s->iVarPivot );
+#else
+        s->var_inc2 = s->var_inc;
+        memcpy( s->activity2, s->activity, sizeof(double) * s->iVarPivot );
+#endif
+#else
         s->var_inc2 = s->var_inc;
         memcpy( s->activity2, s->activity, sizeof(unsigned) * s->iVarPivot );
+#endif
     }
 }
 static inline void sat_solver_set_pivot_variables( sat_solver* s, int * pPivots, int nPivots )