Removing unused feature of the SAT solver (user-guided variable ordering).

src/sat/bsat/satSolver.c

@@ -557,8 +557,6 @@ static void sat_solver_canceluntil(sat_solver* s, int level) {
 
     s->qhead = s->qtail = bound;
     veci_resize(&s->trail_lim,level);
-    // update decision level
-    s->iDeciVar = level;
 }
 
 static void sat_solver_canceluntil_rollback(sat_solver* s, int NewBound) {
@@ -1160,7 +1158,6 @@ void sat_solver_delete(sat_solver* s)
     veci_delete(&s->pivot_vars);
     veci_delete(&s->temp_clause);
     veci_delete(&s->conf_final);
-    veci_delete(&s->vDeciVars);    
 
     // delete arrays
     if (s->reasons != 0){
@@ -1589,7 +1586,6 @@ static lbool sat_solver_search(sat_solver* 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;
-    int fGuided = (veci_size(&s->vDeciVars) > 0);
     ABC_INT64_T  conflictC  = 0;
     veci    learnt_clause;
     int     i;
@@ -1603,15 +1599,6 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts)
 //    veci_resize(&s->model,0);
     veci_new(&learnt_clause);
 
-    // update variable polarity
-    if ( fGuided )
-    {
-        int * pVars = veci_begin(&s->vDeciVars);
-        for ( i = 0; i < veci_size(&s->vDeciVars); i++ )
-            var_set_polar( s, pVars[i], 0 );
-        s->iDeciVar = 0;
-    }
-
     // use activity factors in every even restart
     if ( (s->nRestarts & 1) && veci_size(&s->act_vars) > 0 )
 //    if ( veci_size(&s->act_vars) > 0 )
@@ -1658,16 +1645,6 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts)
         }else{
             // NO CONFLICT
             int next;
- 
-            // Reached bound on number of conflicts:
-            if ( !fGuided )
-            {
-                if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || (s->nRuntimeLimit && (s->stats.conflicts & 63) == 0 && Abc_Clock() > s->nRuntimeLimit)){
-                    s->progress_estimate = sat_solver_progress(s);
-                    sat_solver_canceluntil(s,s->root_level);
-                    veci_delete(&learnt_clause);
-                    return l_Undef; }
-            }
 
             // Reached bound on number of conflicts:
             if ( (s->nConfLimit && s->stats.conflicts > s->nConfLimit) ||
@@ -1690,24 +1667,7 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts)
 
             // New variable decision:
             s->stats.decisions++;
-            if ( fGuided )
-            {
-                int nVars = veci_size(&s->vDeciVars);
-                int * pVars = veci_begin(&s->vDeciVars);
-                next = var_Undef;
-                assert( s->iDeciVar <= nVars );
-                while ( s->iDeciVar < nVars )
-                {
-                    int iVar = pVars[s->iDeciVar++];
-                    if ( var_value(s, iVar) == varX )
-                    {
-                        next = iVar;
-                        break;
-                    }
-                }
-            }
-            else
-                next = order_select(s,(float)random_var_freq);
+            next = order_select(s,(float)random_var_freq);
 
             if (next == var_Undef){
                 // Model found:

src/sat/bsat/satSolver.h

@@ -179,9 +179,6 @@ struct sat_solver_t
     // clause store
     void *      pStore;
     int         fSolved;
-    // decision variables
-    veci        vDeciVars;
-    int         iDeciVar;
 
     // trace recording
     FILE *      pFile;
@@ -226,18 +223,9 @@ static void sat_solver_compress(sat_solver* s)
         (void) RetValue;
     }
 }
-static void sat_solver_prepare_enum(sat_solver* s, int * pVars, int nVars )
-{
-    int v;
-    assert( veci_size(&s->vDeciVars) == 0 );
-    veci_new(&s->vDeciVars);
-    for ( v = 0; v < nVars; v++ )
-        veci_push(&s->vDeciVars,pVars[v]);
-}
 static void sat_solver_clean_polarity(sat_solver* s, int * pVars, int nVars )
 {
     int i;
-    assert( veci_size(&s->vDeciVars) == 0 );
     for ( i = 0; i < nVars; i++ )
         s->polarity[pVars[i]] = 0;
 }