Proof-logging in the updated solver.

5 files changed, 211 insertions, 120 deletions

diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c
index 0a5920c7..3b30910d 100644
--- a/src/sat/bsat/satProof.c
+++ b/src/sat/bsat/satProof.c
@@ -60,15 +60,18 @@ static inline cla     Proof_NodeHandle (Vec_Int_t* p, satset* c)  { return satse
 static inline int     Proof_NodeCheck  (Vec_Int_t* p, satset* c)  { return satset_check( (veci*)p, c );  }
 static inline int     Proof_NodeSize   (int nEnts)                { return sizeof(satset)/4 + nEnts;     }
 
+// iterating through nodes in the proof
 #define Proof_ForeachNode( p, pNode, h )                         \
     for ( h = 1; (h < Vec_IntSize(p)) && ((pNode) = Proof_NodeRead(p, h)); h += Proof_NodeSize(pNode->nEnts) )
 #define Proof_ForeachNodeVec( pVec, p, pNode, i )            \
     for ( i = 0; (i < Vec_IntSize(pVec)) && ((pNode) = Proof_NodeRead(p, Vec_IntEntry(pVec,i))); i++ )
+
+// iterating through fanins of a proof node
 #define Proof_NodeForeachFanin( p, pNode, pFanin, i )        \
     for ( i = 0; (i < (int)pNode->nEnts) && (((pFanin) = (pNode->pEnts[i] & 1) ? NULL : Proof_NodeRead(p, pNode->pEnts[i] >> 2)), 1); i++ )
 #define Proof_NodeForeachLeaf( pLeaves, pNode, pLeaf, i )    \
     for ( i = 0; (i < (int)pNode->nEnts) && (((pLeaf) = (pNode->pEnts[i] & 1) ? Proof_NodeRead(pLeaves, pNode->pEnts[i] >> 2) : NULL), 1); i++ )
-#define Proof_NodeForeachFaninRoot( p, pLeaves, pNode, pFanin, i )    \
+#define Proof_NodeForeachFaninLeaf( p, pLeaves, pNode, pFanin, i )    \
     for ( i = 0; (i < (int)pNode->nEnts) && ((pFanin) = (pNode->pEnts[i] & 1) ? Proof_NodeRead(pLeaves, pNode->pEnts[i] >> 2) : Proof_NodeRead(p, pNode->pEnts[i] >> 2)); i++ )
 
 ////////////////////////////////////////////////////////////////////////
@@ -77,6 +80,26 @@ static inline int     Proof_NodeSize   (int nEnts)                { return sizeo
 
 /**Function*************************************************************
 
+  Synopsis    [Returns the number of proof nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Proof_CountAll( Vec_Int_t * p )
+{
+    satset * pNode;
+    int hNode, Counter = 0;
+    Proof_ForeachNode( p, pNode, hNode )
+        Counter++;
+    return Counter;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Collects all resolution nodes belonging to the proof.]
 
   Description []
@@ -187,7 +210,8 @@ Vec_Int_t * Proof_CollectUsedIter( Vec_Int_t * vProof, Vec_Int_t * vRoots, int h
             Proof_CollectUsed_iter( vProof, pNode, vUsed, vStack );
     }
     Vec_IntFree( vStack );
-    Abc_PrintTime( 1, "Iterative clause collection time", clock() - clk );
+//    Abc_PrintTime( 1, "Iterative clause collection time", clock() - clk );
+
 /*
     // verify topological order
     iPrev = 0;
@@ -200,7 +224,7 @@ Vec_Int_t * Proof_CollectUsedIter( Vec_Int_t * vProof, Vec_Int_t * vRoots, int h
     clk = clock();
 //    Vec_IntSort( vUsed, 0 );
     Abc_Sort( Vec_IntArray(vUsed), Vec_IntSize(vUsed) );
-    Abc_PrintTime( 1, "Postprocessing with sorting time", clock() - clk );
+//    Abc_PrintTime( 1, "Postprocessing with sorting time", clock() - clk );
 
     // verify topological order
     iPrev = 0;
@@ -394,46 +418,6 @@ void Proof_Check( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hRoot )
 
 /**Function*************************************************************
 
-  Synopsis    [Reduces the proof to contain only roots and their children.]
-
-  Description [The result is updated proof and updated roots.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sat_ProofReduce( Vec_Int_t * vProof, Vec_Int_t * vRoots )
-{
-    Vec_Int_t * vUsed;
-    satset * pNode, * pFanin;
-    int i, k, nSize = 1;
-    // collect visited nodes
-    vUsed = Proof_CollectUsedIter( vProof, vRoots, 0 );
-    // relabel nodes to use smaller space
-    Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
-    {
-        pNode->Id = nSize;
-        nSize += Proof_NodeSize(pNode->nEnts);
-        Proof_NodeForeachFanin( vProof, pNode, pFanin, k )
-            if ( pFanin )
-                pNode->pEnts[i] = (pFanin->Id << 2) | (pNode->pEnts[i] & 2);
-    }
-    // compact the nodes
-    Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
-    {
-        memmove( Vec_IntArray(vProof) + pNode->Id, pNode, Proof_NodeSize(pNode->nEnts) );
-        pNode->Id = 0;
-    }
-    // report the result
-    printf( "The proof was reduced from %d to %d (by %6.2f %%)\n", 
-        Vec_IntSize(vProof), nSize, 100.0 * (Vec_IntSize(vProof) - nSize) / Vec_IntSize(vProof) );
-    Vec_IntShrink( vProof, nSize );
-}
-
-
-/**Function*************************************************************
-
   Synopsis    [Collects nodes belonging to the UNSAT core.]
 
   Description [The result is the array of root clause indexes.]
@@ -545,7 +529,7 @@ Aig_Man_t * Sat_ProofInterpolant( Vec_Int_t * vClauses, Vec_Int_t * vProof, int
     Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
     {
         assert( pNode->nEnts > 1 );
-        Proof_NodeForeachFaninRoot( vProof, vClauses, pNode, pFanin, k )
+        Proof_NodeForeachFaninLeaf( vProof, vClauses, pNode, pFanin, k )
         {
             if ( k == 0 )
                 pObj = Aig_ObjFromLit( pAig, pFanin->Id );
@@ -573,7 +557,66 @@ Aig_Man_t * Sat_ProofInterpolant( Vec_Int_t * vClauses, Vec_Int_t * vProof, int
     Vec_IntFree( vCoreNums );
     return pAig;
 }
+ 
+/**Function*************************************************************
+
+  Synopsis    [Reduces the proof to contain only roots and their children.]
+
+  Description [The result is updated proof and updated roots.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sat_ProofReduce( veci * pProof, veci * pRoots )
+{
+    int fVerbose = 0;
+    Vec_Int_t * vProof = (Vec_Int_t *)pProof;
+    Vec_Int_t * vRoots = (Vec_Int_t *)pRoots;
+    Vec_Int_t * vUsed;
+    satset * pNode, * pFanin;
+    int i, k, hTemp, hNewHandle = 1, clk = clock();
+    static int TimeTotal = 0;
+
+    // collect visited nodes
+    vUsed = Proof_CollectUsedIter( vProof, vRoots, 0 );
+//    printf( "The proof uses %d out of %d proof nodes (%.2f %%)\n", 
+//        Vec_IntSize(vUsed), Proof_CountAll(vProof), 
+//        100.0 * Vec_IntSize(vUsed) / Proof_CountAll(vProof) );
+
+    // relabel nodes to use smaller space
+    Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
+    {
+        pNode->Id = hNewHandle; hNewHandle += Proof_NodeSize(pNode->nEnts);
+        Proof_NodeForeachFanin( vProof, pNode, pFanin, k )
+            if ( pFanin )
+            {
+                assert( (pNode->pEnts[k] >> 2) == Proof_NodeHandle(vProof, pFanin) );
+                pNode->pEnts[k] = (pFanin->Id << 2) | (pNode->pEnts[k] & 2);
+            }
+    }
+    // update roots
+    Proof_ForeachNodeVec( vRoots, vProof, pNode, i )
+        Vec_IntWriteEntry( vRoots, i, pNode->Id );
+    // compact the nodes
+    Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
+    {
+        hTemp = pNode->Id; pNode->Id = 0;
+        memmove( Vec_IntArray(vProof) + hTemp, pNode, sizeof(int)*Proof_NodeSize(pNode->nEnts) );
+    }
+    Vec_IntFree( vUsed );
 
+    // report the result
+    if ( fVerbose )
+    {
+        printf( "The proof was reduced from %10d to %10d integers (by %6.2f %%)  ", 
+            Vec_IntSize(vProof), hNewHandle, 100.0 * (Vec_IntSize(vProof) - hNewHandle) / Vec_IntSize(vProof) );
+        TimeTotal += clock() - clk;
+        Abc_PrintTime( 1, "Time", TimeTotal );
+    }
+    Vec_IntShrink( vProof, hNewHandle );
+}
 
 /**Function*************************************************************
 
@@ -591,7 +634,7 @@ void Sat_ProofTest( veci * pClauses, veci * pProof, veci * pRoots, int hRoot )
     Vec_Int_t * vClauses  = (Vec_Int_t *)pClauses;
     Vec_Int_t * vProof    = (Vec_Int_t *)pProof;
     Vec_Int_t * vRoots    = (Vec_Int_t *)pRoots;
-    Vec_Int_t * vUsed, * vCore;
+//    Vec_Int_t * vUsed, * vCore;
 //    int i, Entry;
 /*
     // collect visited clauses
@@ -600,6 +643,7 @@ void Sat_ProofTest( veci * pClauses, veci * pProof, veci * pRoots, int hRoot )
     printf( "Found %d useful resolution nodes.\n", Vec_IntSize(vUsed) );
     Vec_IntFree( vUsed );
 */
+/*
     // collect visited clauses
     vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot );
     Proof_CleanCollected( vProof, vUsed );
@@ -608,7 +652,7 @@ void Sat_ProofTest( veci * pClauses, veci * pProof, veci * pRoots, int hRoot )
 
     vCore = Sat_ProofCore( vClauses, vProof, hRoot );
     Vec_IntFree( vCore );
-
+*/
 /*
     printf( "Found %d useful resolution nodes.\n", Vec_IntSize(vUsed) );
     Vec_IntFree( vUsed );
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 8b6468b2..c448d8c3 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -805,7 +805,6 @@ static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt)
     }
 
     // update size of learnt + statistics
-    s->stats.max_literals += veci_size(learnt);
     veci_resize(learnt,j);
     s->stats.tot_literals += j;
 
@@ -1150,7 +1149,6 @@ sat_solver* sat_solver_new(void)
     s->stats.clauses_literals = 0;
     s->stats.learnts          = 0;
     s->stats.learnts_literals = 0;
-    s->stats.max_literals     = 0;
     s->stats.tot_literals     = 0;
 
 #ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index 325f69cc..843a33b6 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -162,7 +162,7 @@ void   clause_set_partA(sat_solver2* s, int h, int partA)        { clause_read(s
 int    clause_id(sat_solver2* s, int h)                          { return clause_read(s, h)->Id;            }
 
 #define sat_solver_foreach_clause( s, c, h )  satset_foreach_entry( &s->clauses, c, h, 1 )
-#define sat_solver_foreach_learnt( s, c, h )  satset_foreach_entry( &s->clauses, c, h, s->iLearntFirst )
+#define sat_solver_foreach_learnt( s, c, h )  satset_foreach_entry( &s->clauses, c, h, s->hLearntFirst )
 
 //=================================================================================================
 // Simple helpers:
@@ -177,10 +177,10 @@ static inline void proof_chain_start( sat_solver2* s, satset* c )
 {
     if ( s->fProofLogging )
     {
-        s->iStartChain = veci_size(&s->proof_clas);
-        veci_push(&s->proof_clas, 0);
-        veci_push(&s->proof_clas, 0);
-        veci_push(&s->proof_clas, clause_proofid(s, c, 0) );
+        s->iStartChain = veci_size(&s->proofs);
+        veci_push(&s->proofs, 0);
+        veci_push(&s->proofs, 0);
+        veci_push(&s->proofs, clause_proofid(s, c, 0) );
     }
 }
 
@@ -189,7 +189,7 @@ static inline void proof_chain_resolve( sat_solver2* s, satset* cls, int Var )
     if ( s->fProofLogging )
     {
         satset* c = cls ? cls : var_unit_clause( s, Var );
-        veci_push(&s->proof_clas, clause_proofid(s, c, var_is_partA(s,Var)) );
+        veci_push(&s->proofs, clause_proofid(s, c, var_is_partA(s,Var)) );
 //        printf( "%d %d  ", clause_proofid(s, c), Var );
     }
 }
@@ -199,9 +199,9 @@ static inline int proof_chain_stop( sat_solver2* s )
     if ( s->fProofLogging )
     {
         int RetValue = s->iStartChain;
-        satset* c = (satset*)(veci_begin(&s->proof_clas) + s->iStartChain);
-        assert( s->iStartChain > 0 && s->iStartChain < veci_size(&s->proof_clas) );
-        c->nEnts = veci_size(&s->proof_clas) - s->iStartChain - 2;
+        satset* c = (satset*)(veci_begin(&s->proofs) + s->iStartChain);
+        assert( s->iStartChain > 0 && s->iStartChain < veci_size(&s->proofs) );
+        c->nEnts = veci_size(&s->proofs) - s->iStartChain - 2;
         s->iStartChain = 0;
         return RetValue;
     }
@@ -303,9 +303,9 @@ static inline void act_clause_rescale(sat_solver2* s) {
         claActs[i] *= (float)1e-20;
     s->cla_inc *= (float)1e-20;
 
-    printf( "Rescaling...   Cla inc = %10.3f  Conf = %10d   ", s->cla_inc,  s->stats.conflicts );
     Total += clock() - clk;
-    Abc_PrintTime( 1, "Time", Total );
+//    printf( "Rescaling...   Cla inc = %10.3f  Conf = %10d   ", s->cla_inc,  s->stats.conflicts );
+//    Abc_PrintTime( 1, "Time", Total );
 }
 static inline void act_var_bump(sat_solver2* s, int v) {
     s->activity[v] += s->var_inc;
@@ -343,9 +343,9 @@ static inline void act_clause_rescale(sat_solver2* s) {
     s->cla_inc >>= 14;
     s->cla_inc = Abc_MaxInt( s->cla_inc, (1<<10) );
 
-    printf( "Rescaling...   Cla inc = %5d  Conf = %10d   ", s->cla_inc,  s->stats.conflicts );
     Total += clock() - clk;
-    Abc_PrintTime( 1, "Time", Total );
+//    printf( "Rescaling...   Cla inc = %5d  Conf = %10d   ", s->cla_inc,  s->stats.conflicts );
+//    Abc_PrintTime( 1, "Time", Total );
 }
 static inline void act_var_bump(sat_solver2* s, int v) {
     s->activity[v] += s->var_inc;
@@ -425,9 +425,9 @@ static int clause_new(sat_solver2* s, lit* begin, lit* end, int learnt, int proo
     assert(((ABC_PTRUINT_T)c & 3) == 0);
 
     // remember the last one and first learnt
-    s->iLearntLast = Cid;
-    if ( learnt && s->iLearntFirst == -1 )
-        s->iLearntFirst = Cid;
+    s->hLearntLast = Cid;
+    if ( learnt && s->hLearntFirst == -1 )
+        s->hLearntFirst = Cid;
 
     // watch the clause
     if ( nLits > 1 ){
@@ -844,7 +844,6 @@ static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt)
     solver2_clear_marks( s );
 
     // update size of learnt + statistics
-    s->stats.max_literals += veci_size(learnt);
     veci_resize(learnt,j);
     s->stats.tot_literals += j;
 
@@ -972,7 +971,7 @@ WatchFound: i++;
 }
 
 
-
+/*
 static void clause_remove(sat_solver2* s, satset* c)
 {
     assert(lit_neg(c->pEnts[0]) < s->size*2);
@@ -989,7 +988,7 @@ static void clause_remove(sat_solver2* s, satset* c)
         s->stats.clauses_literals -= c->nEnts;
     }
 }
-
+*/
 
 static lbool clause_simplify(sat_solver2* s, satset* c)
 {
@@ -1032,10 +1031,11 @@ int sat_solver2_simplify(sat_solver2* s)
     s->simpdb_props   = (int)(s->stats.clauses_literals + s->stats.learnts_literals);
     return true;
 }
+
+/*
  
 void solver2_reducedb(sat_solver2* s)
 {
-/*
     satset* c;
     cla Cid;
     int clk = clock();
@@ -1068,11 +1068,11 @@ printf( "ReduceDB removed %10d clauses (out of %10d)... Cutoff = %8d  ", Counter
 Abc_PrintTime( 1, "Time", clock() - clk );
     }
     ABC_FREE( pPerm );
-*/
 }
+*/
 
 
-static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts, ABC_INT64_T * nof_learnts)
+static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts)
 {
     double  random_var_freq = s->fNotUseRandom ? 0.0 : 0.02;
 
@@ -1147,13 +1147,6 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts, ABC_INT64
                 // Simplify the set of problem clauses:
 //                sat_solver2_simplify(s);
 
-            if (*nof_learnts >= 0 && s->stats.learnts - s->qtail >= *nof_learnts)
-            {
-                // Reduce the set of learnt clauses:
-                solver2_reducedb(s);
-                *nof_learnts = *nof_learnts * 11 / 10; //*= 1.1;
-            }
-
             // New variable decision:
             s->stats.decisions++;
             next = order_select(s,(float)random_var_freq);
@@ -1206,13 +1199,14 @@ sat_solver2* sat_solver2_new(void)
     veci_new(&s->mark_levels);
     veci_new(&s->min_lit_order); 
     veci_new(&s->min_step_order);
-    veci_new(&s->proof_clas); veci_push(&s->proof_clas, -1);
+    veci_new(&s->learnt_live);
+    veci_new(&s->proofs); veci_push(&s->proofs, -1);
     veci_new(&s->claActs);    veci_push(&s->claActs,    -1);
     veci_new(&s->claProofs);  veci_push(&s->claProofs,  -1);
 
     // initialize other
-    s->iLearntFirst           = -1; // the first learnt clause 
-    s->iLearntLast            = -1; // the last learnt clause 
+    s->hLearntFirst           = -1; // the first learnt clause 
+    s->hLearntLast            = -1; // the last learnt clause 
 #ifdef USE_FLOAT_ACTIVITY
     s->var_inc                = 1;
     s->cla_inc                = 1;
@@ -1233,8 +1227,8 @@ sat_solver2* sat_solver2_new(void)
     // prealloc some arrays
     if ( s->fProofLogging )
     {
-        s->proof_clas.cap = (1 << 20);
-        s->proof_clas.ptr = ABC_REALLOC( int, s->proof_clas.ptr, s->proof_clas.cap );
+        s->proofs.cap = (1 << 20);
+        s->proofs.ptr = ABC_REALLOC( int, s->proofs.ptr, s->proofs.cap );
     }
     return s;
 }
