Experiments with Glucose.

4 files changed, 157 insertions, 27 deletions

diff --git a/src/sat/glucose/AbcGlucose.cpp b/src/sat/glucose/AbcGlucose.cpp
index 8e82e654..8d8868ce 100644
--- a/src/sat/glucose/AbcGlucose.cpp
+++ b/src/sat/glucose/AbcGlucose.cpp
@@ -245,6 +245,49 @@ int bmcg_sat_solver_conflictnum(bmcg_sat_solver* s)
     return ((Gluco::Solver*)s)->conflicts;
 }
 
+int bmcg_sat_solver_minimize_assumptions(bmcg_sat_solver * s, int * plits, int nlits)
+{
+    vec<int>*array = &((Gluco::Solver*)s)->user_vec;
+    int i, nlitsL, nlitsR, nresL, nresR, status;
+    if ( nlits == 1 )
+    {
+        // since the problem is UNSAT, we try to solve it without assuming the last literal
+        // if the result is UNSAT, the last literal can be dropped; otherwise, it is needed
+        status = bmcg_sat_solver_solve( s, NULL, 0 );
+        return status != -1; // return 1 if the problem is not UNSAT
+    }
+    assert( nlits >= 2 );
+    nlitsL = nlits / 2;
+    nlitsR = nlits - nlitsL;
+    // solve with these assumptions
+    status = bmcg_sat_solver_solve( s, plits, nlitsL );
+    if ( status == -1 ) // these are enough
+        return bmcg_sat_solver_minimize_assumptions( s, plits, nlitsL );
+    // these are not enough
+    // solve for the right lits
+// assume left bits
+    nresL = nlitsR == 1 ? 1 : bmcg_sat_solver_minimize_assumptions( s, plits + nlitsL, nlitsR );
+// unassume left bits
+    // swap literals
+    array->clear();
+    for ( i = 0; i < nlitsL; i++ )
+        array->push(plits[i]);
+    for ( i = 0; i < nresL; i++ )
+        plits[i] = plits[nlitsL+i];
+    for ( i = 0; i < nlitsL; i++ )
+        plits[nresL+i] = (*array)[i];
+    // solve with these assumptions
+// assume right bits
+    status = bmcg_sat_solver_solve( s, plits, nresL );
+    if ( status == -1 ) // these are enough
+// unassume right bits
+        return nresL;
+    // solve for the left lits
+    nresR = nlitsL == 1 ? 1 : bmcg_sat_solver_minimize_assumptions( s, plits + nresL, nlitsL );
+// unassume right bits
+    return nresL + nresR;
+}
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -298,7 +341,7 @@ void Glucose_SolveCnf( char * pFilename, Glucose_Pars * pPars )
 ***********************************************************************/
 Vec_Int_t * Glucose_SolverFromAig( Gia_Man_t * p, SimpSolver& S )
 {
-    //abctime clk = Abc_Clock();
+    abctime clk = Abc_Clock();
     int * pLit, * pStop, i;
     Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8 /*nLutSize*/, 0 /*fCnfObjIds*/, 1/*fAddOrCla*/, 0, 0/*verbose*/ );
     for ( i = 0; i < pCnf->nClauses; i++ )
@@ -315,12 +358,104 @@ Vec_Int_t * Glucose_SolverFromAig( Gia_Man_t * p, SimpSolver& S )
         S.addClause(lits);
     }
     Vec_Int_t * vCnfIds = Vec_IntAllocArrayCopy(pCnf->pVarNums,pCnf->nVars);
