Added learned clause recycling to the SAT solver (may impact bmc2, bmc3, dsat, etc).

9 files changed, 727 insertions, 280 deletions

diff --git a/src/aig/aig/aigRepar.c b/src/aig/aig/aigRepar.c
index 210c527e..f730a545 100644
--- a/src/aig/aig/aigRepar.c
+++ b/src/aig/aig/aigRepar.c
@@ -54,13 +54,13 @@ static inline void Aig_ManInterAddBuffer( sat_solver2 * pSat, int iVarA, int iVa
     Lits[1] = toLitCond( iVarB, !fCompl );
     Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
     if ( fMark )
-        clause_set_partA( pSat, Cid, 1 );
+        clause2_set_partA( pSat, Cid, 1 );
 
     Lits[0] = toLitCond( iVarA, 1 );
     Lits[1] = toLitCond( iVarB, fCompl );
     Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
     if ( fMark )
-        clause_set_partA( pSat, Cid, 1 );
+        clause2_set_partA( pSat, Cid, 1 );
 }
 
 /**Function*************************************************************
@@ -85,28 +85,28 @@ static inline void Aig_ManInterAddXor( sat_solver2 * pSat, int iVarA, int iVarB,
     Lits[2] = toLitCond( iVarC, 1 );
     Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
     if ( fMark )
-        clause_set_partA( pSat, Cid, 1 );
+        clause2_set_partA( pSat, Cid, 1 );
 
     Lits[0] = toLitCond( iVarA, !fCompl );
     Lits[1] = toLitCond( iVarB, 0 );
     Lits[2] = toLitCond( iVarC, 0 );
     Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
     if ( fMark )
-        clause_set_partA( pSat, Cid, 1 );
+        clause2_set_partA( pSat, Cid, 1 );
 
     Lits[0] = toLitCond( iVarA, fCompl );
     Lits[1] = toLitCond( iVarB, 1 );
     Lits[2] = toLitCond( iVarC, 0 );
     Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
     if ( fMark )
-        clause_set_partA( pSat, Cid, 1 );
+        clause2_set_partA( pSat, Cid, 1 );
 
     Lits[0] = toLitCond( iVarA, fCompl );
     Lits[1] = toLitCond( iVarB, 0 );
     Lits[2] = toLitCond( iVarC, 1 );
     Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
     if ( fMark )
-        clause_set_partA( pSat, Cid, 1 );
+        clause2_set_partA( pSat, Cid, 1 );
 }
 
 /**Function*************************************************************
@@ -152,7 +152,7 @@ void Aig_ManInterTest( Aig_Man_t * pMan, int fVerbose )
     for ( i = 0; i < pCnf->nClauses; i++ )
     {
         Cid = sat_solver2_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] );
-        clause_set_partA( pSat, Cid, 1 );
+        clause2_set_partA( pSat, Cid, 1 );
     }
 
     // add clauses of B
@@ -283,7 +283,7 @@ Aig_Man_t * Aig_ManInterRepar( Aig_Man_t * pMan, int fVerbose )
         for ( i = 0; i < pCnf->nClauses; i++ )
         {
             Cid = sat_solver2_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] );
-            clause_set_partA( pSat, Cid, k==0 );
+            clause2_set_partA( pSat, Cid, k==0 );
         }
         // add equality p[k] == A1/B1
         Aig_ManForEachCo( pMan, pObj, i )
@@ -293,7 +293,7 @@ Aig_Man_t * Aig_ManInterRepar( Aig_Man_t * pMan, int fVerbose )
         for ( i = 0; i < pCnf->nClauses; i++ )
         {
             Cid = sat_solver2_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] );
-            clause_set_partA( pSat, Cid, k==0 );
+            clause2_set_partA( pSat, Cid, k==0 );
         }
         // add comparator (!p[k] ^ A2/B2) == or[k]
         Vec_IntClear( vVars );
@@ -303,7 +303,7 @@ Aig_Man_t * Aig_ManInterRepar( Aig_Man_t * pMan, int fVerbose )
             Vec_IntPush( vVars, toLitCond(ShiftOr[k] + i, 1) );
         }
         Cid = sat_solver2_addclause( pSat, Vec_IntArray(vVars), Vec_IntArray(vVars) + Vec_IntSize(vVars) );
-        clause_set_partA( pSat, Cid, k==0 );
+        clause2_set_partA( pSat, Cid, k==0 );
         // return to normal
         Cnf_DataLift( pCnf, -ShiftCnf[k]-pCnf->nVars );
     }
@@ -362,7 +362,7 @@ Aig_Man_t * Aig_ManInterRepar( Aig_Man_t * pMan, int fVerbose )
             for ( i = 0; i < pCnfInter->nClauses; i++ )
             {
                 Cid = sat_solver2_addclause( pSat, pCnfInter->pClauses[i], pCnfInter->pClauses[i+1] );
-                clause_set_partA( pSat, Cid, c==0 );
+                clause2_set_partA( pSat, Cid, c==0 );
             }
             // connect to the inputs
             Aig_ManForEachCi( pInter, pObj, i )
diff --git a/src/misc/vec/vecSet.h b/src/misc/vec/vecSet.h
index 72358ea1..8b031e1e 100644
--- a/src/misc/vec/vecSet.h
+++ b/src/misc/vec/vecSet.h
@@ -210,10 +210,11 @@ static inline double Vec_ReportMemory( Vec_Set_t * p )
 ***********************************************************************/
 static inline int Vec_SetAppend( Vec_Set_t * p, int * pArray, int nSize )
 {
+    word * pPage = p->pPages[p->iPage];
     int nWords = Vec_SetWordNum( nSize );
-    assert( nWords < (1 << p->nPageSize) );
-    p->nEntries++;
-    if ( Vec_SetLimit( p->pPages[p->iPage] ) + nWords > (1 << p->nPageSize) )
+    assert( nWords + 3 < (1 << p->nPageSize) );
+    // need two extra at the begining of the page and one extra in the end
+    if ( Vec_SetLimit(pPage) + nWords >= (1 << p->nPageSize) )
     {
         if ( ++p->iPage == p->nPagesAlloc )
         {
@@ -223,12 +224,14 @@ static inline int Vec_SetAppend( Vec_Set_t * p, int * pArray, int nSize )
         }
         if ( p->pPages[p->iPage] == NULL )
             p->pPages[p->iPage] = ABC_ALLOC( word, (1 << p->nPageSize) );
-        Vec_SetWriteLimit( p->pPages[p->iPage], 2 );
-        p->pPages[p->iPage][1] = ~0;
+        pPage = p->pPages[p->iPage];
+        Vec_SetWriteLimit(pPage, 2);
+        pPage[1] = ~0;
     }
     if ( pArray )
-        memcpy( p->pPages[p->iPage] + Vec_SetLimit(p->pPages[p->iPage]), pArray, sizeof(int) * nSize );
-    Vec_SetIncLimit( p->pPages[p->iPage], nWords );
+        memcpy( pPage + Vec_SetLimit(pPage), pArray, sizeof(int) * nSize );
+    p->nEntries++;
+    Vec_SetIncLimit( pPage, nWords );
     return Vec_SetHandCurrent(p) - nWords;
 }
 static inline int Vec_SetAppendS( Vec_Set_t * p, int nSize )
diff --git a/src/sat/bsat/satClause.h b/src/sat/bsat/satClause.h
new file mode 100644
index 00000000..8b1a1294
--- /dev/null
+++ b/src/sat/bsat/satClause.h
@@ -0,0 +1,401 @@
+/**CFile****************************************************************
+
+  FileName    [satMem.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT solver.]
+
+  Synopsis    [Memory management.]
+
+  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 1, 2004.]
+
+  Revision    [$Id: satMem.h,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef ABC__sat__bsat__satMem_h
+#define ABC__sat__bsat__satMem_h
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "misc/util/abc_global.h"
+
+ABC_NAMESPACE_HEADER_START
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    STRUCTURE DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+ 
+//=================================================================================================
+// Clause datatype + minor functions:
+
+typedef int    lit;
+typedef int    cla;
+
+typedef struct clause_t clause;
+struct clause_t
+{
+    unsigned   lrn   :   1;
+    unsigned   mark  :   1;
+    unsigned   partA :   1;
+    unsigned   lbd   :   8;
+    unsigned   size  :  21;
+    lit        lits[0];
+};
+
+// learned clauses have "hidden" literal (c->lits[c->size]) to store clause ID
+
+// data-structure for logging entries
+// memory is allocated in 2^nPageSize word-sized pages
+// the first 'word' of each page are stores the word limit
+
+// although clause memory pieces are aligned to 64-bit words
+// the integer clause handles are in terms of 32-bit unsigneds
+// allowing for the first bit to be used for labeling 2-lit clauses
+
+
+typedef struct Sat_Mem_t_ Sat_Mem_t;
+struct Sat_Mem_t_
+{
+    int                 nEntries[2];  // entry count
+    int                 BookMarkH[2]; // bookmarks for handles
+    int                 BookMarkE[2]; // bookmarks for entries
+    int                 iPage[2];     // current memory page
+    int                 nPageSize;    // page log size in terms of ints
+    unsigned            uPageMask;    // page mask
+    unsigned            uLearnedMask; // learned mask
+    int                 nPagesAlloc;  // page count allocated
+    int **              pPages;       // page pointers
+}; 
+
+static inline int       Sat_MemLimit( int * p )                      { return p[0];                                 }
+static inline int       Sat_MemIncLimit( int * p, int nInts )        { return p[0] += nInts;                        }
+static inline void      Sat_MemWriteLimit( int * p, int nInts )      { p[0] = nInts;                                }
+
+static inline int       Sat_MemHandPage( Sat_Mem_t * p, cla h )      { return h >> p->nPageSize;                    }
+static inline int       Sat_MemHandShift( Sat_Mem_t * p, cla h )     { return h & p->uPageMask;                     }
+
+static inline int       Sat_MemIntSize( int size, int lrn )          { return (size + 2 + lrn) & ~01;               }
+static inline int       Sat_MemClauseSize( clause * p )              { return Sat_MemIntSize(p->size, p->lrn);      }
+
+//static inline clause *  Sat_MemClause( Sat_Mem_t * p, int i, int k ) { assert(i <= p->iPage[i&1] && k <= Sat_MemLimit(p->pPages[i]));  return (clause *)(p->pPages[i] + k ); }
+static inline clause *  Sat_MemClause( Sat_Mem_t * p, int i, int k ) { return (clause *)(p->pPages[i] + k);         }
+//static inline clause *  Sat_MemClauseHand( Sat_Mem_t * p, cla h )    { assert(Sat_MemHandPage(p, h) <= p->iPage[(h & p->uLearnedMask) > 0]); assert(Sat_MemHandShift(p, h) >= 2 && Sat_MemHandShift(p, h) < (int)p->uLearnedMask); return Sat_MemClause( p, Sat_MemHandPage(p, h), Sat_MemHandShift(p, h) );     }
+static inline clause *  Sat_MemClauseHand( Sat_Mem_t * p, cla h )    { return Sat_MemClause( p, Sat_MemHandPage(p, h), Sat_MemHandShift(p, h) );                             }
+static inline int       Sat_MemEntryNum( Sat_Mem_t * p, int lrn )    { return p->nEntries[lrn];                                                                              }
+
+static inline cla       Sat_MemHand( Sat_Mem_t * p, int i, int k )   { return (i << p->nPageSize) | k;                                                                       }
+static inline cla       Sat_MemHandCurrent( Sat_Mem_t * p, int lrn ) { return (p->iPage[lrn] << p->nPageSize) | Sat_MemLimit( p->pPages[p->iPage[lrn]] );                    }
+
+static inline double    Sat_MemMemoryHand( Sat_Mem_t * p, cla h )    { return 1.0 * ((Sat_MemHandPage(p, h) + 2)/2 * (1 << (p->nPageSize+2)) + Sat_MemHandShift(p, h) * 4);  }
+static inline double    Sat_MemMemoryUsed( Sat_Mem_t * p, int lrn )  { return Sat_MemMemoryHand( p, Sat_MemHandCurrent(p, lrn) );                                            }
+static inline double    Sat_MemMemoryAllUsed( Sat_Mem_t * p )        { return Sat_MemMemoryUsed( p, 0 ) + Sat_MemMemoryUsed( p, 1 );                                         }
+static inline double    Sat_MemMemoryAll( Sat_Mem_t * p )            { return 1.0 * (p->iPage[0] + p->iPage[1] + 2) * (1 << (p->nPageSize+2));                               }
+
+// p is memory storage
+// c is clause pointer
+// i is page number
+// k is page offset
+
+#define Sat_MemForEachClause( p, c, i, k )      \
+    for ( i = 0; i <= p->iPage[0]; i += 2 )     \
+        for ( k = 2; k < Sat_MemLimit(p->pPages[i]) && ((c) = Sat_MemClause( p, i, k )); k += Sat_MemClauseSize(c) )
+
+#define Sat_MemForEachLearned( p, c, i, k )     \
+    for ( i = 1; i <= p->iPage[1]; i += 2 )     \
+        for ( k = 2; k < Sat_MemLimit(p->pPages[i]) && ((c) = Sat_MemClause( p, i, k )); k += Sat_MemClauseSize(c) )
+
+////////////////////////////////////////////////////////////////////////
+///                       GLOBAL VARIABLES                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                       MACRO DEFINITIONS                          ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int      clause_from_lit( lit l )                     { return l + l + 1;                            }
+static inline int      clause_is_lit( cla h )                       { return (h & 1);                              }
+static inline lit      clause_read_lit( cla h )                     { return (lit)(h >> 1);                        }
+
+static inline int      clause_learnt_h( Sat_Mem_t * p, cla h )      { return (h & p->uLearnedMask) > 0;            }
+static inline int      clause_learnt( clause * c )                  { return c->lrn;                               }
+static inline int      clause_id( clause * c )                      { assert(c->lrn); return c->lits[c->size];     }
+static inline int      clause_size( clause * c )                    { return c->size;                              }
+static inline lit *    clause_begin( clause * c )                   { return c->lits;                              }
+static inline lit *    clause_end( clause * c )                     { return c->lits + c->size;                    }
+static inline void     clause_print( clause * c )               
+{ 
+    int i;
+    printf( "{ " );
+    for ( i = 0; i < clause_size(c); i++ )
+        printf( "%d ", (clause_begin(c)[i] & 1)? -(clause_begin(c)[i] >> 1) : clause_begin(c)[i] >> 1 );
+    printf( "}\n" );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DECLARATIONS                        ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocating vector.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Sat_MemAlloc_( Sat_Mem_t * p, int nPageSize )
+{
+    assert( nPageSize > 8 && nPageSize < 32 );
+    memset( p, 0, sizeof(Sat_Mem_t) );
+    p->nPageSize    = nPageSize;
+    p->uLearnedMask = (unsigned)(1 << nPageSize);
+    p->uPageMask    = (unsigned)((1 << nPageSize) - 1);
+    p->nPagesAlloc  = 256;
+    p->pPages       = ABC_CALLOC( int *, p->nPagesAlloc );
+    p->pPages[0]    = ABC_ALLOC( int, (1 << p->nPageSize) );
+    p->pPages[1]    = ABC_ALLOC( int, (1 << p->nPageSize) );
+    p->iPage[0]     = 0;
+    p->iPage[1]     = 1;
+    Sat_MemWriteLimit( p->pPages[0], 2 );
+    Sat_MemWriteLimit( p->pPages[1], 2 );
+}
+static inline Sat_Mem_t * Sat_MemAlloc( int nPageSize )
+{
+    Sat_Mem_t * p;
+    p = ABC_CALLOC( Sat_Mem_t, 1 );
+    Sat_MemAlloc_( p, nPageSize );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resetting vector.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Sat_MemRestart( Sat_Mem_t * p )
+{
+    p->nEntries[0]  = 0;
+    p->nEntries[1]  = 0;
+    p->iPage[0]     = 0;
+    p->iPage[1]     = 1;
+    Sat_MemWriteLimit( p->pPages[0], 2 );
+    Sat_MemWriteLimit( p->pPages[1], 2 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the bookmark.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Sat_MemBookMark( Sat_Mem_t * p )
+{
+    p->BookMarkH[0] = Sat_MemHandCurrent( p, 0 );
+    p->BookMarkH[1] = Sat_MemHandCurrent( p, 1 );
+    p->BookMarkE[0] = p->nEntries[0];
+    p->BookMarkE[1] = p->nEntries[1];
+}
+static inline void Sat_MemRollBack( Sat_Mem_t * p )
+{
+    p->nEntries[0]  = p->BookMarkE[0];
+    p->nEntries[1]  = p->BookMarkE[1];
+    p->iPage[0]     = Sat_MemHandPage( p, p->BookMarkH[0] );
+    p->iPage[1]     = Sat_MemHandPage( p, p->BookMarkH[1] );
+    Sat_MemWriteLimit( p->pPages[0], Sat_MemHandShift( p, p->BookMarkH[0] ) );
+    Sat_MemWriteLimit( p->pPages[1], Sat_MemHandShift( p, p->BookMarkH[1] ) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Freeing vector.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Sat_MemFree_( Sat_Mem_t * p )
+{
+    int i;
+    for ( i = 0; i < p->nPagesAlloc; i++ )
+        ABC_FREE( p->pPages[i] );
+    ABC_FREE( p->pPages );
+}
+static inline void Sat_MemFree( Sat_Mem_t * p )
+{
+    Sat_MemFree_( p );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates new clause.]
+
+  Description [The resulting clause is fully initialized.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Sat_MemAppend( Sat_Mem_t * p, int * pArray, int nSize, int lrn )
+{
+    clause * c;
+    int * pPage = p->pPages[p->iPage[lrn]];
+    int nInts = Sat_MemIntSize( nSize, lrn );
+    assert( nInts + 3 < (1 << p->nPageSize) );
+    // need two extra at the begining of the page and one extra in the end
+    if ( Sat_MemLimit(pPage) + nInts >= (1 << p->nPageSize) )
+    {
+        p->iPage[lrn] += 2;
+        if ( p->iPage[lrn] >= p->nPagesAlloc )
+        {
+            p->pPages = ABC_REALLOC( int *, p->pPages, p->nPagesAlloc * 2 );
+            memset( p->pPages + p->nPagesAlloc, 0, sizeof(int *) * p->nPagesAlloc );
+            p->nPagesAlloc *= 2;
+        }
+        if ( p->pPages[p->iPage[lrn]] == NULL )
+            p->pPages[p->iPage[lrn]] = ABC_ALLOC( int, (1 << p->nPageSize) );
+        pPage = p->pPages[p->iPage[lrn]];
+        Sat_MemWriteLimit( pPage, 2 );
+    }
+    pPage[Sat_MemLimit(pPage)] = 0;
+    c = (clause *)(pPage + Sat_MemLimit(pPage));
+    c->size = nSize;
+    c->lrn = lrn;
+    if ( pArray )
+        memcpy( c->lits, pArray, sizeof(int) * nSize );
+    if ( lrn )
+        c->lits[c->size] = p->nEntries[1];
+    p->nEntries[lrn]++;
+    Sat_MemIncLimit( pPage, nInts );
+    return Sat_MemHandCurrent(p, lrn) - nInts;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Shrinking vector size.]
+
+  Description []
+
+  SideEffects [This procedure does not update the number of entries.]
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Sat_MemShrink( Sat_Mem_t * p, int h, int lrn )
+{
+    assert( clause_learnt_h(p, h) == lrn );
+    assert( h && h <= Sat_MemHandCurrent(p, lrn) );
+    p->iPage[lrn] = Sat_MemHandPage(p, h);
+    Sat_MemWriteLimit( p->pPages[p->iPage[lrn]], Sat_MemHandShift(p, h) );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Compacts learned clauses by removing marked entries.]
+
+  Description [Returns the number of remaining entries.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Sat_MemCompactLearned( Sat_Mem_t * p, int fDoMove )
+{
+    clause * c;
+    int i, k, iNew = 1, kNew = 2, nInts, Counter = 0;
+    // iterate through the learned clauses
+    Sat_MemForEachLearned( p, c, i, k )
+    {
+        assert( c->lrn );
+        // skip marked entry
+        if ( c->mark )
+            continue;
+        // compute entry size
+        nInts = Sat_MemClauseSize(c);
+        assert( !(nInts & 1) );
+        // check if we need to scroll to the next page
+        if ( kNew + nInts >= (1 << p->nPageSize) )
+        {
+            // set the limit of the current page
+            if ( fDoMove )
+                Sat_MemWriteLimit( p->pPages[iNew], kNew );
+            // move writing position to the new page
+            iNew += 2;
+            kNew = 2;
+        }
+        if ( fDoMove )
+        {
+            // make sure the result is the same as previous dry run
+            assert( c->lits[c->size] == Sat_MemHand(p, iNew, kNew) );
+            // only copy the clause if it has changed
+            if ( i != iNew || k != kNew )
+            {
+                memmove( p->pPages[iNew] + kNew, c, sizeof(int) * nInts );
+//                c = Sat_MemClause( p, iNew, kNew ); // assersions do not hold during dry run
+                c = (clause *)(p->pPages[iNew] + kNew);
+                assert( nInts == Sat_MemClauseSize(c) );
+            }
+            // set the new ID value
+            c->lits[c->size] = Counter;
+        }
+        else // remember the address of the clause in the new location
+            c->lits[c->size] = Sat_MemHand(p, iNew, kNew);
+        // update writing position
+        kNew += nInts;
+        assert( iNew <= i && kNew < (1 << p->nPageSize) );
+        // update counter
+        Counter++;
+    }
+    if ( fDoMove )
+    {
+        // update the page count
+        p->iPage[1] = iNew;
+        // set the limit of the last page
+        Sat_MemWriteLimit( p->pPages[iNew], kNew );
+        // update the counter
+        p->nEntries[1] = Counter;
+    }
+    return Counter;
+}
+
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 70feaa17..2a759da3 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -29,6 +29,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 ABC_NAMESPACE_IMPL_START
 
+//#define LEARNT_MAX_START  0
+#define LEARNT_MAX_START  20000
+#define LEARNT_MAX_INCRE   1000
+
 #define SAT_USE_ANALYZE_FINAL
 
 //=================================================================================================
@@ -125,39 +129,6 @@ int sat_solver_get_var_value(sat_solver* s, int v)
     assert( 0 );
     return 0;
 }
- 
-//=================================================================================================
-// Clause datatype + minor functions:
-
-struct clause_t
-{
-    int size_learnt;
-    lit lits[0];
-};
-
-static inline clause*  clause_read         (sat_solver* s, int h)  { return (clause *)Vec_SetEntry(&s->Mem, h>>1);     }
-
-static inline int      clause_nlits        (clause* c)             { return c->size_learnt >> 1;                       }
-static inline lit*     clause_begin        (clause* c)             { return c->lits;                                   }
-static inline int      clause_learnt       (clause* c)             { return c->size_learnt & 1;                        }
-static inline float    clause_activity     (clause* c)             { return *((float*)&c->lits[c->size_learnt>>1]);    }
-static inline unsigned clause_activity2    (clause* c)             { return *((unsigned*)&c->lits[c->size_learnt>>1]); }
-static inline void     clause_setactivity  (clause* c, float a)    { *((float*)&c->lits[c->size_learnt>>1]) = a;       }
-static inline void     clause_setactivity2 (clause* c, unsigned a) { *((unsigned*)&c->lits[c->size_learnt>>1]) = a;    }
-static inline void     clause_print        (clause* c)             { 
-    int i;
-    printf( "{ " );
-    for ( i = 0; i < clause_nlits(c); i++ )
-        printf( "%d ", (clause_begin(c)[i] & 1)? -(clause_begin(c)[i] >> 1) : clause_begin(c)[i] >> 1 );
-    printf( "}\n" );
-}
-
-//=================================================================================================
-// Encode literals in clause pointers:
-
-static inline int      clause_from_lit (lit l)       { return l + l + 1;                            }
-static inline int      clause_is_lit   (int h)       { return (h & 1);                              }
-static inline lit      clause_read_lit (int h)       { return (lit)(h >> 1);                        }
 
 //=================================================================================================
 // Simple helpers:
@@ -257,7 +228,7 @@ static inline void act_var_rescale(sat_solver* s)  {
     s->var_inc *= 1e-100;
 }
 static inline void act_clause_rescale(sat_solver* s) {
-//    static int Total = 0;
+//    static clock_t Total = 0;
     clause** cs = (clause**)veci_begin(&s->learnts);
     int i;//, clk = clock();
     for (i = 0; i < veci_size(&s->learnts); i++){
@@ -267,8 +238,8 @@ static inline void act_clause_rescale(sat_solver* s) {
     s->cla_inc *= (float)1e-20;
 
     Total += clock() - clk;
-    printf( "Rescaling...   Cla inc = %10.3f  Conf = %10d   ", s->cla_inc,  s->stats.conflicts );
-    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_solver* s, int v) {
     s->activity[v] += s->var_inc;
@@ -313,24 +284,21 @@ static inline void act_var_rescale(sat_solver* s) {
     s->var_inc >>= 19;
     s->var_inc = Abc_MaxInt( s->var_inc, (1<<4) );
 }
-/*
+
 static inline void act_clause_rescale(sat_solver* s) {
-    static int Total = 0;
-    clause** cs = (clause**)vecp_begin(&s->learnts);
-    int i;
+    static clock_t Total = 0;
     clock_t clk = clock();
-    for (i = 0; i < vecp_size(&s->learnts); i++){
-        unsigned a = clause_activity2(cs[i]);
-        clause_setactivity2(cs[i], a >> 14);
-    }
+    unsigned* activity = (unsigned *)veci_begin(&s->act_clas);
+    int i;
+    for (i = 0; i < veci_size(&s->act_clas); i++)
+        activity[i] >>= 14;
     s->cla_inc >>= 14;
     s->cla_inc = Abc_MaxInt( s->cla_inc, (1<<10) );
-
-//    Total += clock() - clk;
+    Total += clock() - clk;
 //    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_solver* s, int v) {
     s->activity[v] += s->var_inc;
     if (s->activity[v] & 0x80000000)
@@ -356,16 +324,16 @@ static inline void act_var_bump_factor(sat_solver* s, int v) {
     if (s->orderpos[v] != -1)
         order_update(s,v);
 }
-/*
+
 static inline void act_clause_bump(sat_solver* s, clause*c) {
-    unsigned a = clause_activity2(c) + s->cla_inc;
-    clause_setactivity2(c,a);
-    if (a & 0x80000000) 
+    unsigned* act = (unsigned *)veci_begin(&s->act_clas) + c->lits[c->size];
+    *act += s->cla_inc;
+    if ( *act & 0x80000000 )
         act_clause_rescale(s);
 }
-*/
+
 static inline void act_var_decay(sat_solver* s)    { s->var_inc += (s->var_inc >>  4); }
-//static inline void act_clause_decay(sat_solver* s) { s->cla_inc += (s->cla_inc >> 10); }
+static inline void act_clause_decay(sat_solver* s) { s->cla_inc += (s->cla_inc >> 10); }
 
 #endif
 
@@ -416,13 +384,30 @@ static void sortrnd(void** array, int size, int(*comp)(const void *, const void
 //=================================================================================================
 // Clause functions:
 
+static inline int sat_clause_compute_lbd( sat_solver* s, clause* c )
+{
+    int i, lev, minl = 0, lbd = 0;
+    for (i = 0; i < (int)c->size; i++)
+    {
+        lev = var_level(s, lit_var(c->lits[i]));
+        if ( !(minl & (1 << (lev & 31))) )
+        {
+            minl |= 1 << (lev & 31);
+            lbd++;
+//            printf( "%d ", lev );
+        }
+    }
+//    printf( " -> %d\n", lbd );
+    return lbd;
+}
+
 /* pre: size > 1 && no variable occurs twice
  */
 static int clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt)
 {
     int size;
     clause* c;
-    int h, i;
+    int h;
 
     assert(end - begin > 1);
     assert(learnt >= 0 && learnt < 2);
@@ -433,20 +418,33 @@ static int clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt)
     {
         veci_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(clause_from_lit(begin[1])));
         veci_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(clause_from_lit(begin[0])));
+        s->stats.clauses++;
+        s->stats.clauses_literals += size;
         return 0;
     }
 
     // create new clause
-    h = Vec_SetAppend( &s->Mem, NULL, size + learnt + 1 ) << 1;
+//    h = Vec_SetAppend( &s->Mem, NULL, size + learnt + 1 + 1 ) << 1;
+    h = Sat_MemAppend( &s->Mem, begin, size, learnt );
     assert( !(h & 1) );
-    c = clause_read( s, h );
     if ( s->hLearnts == -1 && learnt )
         s->hLearnts = h;
-    c->size_learnt = (size << 1) | learnt;
-    for (i = 0; i < size; i++)
-        c->lits[i] = begin[i];
     if (learnt)
-        *((float*)&c->lits[size]) = 0.0;
+    {
+        c = clause_read( s, h );
+        c->lbd = sat_clause_compute_lbd( s, c );
+        assert( clause_id(c) == veci_size(&s->act_clas) );
+//        veci_push(&s->learned, h);
+//        act_clause_bump(s,clause_read(s, h));
+        veci_push(&s->act_clas, (1<<10));
+        s->stats.learnts++;
+        s->stats.learnts_literals += size;
+    }
+    else
+    {
+        s->stats.clauses++;
+        s->stats.clauses_literals += size;
+    }
 
     assert(begin[0] >= 0);
     assert(begin[0] < s->size*2);
@@ -541,6 +539,7 @@ static void sat_solver_record(sat_solver* s, veci* cls)
     lit*    end   = begin + veci_size(cls);
     int     h     = (veci_size(cls) > 1) ? clause_create_new(s,begin,end,1) : 0;
     sat_solver_enqueue(s,*begin,h);
+    assert(veci_size(cls) > 0);
 
     ///////////////////////////////////
     // add clause to internal storage
@@ -550,15 +549,13 @@ static void sat_solver_record(sat_solver* s, veci* cls)
         assert( RetValue );
     }
     ///////////////////////////////////
-
-    assert(veci_size(cls) > 0);
-
+/*
     if (h != 0) {
-//        veci_push(&s->learnts,c);
-//        act_clause_bump(s,c);
+        act_clause_bump(s,clause_read(s, h));
         s->stats.learnts++;
         s->stats.learnts_literals += veci_size(cls);
     }
+*/
 }
 
 
@@ -602,7 +599,7 @@ static int sat_solver_lit_removable(sat_solver* s, int x, int minl)
             clause* c = clause_read(s, s->reasons[v]);
             lit* lits = clause_begin(c);
             int  i;
-            for (i = 1; i < clause_nlits(c); i++){
+            for (i = 1; i < clause_size(c); i++){
                 int v = lit_var(lits[i]);
                 if (!var_tag(s,v) && var_level(s, v)){
                     if (s->reasons[v] != 0 && ((1 << (var_level(s, v) & 31)) & minl)){
@@ -681,7 +678,7 @@ static void sat_solver_analyze_final(sat_solver* s, int hConf, int skip_first)
     assert( veci_size(&s->tagged) == 0 );
 //    assert( s->tags[lit_var(p)] == l_Undef );
 //    s->tags[lit_var(p)] = l_True;
-    for (i = skip_first ? 1 : 0; i < clause_nlits(conf); i++)
+    for (i = skip_first ? 1 : 0; i < clause_size(conf); i++)
     {
         int x = lit_var(clause_begin(conf)[i]);
         if (var_level(s, x) > 0)
@@ -705,7 +702,7 @@ static void sat_solver_analyze_final(sat_solver* s, int hConf, int skip_first)
                 else{
                     clause* c = clause_read(s, s->reasons[x]);
                     int* lits = clause_begin(c);
-                    for (j = 1; j < clause_nlits(c); j++)
+                    for (j = 1; j < clause_size(c); j++)
                         if (var_level(s, lit_var(lits[j])) > 0)
                             var_set_tag(s, lit_var(lits[j]), 1);
                 }
@@ -717,7 +714,6 @@ static void sat_solver_analyze_final(sat_solver* s, int hConf, int skip_first)
 
 #endif
 
-
 static void sat_solver_analyze(sat_solver* s, int h, veci* learnt)
 {
     lit*     trail   = s->trail;
@@ -741,15 +737,18 @@ static void sat_solver_analyze(sat_solver* s, int h, veci* learnt)
             }
         }else{
             clause* c = clause_read(s, h);
-//            if (clause_learnt(c))
-//                act_clause_bump(s,c);
+            if (clause_learnt(c))
+                act_clause_bump(s,c);
             lits = clause_begin(c);
-            //printlits(lits,lits+clause_nlits(c)); printf("\n");
-            for (j = (p == lit_Undef ? 0 : 1); j < clause_nlits(c); j++){
+            //printlits(lits,lits+clause_size(c)); printf("\n");
+            for (j = (p == lit_Undef ? 0 : 1); j < clause_size(c); j++){
                 int x = lit_var(lits[j]);
                 if (var_tag(s, x) == 0 && var_level(s, x) > 0){
                     var_set_tag(s, x, 1);
                     act_var_bump(s,x);
+                    // bump variables propaged by the LBD=2 clause
+//                    if ( s->reasons[x] && clause_read(s, s->reasons[x])->lbd <= 2 )
+//                        act_var_bump(s,x);
                     if (var_level(s,x) == sat_solver_dl(s))
                         cnt++;
                     else
@@ -785,6 +784,7 @@ static void sat_solver_analyze(sat_solver* s, int h, veci* learnt)
     veci_resize(learnt,j);
     s->stats.tot_literals += j;
 
+
     // clear tags
     solver2_clear_tags(s,0);
 
@@ -836,7 +836,7 @@ int sat_solver_propagate(sat_solver* s)
         int*i, *j;
 
         s->stats.propagations++;
-        s->simpdb_props--;
+//        s->simpdb_props--;
 
         //printf("checking lit %d: "L_LIT"\n", veci_size(ws), L_lit(p));
         for (i = j = begin; i < end; ){
@@ -875,7 +875,7 @@ int sat_solver_propagate(sat_solver* s)
                     *j++ = *i;
                 else{
                     // Look for new watch:
-                    lit* stop = lits + clause_nlits(c);
+                    lit* stop = lits + clause_size(c);
                     lit* k;
                     for (k = lits + 2; k < stop; k++){
                         if (var_value(s, lit_var(*k)) != !lit_sign(*k)){
@@ -887,6 +887,8 @@ int sat_solver_propagate(sat_solver* s)
 
                     *j++ = *i;
                     // Clause is unit under assignment:
+                    if ( c->lrn )
+                        c->lbd = sat_clause_compute_lbd(s, c);
                     if (!sat_solver_enqueue(s,lits[0], *i)){
                         hConfl = *i++;
                         // Copy the remaining watches:
@@ -913,16 +915,20 @@ sat_solver* sat_solver_new(void)
 {
     sat_solver* s = (sat_solver*)ABC_CALLOC( char, sizeof(sat_solver));
 
-    Vec_SetAlloc_(&s->Mem, 15);
+//    Vec_SetAlloc_(&s->Mem, 15);
+    Sat_MemAlloc_(&s->Mem, 14);
     s->hLearnts = -1;
-    s->hBinary = Vec_SetAppend( &s->Mem, NULL, 3 ) << 1;
+    s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0 );
     s->binary = clause_read( s, s->hBinary );
-    s->binary->size_learnt = (2 << 1);
+
+    s->nLearntMax = LEARNT_MAX_START;
 
     // initialize vectors
     veci_new(&s->order);
     veci_new(&s->trail_lim);
     veci_new(&s->tagged);
+//    veci_new(&s->learned);
+    veci_new(&s->act_clas);
     veci_new(&s->stack);
 //    veci_new(&s->model);
     veci_new(&s->act_vars);
@@ -944,15 +950,15 @@ sat_solver* sat_solver_new(void)
 #ifdef USE_FLOAT_ACTIVITY
     s->var_inc                = 1;
     s->cla_inc                = 1;
-    s->var_decay              = (float)(1 / 0.95  );
-    s->cla_decay              = (float)(1 / 0.999 );
+    s->var_decay              = (float)(1 / 0.95 );
+    s->cla_decay              = (float)(1 / 0.999);
 #else
     s->var_inc                = (1 <<  5);
     s->cla_inc                = (1 << 11);
 #endif
     s->root_level             = 0;
-    s->simpdb_assigns         = 0;
-    s->simpdb_props           = 0;
+//    s->simpdb_assigns         = 0;
+//    s->simpdb_props           = 0;
     s->random_seed            = 91648253;
     s->progress_estimate      = 0;
 //    s->binary                 = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit)*2);
@@ -1035,12 +1041,15 @@ void sat_solver_setnvars(sat_solver* s,int n)
 
 void sat_solver_delete(sat_solver* s)
 {
-    Vec_SetFree_( &s->Mem );
+//    Vec_SetFree_( &s->Mem );
+    Sat_MemFree_( &s->Mem );
 
     // delete vectors
     veci_delete(&s->order);
     veci_delete(&s->trail_lim);
     veci_delete(&s->tagged);
+//    veci_delete(&s->learned);
+    veci_delete(&s->act_clas);
     veci_delete(&s->stack);
 //    veci_delete(&s->model);
     veci_delete(&s->act_vars);
@@ -1073,12 +1082,10 @@ void sat_solver_delete(sat_solver* s)
 void sat_solver_rollback( sat_solver* s )
 {
     int i;
-    Vec_SetRestart( &s->Mem );
-
+    Sat_MemRestart( &s->Mem );
     s->hLearnts = -1;
-    s->hBinary = Vec_SetAppend( &s->Mem, NULL, 3 ) << 1;
+    s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0 );
     s->binary = clause_read( s, s->hBinary );
-    s->binary->size_learnt = (2 << 1);
 
     veci_resize(&s->trail_lim, 0);
     veci_resize(&s->order, 0);
@@ -1100,8 +1107,8 @@ void sat_solver_rollback( sat_solver* s )
     s->cla_inc                = (1 << 11);
 #endif
     s->root_level             = 0;
-    s->simpdb_assigns         = 0;
-    s->simpdb_props           = 0;
+//    s->simpdb_assigns         = 0;
+//    s->simpdb_props           = 0;
     s->random_seed            = 91648253;
     s->progress_estimate      = 0;
     s->verbosity              = 0;
@@ -1145,116 +1152,138 @@ double sat_solver_memory( sat_solver* s )
     Mem += s->order.cap * sizeof(int);
     Mem += s->trail_lim.cap * sizeof(int);
     Mem += s->tagged.cap * sizeof(int);
+//    Mem += s->learned.cap * sizeof(int);
     Mem += s->stack.cap * sizeof(int);
     Mem += s->act_vars.cap * sizeof(int);
+    Mem += s->act_clas.cap * sizeof(int);
     Mem += s->temp_clause.cap * sizeof(int);
     Mem += s->conf_final.cap * sizeof(int);
-    Mem += Vec_ReportMemory( &s->Mem );
+    Mem += Sat_MemMemoryAll( &s->Mem );
     return Mem;
 }
 
-
-/*
-static void clause_remove(sat_solver* s, clause* c)
+int sat_solver_simplify(sat_solver* s)
 {
-    lit* lits = clause_begin(c);
-    assert(lit_neg(lits[0]) < s->size*2);
-    assert(lit_neg(lits[1]) < s->size*2);
-
-    //veci_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)c);
-    //veci_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)c);
-
-    assert(lits[0] < s->size*2);
-    veci_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(clause_nlits(c) > 2 ? c : clause_from_lit(lits[1])));
-    veci_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(clause_nlits(c) > 2 ? c : clause_from_lit(lits[0])));
-
-    if (clause_learnt(c)){
-        s->stats.learnts--;
-        s->stats.learnts_literals -= clause_nlits(c);
-    }else{
-        s->stats.clauses--;
-        s->stats.clauses_literals -= clause_nlits(c);
-    }
+    assert(sat_solver_dl(s) == 0);
+    if (sat_solver_propagate(s) != 0)
+        return false;
+    return true;
 }
 
-static lbool clause_simplify(sat_solver* s, clause* c)
+void sat_solver_reducedb(sat_solver* s)
 {
-    lit*   lits   = clause_begin(c);
-    int i;
-
-    assert(sat_solver_dl(s) == 0);
-
-    for (i = 0; i < clause_nlits(c); i++){
-        lbool sig = !lit_sign(lits[i]); sig += sig - 1;
-        if (s->assignss[lit_var(lits[i])] == sig)
-            return l_True;
+    static clock_t TimeTotal = 0;
+    clock_t clk = clock();
+    Sat_Mem_t * pMem = &s->Mem;
+    int nLearnedOld = veci_size(&s->act_clas);
+    int * act_clas = veci_begin(&s->act_clas);
+    int * pPerm, * pArray, * pSortValues, nCutoffValue;
+    int i, k, j, Id, Counter, CounterStart, nSelected;
+    clause * c;
+
+    assert( s->nLearntMax > 0 );
+    assert( nLearnedOld == Sat_MemEntryNum(pMem, 1) );
+    assert( nLearnedOld == (int)s->stats.learnts );
+
+    s->nDBreduces++;
+
+//    printf( "Calling reduceDB with %d learned clause limit.\n", s->nLearntMax );
+    s->nLearntMax = LEARNT_MAX_START + LEARNT_MAX_INCRE * s->nDBreduces;
+//    return;
+
+    // create sorting values
+    pSortValues = ABC_ALLOC( int, nLearnedOld );
+    Sat_MemForEachLearned( pMem, c, i, k )
+    {
+        Id = clause_id(c);
+        pSortValues[Id] = (((7 - Abc_MinInt(c->lbd, 7)) << 28) | (act_clas[Id] >> 4));
+//        pSortValues[Id] = act[Id];
+        assert( pSortValues[Id] >= 0 );
     }
-    return l_False;
-}
-*/
 
-int sat_solver_simplify(sat_solver* s)
-{
-//    clause** reasons;
-//    int type;
-    assert(sat_solver_dl(s) == 0);
+    // preserve 1/20 of last clauses
+    CounterStart  = nLearnedOld - (s->nLearntMax / 20);
 
-    if (sat_solver_propagate(s) != 0)
-        return false;
+    // preserve 3/4 of most active clauses
+    nSelected = nLearnedOld*5/10;
 
-    if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0)
-        return true;
-/*
-    reasons = s->reasons;
-    for (type = 0; type < 2; type++){
-        vecp*    cs  = type ? &s->learnts : &s->clauses;
-        clause** cls = (clause**)vecp_begin(cs);
-
-        int i, j;
-        for (j = i = 0; i < vecp_size(cs); i++){
-            if (reasons[lit_var(*clause_begin(cls[i]))] != cls[i] &&
-                clause_simplify(s,cls[i]) == l_True)
-                clause_remove(s,cls[i]);
-            else
-                cls[j++] = cls[i];
+    // find non-decreasing permutation
+    pPerm = Abc_MergeSortCost( pSortValues, nLearnedOld );
+    assert( pSortValues[pPerm[0]] <= pSortValues[pPerm[nLearnedOld-1]] );
+    nCutoffValue = pSortValues[pPerm[nLearnedOld-nSelected]];
+    ABC_FREE( pPerm );
+//    ActCutOff = ABC_INFINITY;
+
+    // mark learned clauses to remove
+    Counter = j = 0;
+    Sat_MemForEachLearned( pMem, c, i, k )
+    {
+        assert( c->mark == 0 );
+        if ( Counter++ > CounterStart || clause_size(c) < 3 || pSortValues[clause_id(c)] > nCutoffValue || s->reasons[lit_var(c->lits[0])] == Sat_MemHand(pMem, i, k) )
+            act_clas[j++] = act_clas[clause_id(c)];
+        else // delete
+        {
+            c->mark = 1;
+            s->stats.learnts_literals -= clause_size(c);
+            s->stats.learnts--;
         }
-        vecp_resize(cs,j);
     }
-*/
-    s->simpdb_assigns = s->qhead;
-    // (shouldn't depend on 'stats' really, but it will do for now)
-    s->simpdb_props   = (int)(s->stats.clauses_literals + s->stats.learnts_literals);
-    return true;
-}
+    assert( s->stats.learnts == (unsigned)j );
+    assert( Counter == nLearnedOld );
+    veci_resize(&s->act_clas,j);
+    ABC_FREE( pSortValues );
 
+    // update ID of each clause to be its new handle
+    Counter = Sat_MemCompactLearned( pMem, 0 );
+    assert( Counter == (int)s->stats.learnts );
 
-/*
-static int clause_cmp (const void* x, const void* y) {
-    return clause_nlits((clause*)x) > 2 && (clause_nlits((clause*)y) == 2 || clause_activity((clause*)x) < clause_activity((clause*)y)) ? -1 : 1; }
-void sat_solver_reducedb(sat_solver* s)
-{
-    int      i, j;
-    double   extra_lim = s->cla_inc / veci_size(&s->learnts); // Remove any clause below this activity
-    clause** learnts = (clause**)veci_begin(&s->learnts);
-    clause** reasons = s->reasons;
-
-    sat_solver_sort(veci_begin(&s->learnts), veci_size(&s->learnts), &clause_cmp);
+    // update reasons
+    for ( i = 0; i < s->size; i++ )
+    {
+        if ( !s->reasons[i] ) // no reason
+            continue;
+        if ( clause_is_lit(s->reasons[i]) ) // 2-lit clause
+            continue;
+        if ( !clause_learnt_h(pMem, s->reasons[i]) ) // problem clause
+            continue;
+        c = clause_read( s, s->reasons[i] );
+        assert( c->mark == 0 );
+        s->reasons[i] = clause_id(c); // updating handle here!!!
+    }
 
-    for (i = j = 0; i < veci_size(&s->learnts) / 2; i++){
-        if (clause_nlits(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i])
-            clause_remove(s,learnts[i]);
-        else
-            learnts[j++] = learnts[i];
+    // update 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 ( clause_is_lit(pArray[k]) ) // 2-lit clause
+                pArray[j++] = pArray[k];
+            else if ( !clause_learnt_h(pMem, pArray[k]) ) // problem clause
+                pArray[j++] = pArray[k];
+            else 
+            {
+                c = clause_read(s, pArray[k]);
+                if ( !c->mark ) // useful learned clause
+                   pArray[j++] = clause_id(c); // updating handle here!!!
+            }
+        }
+        veci_resize(&s->wlists[i],j);
     }
-    for (; i < veci_size(&s->learnts); i++){
-        if (clause_nlits(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i] && clause_activity(learnts[i]) < extra_lim)
-            clause_remove(s,learnts[i]);
-        else
-            learnts[j++] = learnts[i];
+
+    // perform final move of the clauses
+    Counter = Sat_MemCompactLearned( pMem, 1 );
+    assert( Counter == (int)s->stats.learnts );
+
+    // report the results
+    TimeTotal += clock() - clk;
+    if ( s->fVerbose )
+    {
+    Abc_Print(1, "reduceDB: Keeping %7d out of %7d clauses (%5.2f %%)  ",
+        s->stats.learnts, nLearnedOld, 100.0 * s->stats.learnts / nLearnedOld );
+    Abc_PrintTime( 1, "Time", TimeTotal );
     }
-    veci_resize(&s->learnts,j);
 }
-*/
 
 int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
 {
@@ -1308,9 +1337,6 @@ int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
 
     // create new clause
     clause_create_new(s,begin,j,0);
-
-    s->stats.clauses++;
-    s->stats.clauses_literals += j - begin;
     return true;
 }
 
@@ -1335,7 +1361,7 @@ void luby_test()
     printf( "\n" );
 }
 
-static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT64_T nof_learnts)
+static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts)
 {
 //    double  var_decay       = 0.95;
 //    double  clause_decay    = 0.999;
@@ -1395,36 +1421,37 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT
                 var_set_level(s, lit_var(learnt_clause.ptr[0]), 0);
 #endif
             act_var_decay(s);
-//            act_clause_decay(s);
+            act_clause_decay(s);
 
         }else{
             // NO CONFLICT
             int next;
  
+            // Reached bound on number of conflicts:
             if (nof_conflicts >= 0 && conflictC >= nof_conflicts){
-                // Reached bound on number of conflicts:
                 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) ||
                  (s->nInsLimit  && s->stats.propagations > s->nInsLimit) )
             {
-                // Reached bound on number of conflicts:
                 s->progress_estimate = sat_solver_progress(s);
                 sat_solver_canceluntil(s,s->root_level);
                 veci_delete(&learnt_clause);
                 return l_Undef; 
             }
 
+            // Simplify the set of problem clauses:
             if (sat_solver_dl(s) == 0 && !s->fSkipSimplify)
-                // Simplify the set of problem clauses:
                 sat_solver_simplify(s);
 
-//            if (nof_learnts >= 0 && veci_size(&s->learnts) - s->qtail >= nof_learnts)
-                // Reduce the set of learnt clauses:
-//                sat_solver_reducedb(s);
+            // Reduce the set of learnt clauses:
+//            if (s->nLearntMax && veci_size(&s->learned) - s->qtail >= s->nLearntMax)
+            if (s->nLearntMax && veci_size(&s->act_clas) >= s->nLearntMax)
+                sat_solver_reducedb(s);
 
             // New variable decision:
             s->stats.decisions++;
@@ -1463,7 +1490,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
 {
     int restart_iter = 0;
     ABC_INT64_T  nof_conflicts;
-    ABC_INT64_T  nof_learnts   = sat_solver_nclauses(s) / 3;
+//    ABC_INT64_T  nof_learnts   = sat_solver_nclauses(s) / 3;
     lbool   status        = l_Undef;
     lit*    i;
 
@@ -1623,8 +1650,8 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
             fflush(stdout);
         }
         nof_conflicts = (ABC_INT64_T)( 100 * luby(2, restart_iter++) );
-        status = sat_solver_search(s, nof_conflicts, nof_learnts);
-        nof_learnts    = nof_learnts * 11 / 10; //*= 1.1;
+        status = sat_solver_search(s, nof_conflicts);
+//        nof_learnts    = nof_learnts * 11 / 10; //*= 1.1;
         // quit the loop if reached an external limit
         if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit )
             break;
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index cb9e5c39..5215267b 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -28,6 +28,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <string.h>
 #include <assert.h>
 
+#include "satClause.h"
 #include "satVec.h"
 #include "misc/vec/vecSet.h"
 
@@ -79,8 +80,8 @@ extern void *      sat_solver_store_release( sat_solver * s );
 //=================================================================================================
 // Solver representation:
 
-struct clause_t;
-typedef struct clause_t clause;
+//struct clause_t;
+//typedef struct clause_t clause;
 
 struct varinfo_t;
 typedef struct varinfo_t varinfo;
@@ -93,7 +94,7 @@ struct sat_solver_t
     int         qtail;         // Tail index of queue.
 
     // clauses
-    Vec_Set_t   Mem;
+    Sat_Mem_t   Mem;
     int         hLearnts;      // the first learnt clause
     int         hBinary;       // the special binary clause
     clause *    binary;
@@ -137,8 +138,13 @@ struct sat_solver_t
     double      random_seed;
     double      progress_estimate;
     int         verbosity;     // Verbosity level. 0=silent, 1=some progress report, 2=everything
+    int         fVerbose;
 
     stats_t     stats;
+    int         nLearntMax;    // max number of learned clauses
+    int         nDBreduces;    // number of DB reductions
+//    veci        learned;       // contain learnt clause handles
+    veci        act_clas;      // contain clause activities
 
     ABC_INT64_T nConfLimit;    // external limit on the number of conflicts
     ABC_INT64_T nInsLimit;     // external limit on the number of implications
@@ -166,6 +172,11 @@ struct sat_solver_t
     veci        temp_clause;    // temporary storage for a CNF clause
 };
 
+static inline clause * clause_read( sat_solver * s, cla h )          
+{ 
+    return Sat_MemClauseHand( &s->Mem, h );      
+}
+
 static int sat_solver_var_value( sat_solver* s, int v )
 {
     assert( v >= 0 && v < s->size );
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index c6eedeb5..af03c70d 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -136,28 +136,28 @@ static inline void    solver2_clear_marks(sat_solver2* s)              {
 //=================================================================================================
 // Clause datatype + minor functions:
 
-static inline satset* clause_read   (sat_solver2* s, cla h)      { return (h & 1) ? satset_read(&s->learnts, h>>1)  : satset_read(&s->clauses, h>>1);          }
-static inline cla     clause_handle (sat_solver2* s, satset* c)  { return c->learnt ? (satset_handle(&s->learnts, c)<<1)|1: satset_handle(&s->clauses, c)<<1;  }
-static inline int     clause_check  (sat_solver2* s, satset* c)  { return c->learnt ? satset_check(&s->learnts, c)  : satset_check(&s->clauses, c);            }
-static inline int     clause_proofid(sat_solver2* s, satset* c, int partA)  { return c->learnt ? (veci_begin(&s->claProofs)[c->Id]<<2) | (partA<<1) : (satset_handle(&s->clauses, c)<<2) | (partA<<1) | 1; }
-static inline int     clause_is_used(sat_solver2* s, cla h)      { return (h & 1) ? ((h >> 1) < s->hLearntPivot) : ((h >> 1) < s->hClausePivot);               }
+static inline satset* clause2_read   (sat_solver2* s, cla h)      { return (h & 1) ? satset_read(&s->learnts, h>>1)  : satset_read(&s->clauses, h>>1);          }
+static inline cla     clause2_handle (sat_solver2* s, satset* c)  { return c->learnt ? (satset_handle(&s->learnts, c)<<1)|1: satset_handle(&s->clauses, c)<<1;  }
+static inline int     clause2_check  (sat_solver2* s, satset* c)  { return c->learnt ? satset_check(&s->learnts, c)  : satset_check(&s->clauses, c);            }
+static inline int     clause2_proofid(sat_solver2* s, satset* c, int partA)  { return c->learnt ? (veci_begin(&s->claProofs)[c->Id]<<2) | (partA<<1) : (satset_handle(&s->clauses, c)<<2) | (partA<<1) | 1; }
+static inline int     clause2_is_used(sat_solver2* s, cla h)      { return (h & 1) ? ((h >> 1) < s->hLearntPivot) : ((h >> 1) < s->hClausePivot);               }
 
 //static inline int     var_reason    (sat_solver2* s, int v)      { return (s->reasons[v]&1) ? 0 : s->reasons[v] >> 1;                   }
 //static inline int     lit_reason    (sat_solver2* s, int l)      { return (s->reasons[lit_var(l)&1]) ? 0 : s->reasons[lit_var(l)] >> 1; }
-//static inline satset* var_unit_clause(sat_solver2* s, int v)           { return (s->reasons[v]&1) ? clause_read(s, s->reasons[v] >> 1) : NULL;  }
+//static inline satset* var_unit_clause(sat_solver2* s, int v)           { return (s->reasons[v]&1) ? clause2_read(s, s->reasons[v] >> 1) : NULL;  }
 //static inline void    var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(i && !s->reasons[v]); s->reasons[v] = (i << 1) | 1;             }
 static inline int     var_reason    (sat_solver2* s, int v)            { return s->reasons[v];           }
 static inline int     lit_reason    (sat_solver2* s, int l)            { return s->reasons[lit_var(l)];  }
-static inline satset* var_unit_clause(sat_solver2* s, int v)           { return clause_read(s, s->units[v]);                                          }
+static inline satset* var_unit_clause(sat_solver2* s, int v)           { return clause2_read(s, s->units[v]);                                          }
 static inline void    var_set_unit_clause(sat_solver2* s, int v, cla i){ 
     assert(v >= 0 && v < s->size && !s->units[v]); s->units[v] = i; s->nUnits++; 
 }
 //static inline void    var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(v >= 0 && v < s->size); s->units[v] = i; s->nUnits++; }
 
 // these two only work after creating a clause before the solver is called
-int    clause_is_partA (sat_solver2* s, int h)                   { return clause_read(s, h)->partA;         }
-void   clause_set_partA(sat_solver2* s, int h, int partA)        { clause_read(s, h)->partA = partA;        }
-int    clause_id(sat_solver2* s, int h)                          { return clause_read(s, h)->Id;            }
+int    clause2_is_partA (sat_solver2* s, int h)                   { return clause2_read(s, h)->partA;         }
+void   clause2_set_partA(sat_solver2* s, int h, int partA)        { clause2_read(s, h)->partA = partA;        }
+int    clause2_id(sat_solver2* s, int h)                          { return clause2_read(s, h)->Id;            }
 
 //=================================================================================================
 // Simple helpers:
@@ -172,7 +172,7 @@ static inline void proof_chain_start( sat_solver2* s, satset* c )
 {
     if ( s->fProofLogging )
     {
-        int ProofId = clause_proofid(s, c, 0);
+        int ProofId = clause2_proofid(s, c, 0);
         assert( ProofId > 0 );
         veci_resize( &s->temp_proof, 0 );
         veci_push( &s->temp_proof, 0 );
@@ -186,7 +186,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 );
-        int ProofId = clause_proofid(s, c, var_is_partA(s,Var));
+        int ProofId = clause2_proofid(s, c, var_is_partA(s,Var));
         assert( ProofId > 0 );
         veci_push( &s->temp_proof, ProofId );
     }
@@ -291,7 +291,7 @@ static inline void act_var_rescale(sat_solver2* s)  {
         activity[i] *= 1e-100;
     s->var_inc *= 1e-100;
 }
-static inline void act_clause_rescale(sat_solver2* s) {
+static inline void act_clause2_rescale(sat_solver2* s) {
     static int Total = 0;
     float * claActs = (float *)veci_begin(&s->claActs);
     int i;
@@ -311,15 +311,15 @@ static inline void act_var_bump(sat_solver2* s, int v) {
     if (s->orderpos[v] != -1)
         order_update(s,v);
 }
-static inline void act_clause_bump(sat_solver2* s, satset*c) {
+static inline void act_clause2_bump(sat_solver2* s, satset*c) {
     float * claActs = (float *)veci_begin(&s->claActs);
     assert( c->Id < veci_size(&s->claActs) );
     claActs[c->Id] += s->cla_inc;
     if (claActs[c->Id] > (float)1e20)
-        act_clause_rescale(s);
+        act_clause2_rescale(s);
 }
 static inline void act_var_decay(sat_solver2* s)    { s->var_inc *= s->var_decay; }
-static inline void act_clause_decay(sat_solver2* s) { s->cla_inc *= s->cla_decay; }
+static inline void act_clause2_decay(sat_solver2* s) { s->cla_inc *= s->cla_decay; }
 
 #else
 
@@ -331,7 +331,7 @@ static inline void act_var_rescale(sat_solver2* s) {
     s->var_inc >>= 19;
     s->var_inc = Abc_MaxInt( s->var_inc, (1<<4) );
 }
-static inline void act_clause_rescale(sat_solver2* s) {
+static inline void act_clause2_rescale(sat_solver2* s) {
 //    static int Total = 0;
     int i;//, clk = clock();
     unsigned * claActs = (unsigned *)veci_begin(&s->claActs);
@@ -351,22 +351,22 @@ static inline void act_var_bump(sat_solver2* s, int v) {
     if (s->orderpos[v] != -1)
         order_update(s,v);
 }
-static inline void act_clause_bump(sat_solver2* s, satset*c) {
+static inline void act_clause2_bump(sat_solver2* s, satset*c) {
     unsigned * claActs = (unsigned *)veci_begin(&s->claActs);
     assert( c->Id > 0 && c->Id < veci_size(&s->claActs) );
     claActs[c->Id] += s->cla_inc;
     if (claActs[c->Id] & 0x80000000)
-        act_clause_rescale(s);
+        act_clause2_rescale(s);
 }
 static inline void act_var_decay(sat_solver2* s)    { s->var_inc += (s->var_inc >>  4); }
-static inline void act_clause_decay(sat_solver2* s) { s->cla_inc += (s->cla_inc >> 10); }
+static inline void act_clause2_decay(sat_solver2* s) { s->cla_inc += (s->cla_inc >> 10); }
 
 #endif
 
 //=================================================================================================
 // Clause functions:
 
-static int clause_create_new(sat_solver2* s, lit* begin, lit* end, int learnt, int proof_id)
+static int clause2_create_new(sat_solver2* s, lit* begin, lit* end, int learnt, int proof_id)
 {
     satset* c;
     int i, Cid, nLits = end - begin;
@@ -404,7 +404,7 @@ static int clause_create_new(sat_solver2* s, lit* begin, lit* end, int learnt, i
         if ( proof_id )
             veci_push(&s->claProofs, proof_id);
         if ( nLits > 2 )
-            act_clause_bump( s,c );
+            act_clause2_bump( s,c );
         // extend storage
         Cid = (veci_size(&s->learnts) << 1) | 1;
         s->learnts.size += satset_size(nLits);
@@ -475,7 +475,7 @@ static inline int solver2_enqueue(sat_solver2* s, lit l, cla from)
 /*
         if ( solver2_dlevel(s) == 0 )
         {
-            satset * c = from ? clause_read( s, from ) : NULL;
+            satset * c = from ? clause2_read( s, from ) : NULL;
             Abc_Print(1, "Enqueing var %d on level %d with reason clause  ", v, solver2_dlevel(s) );
             if ( c )
                 satset_print( c );
@@ -554,7 +554,7 @@ static void solver2_record(sat_solver2* s, veci* cls, int proof_id)
 {
     lit* begin = veci_begin(cls);
     lit* end   = begin + veci_size(cls);
-    cla  Cid   = clause_create_new(s,begin,end,1, proof_id);
+    cla  Cid   = clause2_create_new(s,begin,end,1, proof_id);
     assert(veci_size(cls) > 0);
     if ( veci_size(cls) == 1 )
     {
@@ -607,7 +607,7 @@ void Solver::analyzeFinal(satset* confl, bool skip_first)
         Var     x = var(trail[i]);
         if (seen[x]){
             GClause r = reason[x];
-            if (r == GClause_NULL){
+            if (r == Gclause2_NULL){
                 assert(level[x] > 0);
                 conflict.push(~trail[i]);
             }else{
@@ -647,7 +647,7 @@ static int solver2_analyze_final(sat_solver2* s, satset* conf, int skip_first)
     for (i = s->qtail-1; i >= (veci_begin(&s->trail_lim))[0]; i--){
         x = lit_var(s->trail[i]);
         if (var_tag(s,x)){
-            satset* c = clause_read(s, var_reason(s,x));
+            satset* c = clause2_read(s, var_reason(s,x));
             if (c){
                 proof_chain_resolve( s, c, x );
                 satset_foreach_var( c, x, j, 1 ){
@@ -680,7 +680,7 @@ static int solver2_lit_removable_rec(sat_solver2* s, int v)
         return (var_tag(s,v) & 4) > 0;
 
     // skip decisions on a wrong level
-    c = clause_read(s, var_reason(s,v));
+    c = clause2_read(s, var_reason(s,v));
     if ( c == NULL ){
         var_add_tag(s,v,2);
         return 0;
@@ -730,7 +730,7 @@ static int solver2_lit_removable(sat_solver2* s, int x)
             veci_push(&s->stack, x ^ 1 );
         }
         x >>= 1;
-        c = clause_read(s, var_reason(s,x));
+        c = clause2_read(s, var_reason(s,x));
         satset_foreach_var( c, x, i, 1 ){
             if (var_tag(s,x) || !var_level(s,x))
                 continue;
@@ -763,7 +763,7 @@ static void solver2_logging_order(sat_solver2* s, int x)
         }
         veci_push(&s->stack, x ^ 1 );
         x >>= 1;
-        c = clause_read(s, var_reason(s,x));
+        c = clause2_read(s, var_reason(s,x));
 //        if ( !c )
 //            Abc_Print(1, "solver2_logging_order(): Error in conflict analysis!!!\n" );
         satset_foreach_var( c, x, i, 1 ){
@@ -781,7 +781,7 @@ static void solver2_logging_order_rec(sat_solver2* s, int x)
     int i, y;
     if ( (var_tag(s,x) & 8) )
         return;
-    c = clause_read(s, var_reason(s,x));
+    c = clause2_read(s, var_reason(s,x));
     satset_foreach_var( c, y, i, 1 )
         if ( var_level(s,y) && (var_tag(s,y) & 1) == 0 )
             solver2_logging_order_rec(s, y);
@@ -806,7 +806,7 @@ static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt)
     while ( 1 ){
         assert(c != 0);
         if (c->learnt)
-            act_clause_bump(s,c);
+            act_clause2_bump(s,c);
         satset_foreach_var( c, x, j, (int)(p > 0) ){
             assert(x >= 0 && x < s->size);
             if ( var_tag(s, x) )
@@ -827,7 +827,7 @@ static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt)
         while (!var_tag(s, lit_var(s->trail[ind--])));
 
         p = s->trail[ind+1];
-        c = clause_read(s, lit_reason(s,p));
+        c = clause2_read(s, lit_reason(s,p));
         cnt--;
         if ( cnt == 0 )
             break;
@@ -862,7 +862,7 @@ static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt)
         // add them in the reverse order
         vars = veci_begin(&s->min_step_order);
         for (i = veci_size(&s->min_step_order); i > 0; ) { i--;
-            c = clause_read(s, var_reason(s,vars[i]));
+            c = clause2_read(s, var_reason(s,vars[i]));
             proof_chain_resolve( s, c, vars[i] );
             satset_foreach_var(c, x, k, 1)
                 if ( var_level(s,x) == 0 )
@@ -930,7 +930,7 @@ satset* solver2_propagate(sat_solver2* s)
 
         s->stats.propagations++;
         for (i = j = begin; i < end; ){
-            c = clause_read(s,*i);
+            c = clause2_read(s,*i);
             lits = c->pEnts;
 
             // Make sure the false literal is data[1]:
@@ -968,7 +968,7 @@ satset* solver2_propagate(sat_solver2* s)
                     }
                     proof_id = proof_chain_stop( s );
                     // get a new clause
-                    Cid = clause_create_new( s, &Lit, &Lit + 1, 1, proof_id );
+                    Cid = clause2_create_new( s, &Lit, &Lit + 1, 1, proof_id );
                     assert( (var_unit_clause(s, Var) == NULL) != fLitIsFalse );
                     // if variable already has unit clause, it must be with the other polarity 
                     // in this case, we should derive the empty clause here
@@ -976,18 +976,18 @@ satset* solver2_propagate(sat_solver2* s)
                         var_set_unit_clause(s, Var, Cid);
                     else{
                         // Empty clause derived:
-                        proof_chain_start( s, clause_read(s,Cid) );
+                        proof_chain_start( s, clause2_read(s,Cid) );
                         proof_chain_resolve( s, NULL, Var );
                         proof_id = proof_chain_stop( s );
                         s->hProofLast = proof_id;
-//                        clause_create_new( s, &Lit, &Lit, 1, proof_id );
+//                        clause2_create_new( s, &Lit, &Lit, 1, proof_id );
                     }
                 }
 
                 *j++ = *i;
                 // Clause is unit under assignment:
                 if (!solver2_enqueue(s,Lit, *i)){
-                    confl = clause_read(s,*i++);
+                    confl = clause2_read(s,*i++);
                     // Copy the remaining watches:
                     while (i < end)
                         *j++ = *i++;
@@ -1052,7 +1052,7 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts)
             if ( learnt_clause.size == 1 )
                 var_set_level( s, lit_var(learnt_clause.ptr[0]), 0 );
             act_var_decay(s);
-            act_clause_decay(s);
+            act_clause2_decay(s);
 
         }else{
             // NO CONFLICT
@@ -1327,7 +1327,7 @@ int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end)
         assert( i == begin || lit_var(*(i-1)) != lit_var(*i) );
         // consider the value of this literal
         if ( var_value(s, lit_var(*i)) == lit_sign(*i) ) // this clause is always true
-            return clause_create_new( s, begin, end, 0, 0 ); // add it anyway, to preserve proper clause count       
+            return clause2_create_new( s, begin, end, 0, 0 ); // add it anyway, to preserve proper clause count       
         if ( var_value(s, lit_var(*i)) == varX ) // unassigned literal
             iFree = i;
         else
@@ -1341,7 +1341,7 @@ int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end)
     *begin = temp;
 
     // create a new clause
-    Cid = clause_create_new( s, begin, end, 0, 0 );
+    Cid = clause2_create_new( s, begin, end, 0, 0 );
 
     // handle unit clause
     if ( count+1 == end-begin )
@@ -1358,13 +1358,13 @@ int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end)
             {
                 // Log production of top-level unit clause:
                 int x, k, proof_id, CidNew;
-                satset* c = clause_read(s, Cid);
+                satset* c = clause2_read(s, Cid);
                 proof_chain_start( s, c );
                 satset_foreach_var( c, x, k, 1 )
                     proof_chain_resolve( s, NULL, x );
                 proof_id = proof_chain_stop( s );
                 // generate a new clause
-                CidNew = clause_create_new( s, begin, begin+1, 1, proof_id );
+                CidNew = clause2_create_new( s, begin, begin+1, 1, proof_id );
                 var_set_unit_clause( s, lit_var(begin[0]), CidNew );
                 if ( !solver2_enqueue(s,begin[0],Cid) )
                     assert( 0 );
@@ -1458,7 +1458,7 @@ void sat_solver2_reducedb(sat_solver2* s)
     for ( i = 0; i < s->size; i++ )
         if ( s->reasons[i] && (s->reasons[i] & 1) )
         {
-            c = clause_read( s, s->reasons[i] );
+            c = clause2_read( s, s->reasons[i] );
             assert( c->mark == 0 );
             s->reasons[i] = (c->Id << 1) | 1;
         }
@@ -1470,7 +1470,7 @@ void sat_solver2_reducedb(sat_solver2* s)
         for ( j = k = 0; k < veci_size(&s->wlists[i]); k++ )
             if ( !(pArray[k] & 1) ) // problem clause
                 pArray[j++] = pArray[k];
-            else if ( !(c = clause_read(s, pArray[k]))->mark ) // useful learned clause
+            else if ( !(c = clause2_read(s, pArray[k]))->mark ) // useful learned clause
                 pArray[j++] = (c->Id << 1) | 1;
         veci_resize(&s->wlists[i],j);
     }
@@ -1479,7 +1479,7 @@ void sat_solver2_reducedb(sat_solver2* s)
     for ( i = 0; i < s->size; i++ )
         if ( s->units[i] && (s->units[i] & 1) )
         {
-            c = clause_read( s, s->units[i] );
+            c = clause2_read( s, s->units[i] );
             assert( c->mark == 0 );
             s->units[i] = (c->Id << 1) | 1;
         }
@@ -1544,7 +1544,7 @@ void sat_solver2_rollback( sat_solver2* s )
         {
             cla* pArray = veci_begin(&s->wlists[i]);
             for ( j = k = 0; k < veci_size(&s->wlists[i]); k++ )
-                if ( clause_is_used(s, pArray[k]) )
+                if ( clause2_is_used(s, pArray[k]) )
                     pArray[j++] = pArray[k];
             veci_resize(&s->wlists[i],j);
         }
@@ -1759,7 +1759,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
         assert(var(p) < nVars());
         if (!solver2_assume(p)){
             GClause r = reason[var(p)];
-            if (r != GClause_NULL){
+            if (r != Gclause2_NULL){
                 satset* confl;
                 if (r.isLit()){
                     confl = propagate_tmpbin;
@@ -1792,7 +1792,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
         veci_push(&s->trail_lim,s->qtail);
         if (!solver2_enqueue(s,p,0))
         {
-            satset* r = clause_read(s, lit_reason(s,p));
+            satset* r = clause2_read(s, lit_reason(s,p));
             if (r != NULL)
             {
                 satset* confl = r;
diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h
index 5f847f68..bca9bc97 100644
--- a/src/sat/bsat/satSolver2.h
+++ b/src/sat/bsat/satSolver2.h
@@ -28,6 +28,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <string.h>
 #include <assert.h>
 
+#include "satClause.h"
 #include "satVec.h"
 #include "misc/vec/vecSet.h"
 
@@ -63,10 +64,10 @@ extern void         Sat_Solver2DoubleClauses( sat_solver2 * p, int iVar );
 extern int          var_is_partA (sat_solver2* s, int v);
 extern void         var_set_partA(sat_solver2* s, int v, int partA);
 // clause grouping (these two only work after creating a clause before the solver is called)
-extern int          clause_is_partA (sat_solver2* s, int handle);
-extern void         clause_set_partA(sat_solver2* s, int handle, int partA);
+extern int          clause2_is_partA (sat_solver2* s, int handle);
+extern void         clause2_set_partA(sat_solver2* s, int handle, int partA);
 // other clause functions
-extern int          clause_id(sat_solver2* s, int h);
+extern int          clause2_id(sat_solver2* s, int h);
  
 // proof-based APIs
 extern void *       Sat_ProofCore( sat_solver2 * s );
@@ -274,7 +275,7 @@ static inline int sat_solver2_add_const( sat_solver2 * pSat, int iVar, int fComp
     Lits[0] = toLitCond( iVar, fCompl );
     Cid = sat_solver2_addclause( pSat, Lits, Lits + 1 );
     if ( fMark )
-        clause_set_partA( pSat, Cid, 1 );
+        clause2_set_partA( pSat, Cid, 1 );
     return 1;
 }
 static inline int sat_solver2_add_buffer( sat_solver2 * pSat, int iVarA, int iVarB, int fCompl, int fMark )
@@ -287,13 +288,13 @@ static inline int sat_solver2_add_buffer( sat_solver2 * pSat, int iVarA, int iVa
     Lits[1] = toLitCond( iVarB, !fCompl );
     Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
     if ( fMark )
-        clause_set_partA( pSat, Cid, 1 );
+        clause2_set_partA( pSat, Cid, 1 );
 
     Lits[0] = toLitCond( iVarA, 1 );
     Lits[1] = toLitCond( iVarB, fCompl );
     Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
     if ( fMark )
-        clause_set_partA( pSat, Cid, 1 );
+        clause2_set_partA( pSat, Cid, 1 );
     return 2;
 }
 static inline int sat_solver2_add_and( sat_solver2 * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fMark )
@@ -305,20 +306,20 @@ static inline int sat_solver2_add_and( sat_solver2 * pSat, int iVar, int iVar0,
     Lits[1] = toLitCond( iVar0, fCompl0 );
     Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
     if ( fMark )
-        clause_set_partA( pSat, Cid, 1 );
+        clause2_set_partA( pSat, Cid, 1 );
 
     Lits[0] = toLitCond( iVar, 1 );
     Lits[1] = toLitCond( iVar1, fCompl1 );
     Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
     if ( fMark )
-        clause_set_partA( pSat, Cid, 1 );
+        clause2_set_partA( pSat, Cid, 1 );
 
     Lits[0] = toLitCond( iVar, 0 );
     Lits[1] = toLitCond( iVar0, !fCompl0 );
     Lits[2] = toLitCond( iVar1, !fCompl1 );
     Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
     if ( fMark )
-        clause_set_partA( pSat, Cid, 1 );
+        clause2_set_partA( pSat, Cid, 1 );
     return 3;
 }
 static inline int sat_solver2_add_xor( sat_solver2 * pSat, int iVarA, int iVarB, int iVarC, int fCompl, int fMark )
@@ -332,28 +333,28 @@ static inline int sat_solver2_add_xor( sat_solver2 * pSat, int iVarA, int iVarB,
     Lits[2] = toLitCond( iVarC, 1 );
     Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
     if ( fMark )
-        clause_set_partA( pSat, Cid, 1 );
+        clause2_set_partA( pSat, Cid, 1 );
 
     Lits[0] = toLitCond( iVarA, !fCompl );
     Lits[1] = toLitCond( iVarB, 0 );
     Lits[2] = toLitCond( iVarC, 0 );
     Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
     if ( fMark )
-        clause_set_partA( pSat, Cid, 1 );
+        clause2_set_partA( pSat, Cid, 1 );
 
     Lits[0] = toLitCond( iVarA, fCompl );
     Lits[1] = toLitCond( iVarB, 1 );
     Lits[2] = toLitCond( iVarC, 0 );
     Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
     if ( fMark )
-        clause_set_partA( pSat, Cid, 1 );
+        clause2_set_partA( pSat, Cid, 1 );
 
     Lits[0] = toLitCond( iVarA, fCompl );
     Lits[1] = toLitCond( iVarB, 0 );
     Lits[2] = toLitCond( iVarC, 1 );
     Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
     if ( fMark )
-        clause_set_partA( pSat, Cid, 1 );
+        clause2_set_partA( pSat, Cid, 1 );
     return 4;
 }
 static inline int sat_solver2_add_constraint( sat_solver2 * pSat, int iVar, int iVar2, int fCompl, int fMark )
@@ -366,13 +367,13 @@ static inline int sat_solver2_add_constraint( sat_solver2 * pSat, int iVar, int
     Lits[1] = toLitCond( iVar2, 0 );
     Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
     if ( fMark )
-        clause_set_partA( pSat, Cid, 1 );
+        clause2_set_partA( pSat, Cid, 1 );
 
     Lits[0] = toLitCond( iVar, fCompl );
     Lits[1] = toLitCond( iVar2, 1 );
     Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
     if ( fMark )
-        clause_set_partA( pSat, Cid, 1 );
+        clause2_set_partA( pSat, Cid, 1 );
     return 2;
 }
 
diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c
index 70d09638..67f45b16 100644
--- a/src/sat/bsat/satUtil.c
+++ b/src/sat/bsat/satUtil.c
@@ -30,14 +30,18 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+/*
 struct clause_t
 {
-    int size_learnt;
+    unsigned   size  :  24;
+    unsigned   lbd   :   6;
+    unsigned   leant :   1;
+    unsigned   mark  :   1;
     lit lits[0];
 };
-
-static inline int  clause_size( clause* c )  { return c->size_learnt >> 1; }
+static inline int  clause_size( clause* c )  { return c->size;             }
 static inline lit* clause_begin( clause* c ) { return c->lits;             }
+*/
 
 static void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, int fIncrement );
 
@@ -127,6 +131,7 @@ void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBe
 ***********************************************************************/
 void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, int fIncrement )
 {
+/*
     lit * pLits = clause_begin(pC);
     int nLits = clause_size(pC);
     int i;
@@ -136,6 +141,7 @@ void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, int fIncrement )
     if ( fIncrement )
         fprintf( pFile, "0" );
     fprintf( pFile, "\n" );
+*/
 }
 
 /**Function*************************************************************
diff --git a/src/sat/bsat/satVec.h b/src/sat/bsat/satVec.h
index 27eed39a..35cd3cb4 100644
--- a/src/sat/bsat/satVec.h
+++ b/src/sat/bsat/satVec.h
@@ -127,8 +127,6 @@ static inline void   vecp_remove(vecp* v, void* e)
 #endif
 #endif
 
-typedef int                lit;
-typedef int                cla;
 typedef char               lbool;
 
 static const int   var_Undef = -1;