@@ -1281,13 +1275,13 @@ void sat_solver2_setnvars(sat_solver2* s,int n)
 
 void sat_solver2_delete(sat_solver2* s)
 {
-    satset * c = clause_read(s, s->iLearntLast);
+    satset * c = clause_read(s, s->hLearntLast);
     // report statistics
-    printf( "Used %6.2f Mb for proof-logging.   Unit clauses = %d.\n", 2.0 * veci_size(&s->proof_clas) / (1<<20), s->nUnits );
+    printf( "Used %6.2f Mb for proof-logging.   Unit clauses = %d.\n", 2.0 * veci_size(&s->proofs) / (1<<20), s->nUnits );
 
     Sat_ProofTest( 
         &s->clauses,      // clauses
-        &s->proof_clas,   // proof clauses
+        &s->proofs,   // proof clauses
         NULL,             // proof roots
         veci_begin(&s->claProofs)[c->Id]  // one root
          );  
@@ -1303,7 +1297,8 @@ void sat_solver2_delete(sat_solver2* s)
     veci_delete(&s->mark_levels);
     veci_delete(&s->min_lit_order);
     veci_delete(&s->min_step_order);
-    veci_delete(&s->proof_clas);
+    veci_delete(&s->learnt_live);
+    veci_delete(&s->proofs);
     veci_delete(&s->claActs);
     veci_delete(&s->claProofs);
     veci_delete(&s->clauses);
@@ -1448,6 +1443,73 @@ void luby2_test()
     printf( "\n" );
 }
 
