Started experiments with a new solver.

2 files changed, 265 insertions, 645 deletions

diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index 60ae1bf6..5cb62cf6 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -30,7 +30,6 @@ ABC_NAMESPACE_IMPL_START
 
 
 #define SAT_USE_ANALYZE_FINAL
-//#define SAT_USE_WATCH_ARRAYS
 
 //=================================================================================================
 // Debug:
@@ -103,28 +102,24 @@ static inline void    var_set_level (sat_solver2 * s, int v, int lev )  { s->vi[
 //=================================================================================================
 // Clause datatype + minor functions:
 
-struct clause_t // should have odd number of entries!
+struct clause_t // should have even number of entries!
 {
     unsigned learnt :  1;
     unsigned fMark  :  1;
     unsigned fPartA :  1;
     unsigned fRefed :  1;
     unsigned nLits  : 28;
-    unsigned act;
-    unsigned proof;
-#ifndef SAT_USE_WATCH_ARRAYS
-    int      pNext[2];
-#endif
+    int      Id;
     lit lits[0];
 };
 
 static inline lit*    clause_begin  (clause* c)                  { return c->lits;                                 }
 static inline int     clause_learnt (clause* c)                  { return c->learnt;                               }
 static inline int     clause_nlits  (clause* c)                  { return c->nLits;                                }
-static inline int     clause_size   (int nLits)                  { return sizeof(clause)/4 + nLits + !(nLits & 1); }
+static inline int     clause_size   (int nLits)                  { return sizeof(clause)/4 + nLits + (nLits & 1);  }
 
 static inline clause* get_clause    (sat_solver2* s, int c)      { return (clause *)(s->pMemArray + c);            }
-static inline int     clause_id     (sat_solver2* s, clause* c)  { return ((int *)c - s->pMemArray);               }
+static inline cla     clause_id     (sat_solver2* s, clause* c)  { return (cla)((int *)c - s->pMemArray);          }
 
 #define sat_solver_foreach_clause( s, c, i )  \
     for ( i = 16; (i < s->nMemSize) && (((c) = get_clause(s, i)), 1); i += clause_size(c->nLits) )
@@ -138,6 +133,65 @@ static inline int     sat_solver2_dlevel(sat_solver2* s)            { return vec
 static inline veci*   sat_solver2_read_wlist(sat_solver2* s, lit l) { return &s->wlists[l]; }
 
 //=================================================================================================
+// Clause functions:
+
+static int clause_new(sat_solver2* s, lit* begin, lit* end, int learnt)
+{
+    clause* c;
+    int i, Cid, nLits = end - begin;
+    assert(nLits > 1);
+    assert(begin[0] >= 0);
+    assert(begin[1] >= 0);
+    assert(lit_var(begin[0]) < s->size);
+    assert(lit_var(begin[1]) < s->size);
+    // add memory if needed
+    if ( s->nMemSize + clause_size(nLits) > s->nMemAlloc )
+    {
+        int nMemAlloc = s->nMemAlloc ? s->nMemAlloc * 2 : (1 << 24);
+        s->pMemArray  = ABC_REALLOC( int, s->pMemArray, nMemAlloc );
+        memset( s->pMemArray + s->nMemAlloc, 0, sizeof(int) * (nMemAlloc - s->nMemAlloc) );
+        printf( "Reallocing from %d to %d...\n", s->nMemAlloc, nMemAlloc );
+        s->nMemAlloc = nMemAlloc;
+        s->nMemSize = Abc_MaxInt( s->nMemSize, 16 ); 
+    }
+    // create clause
+    c = (clause*)(s->pMemArray + s->nMemSize);
+    c->learnt = learnt;
+    c->nLits  = nLits;
+    for (i = 0; i < nLits; i++)
+        c->lits[i] = begin[i];
+    // assign clause ID
+    if ( learnt )
+    {
+        c->Id = s->stats.learnts + 1;
+        assert( c->Id == veci_size(&s->claActs) );
+        veci_push(&s->claActs, 0);
+    }
+    else
+    {
+        c->Id = -(s->stats.clauses + 1);
+    }
+
+    // extend storage
+    Cid = s->nMemSize;
+    s->nMemSize += clause_size(nLits);
+    if ( s->nMemSize > s->nMemAlloc )
+        printf( "Out of memory!!!\n" );
+    assert( s->nMemSize <= s->nMemAlloc );
+    assert(((ABC_PTRUINT_T)c & 7) == 0);
+
+    // watch the clause
+    veci_push(sat_solver2_read_wlist(s,lit_neg(begin[0])),clause_id(s,c));
+    veci_push(sat_solver2_read_wlist(s,lit_neg(begin[1])),clause_id(s,c));
+
+    // remember the last one and first learnt
+    s->iLast = Cid;
+    if ( learnt && s->iLearnt == -1 )
+        s->iLearnt = Cid;
+    return Cid;
+}
+
+//=================================================================================================
 // Variable order functions:
 
 static inline void order_update(sat_solver2* s, int v) // updateorder
@@ -178,13 +232,11 @@ static inline int  order_select(sat_solver2* s, float random_var_freq) // select
 {
     int*      heap     = veci_begin(&s->order);
     int*      orderpos = s->orderpos;
-//    lbool*    values   = s->assigns;
 
     // Random decision:
     if (drand(&s->random_seed) < random_var_freq){
         int next = irand(&s->random_seed,s->size);
         assert(next >= 0 && next < s->size);
-//        if (values[next] == l_Undef)
         if (var_value(s, next) == varX)
             return next;
     }
@@ -222,15 +274,13 @@ static inline int  order_select(sat_solver2* s, float random_var_freq) // select
             orderpos[heap[i]] = i;
         }
 
-//printf( "-%d ", next );
-//        if (values[next] == l_Undef)
         if (var_value(s, next) == varX)
             return next;
     }
-
     return var_Undef;
 }
 
+
 //=================================================================================================
 // Activity functions:
 
@@ -261,11 +311,11 @@ static inline void act_var_bump(sat_solver2* s, int v) {
 static inline void act_var_decay(sat_solver2* s) { s->var_inc += (s->var_inc >> 4); }
 
 static inline void act_clause_rescale(sat_solver2* s) {
-    clause * c;
-    int i, clk = clock();
     static int Total = 0;
-    sat_solver_foreach_learnt( s, c, i )
-        c->act >>= 14;
+    int i, clk = clock();
+    unsigned * tagged = (unsigned *)veci_begin(&s->claActs);
+    for (i = 1; i < veci_size(&s->claActs); i++)
+        tagged[i] >>= 14;
     s->cla_inc >>= 14;
 //    assert( s->cla_inc > (1<<10)-1 );
     s->cla_inc = Abc_MaxInt( s->cla_inc, (1<<10) );
@@ -274,219 +324,20 @@ static inline void act_clause_rescale(sat_solver2* s) {
     Abc_PrintTime( 1, "Time", Total );
 }
 
-
 static inline void act_clause_bump(sat_solver2* s, clause *c) {
-    c->act += s->cla_inc;
-    if (c->act & 0x80000000) 
+    assert( c->Id > 0 && c->Id < veci_size(&s->claActs) );
+    ((unsigned *)veci_begin(&s->claActs))[c->Id] += s->cla_inc;
+    if (((unsigned *)veci_begin(&s->claActs))[c->Id] & 0x80000000) 
         act_clause_rescale(s);
 }
 
 //static inline void act_clause_decay(sat_solver2* s) { s->cla_inc *= s->cla_decay; }
 static inline void act_clause_decay(sat_solver2* s) { s->cla_inc += (s->cla_inc >> 10); }
 
-//=================================================================================================
-// Clause functions:
-#ifndef SAT_USE_WATCH_ARRAYS
-
-static inline void clause_watch_front( sat_solver2* s, clause* c, lit Lit )
-{
-    if ( c->lits[0] == Lit )
-        c->pNext[0] = s->pWatches[lit_neg(Lit)];  
-    else
-    {
-        assert( c->lits[1] == Lit );
-        c->pNext[1] = s->pWatches[lit_neg(Lit)];  
-    }
-    s->pWatches[lit_neg(Lit)] = clause_id(s, c);
-}
-static inline void clause_watch( sat_solver2* s, clause* c, lit Lit )
-{
-    clause * pList;
-    cla * ppList = s->pWatches + lit_neg(Lit), * ppNext;
-    if ( c->lits[0] == Lit )
-        ppNext = &c->pNext[0];  
-    else
-    {
-        assert( c->lits[1] == Lit );
-        ppNext = &c->pNext[1];
-    }
-    if ( *ppList == 0 )
-    {
-        *ppList = clause_id(s, c);
-        *ppNext = clause_id(s, c);
-        return;
-    }
-    // add at the tail
-    pList = get_clause( s, *ppList );
-    if ( pList->lits[0] == Lit )
-    {
-        assert( pList->pNext[0] != 0 );
-        *ppNext = pList->pNext[0];
-        pList->pNext[0] = clause_id(s, c);  
-    }
-    else
-    {
-        assert( pList->lits[1] == Lit );
-        assert( pList->pNext[1] != 0 );
-        *ppNext = pList->pNext[1];
-        pList->pNext[1] = clause_id(s, c);  
-    }
-    *ppList = clause_id(s, c);
-}
-/*
-static inline void clause_watch( sat_solver2* s, clause* c, lit Lit )
-{
-    int * ppList = s->pWatches[lit_neg(Lit)];
-    assert( c->lits[0] == Lit || c->lits[1] == Lit );
-    if ( *ppList == NULL )
-        c->pNext[c->lits[1] == Lit] = clause_id(s, c);
-    else
-    {
-        clause * pList = get_clause( s, *ppList );
-        assert( pList->lits[0] == Lit || pList->lits[1] == Lit );
-        c->pNext[c->lits[1] == Lit] = pList->pNext[pList->lits[1] == Lit];
-        pList->pNext[pList->lits[1] == Lit] = clause_id(s, c);  
-    }
-    s->pWatches[lit_neg(Lit)] = clause_id(s, c);
-}
-*/
-#endif
-
-static int clause_new(sat_solver2* s, lit* begin, lit* end, int learnt)
-{
-    clause* c;
-    int i, Cid, nLits = end - begin;
-    assert(nLits > 1);
-    assert(begin[0] >= 0);
-    assert(begin[1] >= 0);
-    assert(lit_var(begin[0]) < s->size);
-    assert(lit_var(begin[1]) < s->size);
-    // add memory if needed
-    if ( s->nMemSize + clause_size(nLits) > s->nMemAlloc )
-    {
-        int nMemAlloc = s->nMemAlloc ? s->nMemAlloc * 2 : (1 << 24);
-        s->pMemArray  = ABC_REALLOC( int, s->pMemArray, nMemAlloc );
-        memset( s->pMemArray + s->nMemAlloc, 0, sizeof(int) * (nMemAlloc - s->nMemAlloc) );
-        printf( "Reallocing from %d to %d...\n", s->nMemAlloc, nMemAlloc );
-        s->nMemAlloc = nMemAlloc;
-        s->nMemSize = Abc_MaxInt( s->nMemSize, 16 ); 
-    }
-    // create clause
-    c = (clause*)(s->pMemArray + s->nMemSize);
-    c->learnt = learnt;
-    c->nLits  = nLits;
-    for (i = 0; i < nLits; i++)
-        c->lits[i] = begin[i];
-
-    // extend storage
-    Cid = s->nMemSize;
-    s->nMemSize += clause_size(nLits);
-    if ( s->nMemSize > s->nMemAlloc )
-        printf( "Out of memory!!!\n" );
-    assert( s->nMemSize <= s->nMemAlloc );
-    assert(((ABC_PTRUINT_T)c & 7) == 0);
-
-
-#ifdef SAT_USE_WATCH_ARRAYS
-    veci_push(sat_solver2_read_wlist(s,lit_neg(begin[0])),clause_id(s,c));
-    veci_push(sat_solver2_read_wlist(s,lit_neg(begin[1])),clause_id(s,c));
-#else
-    clause_watch( s, c, begin[0] );
-    clause_watch( s, c, begin[1] );
-#endif
-
-    // remember the last one and first learnt
-    s->iLast = Cid;
-    if ( learnt && s->iLearnt == -1 )
-        s->iLearnt = Cid;
-    return Cid;
-}
-
-
-static void clause_remove(sat_solver2* s, clause* c)
-{
-    lit* lits = clause_begin(c);
-    assert(lit_neg(lits[0]) < s->size*2);
-    assert(lit_neg(lits[1]) < s->size*2);
-
-#ifdef SAT_USE_WATCH_ARRAYS
-    veci_remove(sat_solver2_read_wlist(s,lit_neg(lits[0])),clause_id(s,c));
-    veci_remove(sat_solver2_read_wlist(s,lit_neg(lits[1])),clause_id(s,c));
-#endif
-
-    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);
-    }
-}
-
-
-static lbool clause_simplify(sat_solver2* s, clause* c)
-{
-    lit*   lits   = clause_begin(c);
-//    lbool* values = s->assigns;
-    int i;
-
-    assert(sat_solver2_dlevel(s) == 0);
-
-    for (i = 0; i < clause_nlits(c); i++){
-//        lbool sig = !lit_sign(lits[i]); sig += sig - 1;
-//        if (values[lit_var(lits[i])] == sig)
-        if (var_value(s, lit_var(lits[i])) == lit_sign(lits[i]))
-            return l_True;
-    }
-    return l_False;
-}
 
 //=================================================================================================
 // Minor (solver) functions:
 
-void sat_solver2_setnvars(sat_solver2* s,int n)
-{
-    int var;
-
-    if (s->cap < n){
- 
-        while (s->cap < n) s->cap = s->cap*2+1;
-
-#ifdef SAT_USE_WATCH_ARRAYS
-        s->wlists    = ABC_REALLOC(veci,     s->wlists,   s->cap*2);
-#else
-        s->pWatches  = ABC_REALLOC(cla,      s->pWatches, s->cap*2);
-#endif
-        s->vi        = ABC_REALLOC(varinfo,  s->vi,       s->cap);
-        s->activity  = ABC_REALLOC(unsigned, s->activity, s->cap);
-        s->orderpos  = ABC_REALLOC(int,      s->orderpos, s->cap);
-        s->reasons   = ABC_REALLOC(cla,      s->reasons,  s->cap);
-        s->trail     = ABC_REALLOC(lit,      s->trail,    s->cap);
-    }
-
-    for (var = s->size; var < n; var++){
-#ifdef SAT_USE_WATCH_ARRAYS
-        veci_new(&s->wlists[2*var]);
-        veci_new(&s->wlists[2*var+1]);
-#else
-        s->pWatches[2*var]   = 0;
-        s->pWatches[2*var+1] = 0;
-#endif
-        *((int*)s->vi + var) = 0; s->vi[var].val = varX;
-        s->activity [var]    = (1<<10);
-        s->orderpos [var]    = veci_size(&s->order);
-        s->reasons  [var]    = 0;
-        
-        // does not hold because variables enqueued at top level will not be reinserted in the heap
-        // assert(veci_size(&s->order) == var); 
-        veci_push(&s->order,var);
-        order_update(s, var);
-    }
-
-    s->size = n > s->size ? n : s->size;
-}
-
-
 static inline int enqueue(sat_solver2* s, lit l, int from)
 {
     int    v      = lit_var(l);
@@ -579,44 +430,6 @@ static double sat_solver2_progress(sat_solver2* s)
 //=================================================================================================
 // Major methods:
 
-static int sat_solver2_lit_removable(sat_solver2* s, lit l, int minl)
-{
-    clause* c;
-    lit* lits;
-    int i, j, v, top = veci_size(&s->tagged);
-    assert(lit_var(l) >= 0 && lit_var(l) < s->size);
-    assert(s->reasons[lit_var(l)] != 0);
-    veci_resize(&s->stack,0);
-    veci_push(&s->stack,lit_var(l));
-    while (veci_size(&s->stack) > 0)
-    {
-        v = veci_begin(&s->stack)[veci_size(&s->stack)-1];
-        assert(v >= 0 && v < s->size);
-        veci_resize(&s->stack,veci_size(&s->stack)-1);
-        assert(s->reasons[v] != 0);
-        c = get_clause(s, s->reasons[v]);
-        lits = clause_begin(c);
-        for (i = 1; i < clause_nlits(c); i++){
-            int v = lit_var(lits[i]);
-            if (s->vi[v].tag == 0 && var_level(s,v)){
-                if (s->reasons[v] != 0 && ((1 << (var_level(s,v) & 31)) & minl)){
-                    veci_push(&s->stack,lit_var(lits[i]));
-                    var_set_tag(s, v, 1);
-                    veci_push(&s->tagged,v);
-                }else{
-                    int* tagged = veci_begin(&s->tagged);
-                    for (j = top; j < veci_size(&s->tagged); j++)
-                        var_set_tag(s, tagged[j], 0);
-                    veci_resize(&s->tagged,top);
-                    return false;
-                }
-            }
-        }
-    }
-    return true;
-}
-
-
 /*_________________________________________________________________________________________________
 |
 |  analyzeFinal : (p : Lit)  ->  [void]
@@ -714,6 +527,43 @@ static void sat_solver2_analyze_final(sat_solver2* s, clause* conf, int skip_fir
 #endif
 
 
+static int sat_solver2_lit_removable(sat_solver2* s, lit l, int minl)
+{
+    clause* c;
+    lit* lits;
+    int i, j, v, top = veci_size(&s->tagged);
+    assert(lit_var(l) >= 0 && lit_var(l) < s->size);
+    assert(s->reasons[lit_var(l)] != 0);
+    veci_resize(&s->stack,0);
+    veci_push(&s->stack,lit_var(l));
+    while (veci_size(&s->stack) > 0)
+    {
+        v = veci_begin(&s->stack)[veci_size(&s->stack)-1];
+        assert(v >= 0 && v < s->size);
+        veci_resize(&s->stack,veci_size(&s->stack)-1);
+        assert(s->reasons[v] != 0);
+        c = get_clause(s, s->reasons[v]);
+        lits = clause_begin(c);
+        for (i = 1; i < clause_nlits(c); i++){
+            int v = lit_var(lits[i]);
+            if (s->vi[v].tag == 0 && var_level(s,v)){
+                if (s->reasons[v] != 0 && ((1 << (var_level(s,v) & 31)) & minl)){
+                    veci_push(&s->stack,lit_var(lits[i]));
+                    var_set_tag(s, v, 1);
+                    veci_push(&s->tagged,v);
+                }else{
+                    int* tagged = veci_begin(&s->tagged);
+                    for (j = top; j < veci_size(&s->tagged); j++)
+                        var_set_tag(s, tagged[j], 0);
+                    veci_resize(&s->tagged,top);
+                    return false;
+                }
+            }
+        }
+    }
+    return true;
+}
+
 static void sat_solver2_analyze(sat_solver2* s, clause* c, veci* learnt)
 {
     lit*     trail   = s->trail;
@@ -810,236 +660,6 @@ static void sat_solver2_analyze(sat_solver2* s, clause* c, veci* learnt)
 #endif
 }
 
-#ifndef SAT_USE_WATCH_ARRAYS
-
-static inline clause* clause_propagate__front( sat_solver2* s, lit Lit )
-{
-    clause * pCur;
-    cla * ppPrev, pThis, pTemp;
-    lit LitF = lit_neg(Lit);
-    int i, Counter = 0;
-    s->stats.propagations++;
-    if ( s->pWatches[Lit] == 0 )
-        return NULL;
-    // iterate through the literals
-    ppPrev = s->pWatches + Lit;
-    for ( pThis = *ppPrev; pThis; pThis = *ppPrev )
-    {
-        Counter++;
-        // make sure the false literal is in the second literal of the clause
-        pCur = get_clause( s, pThis );
-        if ( pCur->lits[0] == LitF )
-        {
-            pCur->lits[0] = pCur->lits[1];
-            pCur->lits[1] = LitF;
-            pTemp = pCur->pNext[0];
-            pCur->pNext[0] = pCur->pNext[1];
-            pCur->pNext[1] = pTemp;
-        }
-        assert( pCur->lits[1] == LitF );
-
-        // if the first literal is true, the clause is satisfied
-//        if ( pCur->lits[0] == s->pAssigns[lit_var(pCur->lits[0])] )
-//        sig = !lit_sign(pCur->lits[0]); sig += sig - 1;
-//        if (s->assigns[lit_var(pCur->lits[0])] == sig)
-        if (var_value(s, lit_var(pCur->lits[0])) == lit_sign(pCur->lits[0]))
-        {
-            ppPrev = &pCur->pNext[1];
-            continue;
-        }
-
-        // look for a new literal to watch
-        for ( i = 2; i < clause_nlits(pCur); i++ )
-        {
-            // skip the case when the literal is false
-//            if ( lit_neg(pCur->lits[i]) == p->pAssigns[lit_var(pCur->lits[i])] )
-//            sig = lit_sign(pCur->lits[i]); sig += sig - 1;
-//            if (s->assigns[lit_var(pCur->lits[i])] == sig)
-            if (var_value(s, lit_var(pCur->lits[i])) == !lit_sign(pCur->lits[i]))
-                continue;
-            // the literal is either true or unassigned - watch it
-            pCur->lits[1] = pCur->lits[i];
-            pCur->lits[i] = LitF;
-            // remove this clause from the watch list of Lit
-            *ppPrev = pCur->pNext[1];
-            // add this clause to the watch list of pCur->lits[i] (now it is pCur->lits[1])
-            clause_watch( s, pCur, pCur->lits[1] );
-            break;
-        }
-        if ( i < clause_nlits(pCur) ) // found new watch
-            continue;
-
-        // clause is unit - enqueue new implication
-        if ( enqueue(s, pCur->lits[0], clause_id(s,pCur)) )
-        {
-            ppPrev = &pCur->pNext[1];
-            continue;
-        }
-
-        // conflict detected - return the conflict clause
-//        printf( "%d ", Counter );
-        return pCur;
-    }
-//    printf( "%d ", Counter );
-    return NULL;
-}
-clause* sat_solver2_propagate_new__front( sat_solver2* s )
-{
-    clause* pClause;
-    lit Lit;
-    while ( s->qtail - s->qhead > 0 )
-    {
-        Lit = s->trail[s->qhead++];
-        pClause = clause_propagate__front( s, Lit );
-        if ( pClause )
-            return pClause;
-    }
-    return NULL;
-}
-
-static inline clause* clause_propagate( sat_solver2* s, lit Lit, int * ppHead, int * ppTail )
-{
-    clause * pCur;
-    cla * ppPrev = ppHead, pThis, pTemp, pPrev = 0;
-    lit LitF = lit_neg(Lit);
-    int i, Counter = 0;
-    // iterate through the literals
-    for ( pThis = *ppPrev; pThis; pThis = *ppPrev )
-    {
-        Counter++;
-        // make sure the false literal is in the second literal of the clause
-        pCur = get_clause( s, pThis );
-        if ( pCur->lits[0] == LitF )
-        {
-            pCur->lits[0] = pCur->lits[1];
-            pCur->lits[1] = LitF;
-            pTemp = pCur->pNext[0];
-            pCur->pNext[0] = pCur->pNext[1];
-            pCur->pNext[1] = pTemp;
-        }
-        assert( pCur->lits[1] == LitF );
-
-        // if the first literal is true, the clause is satisfied
-//        if ( pCur->lits[0] == s->pAssigns[lit_var(pCur->lits[0])] )
-//        sig = !lit_sign(pCur->lits[0]); sig += sig - 1;
-//        if ( s->assigns[lit_var(pCur->lits[0])] == sig )
-        if (var_value(s, lit_var(pCur->lits[0])) == lit_sign(pCur->lits[0]))
-        {
-            pPrev = pThis;
-            ppPrev = &pCur->pNext[1];
-            continue;
-        }
-
-        // look for a new literal to watch
-        for ( i = 2; i < clause_nlits(pCur); i++ )
-        {
-            // skip the case when the literal is false
-//            if ( lit_neg(pCur->lits[i]) == p->pAssigns[lit_var(pCur->lits[i])] )
-//            sig = lit_sign(pCur->lits[i]); sig += sig - 1;
-//            if ( s->assigns[lit_var(pCur->lits[i])] == sig )
-            if (var_value(s, lit_var(pCur->lits[i])) == !lit_sign(pCur->lits[i]))
-                continue;
-            // the literal is either true or unassigned - watch it
-            pCur->lits[1] = pCur->lits[i];
-            pCur->lits[i] = LitF;
-            // remove this clause from the watch list of Lit
-            if ( pCur->pNext[1] == 0 )
-            {
-                assert( *ppTail == pThis );
-                *ppTail = pPrev;
-            }
-            *ppPrev = pCur->pNext[1];
-            // add this clause to the watch list of pCur->lits[i] (now it is pCur->lits[1])
-            clause_watch( s, pCur, pCur->lits[1] );
-            break;
-        }
-        if ( i < clause_nlits(pCur) ) // found new watch
-            continue;
-
-        // clause is unit - enqueue new implication
-        if ( enqueue(s, pCur->lits[0], clause_id(s,pCur)) )
-        {
-            pPrev = pThis;
-            ppPrev = &pCur->pNext[1];
-            continue;
-        }
-
-        // conflict detected - return the conflict clause
-//        printf( "%d ", Counter );
-        return pCur;
-    }
-//    printf( "%d ", Counter );
-    return NULL;
-
-}
-clause* sat_solver2_propagate_new( sat_solver2* s )
-{ 
-    clause * pClause, * pTailC;
-    cla pHead, pTail;
-    lit Lit;
-    while ( s->qtail - s->qhead > 0 )
-    {
-        s->stats.propagations++;
-        Lit = s->trail[s->qhead++];
-        if ( s->pWatches[Lit] == 0 )
-            continue;
-        // get head and tail
-        pTail = s->pWatches[Lit];
-        pTailC = get_clause( s, pTail );
-/*
-        if ( pTailC->lits[0] == lit_neg(Lit) )
-        {
-            pHead = pTailC->pNext[0]; 
-            pTailC->pNext[0] = NULL;
-        }
-        else
-        {
-            assert( pTailC->lits[1] == lit_neg(Lit) );
-            pHead = pTailC->pNext[1];  
-            pTailC->pNext[1] = NULL;
-        }
-*/
-        if ( s->stats.propagations == 10 )
-        {
-            int s = 0;
-        }
-        assert( pTailC->lits[0] == lit_neg(Lit) || pTailC->lits[1] == lit_neg(Lit) );
-        pHead = pTailC->pNext[pTailC->lits[1] == lit_neg(Lit)]; 
-        pTailC->pNext[pTailC->lits[1] == lit_neg(Lit)] = 0;
-
-        // propagate
-        pClause = clause_propagate( s, Lit, &pHead, &pTail );
-        assert( (pHead == 0) == (pTail == 0) );
-
-        // create new list
-        s->pWatches[Lit] = pTail;
-/*
-        if ( pTail )
-        {
-            pTailC = get_clause( s, pTail );
-            if ( pTailC->lits[0] == lit_neg(Lit) )
-                pTailC->pNext[0] = pHead;
-            else
-            {
-                assert( pTailC->lits[1] == lit_neg(Lit) );
-                pTailC->pNext[1] = pHead;
-            }
-        }
-*/
-        if ( pTail )
-        {
-            pTailC = get_clause( s, pTail );
-            assert( pTailC->lits[0] == lit_neg(Lit) || pTailC->lits[1] == lit_neg(Lit) );
-            pTailC->pNext[pTailC->lits[1] == lit_neg(Lit)] = pHead;
-        }
-        if ( pClause )
-            return pClause;
-    }
-    return NULL;
-}
-
-#endif
-
 clause* sat_solver2_propagate(sat_solver2* s)
 {
     clause * c, * confl  = NULL;
@@ -1047,11 +667,6 @@ clause* sat_solver2_propagate(sat_solver2* s)
     lit* lits, false_lit, p, * stop, * k;
     cla* begin,* end, *i, *j;
 
-
-#ifndef SAT_USE_WATCH_ARRAYS
-    return sat_solver2_propagate_new( s );
-#endif
-
     while (confl == 0 && s->qtail - s->qhead > 0){
         p  = s->trail[s->qhead++];
         ws = sat_solver2_read_wlist(s,p);
@@ -1113,44 +728,107 @@ next:       i++;
 }
 
 
-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; }
-    return clause_nlits((clause*)x) > 2 && (clause_nlits((clause*)y) == 2 || ((clause*)x)->act < ((clause*)y)->act) ? -1 : 1; }
+
+static void clause_remove(sat_solver2* s, clause* c)
+{
+    lit* lits = clause_begin(c);
+    assert(lit_neg(lits[0]) < s->size*2);
+    assert(lit_neg(lits[1]) < s->size*2);
+
+    veci_remove(sat_solver2_read_wlist(s,lit_neg(lits[0])),clause_id(s,c));
+    veci_remove(sat_solver2_read_wlist(s,lit_neg(lits[1])),clause_id(s,c));
+
+    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);
+    }
+}
+
+
+static lbool clause_simplify(sat_solver2* s, clause* c)
+{
+    lit*   lits   = clause_begin(c);
+    int i;
+    assert(sat_solver2_dlevel(s) == 0);
+    for (i = 0; i < clause_nlits(c); i++){
+        if (var_value(s, lit_var(lits[i])) == lit_sign(lits[i]))
+            return l_True;
+    }
+    return l_False;
+}
+
+int sat_solver2_simplify(sat_solver2* s)
+{
+//    int type;
+    int Counter = 0;
+    assert(sat_solver2_dlevel(s) == 0);
+    if (sat_solver2_propagate(s) != 0)
+        return false;
+    if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0)
+        return true;
+/*
+    for (type = 0; type < 2; type++){
+        veci* cs  = type ? &s->learnts : &s->clauses;
+        int*  cls = (int*)veci_begin(cs);
+        int i, j;
+        for (j = i = 0; i < veci_size(cs); i++){
+            clause * c = get_clause(s,cls[i]);
+            if (s->reasons[lit_var(*clause_begin(c))] != cls[i] &&
+                clause_simplify(s,c) == l_True)
+                clause_remove(s,c), Counter++;
+            else
+                cls[j++] = cls[i];
+        }
+        veci_resize(cs,j);
+    }
+*/
+//printf( "Simplification removed %d clauses (out of %d)...\n", Counter, s->stats.clauses );
+    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;
+}
  
 void sat_solver2_reducedb(sat_solver2* s)
 {
-/*
-    vecp     Vec, * pVec = &Vec;
-    double   extra_limD = (double)s->cla_inc / veci_size(&s->learnts); // Remove any clause below this activity
-    unsigned extra_lim  = (extra_limD < 1.0) ? 1 : (int)extra_limD;
-    int      i, j, * pBeg, * pEnd;
-
-    // move clauses into vector
-    vecp_new( pVec );
-    pBeg = (int*)veci_begin(&s->learnts);
-    pEnd = pBeg + veci_size(&s->learnts);
-    while ( pBeg < pEnd )
-        vecp_push( pVec, get_clause(s,*pBeg++) );
-    sat_solver2_sort( vecp_begin(pVec), vecp_size(pVec), &clause_cmp );
-    vecp_delete( pVec );
-
-    // compact clauses
-    pBeg = (int*)veci_begin(&s->learnts);
-    for (i = j = 0; i < vecp_size(pVec); i++)
+    clause * c;
+    cla Cid;
+    int clk = clock();
+
+    // sort the clauses by activity
+    int nLearnts = veci_size(&s->claActs) - 1;
+    extern int * Abc_SortCost( int * pCosts, int nSize );
+    int * pPerm, * pCosts = veci_begin(&s->claActs);
+    pPerm = Abc_SortCost( pCosts, veci_size(&s->claActs) );
+    assert( pCosts[pPerm[1]] <= pCosts[pPerm[veci_size(&s->claActs)-1]] );
+
+    // mark clauses to be removed
     {
-        clause * c = ((clause**)vecp_begin(pVec))[i]; 
-        int Cid = clause_id(s,c);
-//        printf( "%d ", c->act );
-        if (clause_nlits(c) > 2 && s->reasons[lit_var(*clause_begin(c))] != Cid && (i < vecp_size(pVec)/2 || c->act < extra_lim) )
-            clause_remove(s,c);
-        else
-            pBeg[j++] = Cid;
+        double   extra_limD = (double)s->cla_inc / nLearnts; // Remove any clause below this activity
+        unsigned extra_lim  = (extra_limD < 1.0) ? 1 : (int)extra_limD;
+        unsigned * pActs = (unsigned *)veci_begin(&s->claActs);
+        int k = 1, Counter = 0;
+        sat_solver_foreach_learnt( s, c, Cid )
+        {
+            assert( c->Id == k );
+            c->fMark = 0;
+            if ( clause_nlits(c) > 2 && s->reasons[lit_var(*clause_begin(c))] != Cid && (k < nLearnts/2 || pActs[k] < extra_lim) )
+            {
+                c->fMark = 1;
+                Counter++;
+            }
+            k++;
+        }
+printf( "ReduceDB removed %10d clauses (out of %10d)... Cutoff = %8d  ", Counter, nLearnts, extra_lim );
+Abc_PrintTime( 1, "Time", clock() - clk );
     }
-printf( "Reduction removed %10d clauses (out of %10d)... Value = %d\n", veci_size(&s->learnts) - j, veci_size(&s->learnts), extra_lim );
-    veci_resize(&s->learnts,j);
-*/
+    ABC_FREE( pPerm );
 }
 
+
 static lbool sat_solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts, ABC_INT64_T * nof_learnts)
 {
     double  var_decay       = 0.95;
@@ -1230,8 +908,8 @@ static lbool sat_solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts, ABC_I
             if (*nof_learnts >= 0 && s->stats.learnts - s->qtail >= *nof_learnts)
             {
                 // Reduce the set of learnt clauses:
-//                sat_solver2_reducedb(s);
-//                *nof_learnts = *nof_learnts * 12 / 10; //*= 1.1;
+                sat_solver2_reducedb(s);
+                *nof_learnts = *nof_learnts * 11 / 10; //*= 1.1;
             }
 
             // New variable decision:
@@ -1273,8 +951,7 @@ static lbool sat_solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts, ABC_I
 
 sat_solver2* sat_solver2_new(void)
 {
-    sat_solver2 * s;
-    s = (sat_solver2 *)ABC_CALLOC( char, sizeof(sat_solver2) );
+    sat_solver2 * s = (sat_solver2 *)ABC_CALLOC( char, sizeof(sat_solver2) );
 
     // initialize vectors
     veci_new(&s->order);
@@ -1284,6 +961,10 @@ sat_solver2* sat_solver2_new(void)
     veci_new(&s->model);
     veci_new(&s->temp_clause);
     veci_new(&s->conf_final);
+    veci_new(&s->claActs);
+    veci_new(&s->claProofs);
+    veci_push(&s->claActs,   -1);
+    veci_push(&s->claProofs, -1);
 
     // initialize other
     s->iLearnt                = -1; // the first learnt clause 
@@ -1294,6 +975,36 @@ sat_solver2* sat_solver2_new(void)
     return s;
 }
 
+void sat_solver2_setnvars(sat_solver2* s,int n)
+{
+    int var;
+
+    if (s->cap < n){
+ 
+        while (s->cap < n) s->cap = s->cap*2+1;
+
+        s->wlists    = ABC_REALLOC(veci,     s->wlists,   s->cap*2);
+        s->vi        = ABC_REALLOC(varinfo,  s->vi,       s->cap);
+        s->activity  = ABC_REALLOC(unsigned, s->activity, s->cap);
+        s->orderpos  = ABC_REALLOC(int,      s->orderpos, s->cap);
+        s->reasons   = ABC_REALLOC(cla,      s->reasons,  s->cap);
+        s->trail     = ABC_REALLOC(lit,      s->trail,    s->cap);
+    }
+
+    for (var = s->size; var < n; var++){
+        veci_new(&s->wlists[2*var]);
+        veci_new(&s->wlists[2*var+1]);
+        *((int*)s->vi + var) = 0; s->vi[var].val = varX;
+        s->activity [var]    = (1<<10);
+        s->orderpos [var]    = veci_size(&s->order);
+        s->reasons  [var]    = 0;        
+        // does not hold because variables enqueued at top level will not be reinserted in the heap
+        // assert(veci_size(&s->order) == var); 
+        veci_push(&s->order,var);
+        order_update(s, var);
+    }
+    s->size = n > s->size ? n : s->size;
+}
 
 void sat_solver2_delete(sat_solver2* s)
 {
@@ -1307,6 +1018,8 @@ void sat_solver2_delete(sat_solver2* s)
     veci_delete(&s->model);
     veci_delete(&s->temp_clause);
     veci_delete(&s->conf_final);
+    veci_delete(&s->claActs);
+    veci_delete(&s->claProofs);
 
     // delete arrays
     if (s->vi != 0){
@@ -1315,7 +1028,6 @@ void sat_solver2_delete(sat_solver2* s)
             for (i = 0; i < s->size*2; i++)
                 veci_delete(&s->wlists[i]);
         ABC_FREE(s->wlists   );
-        ABC_FREE(s->pWatches );
         ABC_FREE(s->vi       );
         ABC_FREE(s->activity );
         ABC_FREE(s->orderpos );
@@ -1388,45 +1100,6 @@ int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end)
 }
 
 
-int sat_solver2_simplify(sat_solver2* s)
-{
-//    int type;
-    int Counter = 0;
-
-    assert(sat_solver2_dlevel(s) == 0);
-
-    if (sat_solver2_propagate(s) != 0)
-        return false;
-
-    if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0)
-        return true;
-
-/*
-    for (type = 0; type < 2; type++){
-        veci* cs  = type ? &s->learnts : &s->clauses;
-        int*  cls = (int*)veci_begin(cs);
-
-        int i, j;
-        for (j = i = 0; i < veci_size(cs); i++){
-            clause * c = get_clause(s,cls[i]);
-            if (s->reasons[lit_var(*clause_begin(c))] != cls[i] &&
-                clause_simplify(s,c) == l_True)
-                clause_remove(s,c), Counter++;
-            else
-                cls[j++] = cls[i];
-        }
-        veci_resize(cs,j);
-    }
-*/
-//printf( "Simplification removed %d clauses (out of %d)...\n", Counter, s->stats.clauses );
-
-    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;
-}
-
 double luby2(double y, int x)
 {
     int size, seq;
@@ -1625,74 +1298,5 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
 }
 
 
-int sat_solver2_nvars(sat_solver2* s)
-{
-    return s->size;
-}
-
-
-int sat_solver2_nclauses(sat_solver2* s)
-{
-    return (int)s->stats.clauses;
-}
-
-
-int sat_solver2_nconflicts(sat_solver2* s)
-{
-    return (int)s->stats.conflicts;
-}
-
-//=================================================================================================
-// Sorting functions (sigh):
-
-static inline void selectionsort(void** array, int size, int(*comp)(const void *, const void *))
-{
-    int     i, j, best_i;
-    void*   tmp;
-
-    for (i = 0; i < size-1; i++){
-        best_i = i;
-        for (j = i+1; j < size; j++){
-            if (comp(array[j], array[best_i]) < 0)
-                best_i = j;
-        }
-        tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp;
-    }
-}
-
-
-static void sortrnd(void** array, int size, int(*comp)(const void *, const void *), double* seed)
-{
-    if (size <= 15)
-        selectionsort(array, size, comp);
-
-    else{
-        void*       pivot = array[irand(seed, size)];
-        void*       tmp;
-        int         i = -1;
-        int         j = size;
-
-        for(;;){
-            do i++; while(comp(array[i], pivot)<0);
-            do j--; while(comp(pivot, array[j])<0);
-
-            if (i >= j) break;
-
-            tmp = array[i]; array[i] = array[j]; array[j] = tmp;
-        }
-
-        sortrnd(array    , i     , comp, seed);
-        sortrnd(&array[i], size-i, comp, seed);
-    }
-}
-
-void sat_solver2_sort(void** array, int size, int(*comp)(const void *, const void *))
-{
-//    int i;
-    double seed = 91648253;
-    sortrnd(array,size,comp,&seed);
-//    for ( i = 1; i < size; i++ )
-//        assert(comp(array[i-1], array[i])<0);
-}
 ABC_NAMESPACE_IMPL_END
 
diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h
index 2725c92b..5ccb2c33 100644
--- a/src/sat/bsat/satSolver2.h
+++ b/src/sat/bsat/satSolver2.h
@@ -100,7 +100,6 @@ struct sat_solver2_t
     int           iLearnt;       // the first learnt clause 
     int           iLast;         // the last learnt clause 
     veci*         wlists;        // watcher lists (for each literal)
-    cla*          pWatches;      // watcher lists (for each literal)
 
     // clause memory
     int *         pMemArray;
@@ -111,6 +110,8 @@ struct sat_solver2_t
     int           var_inc;       // Amount to bump next variable with.
     int           cla_inc;       // Amount to bump next clause with.
     unsigned*     activity;      // A heuristic measurement of the activity of a variable.
+    veci          claActs;       // clause activities
+    veci          claProofs;     // clause proofs
 
     // internal state
     varinfo *     vi;            // variable information
@@ -134,24 +135,39 @@ struct sat_solver2_t
 
 };
 
-static int sat_solver2_var_value( sat_solver2* s, int v ) 
+static inline int sat_solver2_nvars(sat_solver2* s)
+{
+    return s->size;
+}
+
+static inline int sat_solver2_nclauses(sat_solver2* s)
+{
+    return (int)s->stats.clauses;
+}
+
+static inline int sat_solver2_nconflicts(sat_solver2* s)
+{
+    return (int)s->stats.conflicts;
+}
+
+static inline int sat_solver2_var_value( sat_solver2* s, int v ) 
 {
     assert( s->model.ptr != NULL && v < s->size );
     return (int)(s->model.ptr[v] == l_True);
 }
-static int sat_solver2_var_literal( sat_solver2* s, int v ) 
+static inline int sat_solver2_var_literal( sat_solver2* s, int v ) 
 {
     assert( s->model.ptr != NULL && v < s->size );
     return toLitCond( v, s->model.ptr[v] != l_True );
 }
-static void sat_solver2_act_var_clear(sat_solver2* s) 
+static inline void sat_solver2_act_var_clear(sat_solver2* s) 
 {
     int i;
     for (i = 0; i < s->size; i++)
         s->activity[i] = 0;//.0;
     s->var_inc = 1.0;
 }
-static void sat_solver2_compress(sat_solver2* s) 
+static inline void sat_solver2_compress(sat_solver2* s) 
 {
     if ( s->qtail != s->qhead )
     {
@@ -160,20 +176,20 @@ static void sat_solver2_compress(sat_solver2* s)
     }
 }
 
-static int sat_solver2_final(sat_solver2* s, int ** ppArray)
+static inline int sat_solver2_final(sat_solver2* s, int ** ppArray)
 {
     *ppArray = s->conf_final.ptr;
     return s->conf_final.size;
 }
 
-static int sat_solver2_set_runtime_limit(sat_solver2* s, int Limit)
+static inline int sat_solver2_set_runtime_limit(sat_solver2* s, int Limit)
 {
     int nRuntimeLimit = s->nRuntimeLimit;
     s->nRuntimeLimit = Limit;
     return nRuntimeLimit;
 }
 
-static int sat_solver2_set_random(sat_solver2* s, int fNotUseRandom)
+static inline int sat_solver2_set_random(sat_solver2* s, int fNotUseRandom)
 {
     int fNotUseRandomOld = s->fNotUseRandom;
     s->fNotUseRandom = fNotUseRandom;