Experiments with SAT-based collapsing.

4 files changed, 125 insertions, 8 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 148d8451..83077cb8 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -445,6 +445,7 @@ static int Abc_CommandAbc9FFTest             ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9Qbf                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9GenQbf             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9SatFx              ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9SatClp             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Inse               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Maxi               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Bmci               ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -1059,6 +1060,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&qbf",          Abc_CommandAbc9Qbf,          0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&genqbf",       Abc_CommandAbc9GenQbf,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&satfx",        Abc_CommandAbc9SatFx,        0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&satclp",       Abc_CommandAbc9SatClp,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&inse",         Abc_CommandAbc9Inse,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&maxi",         Abc_CommandAbc9Maxi,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&bmci",         Abc_CommandAbc9Bmci,         0 );
@@ -37120,6 +37122,77 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9SatClp( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern int Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fVerbose );
+    int nCubeLim = 1000;
+    int nBTLimit = 1000000;
+    int c, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "LCvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nCubeLim = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nCubeLim < 0 )
+                goto usage;
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nBTLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nBTLimit < 0 )
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9SatClp(): There is no AIG.\n" );
+        return 0;
+    }
+    Bmc_CollapseOne( pAbc->pGia, nCubeLim, nBTLimit, fVerbose );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &satclp [-LC num] [-vh]\n" );
+    Abc_Print( -2, "\t         performs SAT based collapsing\n" );
+    Abc_Print( -2, "\t-L num : the limit on the SOP size of one output [default = %d]\n", nCubeLim );
+    Abc_Print( -2, "\t-C num : the limit on the number of conflicts in one call [default = %d]\n", nBTLimit );
+    Abc_Print( -2, "\t-v     : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
 
 /**Function*************************************************************
 
diff --git a/src/sat/bmc/module.make b/src/sat/bmc/module.make
index 57039320..6d09b15c 100644
--- a/src/sat/bmc/module.make
+++ b/src/sat/bmc/module.make
@@ -11,6 +11,7 @@ SRC +=    src/sat/bmc/bmcBCore.c \
     src/sat/bmc/bmcCexMin2.c \
     src/sat/bmc/bmcCexTools.c \
     src/sat/bmc/bmcChain.c \
+    src/sat/bmc/bmcClp.c \
     src/sat/bmc/bmcEco.c \
     src/sat/bmc/bmcFault.c \
     src/sat/bmc/bmcFx.c \
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)
 {