+
+// updates clauses, watches, units, and proof
+void solver2_reducedb(sat_solver2* s)
+{
+    extern void Sat_ProofReduce( veci * pProof, veci * pRoots );
+    satset * c;
+    cla h,* pArray,* pArray2;
+    int Counter = 0, CounterStart = s->stats.learnts * 2 / 3;
+    int i, j, k, hTemp, hHandle, clk = clock();
+    static int TimeTotal = 0;
+
+    // remove 2/3 of learned clauses while skipping small clauses
+    veci_resize( &s->learnt_live, 0 );
+    sat_solver_foreach_learnt( s, c, h )
+        if ( Counter++ > CounterStart || c->nEnts < 3 )
+            veci_push( &s->learnt_live, h );
+        else
+            c->mark = 1;
+    // report the results
+    printf( "reduceDB: Keeping %7d out of %7d clauses (%5.2f %%)  ", 
+        veci_size(&s->learnt_live), s->stats.learnts, 100.0 * veci_size(&s->learnt_live) / s->stats.learnts );
+
+    // remap clause proofs and clauses
+    hHandle = s->hLearntFirst;
+    pArray  = veci_begin(&s->claProofs);
+    pArray2 = veci_begin(&s->claActs);
+    satset_foreach_entry_vec( &s->learnt_live, &s->clauses, c, i )
+    {
+        pArray[i+1]  = pArray[c->Id];
+        pArray2[i+1] = pArray2[c->Id];
+        c->Id = hHandle; hHandle += satset_size(c->nEnts);
+    }
+    veci_resize(&s->claProofs,veci_size(&s->learnt_live)+1);
+    veci_resize(&s->claActs,veci_size(&s->learnt_live)+1);
+
+    // compact watches 
+    for ( i = 0; i < s->size*2; i++ )
+    {
+        pArray = veci_begin(&s->wlists[i]);
+        for ( j = k = 0; k < veci_size(&s->wlists[i]); k++ )
+            if ( pArray[k] < s->hLearntFirst )
+                pArray[j++] = pArray[k];
+            else if ( !(c = clause_read(s, pArray[k]))->mark )
+                pArray[j++] = c->Id;
+        veci_resize(&s->wlists[i],j);
+    }
+    // compact units
+    for ( i = 0; i < s->size; i++ )
+        if ( s->units[i] >= s->hLearntFirst )
+            s->units[i] = clause_read(s, s->units[i])->Id;
+    // compact clauses
+    satset_foreach_entry_vec( &s->learnt_live, &s->clauses, c, i )
+    {
+        hTemp = c->Id; c->Id = i + 1;
+        memmove( veci_begin(&s->clauses) + hTemp, c, sizeof(int)*satset_size(c->nEnts) );
+    }
+    assert( hHandle == hTemp + satset_size(c->nEnts) );
+    veci_resize(&s->clauses,hHandle);
+    s->stats.learnts = veci_size(&s->learnt_live);
+
+    // compact proof (compacts 'proofs' and update 'claProofs')
+    Sat_ProofReduce( &s->proofs, &s->claProofs );
+
+    TimeTotal += clock() - clk;
+    Abc_PrintTime( 1, "Time", TimeTotal );
+}
+
 int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
 {
     int restart_iter = 0;
@@ -1457,7 +1519,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
 //    lbool*  values        = s->assigns;
     lit*    i;
 
-    s->iLearntLast = -1;
+    s->hLearntLast = -1;
 
     // set the external limits
 //    s->nCalls++;
@@ -1570,8 +1632,6 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
     assert(s->root_level == solver2_dlevel(s));
 #endif
 
-//    s->nCalls2++;
-
     if (s->verbosity >= 1){
         printf("==================================[MINISAT]===================================\n");
         printf("| Conflicts |     ORIGINAL     |              LEARNT              | Progress |\n");
@@ -1580,12 +1640,6 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
     }
 
     while (status == l_Undef){
-//        int nConfs = 0;
-        double Ratio = (s->stats.learnts == 0)? 0.0 :
-            s->stats.learnts_literals / (double)s->stats.learnts;
-        if ( s->nRuntimeLimit && time(NULL) > s->nRuntimeLimit )
-            break;
-
         if (s->verbosity >= 1)
         {
             printf("| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %6.3f %% |\n", 
@@ -1595,35 +1649,27 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
                 (double)nof_learnts, 
                 (double)s->stats.learnts, 
                 (double)s->stats.learnts_literals,
-                Ratio,
+                (s->stats.learnts == 0)? 0.0 : (double)s->stats.learnts_literals / s->stats.learnts,
                 s->progress_estimate*100);
             fflush(stdout);
         }
+        if ( s->nRuntimeLimit && time(NULL) > s->nRuntimeLimit )
+            break;
+         // reduce the set of learnt clauses:
+        if (nof_learnts > 0 && s->stats.learnts > nof_learnts)
+        {
+            solver2_reducedb(s);
+            nof_learnts = nof_learnts * 11 / 10;
+        }
+        // perform next run
         nof_conflicts = (ABC_INT64_T)( 100 * luby2(2, restart_iter++) );
-//printf( "%d ", (int)nof_conflicts );
-//        nConfs = s->stats.conflicts;
-        status = solver2_search(s, nof_conflicts, &nof_learnts);
-//        if ( status == l_True )
-//            printf( "%d ", s->stats.conflicts - nConfs );
-
-//        nof_conflicts = nof_conflicts * 3 / 2; //*= 1.5;
-//printf( "%d ", s->stats.conflicts  );
+        status = solver2_search(s, nof_conflicts);
         // quit the loop if reached an external limit
         if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit )
-        {
-//            printf( "Reached the limit on the number of conflicts (%d).\n", s->nConfLimit );
             break;
-        }
-//        if ( s->nInsLimit  && s->stats.inspects > s->nInsLimit )
         if ( s->nInsLimit  && s->stats.propagations > s->nInsLimit )
-        {
-//            printf( "Reached the limit on the number of implications (%d).\n", s->nInsLimit );
-            break;
-        }
-        if ( s->nRuntimeLimit && time(NULL) > s->nRuntimeLimit )
             break;
     }
-//printf( "\n" );
     if (s->verbosity >= 1)
         printf("==============================================================================\n");
 
diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h
index d77c0141..01216146 100644
--- a/src/sat/bsat/satSolver2.h
+++ b/src/sat/bsat/satSolver2.h
@@ -103,8 +103,8 @@ struct sat_solver2_t
     // clauses
     veci            clauses;        // clause memory
     veci*           wlists;         // watcher lists (for each literal)
-    int             iLearntFirst;   // the first learnt clause 
-    int             iLearntLast;    // in proof-logging mode, the ID of the final conflict clause (conf_final)
+    int             hLearntFirst;   // the first learnt clause 
+    int             hLearntLast;    // in proof-logging mode, the ID of the final conflict clause (conf_final)
 
     // activities
 #ifdef USE_FLOAT_ACTIVITY
@@ -139,10 +139,10 @@ struct sat_solver2_t
     veci            mark_levels;    // temporary storage for labeled levels
     veci            min_lit_order;  // ordering of removable literals
     veci            min_step_order; // ordering of resolution steps
-    veci            glob_vars;      // global variables
+    veci            learnt_live;    // remaining clauses after reduce DB
 
     // proof logging
-    veci            proof_clas;     // sequence of proof clauses
+    veci            proofs;         // sequence of proof records
     int             iStartChain;    // temporary variable to remember beginning of the current chain in proof logging
     int             nUnits;         // the total number of unit clauses
 
@@ -178,6 +178,8 @@ static inline void    satset_print  (satset * c)          {
 
 #define satset_foreach_entry( p, c, h, s )            \
     for ( h = s; (h < veci_size(p)) && (((c) = satset_read(p, h)), 1); h += satset_size(c->nEnts) )
+#define satset_foreach_entry_vec( pVec, p, c, i )     \
+    for ( i = 0; (i < veci_size(pVec)) && ((c) = satset_read(p, veci_begin(pVec)[i])); i++ )
 #define satset_foreach_var( p, var, i, start )        \
     for ( i = start; (i < (int)(p)->nEnts) && ((var) = lit_var((p)->pEnts[i])); i++ )
 
diff --git a/src/sat/bsat/satVec.h b/src/sat/bsat/satVec.h
index 441ec974..bf117521 100644
--- a/src/sat/bsat/satVec.h
+++ b/src/sat/bsat/satVec.h
@@ -139,8 +139,9 @@ static inline int  lit_check(lit l, int n) { return l >= 0 && lit_var(l) < n;
 
 struct stats_t
 {
-    ABC_INT64_T   starts, decisions, propagations, inspects, conflicts;
-    ABC_INT64_T   clauses, clauses_literals, learnts, learnts_literals, max_literals, tot_literals;
+    unsigned starts, clauses, learnts;
+    ABC_INT64_T decisions, propagations, inspects, conflicts;
+    ABC_INT64_T clauses_literals, learnts_literals, tot_literals;
 };
 typedef struct stats_t stats_t;