SAT variable profiling.

src/sat/bmc/bmcBmc3.c

@@ -1636,6 +1636,7 @@ nTimeUndec += clock() - clk2;
             }
             printf( "%4d %s : ", f, fUnfinished ? "-" : "+" );
             printf( "Var =%8.0f. ", (double)p->nSatVars );
+            printf( "Var2 =%8.0f. ", (double)sat_solver_count_usedvars(p->pSat) );
             printf( "Cla =%9.0f. ", (double)p->pSat->stats.clauses );
             printf( "Cnf =%7.0f. ",(double)p->pSat->stats.conflicts );
 //            printf( "Imp =%10.0f. ", (double)p->pSat->stats.propagations );

src/sat/bsat/satClause.h

@@ -35,8 +35,8 @@ ABC_NAMESPACE_HEADER_START
 
 //#define LEARNT_MAX_START_DEFAULT  0
 #define LEARNT_MAX_START_DEFAULT  10000
-#define LEARNT_MAX_INCRE_DEFAULT   1000
-#define LEARNT_MAX_RATIO_DEFAULT     50
+#define LEARNT_MAX_INCRE_DEFAULT   2000
+#define LEARNT_MAX_RATIO_DEFAULT     80
 
 ////////////////////////////////////////////////////////////////////////
 ///                    STRUCTURE DEFINITIONS                         ///

src/sat/bsat/satSolver.c

@@ -466,6 +466,12 @@ static int clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt)
 static inline int sat_solver_enqueue(sat_solver* s, lit l, int from)
 {
     int v  = lit_var(l);
+    if ( s->pFreqs[v] == 0 )
+//    {
+        s->pFreqs[v] = 1;
+//        s->nVarUsed++;
+//    }
+
 #ifdef VERBOSEDEBUG
     printf(L_IND"enqueue("L_LIT")\n", L_ind, L_lit(l));
 #endif
@@ -1033,6 +1039,8 @@ void sat_solver_setnvars(sat_solver* s,int n)
         s->activity  = ABC_REALLOC(unsigned, s->activity, s->cap);
         s->activity2 = ABC_REALLOC(unsigned, s->activity2,s->cap);
 #endif
+        s->pFreqs    = ABC_REALLOC(char,   s->tags,     s->cap);
+
         if ( s->factors )
         s->factors   = ABC_REALLOC(double, s->factors,  s->cap);
         s->orderpos  = ABC_REALLOC(int,    s->orderpos, s->cap);
@@ -1054,6 +1062,7 @@ void sat_solver_setnvars(sat_solver* s,int n)
 #else
         s->activity[var] = (1<<10);
 #endif
+        s->pFreqs[var]   = 0;
         if ( s->factors )
         s->factors [var] = 0;
 //        *((int*)s->vi + var) = 0; s->vi[var].val = varX;
@@ -1106,6 +1115,7 @@ void sat_solver_delete(sat_solver* s)
         ABC_FREE(s->tags     );
         ABC_FREE(s->activity );
         ABC_FREE(s->activity2);
+        ABC_FREE(s->pFreqs   );
         ABC_FREE(s->factors  );
         ABC_FREE(s->orderpos );
         ABC_FREE(s->reasons  );
@@ -1321,7 +1331,7 @@ void sat_solver_reducedb(sat_solver* s)
 
     // report the results
     TimeTotal += clock() - clk;
-    if ( s->fVerbose )
+//    if ( s->fVerbose )
     {
     Abc_Print(1, "reduceDB: Keeping %7d out of %7d clauses (%5.2f %%)  ",
         s->stats.learnts, nLearnedOld, 100.0 * s->stats.learnts / nLearnedOld );

src/sat/bsat/satSolver.h

@@ -121,6 +121,8 @@ struct sat_solver_t
     unsigned*   activity;      // A heuristic measurement of the activity of a variable.
     unsigned*   activity2;     // backup variable activity
 #endif
+    char *      pFreqs;        // how many times this variable was assigned a value
+    int         nVarUsed;
 
 //    varinfo *   vi;            // variable information
     int*        levels;        //
@@ -248,6 +250,18 @@ static inline void sat_solver_bookmark(sat_solver* s)
     }
 }
 
+static inline int sat_solver_count_usedvars(sat_solver* s)
+{
+    int i, nVars = 0;
+    for ( i = 0; i < s->size; i++ )
+        if ( s->pFreqs[i] )
+        {
+            s->pFreqs[i] = 0;
+            nVars++;
+        }
+    return nVars;
+}
+
 static inline int sat_solver_add_const( sat_solver * pSat, int iVar, int fCompl )
 {
     lit Lits[1];