From 5bcde4be2ba7c3cb873911f44b803638b6e6bc11 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Thu, 3 Sep 2015 21:56:29 -0700
Subject: Experiments with SAT-based collapsing.

---
 src/sat/bsat/satSolver.c | 48 ++++++++++++++++++++++++++++++++++++++++--------
 src/sat/bsat/satSolver.h | 11 +++++++++++
 2 files changed, 51 insertions(+), 8 deletions(-)

(limited to 'src/sat/bsat')

diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 5ea0b348..053b0587 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -556,6 +556,8 @@ 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) {
@@ -1156,6 +1158,7 @@ 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){
@@ -1577,8 +1580,8 @@ 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;
-
-    ABC_INT64_T  conflictC       = 0;
+    int fGuided = (veci_size(&s->vDeciVars) > 0);
+    ABC_INT64_T  conflictC  = 0;
     veci    learnt_clause;
     int     i;
 
@@ -1591,6 +1594,15 @@ 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 )
@@ -1639,11 +1651,14 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts)
             int next;
  
             // Reached bound on number of conflicts:
-            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; }
+            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) ||
@@ -1666,7 +1681,24 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts)
 
             // New variable decision:
             s->stats.decisions++;
-            next = order_select(s,(float)random_var_freq);
+            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);
 
             if (next == var_Undef){
                 // Model found:
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index d328e6d5..8e171031 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -179,6 +179,9 @@ struct sat_solver_t
     // clause store
     void *      pStore;
     int         fSolved;
+    // decision variables
+    veci        vDeciVars;
+    int         iDeciVar;
 
     // trace recording
     FILE *      pFile;
@@ -223,6 +226,14 @@ 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 int sat_solver_final(sat_solver* s, int ** ppArray)
 {
-- 
cgit v1.2.3