+    printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+    Cnf_DataFree(pCnf);
+    return vCnfIds;
+}
+
+// procedure below does not work because glucose_solver_addclause() expects Solver
+Vec_Int_t * Glucose_SolverFromAig2( Gia_Man_t * p, SimpSolver& S ) 
+{
+    Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8 /*nLutSize*/, 0 /*fCnfObjIds*/, 1/*fAddOrCla*/, 0, 0/*verbose*/ );
+    for ( int i = 0; i < pCnf->nClauses; i++ )
+        if ( !glucose_solver_addclause( &S, pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) )
+            assert( 0 );
+    Vec_Int_t * vCnfIds = Vec_IntAllocArrayCopy(pCnf->pVarNums,pCnf->nVars);
     //printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
     //Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
     Cnf_DataFree(pCnf);
     return vCnfIds;
 }
 
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Glucose_GenerateSop( Gia_Man_t * p )
+{
+    bmcg_sat_solver * pSat[2] = { bmcg_sat_solver_start(), bmcg_sat_solver_start() };
+
+    // generate CNF for the on-set and off-set
+    Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8 /*nLutSize*/, 0 /*fCnfObjIds*/, 0/*fAddOrCla*/, 0, 0/*verbose*/ );
+    int i,n,nVars = Gia_ManCiNum(p);
+    int iFirstVar = pCnf->nVars - nVars;
+    assert( Gia_ManCoNum(p) == 1 );
+    for ( n = 0; n < 2; n++ )
+    {
+        int Lit = Abc_Var2Lit( 1, !n );  // output variable is 1
+        for ( i = 0; i < pCnf->nClauses; i++ )
+            if ( !bmcg_sat_solver_addclause( pSat[n], pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) )
+                assert( 0 );
+        if ( !bmcg_sat_solver_addclause( pSat[n], &Lit, 1 ) )
+            assert( 0 );
+    }
+    Cnf_DataFree( pCnf );
+
+    // generate assignments
+    Vec_Int_t * vLits = Vec_IntAlloc( nVars );
+    Vec_Str_t * vCube = Vec_StrAlloc( nVars + 4 );
+    while ( 1 )
+    {
+        // generate onset minterm
+        int status = bmcg_sat_solver_solve( pSat[1], NULL, 0 );
+        if ( status == -1 )
+            break;
+        assert( status == 1 );
+        Vec_IntClear( vLits );
+        for ( i = 0; i < nVars; i++ )
+            Vec_IntPush( vLits, Abc_Var2Lit(iFirstVar+i, !bmcg_sat_solver_read_cex_varvalue(pSat[1], iFirstVar+i)) );
+        // expand it against offset
+        status = bmcg_sat_solver_solve( pSat[0], Vec_IntArray(vLits), Vec_IntSize(vLits) );
+        assert( status == -1 );
+        int * pFinal, nFinal = bmcg_sat_solver_final( pSat[0], &pFinal );
+        // print cube
+        Vec_StrFill( vCube, nVars, '-' );
+        Vec_StrPrintF( vCube, " 1\n\0" );
+        for ( i = 0; i < nFinal; i++ )
+            Vec_StrWriteEntry( vCube, Abc_Lit2Var(pFinal[i]) - iFirstVar, (char)('0' + Abc_LitIsCompl(pFinal[i])) );
+        printf( "%s", Vec_StrArray(vCube) );
+        // add blocking clause
+        if ( !bmcg_sat_solver_addclause( pSat[1], pFinal, nFinal ) )
+            break;
+    }
+    Vec_IntFree( vLits );
+    Vec_StrFree( vCube );
+
+    bmcg_sat_solver_stop( pSat[0] );
+    bmcg_sat_solver_stop( pSat[1] );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Glucose_SolveAig(Gia_Man_t * p, Glucose_Pars * pPars)
 {  
     abctime clk = Abc_Clock();
@@ -329,6 +464,7 @@ int Glucose_SolveAig(Gia_Man_t * p, Glucose_Pars * pPars)
     S.verbosity = pPars->verb;
     S.verbEveryConflicts = 50000;
     S.showModel = false;
+    //S.verbosity = 2;
     S.setConfBudget( pPars->nConfls > 0 ? (int64_t)pPars->nConfls : -1 );
 
     S.parsing = 1;
@@ -347,7 +483,7 @@ int Glucose_SolveAig(Gia_Man_t * p, Glucose_Pars * pPars)
         S.eliminate(true);
     
     vec<Lit> dummy;
-    lbool ret = S.solveLimited(dummy);
+    lbool ret = S.solveLimited(dummy, 0);
 
     if ( pPars->verb ) glucose_print_stats(S, Abc_Clock() - clk);
     printf(ret == l_True ? "SATISFIABLE" : ret == l_False ? "UNSATISFIABLE" : "INDETERMINATE");
diff --git a/src/sat/glucose/Glucose.cpp b/src/sat/glucose/Glucose.cpp
index e90bf402..479f08f9 100644
--- a/src/sat/glucose/Glucose.cpp
+++ b/src/sat/glucose/Glucose.cpp
@@ -224,6 +224,12 @@ bool Solver::addClause_(vec<Lit>& ps)
     assert(decisionLevel() == 0);
     if (!ok) return false;
 
+    if ( 0 ) {
+        for ( int i = 0; i < ps.size(); i++ )
+            printf( "%d ", ps[i] );
+        printf( "\n" );
+    }
+
     // Check if clause is satisfied and remove false/duplicate literals:
     sort(ps);
 
@@ -797,25 +803,18 @@ CRef Solver::propagate()
         vec<Watcher>&  ws  = watches[p];
         Watcher        *i, *j, *end;
         num_props++;
-
         
-            // First, Propagate binary clauses 
+        // First, Propagate binary clauses 
         vec<Watcher>&  wbin  = watchesBin[p];
-        
         for(int k = 0;k<wbin.size();k++) {
-          
           Lit imp = wbin[k].blocker;
-          
           if(value(imp) == l_False) {
             return wbin[k].cref;
           }
-          
           if(value(imp) == l_Undef) {
             uncheckedEnqueue(imp,wbin[k].cref);
           }
         }
-    
-
 
         for (i = j = (Watcher*)ws, end = i + ws.size();  i != end;){
             // Try to avoid inspecting the clause:
@@ -836,7 +835,6 @@ CRef Solver::propagate()
             Lit     first = c[0];
             Watcher w     = Watcher(cr, first);
             if (first != blocker && value(first) == l_True){
-              
               *j++ = w; continue; }
 
             // Look for new watch:
@@ -912,40 +910,35 @@ struct reduceDB_lt {
     // Main criteria... Like in MiniSat we keep all binary clauses
     if(ca[x].size()> 2 && ca[y].size()==2) return 1;
     
-    if(ca[y].size()>2 && ca[x].size()==2) return 0;
+    if(ca[y].size()> 2 && ca[x].size()==2) return 0;
     if(ca[x].size()==2 && ca[y].size()==2) return 0;
     
     // Second one  based on literal block distance
     if(ca[x].lbd()> ca[y].lbd()) return 1;
     if(ca[x].lbd()< ca[y].lbd()) return 0;    
     
-    
     // Finally we can use old activity or size, we choose the last one
-        return ca[x].activity() < ca[y].activity();
-        //return x->size() < y->size();
-
-        //return ca[x].size() > 2 && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity()); } 
+    return ca[x].activity() < ca[y].activity();
+    //return x->size() < y->size();
+    //return ca[x].size() > 2 && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity()); } 
     }    
 };
 
 void Solver::reduceDB()
-{
- 
-  int     i, j;
+{ 
+  int i, j;
   nbReduceDB++;
   sort(learnts, reduceDB_lt(ca));
 
   // We have a lot of "good" clauses, it is difficult to compare them. Keep more !
   if(ca[learnts[learnts.size() / RATIOREMOVECLAUSES]].lbd()<=3) nbclausesbeforereduce +=specialIncReduceDB; 
   // Useless :-)
-  if(ca[learnts.last()].lbd()<=5)  nbclausesbeforereduce +=specialIncReduceDB; 
-  
+  if(ca[learnts.last()].lbd()<=5)  nbclausesbeforereduce +=specialIncReduceDB;   
   
   // Don't delete binary or locked clauses. From the rest, delete clauses from the first half
   // Keep clauses which seem to be usefull (their lbd was reduce during this sequence)
 
   int limit = learnts.size() / 2;
-
   for (i = j = 0; i < learnts.size(); i++){
     Clause& c = ca[learnts[i]];
     if (c.lbd()>2 && c.size() > 2 && c.canBeDel() &&  !locked(c) && (i < limit)) {
@@ -965,12 +958,9 @@ void Solver::reduceDB()
 
 void Solver::removeSatisfied(vec<CRef>& cs)
 {
-  
     int i, j;
     for (i = j = 0; i < cs.size(); i++){
         Clause& c = ca[cs[i]];
-
-
         if (satisfied(c)) 
             removeClause(cs[i]);
         else
diff --git a/src/sat/glucose/SimpSolver.cpp b/src/sat/glucose/SimpSolver.cpp
index 566472fe..83d97e77 100644
--- a/src/sat/glucose/SimpSolver.cpp
+++ b/src/sat/glucose/SimpSolver.cpp
@@ -604,6 +604,7 @@ void SimpSolver::extendModel()
 
 bool SimpSolver::eliminate(bool turn_off_elim)
 {
+    abctime clk = Abc_Clock();
     if (!simplify())
         return false;
     else if (!use_simplification)
@@ -690,6 +691,7 @@ bool SimpSolver::eliminate(bool turn_off_elim)
         printf("c |  Eliminated clauses:     %10.2f Mb                                                                |\n", 
                double(elimclauses.size() * sizeof(uint32_t)) / (1024*1024));
 
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
     return ok;
 }
 
@@ -702,6 +704,7 @@ void SimpSolver::cleanUpClauses()
         if (ca[clauses[i]].mark() == 0)
             clauses[j++] = clauses[i];
     clauses.shrink(i - j);
+    printf( "Simplication removed %d variables and %d clauses.  ", eliminated_vars, i - j );
 }
 
 
diff --git a/src/sat/glucose/Solver.h b/src/sat/glucose/Solver.h
index dfc8f954..3a90f847 100644
--- a/src/sat/glucose/Solver.h
+++ b/src/sat/glucose/Solver.h
@@ -60,6 +60,7 @@ public:
     bool terminate_search_early;         // used to stop the solver early if it as instructed by an external caller
     int * pstop;                         // another callback
     uint64_t nRuntimeLimit;              // runtime limit
+    vec<int> user_vec;
 
     // Problem specification:
     //
@@ -229,7 +230,7 @@ protected:
     vec<char>           polarity;         // The preferred polarity of each variable.
     vec<char>           decision;         // Declares if a variable is eligible for selection in the decision heuristic.
     vec<Lit>            trail;            // Assignment stack; stores all assigments made in the order they were made.
-        vec<int>            nbpos;
+    vec<int>            nbpos;
     vec<int>            trail_lim;        // Separator indices for different decision levels in 'trail'.
     vec<VarData>        vardata;          // Stores reason and level for each variable.
     int                 qhead;            // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat).