Transforming the solver to use different clause representation.

11 files changed, 2489 insertions, 543 deletions

diff --git a/src/aig/cec/cecSolve.c b/src/aig/cec/cecSolve.c
index dc1b88eb..e86c2f35 100644
--- a/src/aig/cec/cecSolve.c
+++ b/src/aig/cec/cecSolve.c
@@ -376,6 +376,7 @@ void Cec_ManSatSolverRecycle( Cec_ManSat_t * p )
         sat_solver_delete( p->pSat );
     }
     p->pSat = sat_solver_new();
+    p->pSat->factors = ABC_CALLOC( double, 1 );
     sat_solver_setnvars( p->pSat, 1000 );
     // var 0 is not used
     // var 1 is reserved for const0 node - add the clause
diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c
index b53805b4..f7c0743b 100644
--- a/src/aig/ivy/ivyFraig.c
+++ b/src/aig/ivy/ivyFraig.c
@@ -2113,6 +2113,7 @@ int Ivy_FraigNodesAreEquiv( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pN
     if ( p->pSat == NULL )
     {
         p->pSat = sat_solver_new();
+        p->pSat->factors = ABC_CALLOC( double, 1 );
         p->nSatVars = 1;
         sat_solver_setnvars( p->pSat, 1000 );
         // var 0 is reserved for const1 node - add the clause
@@ -2264,6 +2265,7 @@ int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pNew )
     if ( p->pSat == NULL )
     {
         p->pSat = sat_solver_new();
+        p->pSat->factors = ABC_CALLOC( double, 1 );
         p->nSatVars = 1;
         sat_solver_setnvars( p->pSat, 1000 );
         // var 0 is reserved for const1 node - add the clause
diff --git a/src/aig/saig/saigConstr2.c b/src/aig/saig/saigConstr2.c
index 6665d9f1..7f2eab6a 100644
--- a/src/aig/saig/saigConstr2.c
+++ b/src/aig/saig/saigConstr2.c
@@ -596,7 +596,8 @@ Vec_Vec_t * Ssw_ManFindDirectImplications( Aig_Man_t * p, int nFrames, int nConf
                 pReprR = Aig_Regular(pRepr);
                 if ( pCnf->pVarNums[Aig_ObjId(pReprR)] < 0 )
                     continue;
-                value = pSat->assigns[ pCnf->pVarNums[Aig_ObjId(pReprR)] ];
+//                value = pSat->assigns[ pCnf->pVarNums[Aig_ObjId(pReprR)] ];
+                value = sat_solver_get_var_value( pSat, pCnf->pVarNums[Aig_ObjId(pReprR)] );
                 if ( value == l_Undef )
                     continue;
                 // label this node as taken
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 4d851d0f..5a05e3b0 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -29,7 +29,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 ABC_NAMESPACE_IMPL_START
 
-//#define SAT_USE_SYSTEM_MEMORY_MANAGEMENT
 #define SAT_USE_ANALYZE_FINAL
 
 //=================================================================================================
@@ -77,6 +76,62 @@ static inline int irand(double* seed, int size) {
 static void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *));
 
 //=================================================================================================
+// Variable datatype + minor functions:
+
+static const int var0  = 1;
+static const int var1  = 0;
+static const int varX  = 3;
+
+struct varinfo_t
+{
+    unsigned val    :  2;  // variable value 
+    unsigned pol    :  1;  // last polarity
+    unsigned tag    :  1;  // conflict analysis tag
+    unsigned lev    : 28;  // variable level
+};
+
+static inline int     var_level     (sat_solver* s, int v)            { return s->levels[v]; }
+static inline int     var_value     (sat_solver* s, int v)            { return s->assigns[v]; }
+static inline int     var_polar     (sat_solver* s, int v)            { return s->polarity[v]; }
+
+static inline void    var_set_level (sat_solver* s, int v, int lev)   { s->levels[v] = lev;  }
+static inline void    var_set_value (sat_solver* s, int v, int val)   { s->assigns[v] = val;  }
+static inline void    var_set_polar (sat_solver* s, int v, int pol)   { s->polarity[v] = pol;  }
+
+// variable tags
+static inline int     var_tag       (sat_solver* s, int v)            { return s->tags[v]; }
+static inline void    var_set_tag   (sat_solver* s, int v, int tag)   { 
+    assert( tag > 0 && tag < 16 );
+    if ( s->tags[v] == 0 )
+        veci_push( &s->tagged, v );
+    s->tags[v] = tag;                           
+}
+static inline void    var_add_tag   (sat_solver* s, int v, int tag)   { 
+    assert( tag > 0 && tag < 16 );
+    if ( s->tags[v] == 0 )
+        veci_push( &s->tagged, v );
+    s->tags[v] |= tag;                           
+}
+static inline void    solver2_clear_tags(sat_solver* s, int start)    { 
+    int i, * tagged = veci_begin(&s->tagged);
+    for (i = start; i < veci_size(&s->tagged); i++)
+        s->tags[tagged[i]] = 0;
+    veci_resize(&s->tagged,start);
+}
+
+int sat_solver_get_var_value(sat_solver* s, int v)
+{
+    if ( var_value(s, v) == var0 )
+        return l_False;
+    if ( var_value(s, v) == var1 )
+        return l_True;
+    if ( var_value(s, v) == varX )
+        return l_Undef;
+    assert( 0 );
+    return 0;
+}
+
+//=================================================================================================
 // Clause datatype + minor functions:
 
 struct clause_t
@@ -85,7 +140,7 @@ struct clause_t
     lit lits[0];
 };
 
-static inline int      clause_size         (clause* c)             { return c->size_learnt >> 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]);    }
@@ -95,23 +150,26 @@ static inline void     clause_setactivity2 (clause* c, unsigned a) { *((unsigned
 static inline void     clause_print        (clause* c)             { 
     int i;
     printf( "{ " );
-    for ( i = 0; i < clause_size(c); i++ )
+    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" );
 }
 
+static inline clause* clause_read( sat_solver* s, int h )          { return (clause *)Vec_RecEntryP(&s->Mem, h);       }
+static inline int     clause_size( int nLits, int fLearnt )        { int a = nLits + fLearnt + 1; return a + (a & 1);  }
+
 //=================================================================================================
 // Encode literals in clause pointers:
 
-static inline clause* clause_from_lit (lit l)     { return (clause*)((ABC_PTRUINT_T)l + (ABC_PTRUINT_T)l + 1);  }
-static inline int     clause_is_lit   (clause* c) { return ((ABC_PTRUINT_T)c & 1);                              }
-static inline lit     clause_read_lit (clause* c) { return (lit)((ABC_PTRUINT_T)c >> 1);                        }
+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:
 
 static inline int     sat_solver_dl(sat_solver* s)                { return veci_size(&s->trail_lim); }
-static inline vecp*   sat_solver_read_wlist(sat_solver* s, lit l) { return &s->wlists[l];            }
+static inline veci*   sat_solver_read_wlist(sat_solver* s, lit l) { return &s->wlists[l];            }
 
 //=================================================================================================
 // Variable order functions:
@@ -153,49 +211,31 @@ static inline void order_unassigned(sat_solver* s, int v) // undoorder
 
 static inline int  order_select(sat_solver* s, float random_var_freq) // selectvar
 {
-    int*    heap;
-    int*    orderpos;
-
-    lbool* values = s->assigns;
-
+    int*      heap     = veci_begin(&s->order);
+    int*      orderpos = s->orderpos;
     // 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;
     }
-
     // Activity based decision:
-
-    heap     = veci_begin(&s->order);
-    orderpos = s->orderpos;
-
-
     while (veci_size(&s->order) > 0){
         int    next  = heap[0];
         int    size  = veci_size(&s->order)-1;
         int    x     = heap[size];
-
         veci_resize(&s->order,size);
-
         orderpos[next] = -1;
-
         if (size > 0){
-
             int    i     = 0;
             int    child = 1;
-
-
             while (child < size){
                 if (child+1 < size && s->activity[heap[child]] < s->activity[heap[child+1]])
                     child++;
-
                 assert(child < size);
-
                 if (s->activity[x] >= s->activity[heap[child]])
                     break;
-
                 heap[i]           = heap[child];
                 orderpos[heap[i]] = i;
                 i                 = child;
@@ -204,12 +244,9 @@ static inline int  order_select(sat_solver* s, float random_var_freq) // selectv
             heap[i]           = x;
             orderpos[heap[i]] = i;
         }
-
-//printf( "-%d ", next );
-        if (values[next] == l_Undef)
+        if (var_value(s, next) == varX)
             return next;
     }
-
     return var_Undef;
 }
 
@@ -227,9 +264,9 @@ static inline void act_var_rescale(sat_solver* s)  {
 }
 static inline void act_clause_rescale(sat_solver* s) {
     static int Total = 0;
-    clause** cs = (clause**)vecp_begin(&s->learnts);
+    clause** cs = (clause**)veci_begin(&s->learnts);
     int i, clk = clock();
-    for (i = 0; i < vecp_size(&s->learnts); i++){
+    for (i = 0; i < veci_size(&s->learnts); i++){
         float a = clause_activity(cs[i]);
         clause_setactivity(cs[i], a * (float)1e-20);
     }
@@ -247,6 +284,8 @@ static inline void act_var_bump(sat_solver* s, int v) {
         order_update(s,v);
 }
 static inline void act_var_bump_global(sat_solver* s, int v) {
+    if ( !s->pGlobalVars )
+        return;
     s->activity[v] += (s->var_inc * 3.0 * s->pGlobalVars[v]);
     if (s->activity[v] > 1e100)
         act_var_rescale(s);
@@ -254,6 +293,8 @@ static inline void act_var_bump_global(sat_solver* s, int v) {
         order_update(s,v);
 }
 static inline void act_var_bump_factor(sat_solver* s, int v) {
+    if ( !s->factors )
+        return;
     s->activity[v] += (s->var_inc * s->factors[v]);
     if (s->activity[v] > 1e100)
         act_var_rescale(s);
@@ -278,6 +319,7 @@ 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);
@@ -293,6 +335,7 @@ static inline void act_clause_rescale(sat_solver* s) {
 //    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)
@@ -300,30 +343,100 @@ static inline void act_var_bump(sat_solver* s, int v) {
     if (s->orderpos[v] != -1)
         order_update(s,v);
 }
-static inline void act_var_bump_global(sat_solver* s, int v) {}
-static inline void act_var_bump_factor(sat_solver* s, int v) {}
+static inline void act_var_bump_global(sat_solver* s, int v) {
+    if ( !s->pGlobalVars )
+        return;
+    s->activity[v] += (int)(s->var_inc * 3 * s->pGlobalVars[v]);
+    if (s->activity[v] & 0x80000000)
+        act_var_rescale(s);
+    if (s->orderpos[v] != -1)
+        order_update(s,v);
+}
+static inline void act_var_bump_factor(sat_solver* s, int v) {
+    if ( !s->factors )
+        return;
+    s->activity[v] += (int)(s->var_inc * s->factors[v]);
+    if (s->activity[v] & 0x80000000)
+        act_var_rescale(s);
+    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) 
         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
 
 
 //=================================================================================================
+// 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_solver_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);
+}
+
+//=================================================================================================
 // Clause functions:
 
 /* pre: size > 1 && no variable occurs twice
  */
-static clause* clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt)
+static int clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt)
 {
     int size;
     clause* c;
-    int i;
+    int h, i;
 
     assert(end - begin > 1);
     assert(learnt >= 0 && learnt < 2);
@@ -332,23 +445,20 @@ static clause* clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt
     // do not allocate memory for the two-literal problem clause
     if ( size == 2 && !learnt )
     {
-        vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)(clause_from_lit(begin[1])));
-        vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)(clause_from_lit(begin[0])));
-        return NULL;
+        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])));
+        return 0;
     }
 
-#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
-    c = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
-#else
-    c = (clause*)Sat_MmStepEntryFetch( s->pMem, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float) );
-#endif
-
+    // create new clause
+    h = Vec_RecAppend( &s->Mem, clause_size(size, learnt) );
+    c = clause_read( s, h );
+    assert( !(h & 1) );
+    if ( s->hLearnts == -1 && learnt )
+        s->hLearnts = h;
     c->size_learnt = (size << 1) | learnt;
-    assert(((ABC_PTRUINT_T)c & 1) == 0);
-
     for (i = 0; i < size; i++)
         c->lits[i] = begin[i];
-
     if (learnt)
         *((float*)&c->lits[size]) = 0.0;
 
@@ -360,44 +470,35 @@ static clause* clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt
     assert(lit_neg(begin[0]) < s->size*2);
     assert(lit_neg(begin[1]) < s->size*2);
 
-    //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)c);
-    //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)c);
-
-    vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)(size > 2 ? c : clause_from_lit(begin[1])));
-    vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)(size > 2 ? c : clause_from_lit(begin[0])));
+    //veci_push(sat_solver_read_wlist(s,lit_neg(begin[0])),c);
+    //veci_push(sat_solver_read_wlist(s,lit_neg(begin[1])),c);
+    veci_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(size > 2 ? h : clause_from_lit(begin[1])));
+    veci_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(size > 2 ? h : clause_from_lit(begin[0])));
 
-    return c;
+    return h;
 }
 
 
 //=================================================================================================
 // Minor (solver) functions:
 
-static inline int sat_solver_enqueue(sat_solver* s, lit l, clause* from)
+static inline int sat_solver_enqueue(sat_solver* s, lit l, int from)
 {
-    lbool* values = s->assigns;
-    int    v      = lit_var(l);
-    lbool  val    = values[v];
-    lbool  sig;
+    int v  = lit_var(l);
 #ifdef VERBOSEDEBUG
     printf(L_IND"enqueue("L_LIT")\n", L_ind, L_lit(l));
 #endif
-
-    sig = !lit_sign(l); sig += sig - 1;
-    if (val != l_Undef){
-        return val == sig;
-    }else{
-        int*     levels  = s->levels;
-        clause** reasons = s->reasons;
+    if (var_value(s, v) != varX)
+        return var_value(s, v) == lit_sign(l);
+    else{
         // New fact -- store it.
 #ifdef VERBOSEDEBUG
         printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(l));
 #endif
-        values [v] = sig;
-        levels [v] = sat_solver_dl(s);
-        reasons[v] = from;
+        var_set_value(s, v, lit_sign(l));
+        var_set_level(s, v, sat_solver_dl(s));
+        s->reasons[v] = from;
         s->trail[s->qtail++] = l;
-
         order_assigned(s, v);
         return true;
     }
@@ -406,20 +507,17 @@ static inline int sat_solver_enqueue(sat_solver* s, lit l, clause* from)
 
 static inline int sat_solver_assume(sat_solver* s, lit l){
     assert(s->qtail == s->qhead);
-    assert(s->assigns[lit_var(l)] == l_Undef);
+    assert(var_value(s, lit_var(l)) == varX);
 #ifdef VERBOSEDEBUG
     printf(L_IND"assume("L_LIT")  ", L_ind, L_lit(l));
     printf( "act = %.20f\n", s->activity[lit_var(l)] );
 #endif
     veci_push(&s->trail_lim,s->qtail);
-    return sat_solver_enqueue(s,l,(clause*)0);
+    return sat_solver_enqueue(s,l,0);
 }
 
 
 static void sat_solver_canceluntil(sat_solver* s, int level) {
-    lit*     trail;   
-    lbool*   values;  
-    clause** reasons; 
     int      bound;
     int      lastLev;
     int      c;
@@ -427,9 +525,6 @@ static void sat_solver_canceluntil(sat_solver* s, int level) {
     if (sat_solver_dl(s) <= level)
         return;
 
-    trail   = s->trail;
-    values  = s->assigns;
-    reasons = s->reasons;
     bound   = (veci_begin(&s->trail_lim))[level];
     lastLev = (veci_begin(&s->trail_lim))[veci_size(&s->trail_lim)-1];
 
@@ -440,15 +535,15 @@ static void sat_solver_canceluntil(sat_solver* s, int level) {
     ////////////////////////////////////////
 
     for (c = s->qtail-1; c >= bound; c--) {
-        int     x  = lit_var(trail[c]);
-        values [x] = l_Undef;
-        reasons[x] = (clause*)0;
+        int     x  = lit_var(s->trail[c]);
+        var_set_value(s, x, varX);
+        s->reasons[x] = 0;
         if ( c < lastLev )
-            s->polarity[x] = !lit_sign(trail[c]);
+            var_set_polar( s, x, !lit_sign(s->trail[c]) );
     }
 
     for (c = s->qhead-1; c >= bound; c--)
-        order_unassigned(s,lit_var(trail[c]));
+        order_unassigned(s,lit_var(s->trail[c]));
 
     s->qhead = s->qtail = bound;
     veci_resize(&s->trail_lim,level);
@@ -458,8 +553,8 @@ static void sat_solver_record(sat_solver* s, veci* cls)
 {
     lit*    begin = veci_begin(cls);
     lit*    end   = begin + veci_size(cls);
-    clause* c     = (veci_size(cls) > 1) ? clause_create_new(s,begin,end,1) : (clause*)0;
-    sat_solver_enqueue(s,*begin,c);
+    int     h     = (veci_size(cls) > 1) ? clause_create_new(s,begin,end,1) : 0;
+    sat_solver_enqueue(s,*begin,h);
 
     ///////////////////////////////////
     // add clause to internal storage
@@ -472,9 +567,9 @@ static void sat_solver_record(sat_solver* s, veci* cls)
 
     assert(veci_size(cls) > 0);
 
-    if (c != 0) {
-        vecp_push(&s->learnts,c);
-        act_clause_bump(s,c);
+    if (h != 0) {
+//        veci_push(&s->learnts,c);
+//        act_clause_bump(s,c);
         s->stats.learnts++;
         s->stats.learnts_literals += veci_size(cls);
     }
@@ -483,82 +578,59 @@ static void sat_solver_record(sat_solver* s, veci* cls)
 
 static double sat_solver_progress(sat_solver* s)
 {
-    lbool*  values = s->assigns;
-    int*    levels = s->levels;
     int     i;
-
     double  progress = 0;
     double  F        = 1.0 / s->size;
     for (i = 0; i < s->size; i++)
-        if (values[i] != l_Undef)
-            progress += pow(F, levels[i]);
+        if (var_value(s, i) != varX)
+            progress += pow(F, var_level(s, i));
     return progress / s->size;
 }
 
 //=================================================================================================
 // Major methods:
 
-static int sat_solver_lit_removable(sat_solver* s, lit l, int minl)
+static int sat_solver_lit_removable(sat_solver* s, int x, int minl)
 {
-    lbool*   tags    = s->tags;
-    clause** reasons = s->reasons;
-    int*     levels  = s->levels;
     int      top     = veci_size(&s->tagged);
 
-    assert(lit_var(l) >= 0 && lit_var(l) < s->size);
-    assert(reasons[lit_var(l)] != 0);
+    assert(s->reasons[x] != 0);
     veci_resize(&s->stack,0);
-    veci_push(&s->stack,lit_var(l));
-
-    while (veci_size(&s->stack) > 0){
-        clause* c;
-        int 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(reasons[v] != 0);
-        c    = reasons[v];
-
-        if (clause_is_lit(c)){
-            int v = lit_var(clause_read_lit(c));
-            if (tags[v] == l_Undef && levels[v] != 0){
-                if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){
+    veci_push(&s->stack,x);
+
+    while (veci_size(&s->stack)){
+        int v = veci_pop(&s->stack);
+        assert(s->reasons[v] != 0);
+        if (clause_is_lit(s->reasons[v])){
+            v = lit_var(clause_read_lit(s->reasons[v]));
+            if (!var_tag(s,v) && var_level(s, v)){
+                if (s->reasons[v] != 0 && ((1 << (var_level(s, v) & 31)) & minl)){
                     veci_push(&s->stack,v);
-                    tags[v] = l_True;
-                    veci_push(&s->tagged,v);
+                    var_set_tag(s, v, 1);
                 }else{
-                    int* tagged = veci_begin(&s->tagged);
-                    int j;
-                    for (j = top; j < veci_size(&s->tagged); j++)
-                        tags[tagged[j]] = l_Undef;
-                    veci_resize(&s->tagged,top);
-                    return false;
+                    solver2_clear_tags(s, top);
+                    return 0;
                 }
             }
         }else{
-            lit*    lits = clause_begin(c);
-            int     i, j;
-
-            for (i = 1; i < clause_size(c); i++){
+            clause* c = clause_read(s, s->reasons[v]);
+            lit* lits = clause_begin(c);
+            int  i;
+            for (i = 1; i < clause_nlits(c); i++){
                 int v = lit_var(lits[i]);
-                if (tags[v] == l_Undef && levels[v] != 0){
-                    if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){
-
+                if (!var_tag(s,v) && var_level(s, v)){
+                    if (s->reasons[v] != 0 && ((1 << (var_level(s, v) & 31)) & minl)){
                         veci_push(&s->stack,lit_var(lits[i]));
-                        tags[v] = l_True;
-                        veci_push(&s->tagged,v);
+                        var_set_tag(s, v, 1);
                     }else{
-                        int* tagged = veci_begin(&s->tagged);
-                        for (j = top; j < veci_size(&s->tagged); j++)
-                            tags[tagged[j]] = l_Undef;
-                        veci_resize(&s->tagged,top);
-                        return false;
+                        solver2_clear_tags(s, top);
+                        return 0;
                     }
                 }
             }
         }
     }
-
-    return true;
+    return 1;
 }
 
 
@@ -613,8 +685,9 @@ void Solver::analyzeFinal(Clause* confl, bool skip_first)
 
 #ifdef SAT_USE_ANALYZE_FINAL
 
-static void sat_solver_analyze_final(sat_solver* s, clause* conf, int skip_first)
+static void sat_solver_analyze_final(sat_solver* s, int hConf, int skip_first)
 {
+    clause* conf = clause_read(s, hConf);
     int i, j, start;
     veci_resize(&s->conf_final,0);
     if ( s->root_level == 0 )
@@ -622,110 +695,87 @@ static void sat_solver_analyze_final(sat_solver* s, clause* conf, 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_size(conf); i++)
+    for (i = skip_first ? 1 : 0; i < clause_nlits(conf); i++)
     {
         int x = lit_var(clause_begin(conf)[i]);
-        if (s->levels[x] > 0)
-        {
-            s->tags[x] = l_True;
-            veci_push(&s->tagged,x);
-        }
+        if (var_level(s, x) > 0)
+            var_set_tag(s, x, 1);
     }
 
     start = (s->root_level >= veci_size(&s->trail_lim))? s->qtail-1 : (veci_begin(&s->trail_lim))[s->root_level];
     for (i = start; i >= (veci_begin(&s->trail_lim))[0]; i--){
         int x = lit_var(s->trail[i]);
-        if (s->tags[x] == l_True){
-            if (s->reasons[x] == NULL){
-                assert(s->levels[x] > 0);
+        if (var_tag(s,x)){
+            if (s->reasons[x] == 0){
+                assert(var_level(s, x) > 0);
                 veci_push(&s->conf_final,lit_neg(s->trail[i]));
             }else{
-                clause* c = s->reasons[x];
-                if (clause_is_lit(c)){
-                    lit q = clause_read_lit(c);
+                if (clause_is_lit(s->reasons[x])){
+                    lit q = clause_read_lit(s->reasons[x]);
                     assert(lit_var(q) >= 0 && lit_var(q) < s->size);
-                    if (s->levels[lit_var(q)] > 0)
-                    {
-                        s->tags[lit_var(q)] = l_True;
-                        veci_push(&s->tagged,lit_var(q));
-                    }
+                    if (var_level(s, lit_var(q)) > 0)
+                        var_set_tag(s, lit_var(q), 1);
                 }
                 else{
+                    clause* c = clause_read(s, s->reasons[x]);
                     int* lits = clause_begin(c);
-                    for (j = 1; j < clause_size(c); j++)
-                        if (s->levels[lit_var(lits[j])] > 0)
-                        {
-                            s->tags[lit_var(lits[j])] = l_True;
-                            veci_push(&s->tagged,lit_var(lits[j]));
-                        }
+                    for (j = 1; j < clause_nlits(c); j++)
+                        if (var_level(s, lit_var(lits[j])) > 0)
+                            var_set_tag(s, lit_var(lits[j]), 1);
                 }
             }
         }
     }
-    for (i = 0; i < veci_size(&s->tagged); i++)
-        s->tags[veci_begin(&s->tagged)[i]] = l_Undef;
-    veci_resize(&s->tagged,0);
+    solver2_clear_tags(s,0);
 }
 
 #endif
 
 
-static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt)
+static void sat_solver_analyze(sat_solver* s, int h, veci* learnt)
 {
     lit*     trail   = s->trail;
-    lbool*   tags    = s->tags;
-    clause** reasons = s->reasons;
-    int*     levels  = s->levels;
     int      cnt     = 0;
     lit      p       = lit_Undef;
     int      ind     = s->qtail-1;
     lit*     lits;
     int      i, j, minl;
-    int*     tagged;
-
     veci_push(learnt,lit_Undef);
-
     do{
-        assert(c != 0);
-
-        if (clause_is_lit(c)){
-            lit q = clause_read_lit(c);
-            assert(lit_var(q) >= 0 && lit_var(q) < s->size);
-            if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){
-                tags[lit_var(q)] = l_True;
-                veci_push(&s->tagged,lit_var(q));
-                act_var_bump(s,lit_var(q));
-                if (levels[lit_var(q)] == sat_solver_dl(s))
+        assert(h != 0);
+        if (clause_is_lit(h)){
+            int x = lit_var(clause_read_lit(h));
+            if (var_tag(s, x) == 0 && var_level(s, x) > 0){
+                var_set_tag(s, x, 1);
+                act_var_bump(s,x);
+                if (var_level(s, x) == sat_solver_dl(s))
                     cnt++;
                 else
-                    veci_push(learnt,q);
+                    veci_push(learnt,clause_read_lit(h));
             }
         }else{
-
-            if (clause_learnt(c))
-                act_clause_bump(s,c);
-
+            clause* c = clause_read(s, h);
+//            if (clause_learnt(c))
+//                act_clause_bump(s,c);
             lits = clause_begin(c);
-            //printlits(lits,lits+clause_size(c)); printf("\n");
-            for (j = (p == lit_Undef ? 0 : 1); j < clause_size(c); j++){
-                lit q = lits[j];
-                assert(lit_var(q) >= 0 && lit_var(q) < s->size);
-                if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){
-                    tags[lit_var(q)] = l_True;
-                    veci_push(&s->tagged,lit_var(q));
-                    act_var_bump(s,lit_var(q));
-                    if (levels[lit_var(q)] == sat_solver_dl(s))
+            //printlits(lits,lits+clause_nlits(c)); printf("\n");
+            for (j = (p == lit_Undef ? 0 : 1); j < clause_nlits(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);
+                    if (var_level(s,x) == sat_solver_dl(s))
                         cnt++;
                     else
-                        veci_push(learnt,q);
+                        veci_push(learnt,lits[j]);
                 }
             }
         }
 
-        while (tags[lit_var(trail[ind--])] == l_Undef);
+        while ( !var_tag(s, lit_var(trail[ind--])) );
 
         p = trail[ind+1];
-        c = reasons[lit_var(p)];
+        h = s->reasons[lit_var(p)];
         cnt--;
 
     }while (cnt > 0);
@@ -735,13 +785,13 @@ static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt)
     lits = veci_begin(learnt);
     minl = 0;
     for (i = 1; i < veci_size(learnt); i++){
-        int lev = levels[lit_var(lits[i])];
+        int lev = var_level(s, lit_var(lits[i]));
         minl    |= 1 << (lev & 31);
     }
 
     // simplify (full)
     for (i = j = 1; i < veci_size(learnt); i++){
-        if (reasons[lit_var(lits[i])] == 0 || !sat_solver_lit_removable(s,lits[i],minl))
+        if (s->reasons[lit_var(lits[i])] == 0 || !sat_solver_lit_removable(s,lit_var(lits[i]),minl))
             lits[j++] = lits[i];
     }
 
@@ -750,14 +800,11 @@ static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt)
     s->stats.tot_literals += j;
 
     // clear tags
-    tagged = veci_begin(&s->tagged);
-    for (i = 0; i < veci_size(&s->tagged); i++)
-        tags[tagged[i]] = l_Undef;
-    veci_resize(&s->tagged,0);
+    solver2_clear_tags(s,0);
 
 #ifdef DEBUG
     for (i = 0; i < s->size; i++)
-        assert(tags[i] == l_Undef);
+        assert(!var_tag(s, i));
 #endif
 
 #ifdef VERBOSEDEBUG
@@ -766,12 +813,12 @@ static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt)
 #endif
     if (veci_size(learnt) > 1){
         int max_i = 1;
-        int max   = levels[lit_var(lits[1])];
+        int max   = var_level(s, lit_var(lits[1]));
         lit tmp;
 
         for (i = 2; i < veci_size(learnt); i++)
-            if (levels[lit_var(lits[i])] > max){
-                max   = levels[lit_var(lits[i])];
+            if (var_level(s, lit_var(lits[i])) > max){
+                max   = var_level(s, lit_var(lits[i]));
                 max_i = i;
             }
 
@@ -781,28 +828,26 @@ static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt)
     }
 #ifdef VERBOSEDEBUG
     {
-        int lev = veci_size(learnt) > 1 ? levels[lit_var(lits[1])] : 0;
+        int lev = veci_size(learnt) > 1 ? var_level(s, lit_var(lits[1])) : 0;
         printf(" } at level %d\n", lev);
     }
 #endif
 }
 
 
-clause* sat_solver_propagate(sat_solver* s)
+int sat_solver_propagate(sat_solver* s)
 {
-    lbool*  values = s->assigns;
-    clause* confl  = (clause*)0;
+    int     hConfl = 0;
     lit*    lits;
     lit false_lit;
-    lbool sig;
 
     //printf("sat_solver_propagate\n");
-    while (confl == 0 && s->qtail - s->qhead > 0){
-        lit  p  = s->trail[s->qhead++];
-        vecp* ws = sat_solver_read_wlist(s,p);
-        clause **begin = (clause**)vecp_begin(ws);
-        clause **end   = begin + vecp_size(ws);
-        clause **i, **j;
+    while (hConfl == 0 && s->qtail - s->qhead > 0){
+        lit   p     = s->trail[s->qhead++];
+        veci* ws    = sat_solver_read_wlist(s,p);
+        int*  begin = veci_begin(ws);
+        int*  end   = begin + veci_size(ws);
+        int*i, *j;
 
         s->stats.propagations++;
         s->simpdb_props--;
@@ -812,24 +857,24 @@ clause* sat_solver_propagate(sat_solver* s)
             if (clause_is_lit(*i)){
 
                 int Lit = clause_read_lit(*i);
-                sig = !lit_sign(Lit); sig += sig - 1;
-                if (values[lit_var(Lit)] == sig){
+                if (var_value(s, lit_var(Lit)) == lit_sign(Lit)){
                     *j++ = *i++;
                     continue;
                 }
 
                 *j++ = *i;
                 if (!sat_solver_enqueue(s,clause_read_lit(*i),clause_from_lit(p))){
-                    confl = s->binary;
-                    (clause_begin(confl))[1] = lit_neg(p);
-                    (clause_begin(confl))[0] = clause_read_lit(*i++);
+                    hConfl = s->hBinary;
+                    (clause_begin(s->binary))[1] = lit_neg(p);
+                    (clause_begin(s->binary))[0] = clause_read_lit(*i++);
                     // Copy the remaining watches:
                     while (i < end)
                         *j++ = *i++;
                 }
             }else{
 
-                lits = clause_begin(*i);
+                clause* c = clause_read(s,*i);
+                lits = clause_begin(c);
 
                 // Make sure the false literal is data[1]:
                 false_lit = lit_neg(p);
@@ -838,29 +883,26 @@ clause* sat_solver_propagate(sat_solver* s)
                     lits[1] = false_lit;
                 }
                 assert(lits[1] == false_lit);
-                //printf("checking clause: "); printlits(lits, lits+clause_size(*i)); printf("\n");
 
                 // If 0th watch is true, then clause is already satisfied.
-                sig = !lit_sign(lits[0]); sig += sig - 1;
-                if (values[lit_var(lits[0])] == sig){
+                if (var_value(s, lit_var(lits[0])) == lit_sign(lits[0]))
                     *j++ = *i;
-                }else{
+                else{
                     // Look for new watch:
-                    lit* stop = lits + clause_size(*i);
+                    lit* stop = lits + clause_nlits(c);
                     lit* k;
                     for (k = lits + 2; k < stop; k++){
-                        lbool sig = lit_sign(*k); sig += sig - 1;
-                        if (values[lit_var(*k)] != sig){
+                        if (var_value(s, lit_var(*k)) != !lit_sign(*k)){
                             lits[1] = *k;
                             *k = false_lit;
-                            vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i);
+                            veci_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i);
                             goto next; }
                     }
 
                     *j++ = *i;
                     // Clause is unit under assignment:
                     if (!sat_solver_enqueue(s,lits[0], *i)){
-                        confl = *i++;
+                        hConfl = *i++;
                         // Copy the remaining watches:
                         while (i < end)
                             *j++ = *i++;
@@ -871,11 +913,11 @@ clause* sat_solver_propagate(sat_solver* s)
             i++;
         }
 
-        s->stats.inspects += j - (clause**)vecp_begin(ws);
-        vecp_resize(ws,j - (clause**)vecp_begin(ws));
+        s->stats.inspects += j - veci_begin(ws);
+        veci_resize(ws,j - veci_begin(ws));
     }
 
-    return confl;
+    return hConfl;
 }
 
 //=================================================================================================
@@ -883,12 +925,15 @@ clause* sat_solver_propagate(sat_solver* s)
 
 sat_solver* sat_solver_new(void)
 {
-    sat_solver* s = (sat_solver*)ABC_ALLOC( char, sizeof(sat_solver));
-    memset( s, 0, sizeof(sat_solver) );
+    sat_solver* s = (sat_solver*)ABC_CALLOC( char, sizeof(sat_solver));
+
+    Vec_RecAlloc_(&s->Mem);
+    s->hLearnts = -1;
+    s->hBinary = Vec_RecAppend( &s->Mem, clause_size(2, 0) );
+    s->binary = clause_read( s, s->hBinary );
+    s->binary->size_learnt = (2 << 1);
 
     // initialize vectors
-    vecp_new(&s->clauses);
-    vecp_new(&s->learnts);
     veci_new(&s->order);
     veci_new(&s->trail_lim);
     veci_new(&s->tagged);
@@ -901,15 +946,10 @@ sat_solver* sat_solver_new(void)
     // initialize arrays
     s->wlists    = 0;
     s->activity  = 0;
-    s->factors   = 0;
-    s->assigns   = 0;
     s->orderpos  = 0;
     s->reasons   = 0;
-    s->levels    = 0;
-    s->tags      = 0;
     s->trail     = 0;
 
-
     // initialize other vars
     s->size                   = 0;
     s->cap                    = 0;
@@ -929,8 +969,8 @@ sat_solver* sat_solver_new(void)
     s->simpdb_props           = 0;
     s->random_seed            = 91648253;
     s->progress_estimate      = 0;
-    s->binary                 = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit)*2);
-    s->binary->size_learnt    = (2 << 1);
+//    s->binary                 = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit)*2);
+//    s->binary->size_learnt    = (2 << 1);
     s->verbosity              = 0;
 
     s->stats.starts           = 0;
@@ -943,12 +983,6 @@ sat_solver* sat_solver_new(void)
     s->stats.learnts          = 0;
     s->stats.learnts_literals = 0;
     s->stats.tot_literals     = 0;
-
-#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
-    s->pMem = NULL;
-#else
-    s->pMem = Sat_MmStepStart( 10 );
-#endif
     return s;
 }
 
@@ -960,42 +994,46 @@ void sat_solver_setnvars(sat_solver* s,int n)
         int old_cap = s->cap;
         while (s->cap < n) s->cap = s->cap*2+1;
 
-        s->wlists    = ABC_REALLOC(vecp,   s->wlists,   s->cap*2);
+        s->wlists    = ABC_REALLOC(veci,   s->wlists,   s->cap*2);
+//        s->vi        = ABC_REALLOC(varinfo,s->vi,       s->cap);
+        s->levels    = ABC_REALLOC(int,    s->levels,   s->cap);
+        s->assigns   = ABC_REALLOC(char,   s->assigns,  s->cap);
+        s->polarity  = ABC_REALLOC(char,   s->polarity, s->cap);
+        s->tags      = ABC_REALLOC(char,   s->tags,     s->cap);
 #ifdef USE_FLOAT_ACTIVITY
         s->activity  = ABC_REALLOC(double,   s->activity, s->cap);
 #else
         s->activity  = ABC_REALLOC(unsigned, s->activity, s->cap);
 #endif
+        if ( s->factors )
         s->factors   = ABC_REALLOC(double, s->factors,  s->cap);
-        s->assigns   = ABC_REALLOC(lbool,  s->assigns,  s->cap);
         s->orderpos  = ABC_REALLOC(int,    s->orderpos, s->cap);
-        s->reasons   = ABC_REALLOC(clause*,s->reasons,  s->cap);
-        s->levels    = ABC_REALLOC(int,    s->levels,   s->cap);
-        s->tags      = ABC_REALLOC(lbool,  s->tags,     s->cap);
+        s->reasons   = ABC_REALLOC(int,    s->reasons,  s->cap);
         s->trail     = ABC_REALLOC(lit,    s->trail,    s->cap);
-        s->polarity  = ABC_REALLOC(char,   s->polarity, s->cap);
-        memset( s->wlists + 2*old_cap, 0, 2*(s->cap-old_cap)*sizeof(vecp) );
-    }
+        memset( s->wlists + 2*old_cap, 0, 2*(s->cap-old_cap)*sizeof(veci) );
+    } 
 
     for (var = s->size; var < n; var++){
         assert(!s->wlists[2*var].size);
         assert(!s->wlists[2*var+1].size);
         if ( s->wlists[2*var].ptr == NULL )
-            vecp_new(&s->wlists[2*var]);
+            veci_new(&s->wlists[2*var]);
         if ( s->wlists[2*var+1].ptr == NULL )
-            vecp_new(&s->wlists[2*var+1]);
+            veci_new(&s->wlists[2*var+1]);
 #ifdef USE_FLOAT_ACTIVITY
         s->activity[var] = 0;
 #else
         s->activity[var] = (1<<10);
 #endif
-        s->factors  [var] = 0;
-        s->assigns  [var] = l_Undef;
-        s->orderpos [var] = veci_size(&s->order);
-        s->reasons  [var] = (clause*)0;
-        s->levels   [var] = 0;
-        s->tags     [var] = l_Undef;
-        s->polarity [var] = 0;
+        if ( s->factors )
+        s->factors [var] = 0;
+//        *((int*)s->vi + var) = 0; s->vi[var].val = varX;
+        s->levels  [var] = 0;
+        s->assigns [var] = varX;
+        s->polarity[var] = 0;
+        s->tags    [var] = 0;
+        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); 
@@ -1009,20 +1047,9 @@ void sat_solver_setnvars(sat_solver* s,int n)
 
 void sat_solver_delete(sat_solver* s)
 {
-
-#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
-    int i;
-    for (i = 0; i < vecp_size(&s->clauses); i++)
-        ABC_FREE(vecp_begin(&s->clauses)[i]);
-    for (i = 0; i < vecp_size(&s->learnts); i++)
-        ABC_FREE(vecp_begin(&s->learnts)[i]);
-#else
-    Sat_MmStepStop( s->pMem, 0 );
-#endif
+    Vec_RecFree_( &s->Mem );
 
     // delete vectors
-    vecp_delete(&s->clauses);
-    vecp_delete(&s->learnts);
     veci_delete(&s->order);
     veci_delete(&s->trail_lim);
     veci_delete(&s->tagged);
@@ -1031,23 +1058,23 @@ void sat_solver_delete(sat_solver* s)
     veci_delete(&s->act_vars);
     veci_delete(&s->temp_clause);
     veci_delete(&s->conf_final);
-    ABC_FREE(s->binary);
 
     // delete arrays
-    if (s->wlists != 0){
+    if (s->reasons != 0){
         int i;
         for (i = 0; i < s->cap*2; i++)
-            vecp_delete(&s->wlists[i]);
+            veci_delete(&s->wlists[i]);
         ABC_FREE(s->wlists   );
+//        ABC_FREE(s->vi       );
+        ABC_FREE(s->levels   );
+        ABC_FREE(s->assigns  );
+        ABC_FREE(s->polarity );
+        ABC_FREE(s->tags     );
         ABC_FREE(s->activity );
         ABC_FREE(s->factors  );
-        ABC_FREE(s->assigns  );
         ABC_FREE(s->orderpos );
         ABC_FREE(s->reasons  );
-        ABC_FREE(s->levels   );
         ABC_FREE(s->trail    );
-        ABC_FREE(s->tags     );
-        ABC_FREE(s->polarity );
     }
 
     sat_solver_store_free(s);
@@ -1057,16 +1084,13 @@ void sat_solver_delete(sat_solver* s)
 void sat_solver_rollback( sat_solver* s )
 {
     int i;
-#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
-    for (i = 0; i < vecp_size(&s->clauses); i++)
-        ABC_FREE(vecp_begin(&s->clauses)[i]);
-    for (i = 0; i < vecp_size(&s->learnts); i++)
-        ABC_FREE(vecp_begin(&s->learnts)[i]);
-#else
-    Sat_MmStepRestart( s->pMem );
-#endif
-    vecp_resize(&s->clauses, 0);
-    vecp_resize(&s->learnts, 0);
+    Vec_RecRestart( &s->Mem );
+
+    s->hLearnts = -1;
+    s->hBinary = Vec_RecAppend( &s->Mem, clause_size(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);
     for ( i = 0; i < s->size*2; i++ )
@@ -1105,56 +1129,49 @@ void sat_solver_rollback( sat_solver* s )
     s->stats.tot_literals     = 0;
 }
 
-
+/*
 static void clause_remove(sat_solver* s, clause* c)
 {
     lit* lits = clause_begin(c);
     assert(lit_neg(lits[0]) < s->size*2);
     assert(lit_neg(lits[1]) < s->size*2);
 
-    //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)c);
-    //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)c);
+    //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);
-    vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1])));
-    vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0])));
+    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_size(c);
+        s->stats.learnts_literals -= clause_nlits(c);
     }else{
         s->stats.clauses--;
-        s->stats.clauses_literals -= clause_size(c);
+        s->stats.clauses_literals -= clause_nlits(c);
     }
-
-#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
-    ABC_FREE(c);
-#else
-    Sat_MmStepEntryRecycle( s->pMem, (char *)c, sizeof(clause) + sizeof(lit) * clause_size(c) + clause_learnt(c) * sizeof(float) );
-#endif
 }
 
 static lbool clause_simplify(sat_solver* s, clause* c)
 {
     lit*   lits   = clause_begin(c);
-    lbool* values = s->assigns;
     int i;
 
     assert(sat_solver_dl(s) == 0);
 
-    for (i = 0; i < clause_size(c); i++){
+    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 (s->assignss[lit_var(lits[i])] == sig)
             return l_True;
     }
     return l_False;
 }
+*/
 
 int sat_solver_simplify(sat_solver* s)
 {
-    clause** reasons;
-    int type;
-
+//    clause** reasons;
+//    int type;
     assert(sat_solver_dl(s) == 0);
 
     if (sat_solver_propagate(s) != 0)
@@ -1162,7 +1179,7 @@ int sat_solver_simplify(sat_solver* s)
 
     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;
@@ -1178,53 +1195,48 @@ int sat_solver_simplify(sat_solver* s)
         }
         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;
 }
 
 
+/*
 static int clause_cmp (const void* x, const void* y) {
-    return clause_size((clause*)x) > 2 && (clause_size((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_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 / vecp_size(&s->learnts); // Remove any clause below this activity
-    clause** learnts = (clause**)vecp_begin(&s->learnts);
+    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(vecp_begin(&s->learnts), vecp_size(&s->learnts), &clause_cmp);
+    sat_solver_sort(veci_begin(&s->learnts), veci_size(&s->learnts), &clause_cmp);
 
-    for (i = j = 0; i < vecp_size(&s->learnts) / 2; i++){
-        if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i])
+    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];
     }
-    for (; i < vecp_size(&s->learnts); i++){
-        if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i] && clause_activity(learnts[i]) < extra_lim)
+    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];
     }
-
-    //printf("reducedb deleted %d\n", vecp_size(&s->learnts) - j);
-
-
-    vecp_resize(&s->learnts,j);
+    veci_resize(&s->learnts,j);
 }
+*/
 
 int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
 {
-    clause * c;
     lit *i,*j;
     int maxvar;
-    lbool* values;
     lit last;
+    assert( begin < end );
 
     veci_resize( &s->temp_clause, 0 );
     for ( i = begin; i < end; i++ )
@@ -1232,10 +1244,6 @@ int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
     begin = veci_begin( &s->temp_clause );
     end = begin + veci_size( &s->temp_clause );
 
-    if (begin == end) 
-        return false;
-
-    //printlits(begin,end); printf("\n");
     // insertion sort
     maxvar = lit_var(*begin);
     for (i = begin + 1; i < end; i++){
@@ -1246,7 +1254,6 @@ int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
         *j = l;
     }
     sat_solver_setnvars(s,maxvar+1);
-//    sat_solver_setnvars(s, lit_var(*(end-1))+1 );
 
     ///////////////////////////////////
     // add clause to internal storage
@@ -1257,17 +1264,13 @@ int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
     }
     ///////////////////////////////////
 
-    //printlits(begin,end); printf("\n");
-    values = s->assigns;
-
     // delete duplicates
     last = lit_Undef;
     for (i = j = begin; i < end; i++){
-        //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]));
-        lbool sig = !lit_sign(*i); sig += sig - 1;
-        if (*i == lit_neg(last) || sig == values[lit_var(*i)])
+        //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -s->assignss[lit_var(*i)] : s->assignss[lit_var(*i)]));
+        if (*i == lit_neg(last) || var_value(s, lit_var(*i)) == lit_sign(*i))
             return true;   // tautology
-        else if (*i != last && values[lit_var(*i)] == l_Undef)
+        else if (*i != last && var_value(s, lit_var(*i)) == varX)
             last = *j++ = *i;
     }
 //    j = i;
@@ -1276,17 +1279,13 @@ int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
         return false;
 
     if (j - begin == 1) // unit clause
-        return sat_solver_enqueue(s,*begin,(clause*)0);
+        return sat_solver_enqueue(s,*begin,0);
 
     // create new clause
-    c = clause_create_new(s,begin,j,0);
-    if ( c )
-        vecp_push(&s->clauses,c);
-
+    clause_create_new(s,begin,j,0);
 
     s->stats.clauses++;
     s->stats.clauses_literals += j - begin;
-
     return true;
 }
 
@@ -1313,7 +1312,6 @@ void luby_test()
 
 static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT64_T nof_learnts)
 {
-    int*    levels          = s->levels;
     double  var_decay       = 0.95;
     double  clause_decay    = 0.999;
     double  random_var_freq = s->fNotUseRandom ? 0.0 : 0.02;
@@ -1343,8 +1341,8 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT
             act_var_bump_global(s, s->act_vars.ptr[i]);
 
     for (;;){
-        clause* confl = sat_solver_propagate(s);
-        if (confl != 0){
+        int hConfl = sat_solver_propagate(s);
+        if (hConfl != 0){
             // CONFLICT
             int blevel;
 
@@ -1354,24 +1352,25 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT
             s->stats.conflicts++; conflictC++;
             if (sat_solver_dl(s) == s->root_level){
 #ifdef SAT_USE_ANALYZE_FINAL
-                sat_solver_analyze_final(s, confl, 0);
+                sat_solver_analyze_final(s, hConfl, 0);
 #endif
                 veci_delete(&learnt_clause);
                 return l_False;
             }
 
             veci_resize(&learnt_clause,0);
-            sat_solver_analyze(s, confl, &learnt_clause);
-            blevel = veci_size(&learnt_clause) > 1 ? levels[lit_var(veci_begin(&learnt_clause)[1])] : s->root_level;
+            sat_solver_analyze(s, hConfl, &learnt_clause);
+            blevel = veci_size(&learnt_clause) > 1 ? var_level(s, lit_var(veci_begin(&learnt_clause)[1])) : s->root_level;
             blevel = s->root_level > blevel ? s->root_level : blevel;
             sat_solver_canceluntil(s,blevel);
             sat_solver_record(s,&learnt_clause);
 #ifdef SAT_USE_ANALYZE_FINAL
 //            if (learnt_clause.size() == 1) level[var(learnt_clause[0])] = 0;    // (this is ugly (but needed for 'analyzeFinal()') -- in future versions, we will backtrack past the 'root_level' and redo the assumptions)
-            if ( learnt_clause.size == 1 ) s->levels[lit_var(learnt_clause.ptr[0])] = 0;
+            if ( learnt_clause.size == 1 ) 
+                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
@@ -1385,7 +1384,6 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT
                 return l_Undef; }
 
             if ( (s->nConfLimit && s->stats.conflicts > s->nConfLimit) ||
-//                 (s->nInsLimit  && s->stats.inspects  > s->nInsLimit) )
                  (s->nInsLimit  && s->stats.propagations > s->nInsLimit) )
             {
                 // Reached bound on number of conflicts:
@@ -1399,7 +1397,7 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT
                 // Simplify the set of problem clauses:
                 sat_solver_simplify(s);
 
-//            if (nof_learnts >= 0 && vecp_size(&s->learnts) - s->qtail >= nof_learnts)
+//            if (nof_learnts >= 0 && veci_size(&s->learnts) - s->qtail >= nof_learnts)
                 // Reduce the set of learnt clauses:
 //                sat_solver_reducedb(s);
 
@@ -1409,11 +1407,10 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT
 
             if (next == var_Undef){
                 // Model found:
-                lbool* values = s->assigns;
                 int i;
                 veci_resize(&s->model, 0);
                 for (i = 0; i < s->size; i++) 
-                    veci_push(&s->model,(int)values[i]);
+                    veci_push( &s->model, var_value(s,i)==var1 ? l_True : l_False );
                 sat_solver_canceluntil(s,s->root_level);
                 veci_delete(&learnt_clause);
 
@@ -1428,7 +1425,7 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT
                 return l_True;
             }
 
-            if ( s->polarity[next] ) // positive polarity
+            if ( var_polar(s, next) ) // positive polarity
                 sat_solver_assume(s,toLit(next));
             else
                 sat_solver_assume(s,lit_neg(toLit(next)));
@@ -1444,7 +1441,6 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
     ABC_INT64_T  nof_conflicts;
     ABC_INT64_T  nof_learnts   = sat_solver_nclauses(s) / 3;
     lbool   status        = l_Undef;
-    lbool*  values        = s->assigns;
     lit*    i;
 
     ////////////////////////////////////////////////
@@ -1478,15 +1474,16 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
 
     //printf("solve: "); printlits(begin, end); printf("\n");
     for (i = begin; i < end; i++){
-        switch (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]){
-        case 1: // l_True: 
+//        switch (lit_sign(*i) ? -s->assignss[lit_var(*i)] : s->assignss[lit_var(*i)]){
+        switch (var_value(s, *i)) {
+        case var1: // l_True: 
             break;
-        case 0: // l_Undef
+        case varX: // l_Undef
             sat_solver_assume(s, *i);
-            if (sat_solver_propagate(s) == NULL)
+            if (sat_solver_propagate(s) == 0)
                 break;
             // fallthrough
-        case -1: // l_False 
+        case var0: // l_False 
             sat_solver_canceluntil(s, 0);
             return l_False;
         }
@@ -1535,21 +1532,18 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
         lit p = *i;
         assert(lit_var(p) < s->size);
         veci_push(&s->trail_lim,s->qtail);
-        if (!sat_solver_enqueue(s,p,(clause*)0))
+        if (!sat_solver_enqueue(s,p,0))
         {
-            clause * r = s->reasons[lit_var(p)];
-            if (r != NULL)
+            int h = s->reasons[lit_var(p)];
+            if (h)
             {
-                clause* confl;
-                if (clause_is_lit(r))
+                if (clause_is_lit(h))
                 {
-                    confl = s->binary;
-                    (clause_begin(confl))[1] = lit_neg(p);
-                    (clause_begin(confl))[0] = clause_read_lit(r);
+                    (clause_begin(s->binary))[1] = lit_neg(p);
+                    (clause_begin(s->binary))[0] = clause_read_lit(h);
+                    h = s->hBinary;
                 }
-                else
-                    confl = r;
-                sat_solver_analyze_final(s, confl, 1);
+                sat_solver_analyze_final(s, h, 1);
                 veci_push(&s->conf_final, lit_neg(p));
             }
             else
@@ -1557,7 +1551,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
                 veci_resize(&s->conf_final,0);
                 veci_push(&s->conf_final, lit_neg(p));
                 // the two lines below are a bug fix by Siert Wieringa 
-                if (s->levels[lit_var(p)] > 0)
+                if (var_level(s, lit_var(p)) > 0)
                     veci_push(&s->conf_final, p);
             }
             sat_solver_canceluntil(s, 0);
@@ -1565,9 +1559,9 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
         }
         else
         {
-            clause* confl = sat_solver_propagate(s);
-            if (confl != NULL){
-                sat_solver_analyze_final(s, confl, 0);
+            int fConfl = sat_solver_propagate(s);
+            if (fConfl){
+                sat_solver_analyze_final(s, fConfl, 0);
                 assert(s->conf_final.size > 0);
                 sat_solver_canceluntil(s, 0);
                 return l_False; }
@@ -1586,12 +1580,10 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
     }
 
     while (status == l_Undef){
-//        int nConfs = 0;
         double Ratio = (s->stats.learnts == 0)? 0.0 :
             s->stats.learnts_literals / (double)s->stats.learnts;
         if ( s->nRuntimeLimit && time(NULL) > s->nRuntimeLimit )
             break;
-
         if (s->verbosity >= 1)
         {
             printf("| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %6.3f %% |\n", 
@@ -1606,31 +1598,16 @@ 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++) );
-//printf( "%d ", (int)nof_conflicts );
-//        nConfs = s->stats.conflicts;
         status = sat_solver_search(s, nof_conflicts, nof_learnts);
-//        if ( status == l_True )
-//            printf( "%d ", s->stats.conflicts - nConfs );
-
-//        nof_conflicts = nof_conflicts * 3 / 2; //*= 1.5;
         nof_learnts    = nof_learnts * 11 / 10; //*= 1.1;
-//printf( "%d ", s->stats.conflicts  );
         // quit the loop if reached an external limit
         if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit )
-        {
-//            printf( "Reached the limit on the number of conflicts (%d).\n", s->nConfLimit );
             break;
-        }
-//        if ( s->nInsLimit  && s->stats.inspects > s->nInsLimit )
         if ( s->nInsLimit  && s->stats.propagations > s->nInsLimit )
-        {
-//            printf( "Reached the limit on the number of implications (%d).\n", s->nInsLimit );
             break;
-        }
         if ( s->nRuntimeLimit && time(NULL) > s->nRuntimeLimit )
             break;
     }
-//printf( "\n" );
     if (s->verbosity >= 1)
         printf("==============================================================================\n");
 
@@ -1655,7 +1632,7 @@ int sat_solver_nvars(sat_solver* s)
 
 int sat_solver_nclauses(sat_solver* s)
 {
-    return vecp_size(&s->clauses);
+    return s->stats.clauses;
 }
 
 
@@ -1710,57 +1687,6 @@ void * sat_solver_store_release( sat_solver * s )
     return pTemp;
 }
 
-//=================================================================================================
-// 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_solver_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/satSolver.h b/src/sat/bsat/satSolver.h
index 4c577b1e..a0e94bfb 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -29,7 +29,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <assert.h>
 
 #include "satVec.h"
-#include "satMem.h"
+#include "vecRec.h"
 
 ABC_NAMESPACE_HEADER_START
 
@@ -54,6 +54,8 @@ extern int         sat_solver_nclauses(sat_solver* s);
 extern int         sat_solver_nconflicts(sat_solver* s);
 
 extern void        sat_solver_setnvars(sat_solver* s,int n);
+extern int         sat_solver_get_var_value(sat_solver* s, int v);
+
 
 extern void        Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars );
 extern void        Sat_SolverPrintStats( FILE * pFile, sat_solver * p );
@@ -79,84 +81,87 @@ extern void *      sat_solver_store_release( sat_solver * s );
 struct clause_t;
 typedef struct clause_t clause;
 
+struct varinfo_t;
+typedef struct varinfo_t varinfo;
+
 struct sat_solver_t
 {
-    int      size;          // nof variables
-    int      cap;           // size of varmaps
-    int      qhead;         // Head index of queue.
-    int      qtail;         // Tail index of queue.
+    int         size;          // nof variables
+    int         cap;           // size of varmaps
+    int         qhead;         // Head index of queue.
+    int         qtail;         // Tail index of queue.
 
     // clauses
-    vecp     clauses;       // List of problem constraints. (contains: clause*)
-    vecp     learnts;       // List of learnt clauses. (contains: clause*)
+    Vec_Rec_t   Mem;
+    int         hLearnts;      // the first learnt clause
+    int         hBinary;       // the special binary clause
+    clause *    binary;
 
     // activities
 #ifdef USE_FLOAT_ACTIVITY
-    double   var_inc;       // Amount to bump next variable with.
-    double   var_decay;     // INVERSE decay factor for variable activity: stores 1/decay. 
-    float    cla_inc;       // Amount to bump next clause with.
-    float    cla_decay;     // INVERSE decay factor for clause activity: stores 1/decay.
-    double*  activity;      // A heuristic measurement of the activity of a variable.
+    double      var_inc;       // Amount to bump next variable with.
+    double      var_decay;     // INVERSE decay factor for variable activity: stores 1/decay. 
+    float       cla_inc;       // Amount to bump next clause with.
+    float       cla_decay;     // INVERSE decay factor for clause activity: stores 1/decay.
+    double*     activity;      // A heuristic measurement of the activity of a variable.
 #else
-    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.
+    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.
 #endif
 
-    vecp*    wlists;        // 
-    lbool*   assigns;       // Current values of variables.
-    int*     orderpos;      // Index in variable order.
-    clause** reasons;       //
-    int*     levels;        //
-    lit*     trail;
-    char*    polarity;
-
-    clause*  binary;        // A temporary binary clause
-    lbool*   tags;          //
-    veci     tagged;        // (contains: var)
-    veci     stack;         // (contains: var)
-
-    veci     order;         // Variable order. (heap) (contains: var)
-    veci     trail_lim;     // Separator indices for different decision levels in 'trail'. (contains: int)
-    veci     model;         // If problem is solved, this vector contains the model (contains: lbool).
-    veci     conf_final;    // If problem is unsatisfiable (possibly under assumptions),
-                            // this vector represent the final conflict clause expressed in the assumptions.
-
-    int      root_level;    // Level of first proper decision.
-    int      simpdb_assigns;// Number of top-level assignments at last 'simplifyDB()'.
-    int      simpdb_props;  // Number of propagations before next 'simplifyDB()'.
-    double   random_seed;
-    double   progress_estimate;
-    int      verbosity;     // Verbosity level. 0=silent, 1=some progress report, 2=everything
-
-    stats_t    stats;
-
-    ABC_INT64_T   nConfLimit;    // external limit on the number of conflicts
-    ABC_INT64_T   nInsLimit;     // external limit on the number of implications
-    int           nRuntimeLimit; // external limit on runtime
-
-    veci     act_vars;      // variables whose activity has changed
-    double*  factors;       // the activity factors
-    int      nRestarts;     // the number of local restarts
-    int      nCalls;        // the number of local restarts
-    int      nCalls2;        // the number of local restarts
- 
-    Sat_MmStep_t * pMem;
-
-    int      fSkipSimplify; // set to one to skip simplification of the clause database
-    int      fNotUseRandom; // do not allow random decisions with a fixed probability
-
-    int *    pGlobalVars;   // for experiments with global vars during interpolation
+    veci*       wlists;        // 
+//    varinfo *   vi;            // variable information
+    int*        levels;        //
+    char*       assigns;       // Current values of variables.
+    char*       polarity;      //
+    char*       tags;          //
+
+    int*        orderpos;      // Index in variable order.
+    int*        reasons;       //
+    lit*        trail;
+    veci        tagged;        // (contains: var)
+    veci        stack;         // (contains: var)
+
+    veci        order;         // Variable order. (heap) (contains: var)
+    veci        trail_lim;     // Separator indices for different decision levels in 'trail'. (contains: int)
+    veci        model;         // If problem is solved, this vector contains the model (contains: lbool).
+    veci        conf_final;    // If problem is unsatisfiable (possibly under assumptions),
+                               // this vector represent the final conflict clause expressed in the assumptions.
+
+    int         root_level;    // Level of first proper decision.
+    int         simpdb_assigns;// Number of top-level assignments at last 'simplifyDB()'.
+    int         simpdb_props;  // Number of propagations before next 'simplifyDB()'.
+    double      random_seed;
+    double      progress_estimate;
+    int         verbosity;     // Verbosity level. 0=silent, 1=some progress report, 2=everything
+
+    stats_t     stats;
+
+    ABC_INT64_T nConfLimit;    // external limit on the number of conflicts
+    ABC_INT64_T nInsLimit;     // external limit on the number of implications
+    int         nRuntimeLimit; // external limit on runtime
+
+    veci        act_vars;      // variables whose activity has changed
+    double*     factors;       // the activity factors
+    int         nRestarts;     // the number of local restarts
+    int         nCalls;        // the number of local restarts
+    int         nCalls2;        // the number of local restarts
+
+    int         fSkipSimplify; // set to one to skip simplification of the clause database
+    int         fNotUseRandom; // do not allow random decisions with a fixed probability
+
+    int *       pGlobalVars;   // for experiments with global vars during interpolation
     // clause store
-    void *   pStore;
-    int      fSolved;
+    void *      pStore;
+    int         fSolved;
 
     // trace recording
-    FILE *   pFile;
-    int      nClauses;
-    int      nRoots;
+    FILE *      pFile;
+    int         nClauses;
+    int         nRoots;
 
-    veci     temp_clause;    // temporary storage for a CNF clause
+    veci        temp_clause;    // temporary storage for a CNF clause
 };
 
 static int sat_solver_var_value( sat_solver* s, int v ) 
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index 5eb65132..0cda3295 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -65,14 +65,6 @@ static inline double drand(double* seed) {
 static inline int irand(double* seed, int size) {
     return (int)(drand(seed) * size); }
 
-static inline int     sat_float2int( float Val )  { union { int x; float y; } v; v.y = Val; return v.x; }
-static inline float   sat_int2float( int Num )    { union { int x; float y; } v; v.x = Num; return v.y; }
-
-//=================================================================================================
-// Predeclarations:
-
-static void solver2_sort(void** array, int size, int(*comp)(const void *, const void *));
-
 //=================================================================================================
 // Variable datatype + minor functions:
 
@@ -82,23 +74,27 @@ static const int varX  = 3;
 
 struct varinfo_t
 {
-    unsigned val    :  2;  // variable value 
+//    unsigned val    :  2;  // variable value 
     unsigned pol    :  1;  // last polarity
     unsigned partA  :  1;  // partA variable
     unsigned tag    :  4;  // conflict analysis tags
-    unsigned lev    : 24;  // variable level
+//    unsigned lev    : 24;  // variable level
 };
 
 int    var_is_partA (sat_solver2* s, int v)              { return s->vi[v].partA;  }
 void   var_set_partA(sat_solver2* s, int v, int partA)   { s->vi[v].partA = partA; }
 
-static inline int     var_value     (sat_solver2* s, int v)            { return s->vi[v].val; }
+//static inline int     var_level     (sat_solver2* s, int v)            { return s->vi[v].lev; }
+static inline int     var_level     (sat_solver2* s, int v)            { return s->levels[v];  }
+//static inline int     var_value     (sat_solver2* s, int v)            { return s->vi[v].val; }
+static inline int     var_value     (sat_solver2* s, int v)            { return s->assigns[v]; }
 static inline int     var_polar     (sat_solver2* s, int v)            { return s->vi[v].pol; }
-static inline int     var_level     (sat_solver2* s, int v)            { return s->vi[v].lev; }
 
-static inline void    var_set_value (sat_solver2* s, int v, int val)   { s->vi[v].val = val;  }
+//static inline void    var_set_level (sat_solver2* s, int v, int lev)   { s->vi[v].lev = lev;  }
+static inline void    var_set_level (sat_solver2* s, int v, int lev)   { s->levels[v] = lev;  }
+//static inline void    var_set_value (sat_solver2* s, int v, int val)   { s->vi[v].val = val;  }
+static inline void    var_set_value (sat_solver2* s, int v, int val)   { s->assigns[v] = val; }
 static inline void    var_set_polar (sat_solver2* s, int v, int pol)   { s->vi[v].pol = pol;  }
-static inline void    var_set_level (sat_solver2* s, int v, int lev)   { s->vi[v].lev = lev;  }
 
 // variable tags
 static inline int     var_tag       (sat_solver2* s, int v)            { return s->vi[v].tag; }
@@ -1268,6 +1264,8 @@ void sat_solver2_setnvars(sat_solver2* s,int n)
 
         s->wlists    = ABC_REALLOC(veci,     s->wlists,   s->cap*2);
         s->vi        = ABC_REALLOC(varinfo,  s->vi,       s->cap);
+        s->levels    = ABC_REALLOC(int,      s->levels,   s->cap);
+        s->assigns   = ABC_REALLOC(char,     s->assigns,  s->cap);
         s->trail     = ABC_REALLOC(lit,      s->trail,    s->cap);
         s->orderpos  = ABC_REALLOC(int,      s->orderpos, s->cap);
         s->reasons   = ABC_REALLOC(cla,      s->reasons,  s->cap);
@@ -1288,7 +1286,9 @@ void sat_solver2_setnvars(sat_solver2* s,int n)
             veci_new(&s->wlists[2*var]);
         if ( s->wlists[2*var+1].ptr == NULL )
             veci_new(&s->wlists[2*var+1]);
-        *((int*)s->vi + var) = 0; s->vi[var].val = varX;
+        *((int*)s->vi + var) = 0; //s->vi[var].val = varX;
+        s->levels  [var] = 0;
+        s->assigns [var] = varX;
         s->orderpos[var] = veci_size(&s->order);
         s->reasons [var] = 0;        
         if ( s->fProofLogging )
@@ -1346,6 +1346,8 @@ void sat_solver2_delete(sat_solver2* s)
                 veci_delete(&s->wlists[i]);
         ABC_FREE(s->wlists   );
         ABC_FREE(s->vi       );
+        ABC_FREE(s->levels   );
+        ABC_FREE(s->assigns  );
         ABC_FREE(s->trail    );
         ABC_FREE(s->orderpos );
         ABC_FREE(s->reasons  );
diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h
index 0c08ac1e..21dc3b21 100644
--- a/src/sat/bsat/satSolver2.h
+++ b/src/sat/bsat/satSolver2.h
@@ -126,6 +126,8 @@ struct sat_solver2_t
 
     // internal state
     varinfo *       vi;             // variable information
+    int*            levels;         // 
+    char*           assigns;        // 
     lit*            trail;          // sequence of assignment and implications
     int*            orderpos;       // Index in variable order.
     cla*            reasons;        // reason clauses
diff --git a/src/sat/bsat/satSolver_old.c b/src/sat/bsat/satSolver_old.c
new file mode 100644
index 00000000..4d851d0f
--- /dev/null
+++ b/src/sat/bsat/satSolver_old.c
@@ -0,0 +1,1766 @@
+/**************************************************************************************************
+MiniSat -- Copyright (c) 2005, Niklas Sorensson
+http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko
+
+#include <stdio.h>
+#include <assert.h>
+#include <string.h>
+#include <math.h>
+
+#include "satSolver.h"
+#include "satStore.h"
+
+ABC_NAMESPACE_IMPL_START
+
+//#define SAT_USE_SYSTEM_MEMORY_MANAGEMENT
+#define SAT_USE_ANALYZE_FINAL
+
+//=================================================================================================
+// Debug:
+
+//#define VERBOSEDEBUG
+
+// For derivation output (verbosity level 2)
+#define L_IND    "%-*d"
+#define L_ind    sat_solver_dl(s)*2+2,sat_solver_dl(s)
+#define L_LIT    "%sx%d"
+#define L_lit(p) lit_sign(p)?"~":"", (lit_var(p))
+
+// Just like 'assert()' but expression will be evaluated in the release version as well.
+static inline void check(int expr) { assert(expr); }
+
+static void printlits(lit* begin, lit* end)
+{
+    int i;
+    for (i = 0; i < end - begin; i++)
+        printf(L_LIT" ",L_lit(begin[i]));
+}
+
+//=================================================================================================
+// Random numbers:
+
+
+// Returns a random float 0 <= x < 1. Seed must never be 0.
+static inline double drand(double* seed) {
+    int q;
+    *seed *= 1389796;
+    q = (int)(*seed / 2147483647);
+    *seed -= (double)q * 2147483647;
+    return *seed / 2147483647; }
+
+
+// Returns a random integer 0 <= x < size. Seed must never be 0.
+static inline int irand(double* seed, int size) {
+    return (int)(drand(seed) * size); }
+
+
+//=================================================================================================
+// Predeclarations:
+
+static void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *));
+
+//=================================================================================================
+// Clause datatype + minor functions:
+
+struct clause_t
+{
+    int size_learnt;
+    lit lits[0];
+};
+
+static inline int      clause_size         (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_size(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 clause* clause_from_lit (lit l)     { return (clause*)((ABC_PTRUINT_T)l + (ABC_PTRUINT_T)l + 1);  }
+static inline int     clause_is_lit   (clause* c) { return ((ABC_PTRUINT_T)c & 1);                              }
+static inline lit     clause_read_lit (clause* c) { return (lit)((ABC_PTRUINT_T)c >> 1);                        }
+
+//=================================================================================================
+// Simple helpers:
+
+static inline int     sat_solver_dl(sat_solver* s)                { return veci_size(&s->trail_lim); }
+static inline vecp*   sat_solver_read_wlist(sat_solver* s, lit l) { return &s->wlists[l];            }
+
+//=================================================================================================
+// Variable order functions:
+
+static inline void order_update(sat_solver* s, int v) // updateorder
+{
+    int*    orderpos = s->orderpos;
+    int*    heap     = veci_begin(&s->order);
+    int     i        = orderpos[v];
+    int     x        = heap[i];
+    int     parent   = (i - 1) / 2;
+
+    assert(s->orderpos[v] != -1);
+
+    while (i != 0 && s->activity[x] > s->activity[heap[parent]]){
+        heap[i]           = heap[parent];
+        orderpos[heap[i]] = i;
+        i                 = parent;
+        parent            = (i - 1) / 2;
+    }
+    heap[i]     = x;
+    orderpos[x] = i;
+}
+
+static inline void order_assigned(sat_solver* s, int v) 
+{
+}
+
+static inline void order_unassigned(sat_solver* s, int v) // undoorder
+{
+    int* orderpos = s->orderpos;
+    if (orderpos[v] == -1){
+        orderpos[v] = veci_size(&s->order);
+        veci_push(&s->order,v);
+        order_update(s,v);
+//printf( "+%d ", v );
+    }
+}
+
+static inline int  order_select(sat_solver* s, float random_var_freq) // selectvar
+{
+    int*    heap;
+    int*    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)
+            return next;
+    }
+
+    // Activity based decision:
+
+    heap     = veci_begin(&s->order);
+    orderpos = s->orderpos;
+
+
+    while (veci_size(&s->order) > 0){
+        int    next  = heap[0];
+        int    size  = veci_size(&s->order)-1;
+        int    x     = heap[size];
+
+        veci_resize(&s->order,size);
+
+        orderpos[next] = -1;
+
+        if (size > 0){
+
+            int    i     = 0;
+            int    child = 1;
+
+
+            while (child < size){
+                if (child+1 < size && s->activity[heap[child]] < s->activity[heap[child+1]])
+                    child++;
+
+                assert(child < size);
+
+                if (s->activity[x] >= s->activity[heap[child]])
+                    break;
+
+                heap[i]           = heap[child];
+                orderpos[heap[i]] = i;
+                i                 = child;
+                child             = 2 * child + 1;
+            }
+            heap[i]           = x;
+            orderpos[heap[i]] = i;
+        }
+
+//printf( "-%d ", next );
+        if (values[next] == l_Undef)
+            return next;
+    }
+
+    return var_Undef;
+}
+
+//=================================================================================================
+// Activity functions:
+
+#ifdef USE_FLOAT_ACTIVITY
+
+static inline void act_var_rescale(sat_solver* s)  {
+    double* activity = s->activity;
+    int i;
+    for (i = 0; i < s->size; i++)
+        activity[i] *= 1e-100;
+    s->var_inc *= 1e-100;
+}
+static inline void act_clause_rescale(sat_solver* s) {
+    static int Total = 0;
+    clause** cs = (clause**)vecp_begin(&s->learnts);
+    int i, clk = clock();
+    for (i = 0; i < vecp_size(&s->learnts); i++){
+        float a = clause_activity(cs[i]);
+        clause_setactivity(cs[i], a * (float)1e-20);
+    }
+    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 );
+}
+static inline void act_var_bump(sat_solver* s, int v) {
+    s->activity[v] += s->var_inc;
+    if (s->activity[v] > 1e100)
+        act_var_rescale(s);
+    if (s->orderpos[v] != -1)
+        order_update(s,v);
+}
+static inline void act_var_bump_global(sat_solver* s, int v) {
+    s->activity[v] += (s->var_inc * 3.0 * s->pGlobalVars[v]);
+    if (s->activity[v] > 1e100)
+        act_var_rescale(s);
+    if (s->orderpos[v] != -1)
+        order_update(s,v);
+}
+static inline void act_var_bump_factor(sat_solver* s, int v) {
+    s->activity[v] += (s->var_inc * s->factors[v]);
+    if (s->activity[v] > 1e100)
+        act_var_rescale(s);
+    if (s->orderpos[v] != -1)
+        order_update(s,v);
+}
+static inline void act_clause_bump(sat_solver* s, clause *c) {
+    float a = clause_activity(c) + s->cla_inc;
+    clause_setactivity(c,a);
+    if (a > 1e20) act_clause_rescale(s);
+}
+static inline void act_var_decay(sat_solver* s)    { s->var_inc *= s->var_decay; }
+static inline void act_clause_decay(sat_solver* s) { s->cla_inc *= s->cla_decay; }
+
+#else
+
+static inline void act_var_rescale(sat_solver* s) {
+    unsigned* activity = s->activity;
+    int i;
+    for (i = 0; i < s->size; i++)
+        activity[i] >>= 19;
+    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, clk = clock();
+    for (i = 0; i < vecp_size(&s->learnts); i++){
+        unsigned a = clause_activity2(cs[i]);
+        clause_setactivity2(cs[i], a >> 14);
+    }
+    s->cla_inc >>= 14;
+    s->cla_inc = Abc_MaxInt( s->cla_inc, (1<<10) );
+
+//    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)
+        act_var_rescale(s);
+    if (s->orderpos[v] != -1)
+        order_update(s,v);
+}
+static inline void act_var_bump_global(sat_solver* s, int v) {}
+static inline void act_var_bump_factor(sat_solver* s, int 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) 
+        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); }
+
+#endif
+
+
+//=================================================================================================
+// Clause functions:
+
+/* pre: size > 1 && no variable occurs twice
+ */
+static clause* clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt)
+{
+    int size;
+    clause* c;
+    int i;
+
+    assert(end - begin > 1);
+    assert(learnt >= 0 && learnt < 2);
+    size           = end - begin;
+
+    // do not allocate memory for the two-literal problem clause
+    if ( size == 2 && !learnt )
+    {
+        vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)(clause_from_lit(begin[1])));
+        vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)(clause_from_lit(begin[0])));
+        return NULL;
+    }
+
+#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
+    c = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
+#else
+    c = (clause*)Sat_MmStepEntryFetch( s->pMem, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float) );
+#endif
+
+    c->size_learnt = (size << 1) | learnt;
+    assert(((ABC_PTRUINT_T)c & 1) == 0);
+
+    for (i = 0; i < size; i++)
+        c->lits[i] = begin[i];
+
+    if (learnt)
+        *((float*)&c->lits[size]) = 0.0;
+
+    assert(begin[0] >= 0);
+    assert(begin[0] < s->size*2);
+    assert(begin[1] >= 0);
+    assert(begin[1] < s->size*2);
+
+    assert(lit_neg(begin[0]) < s->size*2);
+    assert(lit_neg(begin[1]) < s->size*2);
+
+    //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)c);
+    //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)c);
+
+    vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)(size > 2 ? c : clause_from_lit(begin[1])));
+    vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)(size > 2 ? c : clause_from_lit(begin[0])));
+
+    return c;
+}
+
+
+//=================================================================================================
+// Minor (solver) functions:
+
+static inline int sat_solver_enqueue(sat_solver* s, lit l, clause* from)
+{
+    lbool* values = s->assigns;
+    int    v      = lit_var(l);
+    lbool  val    = values[v];
+    lbool  sig;
+#ifdef VERBOSEDEBUG
+    printf(L_IND"enqueue("L_LIT")\n", L_ind, L_lit(l));
+#endif
+
+    sig = !lit_sign(l); sig += sig - 1;
+    if (val != l_Undef){
+        return val == sig;
+    }else{
+        int*     levels  = s->levels;
+        clause** reasons = s->reasons;
+        // New fact -- store it.
+#ifdef VERBOSEDEBUG
+        printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(l));
+#endif
+        values [v] = sig;
+        levels [v] = sat_solver_dl(s);
+        reasons[v] = from;
+        s->trail[s->qtail++] = l;
+
+        order_assigned(s, v);
+        return true;
+    }
+}
+
+
+static inline int sat_solver_assume(sat_solver* s, lit l){
+    assert(s->qtail == s->qhead);
+    assert(s->assigns[lit_var(l)] == l_Undef);
+#ifdef VERBOSEDEBUG
+    printf(L_IND"assume("L_LIT")  ", L_ind, L_lit(l));
+    printf( "act = %.20f\n", s->activity[lit_var(l)] );
+#endif
+    veci_push(&s->trail_lim,s->qtail);
+    return sat_solver_enqueue(s,l,(clause*)0);
+}
+
+
+static void sat_solver_canceluntil(sat_solver* s, int level) {
+    lit*     trail;   
+    lbool*   values;  
+    clause** reasons; 
+    int      bound;
+    int      lastLev;
+    int      c;
+    
+    if (sat_solver_dl(s) <= level)
+        return;
+
+    trail   = s->trail;
+    values  = s->assigns;
+    reasons = s->reasons;
+    bound   = (veci_begin(&s->trail_lim))[level];
+    lastLev = (veci_begin(&s->trail_lim))[veci_size(&s->trail_lim)-1];
+
+    ////////////////////////////////////////
+    // added to cancel all assignments
+//    if ( level == -1 )
+//        bound = 0;
+    ////////////////////////////////////////
+
+    for (c = s->qtail-1; c >= bound; c--) {
+        int     x  = lit_var(trail[c]);
+        values [x] = l_Undef;
+        reasons[x] = (clause*)0;
+        if ( c < lastLev )
+            s->polarity[x] = !lit_sign(trail[c]);
+    }
+
+    for (c = s->qhead-1; c >= bound; c--)
+        order_unassigned(s,lit_var(trail[c]));
+
+    s->qhead = s->qtail = bound;
+    veci_resize(&s->trail_lim,level);
+}
+
+static void sat_solver_record(sat_solver* s, veci* cls)
+{
+    lit*    begin = veci_begin(cls);
+    lit*    end   = begin + veci_size(cls);
+    clause* c     = (veci_size(cls) > 1) ? clause_create_new(s,begin,end,1) : (clause*)0;
+    sat_solver_enqueue(s,*begin,c);
+
+    ///////////////////////////////////
+    // add clause to internal storage
+    if ( s->pStore )
+    {
+        int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, begin, end );
+        assert( RetValue );
+    }
+    ///////////////////////////////////
+
+    assert(veci_size(cls) > 0);
+
+    if (c != 0) {
+        vecp_push(&s->learnts,c);
+        act_clause_bump(s,c);
+        s->stats.learnts++;
+        s->stats.learnts_literals += veci_size(cls);
+    }
+}
+
+
+static double sat_solver_progress(sat_solver* s)
+{
+    lbool*  values = s->assigns;
+    int*    levels = s->levels;
+    int     i;
+
+    double  progress = 0;
+    double  F        = 1.0 / s->size;
+    for (i = 0; i < s->size; i++)
+        if (values[i] != l_Undef)
+            progress += pow(F, levels[i]);
+    return progress / s->size;
+}
+
+//=================================================================================================
+// Major methods:
+
+static int sat_solver_lit_removable(sat_solver* s, lit l, int minl)
+{
+    lbool*   tags    = s->tags;
+    clause** reasons = s->reasons;
+    int*     levels  = s->levels;
+    int      top     = veci_size(&s->tagged);
+
+    assert(lit_var(l) >= 0 && lit_var(l) < s->size);
+    assert(reasons[lit_var(l)] != 0);
+    veci_resize(&s->stack,0);
+    veci_push(&s->stack,lit_var(l));
+
+    while (veci_size(&s->stack) > 0){
+        clause* c;
+        int 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(reasons[v] != 0);
+        c    = reasons[v];
+
+        if (clause_is_lit(c)){
+            int v = lit_var(clause_read_lit(c));
+            if (tags[v] == l_Undef && levels[v] != 0){
+                if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){
+                    veci_push(&s->stack,v);
+                    tags[v] = l_True;
+                    veci_push(&s->tagged,v);
+                }else{
+                    int* tagged = veci_begin(&s->tagged);
+                    int j;
+                    for (j = top; j < veci_size(&s->tagged); j++)
+                        tags[tagged[j]] = l_Undef;
+                    veci_resize(&s->tagged,top);
+                    return false;
+                }
+            }
+        }else{
+            lit*    lits = clause_begin(c);
+            int     i, j;
+
+            for (i = 1; i < clause_size(c); i++){
+                int v = lit_var(lits[i]);
+                if (tags[v] == l_Undef && levels[v] != 0){
+                    if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){
+
+                        veci_push(&s->stack,lit_var(lits[i]));
+                        tags[v] = l_True;
+                        veci_push(&s->tagged,v);
+                    }else{
+                        int* tagged = veci_begin(&s->tagged);
+                        for (j = top; j < veci_size(&s->tagged); j++)
+                            tags[tagged[j]] = l_Undef;
+                        veci_resize(&s->tagged,top);
+                        return false;
+                    }
+                }
+            }
+        }
+    }
+
+    return true;
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  analyzeFinal : (p : Lit)  ->  [void]
+|  
+|  Description:
+|    Specialized analysis procedure to express the final conflict in terms of assumptions.
+|    Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and
+|    stores the result in 'out_conflict'.
+|________________________________________________________________________________________________@*/
+/*
+void Solver::analyzeFinal(Clause* confl, bool skip_first)
+{
+    // -- NOTE! This code is relatively untested. Please report bugs!
+    conflict.clear();
+    if (root_level == 0) return;
+
+    vec<char>& seen  = analyze_seen;
+    for (int i = skip_first ? 1 : 0; i < confl->size(); i++){
+        Var x = var((*confl)[i]);
+        if (level[x] > 0)
+            seen[x] = 1;
+    }
+
+    int start = (root_level >= trail_lim.size()) ? trail.size()-1 : trail_lim[root_level];
+    for (int i = start; i >= trail_lim[0]; i--){
+        Var     x = var(trail[i]);
+        if (seen[x]){
+            GClause r = reason[x];
+            if (r == GClause_NULL){
+                assert(level[x] > 0);
+                conflict.push(~trail[i]);
+            }else{
+                if (r.isLit()){
+                    Lit p = r.lit();
+                    if (level[var(p)] > 0)
+                        seen[var(p)] = 1;
+                }else{
+                    Clause& c = *r.clause();
+                    for (int j = 1; j < c.size(); j++)
+                        if (level[var(c[j])] > 0)
+                            seen[var(c[j])] = 1;
+                }
+            }
+            seen[x] = 0;
+        }
+    }
+}
+*/
+
+#ifdef SAT_USE_ANALYZE_FINAL
+
+static void sat_solver_analyze_final(sat_solver* s, clause* conf, int skip_first)
+{
+    int i, j, start;
+    veci_resize(&s->conf_final,0);
+    if ( s->root_level == 0 )
+        return;
+    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_size(conf); i++)
+    {
+        int x = lit_var(clause_begin(conf)[i]);
+        if (s->levels[x] > 0)
+        {
+            s->tags[x] = l_True;
+            veci_push(&s->tagged,x);
+        }
+    }
+
+    start = (s->root_level >= veci_size(&s->trail_lim))? s->qtail-1 : (veci_begin(&s->trail_lim))[s->root_level];
+    for (i = start; i >= (veci_begin(&s->trail_lim))[0]; i--){
+        int x = lit_var(s->trail[i]);
+        if (s->tags[x] == l_True){
+            if (s->reasons[x] == NULL){
+                assert(s->levels[x] > 0);
+                veci_push(&s->conf_final,lit_neg(s->trail[i]));
+            }else{
+                clause* c = s->reasons[x];
+                if (clause_is_lit(c)){
+                    lit q = clause_read_lit(c);
+                    assert(lit_var(q) >= 0 && lit_var(q) < s->size);
+                    if (s->levels[lit_var(q)] > 0)
+                    {
+                        s->tags[lit_var(q)] = l_True;
+                        veci_push(&s->tagged,lit_var(q));
+                    }
+                }
+                else{
+                    int* lits = clause_begin(c);
+                    for (j = 1; j < clause_size(c); j++)
+                        if (s->levels[lit_var(lits[j])] > 0)
+                        {
+                            s->tags[lit_var(lits[j])] = l_True;
+                            veci_push(&s->tagged,lit_var(lits[j]));
+                        }
+                }
+            }
+        }
+    }
+    for (i = 0; i < veci_size(&s->tagged); i++)
+        s->tags[veci_begin(&s->tagged)[i]] = l_Undef;
+    veci_resize(&s->tagged,0);
+}
+
+#endif
+
+
+static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt)
+{
+    lit*     trail   = s->trail;
+    lbool*   tags    = s->tags;
+    clause** reasons = s->reasons;
+    int*     levels  = s->levels;
+    int      cnt     = 0;
+    lit      p       = lit_Undef;
+    int      ind     = s->qtail-1;
+    lit*     lits;
+    int      i, j, minl;
+    int*     tagged;
+
+    veci_push(learnt,lit_Undef);
+
+    do{
+        assert(c != 0);
+
+        if (clause_is_lit(c)){
+            lit q = clause_read_lit(c);
+            assert(lit_var(q) >= 0 && lit_var(q) < s->size);
+            if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){
+                tags[lit_var(q)] = l_True;
+                veci_push(&s->tagged,lit_var(q));
+                act_var_bump(s,lit_var(q));
+                if (levels[lit_var(q)] == sat_solver_dl(s))
+                    cnt++;
+                else
+                    veci_push(learnt,q);
+            }
+        }else{
+
+            if (clause_learnt(c))
+                act_clause_bump(s,c);
+
+            lits = clause_begin(c);
+            //printlits(lits,lits+clause_size(c)); printf("\n");
+            for (j = (p == lit_Undef ? 0 : 1); j < clause_size(c); j++){
+                lit q = lits[j];
+                assert(lit_var(q) >= 0 && lit_var(q) < s->size);
+                if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){
+                    tags[lit_var(q)] = l_True;
+                    veci_push(&s->tagged,lit_var(q));
+                    act_var_bump(s,lit_var(q));
+                    if (levels[lit_var(q)] == sat_solver_dl(s))
+                        cnt++;
+                    else
+                        veci_push(learnt,q);
+                }
+            }
+        }
+
+        while (tags[lit_var(trail[ind--])] == l_Undef);
+
+        p = trail[ind+1];
+        c = reasons[lit_var(p)];
+        cnt--;
+
+    }while (cnt > 0);
+
+    *veci_begin(learnt) = lit_neg(p);
+
+    lits = veci_begin(learnt);
+    minl = 0;
+    for (i = 1; i < veci_size(learnt); i++){
+        int lev = levels[lit_var(lits[i])];
+        minl    |= 1 << (lev & 31);
+    }
+
+    // simplify (full)
+    for (i = j = 1; i < veci_size(learnt); i++){
+        if (reasons[lit_var(lits[i])] == 0 || !sat_solver_lit_removable(s,lits[i],minl))
+            lits[j++] = lits[i];
+    }
+
+    // update size of learnt + statistics
+    veci_resize(learnt,j);
+    s->stats.tot_literals += j;
+
+    // clear tags
+    tagged = veci_begin(&s->tagged);
+    for (i = 0; i < veci_size(&s->tagged); i++)
+        tags[tagged[i]] = l_Undef;
+    veci_resize(&s->tagged,0);
+
+#ifdef DEBUG
+    for (i = 0; i < s->size; i++)
+        assert(tags[i] == l_Undef);
+#endif
+
+#ifdef VERBOSEDEBUG
+    printf(L_IND"Learnt {", L_ind);
+    for (i = 0; i < veci_size(learnt); i++) printf(" "L_LIT, L_lit(lits[i]));
+#endif
+    if (veci_size(learnt) > 1){
+        int max_i = 1;
+        int max   = levels[lit_var(lits[1])];
+        lit tmp;
+
+        for (i = 2; i < veci_size(learnt); i++)
+            if (levels[lit_var(lits[i])] > max){
+                max   = levels[lit_var(lits[i])];
+                max_i = i;
+            }
+
+        tmp         = lits[1];
+        lits[1]     = lits[max_i];
+        lits[max_i] = tmp;
+    }
+#ifdef VERBOSEDEBUG
+    {
+        int lev = veci_size(learnt) > 1 ? levels[lit_var(lits[1])] : 0;
+        printf(" } at level %d\n", lev);
+    }
+#endif
+}
+
+
+clause* sat_solver_propagate(sat_solver* s)
+{
+    lbool*  values = s->assigns;
+    clause* confl  = (clause*)0;
+    lit*    lits;
+    lit false_lit;
+    lbool sig;
+
+    //printf("sat_solver_propagate\n");
+    while (confl == 0 && s->qtail - s->qhead > 0){
+        lit  p  = s->trail[s->qhead++];
+        vecp* ws = sat_solver_read_wlist(s,p);
+        clause **begin = (clause**)vecp_begin(ws);
+        clause **end   = begin + vecp_size(ws);
+        clause **i, **j;
+
+        s->stats.propagations++;
+        s->simpdb_props--;
+
+        //printf("checking lit %d: "L_LIT"\n", veci_size(ws), L_lit(p));
+        for (i = j = begin; i < end; ){
+            if (clause_is_lit(*i)){
+
+                int Lit = clause_read_lit(*i);
+                sig = !lit_sign(Lit); sig += sig - 1;
+                if (values[lit_var(Lit)] == sig){
+                    *j++ = *i++;
+                    continue;
+                }
+
+                *j++ = *i;
+                if (!sat_solver_enqueue(s,clause_read_lit(*i),clause_from_lit(p))){
+                    confl = s->binary;
+                    (clause_begin(confl))[1] = lit_neg(p);
+                    (clause_begin(confl))[0] = clause_read_lit(*i++);
+                    // Copy the remaining watches:
+                    while (i < end)
+                        *j++ = *i++;
+                }
+            }else{
+
+                lits = clause_begin(*i);
+
+                // Make sure the false literal is data[1]:
+                false_lit = lit_neg(p);
+                if (lits[0] == false_lit){
+                    lits[0] = lits[1];
+                    lits[1] = false_lit;
+                }
+                assert(lits[1] == false_lit);
+                //printf("checking clause: "); printlits(lits, lits+clause_size(*i)); printf("\n");
+
+                // If 0th watch is true, then clause is already satisfied.
+                sig = !lit_sign(lits[0]); sig += sig - 1;
+                if (values[lit_var(lits[0])] == sig){
+                    *j++ = *i;
+                }else{
+                    // Look for new watch:
+                    lit* stop = lits + clause_size(*i);
+                    lit* k;
+                    for (k = lits + 2; k < stop; k++){
+                        lbool sig = lit_sign(*k); sig += sig - 1;
+                        if (values[lit_var(*k)] != sig){
+                            lits[1] = *k;
+                            *k = false_lit;
+                            vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i);
+                            goto next; }
+                    }
+
+                    *j++ = *i;
+                    // Clause is unit under assignment:
+                    if (!sat_solver_enqueue(s,lits[0], *i)){
+                        confl = *i++;
+                        // Copy the remaining watches:
+                        while (i < end)
+                            *j++ = *i++;
+                    }
+                }
+            }
+        next:
+            i++;
+        }
+
+        s->stats.inspects += j - (clause**)vecp_begin(ws);
+        vecp_resize(ws,j - (clause**)vecp_begin(ws));
+    }
+
+    return confl;
+}
+
+//=================================================================================================
+// External solver functions:
+
+sat_solver* sat_solver_new(void)
+{
+    sat_solver* s = (sat_solver*)ABC_ALLOC( char, sizeof(sat_solver));
+    memset( s, 0, sizeof(sat_solver) );
+
+    // initialize vectors
+    vecp_new(&s->clauses);
+    vecp_new(&s->learnts);
+    veci_new(&s->order);
+    veci_new(&s->trail_lim);
+    veci_new(&s->tagged);
+    veci_new(&s->stack);
+    veci_new(&s->model);
+    veci_new(&s->act_vars);
+    veci_new(&s->temp_clause);
+    veci_new(&s->conf_final);
+
+    // initialize arrays
+    s->wlists    = 0;
+    s->activity  = 0;
+    s->factors   = 0;
+    s->assigns   = 0;
+    s->orderpos  = 0;
+    s->reasons   = 0;
+    s->levels    = 0;
+    s->tags      = 0;
+    s->trail     = 0;
+
+
+    // initialize other vars
+    s->size                   = 0;
+    s->cap                    = 0;
+    s->qhead                  = 0;
+    s->qtail                  = 0;
+#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 );
+#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->random_seed            = 91648253;
+    s->progress_estimate      = 0;
+    s->binary                 = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit)*2);
+    s->binary->size_learnt    = (2 << 1);
+    s->verbosity              = 0;
+
+    s->stats.starts           = 0;
+    s->stats.decisions        = 0;
+    s->stats.propagations     = 0;
+    s->stats.inspects         = 0;
+    s->stats.conflicts        = 0;
+    s->stats.clauses          = 0;
+    s->stats.clauses_literals = 0;
+    s->stats.learnts          = 0;
+    s->stats.learnts_literals = 0;
+    s->stats.tot_literals     = 0;
+
+#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
+    s->pMem = NULL;
+#else
+    s->pMem = Sat_MmStepStart( 10 );
+#endif
+    return s;
+}
+
+void sat_solver_setnvars(sat_solver* s,int n)
+{
+    int var;
+
+    if (s->cap < n){
+        int old_cap = s->cap;
+        while (s->cap < n) s->cap = s->cap*2+1;
+
+        s->wlists    = ABC_REALLOC(vecp,   s->wlists,   s->cap*2);
+#ifdef USE_FLOAT_ACTIVITY
+        s->activity  = ABC_REALLOC(double,   s->activity, s->cap);
+#else
+        s->activity  = ABC_REALLOC(unsigned, s->activity, s->cap);
+#endif
+        s->factors   = ABC_REALLOC(double, s->factors,  s->cap);
+        s->assigns   = ABC_REALLOC(lbool,  s->assigns,  s->cap);
+        s->orderpos  = ABC_REALLOC(int,    s->orderpos, s->cap);
+        s->reasons   = ABC_REALLOC(clause*,s->reasons,  s->cap);
+        s->levels    = ABC_REALLOC(int,    s->levels,   s->cap);
+        s->tags      = ABC_REALLOC(lbool,  s->tags,     s->cap);
+        s->trail     = ABC_REALLOC(lit,    s->trail,    s->cap);
+        s->polarity  = ABC_REALLOC(char,   s->polarity, s->cap);
+        memset( s->wlists + 2*old_cap, 0, 2*(s->cap-old_cap)*sizeof(vecp) );
+    }
+
+    for (var = s->size; var < n; var++){
+        assert(!s->wlists[2*var].size);
+        assert(!s->wlists[2*var+1].size);
+        if ( s->wlists[2*var].ptr == NULL )
+            vecp_new(&s->wlists[2*var]);
+        if ( s->wlists[2*var+1].ptr == NULL )
+            vecp_new(&s->wlists[2*var+1]);
+#ifdef USE_FLOAT_ACTIVITY
+        s->activity[var] = 0;
+#else
+        s->activity[var] = (1<<10);
+#endif
+        s->factors  [var] = 0;
+        s->assigns  [var] = l_Undef;
+        s->orderpos [var] = veci_size(&s->order);
+        s->reasons  [var] = (clause*)0;
+        s->levels   [var] = 0;
+        s->tags     [var] = l_Undef;
+        s->polarity [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_solver_delete(sat_solver* s)
+{
+
+#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
+    int i;
+    for (i = 0; i < vecp_size(&s->clauses); i++)
+        ABC_FREE(vecp_begin(&s->clauses)[i]);
+    for (i = 0; i < vecp_size(&s->learnts); i++)
+        ABC_FREE(vecp_begin(&s->learnts)[i]);
+#else
+    Sat_MmStepStop( s->pMem, 0 );
+#endif
+
+    // delete vectors
+    vecp_delete(&s->clauses);
+    vecp_delete(&s->learnts);
+    veci_delete(&s->order);
+    veci_delete(&s->trail_lim);
+    veci_delete(&s->tagged);
+    veci_delete(&s->stack);
+    veci_delete(&s->model);
+    veci_delete(&s->act_vars);
+    veci_delete(&s->temp_clause);
+    veci_delete(&s->conf_final);
+    ABC_FREE(s->binary);
+
+    // delete arrays
+    if (s->wlists != 0){
+        int i;
+        for (i = 0; i < s->cap*2; i++)
+            vecp_delete(&s->wlists[i]);
+        ABC_FREE(s->wlists   );
+        ABC_FREE(s->activity );
+        ABC_FREE(s->factors  );
+        ABC_FREE(s->assigns  );
+        ABC_FREE(s->orderpos );
+        ABC_FREE(s->reasons  );
+        ABC_FREE(s->levels   );
+        ABC_FREE(s->trail    );
+        ABC_FREE(s->tags     );
+        ABC_FREE(s->polarity );
+    }
+
+    sat_solver_store_free(s);
+    ABC_FREE(s);
+}
+
+void sat_solver_rollback( sat_solver* s )
+{
+    int i;
+#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
+    for (i = 0; i < vecp_size(&s->clauses); i++)
+        ABC_FREE(vecp_begin(&s->clauses)[i]);
+    for (i = 0; i < vecp_size(&s->learnts); i++)
+        ABC_FREE(vecp_begin(&s->learnts)[i]);
+#else
+    Sat_MmStepRestart( s->pMem );
+#endif
+    vecp_resize(&s->clauses, 0);
+    vecp_resize(&s->learnts, 0);
+    veci_resize(&s->trail_lim, 0);
+    veci_resize(&s->order, 0);
+    for ( i = 0; i < s->size*2; i++ )
+        s->wlists[i].size = 0;
+
+    // initialize other vars
+    s->size                   = 0;
+//    s->cap                    = 0;
+    s->qhead                  = 0;
+    s->qtail                  = 0;
+#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 );
+#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->random_seed            = 91648253;
+    s->progress_estimate      = 0;
+    s->verbosity              = 0;
+
+    s->stats.starts           = 0;
+    s->stats.decisions        = 0;
+    s->stats.propagations     = 0;
+    s->stats.inspects         = 0;
+    s->stats.conflicts        = 0;
+    s->stats.clauses          = 0;
+    s->stats.clauses_literals = 0;
+    s->stats.learnts          = 0;
+    s->stats.learnts_literals = 0;
+    s->stats.tot_literals     = 0;
+}
+
+
+static void clause_remove(sat_solver* s, clause* c)
+{
+    lit* lits = clause_begin(c);
+    assert(lit_neg(lits[0]) < s->size*2);
+    assert(lit_neg(lits[1]) < s->size*2);
+
+    //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)c);
+    //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)c);
+
+    assert(lits[0] < s->size*2);
+    vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1])));
+    vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0])));
+
+    if (clause_learnt(c)){
+        s->stats.learnts--;
+        s->stats.learnts_literals -= clause_size(c);
+    }else{
+        s->stats.clauses--;
+        s->stats.clauses_literals -= clause_size(c);
+    }
+
+#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
+    ABC_FREE(c);
+#else
+    Sat_MmStepEntryRecycle( s->pMem, (char *)c, sizeof(clause) + sizeof(lit) * clause_size(c) + clause_learnt(c) * sizeof(float) );
+#endif
+}
+
+static lbool clause_simplify(sat_solver* s, clause* c)
+{
+    lit*   lits   = clause_begin(c);
+    lbool* values = s->assigns;
+    int i;
+
+    assert(sat_solver_dl(s) == 0);
+
+    for (i = 0; i < clause_size(c); i++){
+        lbool sig = !lit_sign(lits[i]); sig += sig - 1;
+        if (values[lit_var(lits[i])] == sig)
+            return l_True;
+    }
+    return l_False;
+}
+
+int sat_solver_simplify(sat_solver* s)
+{
+    clause** reasons;
+    int type;
+
+    assert(sat_solver_dl(s) == 0);
+
+    if (sat_solver_propagate(s) != 0)
+        return false;
+
+    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];
+        }
+        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;
+}
+
+
+static int clause_cmp (const void* x, const void* y) {
+    return clause_size((clause*)x) > 2 && (clause_size((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 / vecp_size(&s->learnts); // Remove any clause below this activity
+    clause** learnts = (clause**)vecp_begin(&s->learnts);
+    clause** reasons = s->reasons;
+
+    sat_solver_sort(vecp_begin(&s->learnts), vecp_size(&s->learnts), &clause_cmp);
+
+    for (i = j = 0; i < vecp_size(&s->learnts) / 2; i++){
+        if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i])
+            clause_remove(s,learnts[i]);
+        else
+            learnts[j++] = learnts[i];
+    }
+    for (; i < vecp_size(&s->learnts); i++){
+        if (clause_size(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];
+    }
+
+    //printf("reducedb deleted %d\n", vecp_size(&s->learnts) - j);
+
+
+    vecp_resize(&s->learnts,j);
+}
+
+int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
+{
+    clause * c;
+    lit *i,*j;
+    int maxvar;
+    lbool* values;
+    lit last;
+
+    veci_resize( &s->temp_clause, 0 );
+    for ( i = begin; i < end; i++ )
+        veci_push( &s->temp_clause, *i );
+    begin = veci_begin( &s->temp_clause );
+    end = begin + veci_size( &s->temp_clause );
+
+    if (begin == end) 
+        return false;
+
+    //printlits(begin,end); printf("\n");
+    // insertion sort
+    maxvar = lit_var(*begin);
+    for (i = begin + 1; i < end; i++){
+        lit l = *i;
+        maxvar = lit_var(l) > maxvar ? lit_var(l) : maxvar;
+        for (j = i; j > begin && *(j-1) > l; j--)
+            *j = *(j-1);
+        *j = l;
+    }
+    sat_solver_setnvars(s,maxvar+1);
+//    sat_solver_setnvars(s, lit_var(*(end-1))+1 );
+
+    ///////////////////////////////////
+    // add clause to internal storage
+    if ( s->pStore )
+    {
+        int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, begin, end );
+        assert( RetValue );
+    }
+    ///////////////////////////////////
+
+    //printlits(begin,end); printf("\n");
+    values = s->assigns;
+
+    // delete duplicates
+    last = lit_Undef;
+    for (i = j = begin; i < end; i++){
+        //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]));
+        lbool sig = !lit_sign(*i); sig += sig - 1;
+        if (*i == lit_neg(last) || sig == values[lit_var(*i)])
+            return true;   // tautology
+        else if (*i != last && values[lit_var(*i)] == l_Undef)
+            last = *j++ = *i;
+    }
+//    j = i;
+
+    if (j == begin)          // empty clause
+        return false;
+
+    if (j - begin == 1) // unit clause
+        return sat_solver_enqueue(s,*begin,(clause*)0);
+
+    // create new clause
+    c = clause_create_new(s,begin,j,0);
+    if ( c )
+        vecp_push(&s->clauses,c);
+
+
+    s->stats.clauses++;
+    s->stats.clauses_literals += j - begin;
+
+    return true;
+}
+
+
+double luby(double y, int x)
+{
+    int size, seq;
+    for (size = 1, seq = 0; size < x+1; seq++, size = 2*size + 1);
+    while (size-1 != x){
+        size = (size-1) >> 1;
+        seq--;
+        x = x % size;
+    }
+    return pow(y, (double)seq);
+} 
+
+void luby_test()
+{
+    int i;
+    for ( i = 0; i < 20; i++ )
+        printf( "%d ", (int)luby(2,i) );
+    printf( "\n" );
+}
+
+static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT64_T nof_learnts)
+{
+    int*    levels          = s->levels;
+    double  var_decay       = 0.95;
+    double  clause_decay    = 0.999;
+    double  random_var_freq = s->fNotUseRandom ? 0.0 : 0.02;
+
+    ABC_INT64_T  conflictC       = 0;
+    veci    learnt_clause;
+    int     i;
+
+    assert(s->root_level == sat_solver_dl(s));
+
+    s->nRestarts++;
+    s->stats.starts++;
+//    s->var_decay = (float)(1 / var_decay   );  // move this to sat_solver_new()
+//    s->cla_decay = (float)(1 / clause_decay);  // move this to sat_solver_new()
+    veci_resize(&s->model,0);
+    veci_new(&learnt_clause);
+
+    // use activity factors in every even restart
+    if ( (s->nRestarts & 1) && veci_size(&s->act_vars) > 0 )
+//    if ( veci_size(&s->act_vars) > 0 )
+        for ( i = 0; i < s->act_vars.size; i++ )
+            act_var_bump_factor(s, s->act_vars.ptr[i]);
+
+    // use activity factors in every restart
+    if ( s->pGlobalVars && veci_size(&s->act_vars) > 0 )
+        for ( i = 0; i < s->act_vars.size; i++ )
+            act_var_bump_global(s, s->act_vars.ptr[i]);
+
+    for (;;){
+        clause* confl = sat_solver_propagate(s);
+        if (confl != 0){
+            // CONFLICT
+            int blevel;
+
+#ifdef VERBOSEDEBUG
+            printf(L_IND"**CONFLICT**\n", L_ind);
+#endif
+            s->stats.conflicts++; conflictC++;
+            if (sat_solver_dl(s) == s->root_level){
+#ifdef SAT_USE_ANALYZE_FINAL
+                sat_solver_analyze_final(s, confl, 0);
+#endif
+                veci_delete(&learnt_clause);
+                return l_False;
+            }
+
+            veci_resize(&learnt_clause,0);
+            sat_solver_analyze(s, confl, &learnt_clause);
+            blevel = veci_size(&learnt_clause) > 1 ? levels[lit_var(veci_begin(&learnt_clause)[1])] : s->root_level;
+            blevel = s->root_level > blevel ? s->root_level : blevel;
+            sat_solver_canceluntil(s,blevel);
+            sat_solver_record(s,&learnt_clause);
+#ifdef SAT_USE_ANALYZE_FINAL
+//            if (learnt_clause.size() == 1) level[var(learnt_clause[0])] = 0;    // (this is ugly (but needed for 'analyzeFinal()') -- in future versions, we will backtrack past the 'root_level' and redo the assumptions)
+            if ( learnt_clause.size == 1 ) s->levels[lit_var(learnt_clause.ptr[0])] = 0;
+#endif
+            act_var_decay(s);
+            act_clause_decay(s);
+
+        }else{
+            // NO CONFLICT
+            int next;
+ 
+            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; }
+
+            if ( (s->nConfLimit && s->stats.conflicts > s->nConfLimit) ||
+//                 (s->nInsLimit  && s->stats.inspects  > s->nInsLimit) )
+                 (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; 
+            }
+
+            if (sat_solver_dl(s) == 0 && !s->fSkipSimplify)
+                // Simplify the set of problem clauses:
+                sat_solver_simplify(s);
+
+//            if (nof_learnts >= 0 && vecp_size(&s->learnts) - s->qtail >= nof_learnts)
+                // Reduce the set of learnt clauses:
+//                sat_solver_reducedb(s);
+
+            // New variable decision:
+            s->stats.decisions++;
+            next = order_select(s,(float)random_var_freq);
+
+            if (next == var_Undef){
+                // Model found:
+                lbool* values = s->assigns;
+                int i;
+                veci_resize(&s->model, 0);
+                for (i = 0; i < s->size; i++) 
+                    veci_push(&s->model,(int)values[i]);
+                sat_solver_canceluntil(s,s->root_level);
+                veci_delete(&learnt_clause);
+
+                /*
+                veci apa; veci_new(&apa);
+                for (i = 0; i < s->size; i++) 
+                    veci_push(&apa,(int)(s->model.ptr[i] == l_True ? toLit(i) : lit_neg(toLit(i))));
+                printf("model: "); printlits((lit*)apa.ptr, (lit*)apa.ptr + veci_size(&apa)); printf("\n");
+                veci_delete(&apa);
+                */
+
+                return l_True;
+            }
+
+            if ( s->polarity[next] ) // positive polarity
+                sat_solver_assume(s,toLit(next));
+            else
+                sat_solver_assume(s,lit_neg(toLit(next)));
+        }
+    }
+
+    return l_Undef; // cannot happen
+}
+
+int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
+{
+    int restart_iter = 0;
+    ABC_INT64_T  nof_conflicts;
+    ABC_INT64_T  nof_learnts   = sat_solver_nclauses(s) / 3;
+    lbool   status        = l_Undef;
+    lbool*  values        = s->assigns;
+    lit*    i;
+
+    ////////////////////////////////////////////////
+    if ( s->fSolved )
+    {
+        if ( s->pStore )
+        {
+            int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, NULL, NULL );
+            assert( RetValue );
+        }
+        return l_False;
+    }
+    ////////////////////////////////////////////////
+
+    // set the external limits
+    s->nCalls++;
+    s->nRestarts  = 0;
+    s->nConfLimit = 0;
+    s->nInsLimit  = 0;
+    if ( nConfLimit )
+        s->nConfLimit = s->stats.conflicts + nConfLimit;
+    if ( nInsLimit )
+//        s->nInsLimit = s->stats.inspects + nInsLimit;
+        s->nInsLimit = s->stats.propagations + nInsLimit;
+    if ( nConfLimitGlobal && (s->nConfLimit == 0 || s->nConfLimit > nConfLimitGlobal) )
+        s->nConfLimit = nConfLimitGlobal;
+    if ( nInsLimitGlobal && (s->nInsLimit == 0 || s->nInsLimit > nInsLimitGlobal) )
+        s->nInsLimit = nInsLimitGlobal;
+
+#ifndef SAT_USE_ANALYZE_FINAL
+
+    //printf("solve: "); printlits(begin, end); printf("\n");
+    for (i = begin; i < end; i++){
+        switch (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]){
+        case 1: // l_True: 
+            break;
+        case 0: // l_Undef
+            sat_solver_assume(s, *i);
+            if (sat_solver_propagate(s) == NULL)
+                break;
+            // fallthrough
+        case -1: // l_False 
+            sat_solver_canceluntil(s, 0);
+            return l_False;
+        }
+    }
+    s->root_level = sat_solver_dl(s);
+
+#endif
+
+/*
+    // Perform assumptions:
+    root_level = assumps.size();
+    for (int i = 0; i < assumps.size(); i++){
+        Lit p = assumps[i];
+        assert(var(p) < nVars());
+        if (!sat_solver_assume(p)){
+            GClause r = reason[var(p)];
+            if (r != GClause_NULL){
+                Clause* confl;
+                if (r.isLit()){
+                    confl = propagate_tmpbin;
+                    (*confl)[1] = ~p;
+                    (*confl)[0] = r.lit();
+                }else
+                    confl = r.clause();
+                analyzeFinal(confl, true);
+                conflict.push(~p);
+            }else
+                conflict.clear(),
+                conflict.push(~p);
+            cancelUntil(0);
+            return false; }
+        Clause* confl = propagate();
+        if (confl != NULL){
+            analyzeFinal(confl), assert(conflict.size() > 0);
+            cancelUntil(0);
+            return false; }
+    }
+    assert(root_level == decisionLevel());
+*/
+
+#ifdef SAT_USE_ANALYZE_FINAL
+    // Perform assumptions:
+    s->root_level = end - begin;
+    for ( i = begin; i < end; i++ )
+    {
+        lit p = *i;
+        assert(lit_var(p) < s->size);
+        veci_push(&s->trail_lim,s->qtail);
+        if (!sat_solver_enqueue(s,p,(clause*)0))
+        {
+            clause * r = s->reasons[lit_var(p)];
+            if (r != NULL)
+            {
+                clause* confl;
+                if (clause_is_lit(r))
+                {
+                    confl = s->binary;
+                    (clause_begin(confl))[1] = lit_neg(p);
+                    (clause_begin(confl))[0] = clause_read_lit(r);
+                }
+                else
+                    confl = r;
+                sat_solver_analyze_final(s, confl, 1);
+                veci_push(&s->conf_final, lit_neg(p));
+            }
+            else
+            {
+                veci_resize(&s->conf_final,0);
+                veci_push(&s->conf_final, lit_neg(p));
+                // the two lines below are a bug fix by Siert Wieringa 
+                if (s->levels[lit_var(p)] > 0)
+                    veci_push(&s->conf_final, p);
+            }
+            sat_solver_canceluntil(s, 0);
+            return l_False; 
+        }
+        else
+        {
+            clause* confl = sat_solver_propagate(s);
+            if (confl != NULL){
+                sat_solver_analyze_final(s, confl, 0);
+                assert(s->conf_final.size > 0);
+                sat_solver_canceluntil(s, 0);
+                return l_False; }
+        }
+    }
+    assert(s->root_level == sat_solver_dl(s));
+#endif
+
+    s->nCalls2++;
+
+    if (s->verbosity >= 1){
+        printf("==================================[MINISAT]===================================\n");
+        printf("| Conflicts |     ORIGINAL     |              LEARNT              | Progress |\n");
+        printf("|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |\n");
+        printf("==============================================================================\n");
+    }
+
+    while (status == l_Undef){
+//        int nConfs = 0;
+        double Ratio = (s->stats.learnts == 0)? 0.0 :
+            s->stats.learnts_literals / (double)s->stats.learnts;
+        if ( s->nRuntimeLimit && time(NULL) > s->nRuntimeLimit )
+            break;
+
+        if (s->verbosity >= 1)
+        {
+            printf("| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %6.3f %% |\n", 
+                (double)s->stats.conflicts,
+                (double)s->stats.clauses, 
+                (double)s->stats.clauses_literals,
+                (double)nof_learnts, 
+                (double)s->stats.learnts, 
+                (double)s->stats.learnts_literals,
+                Ratio,
+                s->progress_estimate*100);
+            fflush(stdout);
+        }
+        nof_conflicts = (ABC_INT64_T)( 100 * luby(2, restart_iter++) );
+//printf( "%d ", (int)nof_conflicts );
+//        nConfs = s->stats.conflicts;
+        status = sat_solver_search(s, nof_conflicts, nof_learnts);
+//        if ( status == l_True )
+//            printf( "%d ", s->stats.conflicts - nConfs );
+
+//        nof_conflicts = nof_conflicts * 3 / 2; //*= 1.5;
+        nof_learnts    = nof_learnts * 11 / 10; //*= 1.1;
+//printf( "%d ", s->stats.conflicts  );
+        // quit the loop if reached an external limit
+        if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit )
+        {
+//            printf( "Reached the limit on the number of conflicts (%d).\n", s->nConfLimit );
+            break;
+        }
+//        if ( s->nInsLimit  && s->stats.inspects > s->nInsLimit )
+        if ( s->nInsLimit  && s->stats.propagations > s->nInsLimit )
+        {
+//            printf( "Reached the limit on the number of implications (%d).\n", s->nInsLimit );
+            break;
+        }
+        if ( s->nRuntimeLimit && time(NULL) > s->nRuntimeLimit )
+            break;
+    }
+//printf( "\n" );
+    if (s->verbosity >= 1)
+        printf("==============================================================================\n");
+
+    sat_solver_canceluntil(s,0);
+
+    ////////////////////////////////////////////////
+    if ( status == l_False && s->pStore )
+    {
+        int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, NULL, NULL );
+        assert( RetValue );
+    }
+    ////////////////////////////////////////////////
+    return status;
+}
+
+
+int sat_solver_nvars(sat_solver* s)
+{
+    return s->size;
+}
+
+
+int sat_solver_nclauses(sat_solver* s)
+{
+    return vecp_size(&s->clauses);
+}
+
+
+int sat_solver_nconflicts(sat_solver* s)
+{
+    return (int)s->stats.conflicts;
+}
+
+//=================================================================================================
+// Clause storage functions:
+
+void sat_solver_store_alloc( sat_solver * s )
+{
+    assert( s->pStore == NULL );
+    s->pStore = Sto_ManAlloc();
+}
+
+void sat_solver_store_write( sat_solver * s, char * pFileName )
+{
+    if ( s->pStore ) Sto_ManDumpClauses( (Sto_Man_t *)s->pStore, pFileName );
+}
+
+void sat_solver_store_free( sat_solver * s )
+{
+    if ( s->pStore ) Sto_ManFree( (Sto_Man_t *)s->pStore );
+    s->pStore = NULL;
+}
+
+int sat_solver_store_change_last( sat_solver * s )
+{
+    if ( s->pStore ) return Sto_ManChangeLastClause( (Sto_Man_t *)s->pStore );
+    return -1;
+}
+ 
+void sat_solver_store_mark_roots( sat_solver * s )
+{
+    if ( s->pStore ) Sto_ManMarkRoots( (Sto_Man_t *)s->pStore );
+}
+
+void sat_solver_store_mark_clauses_a( sat_solver * s )
+{
+    if ( s->pStore ) Sto_ManMarkClausesA( (Sto_Man_t *)s->pStore );
+}
+
+void * sat_solver_store_release( sat_solver * s )
+{
+    void * pTemp;
+    if ( s->pStore == NULL )
+        return NULL;
+    pTemp = s->pStore;
+    s->pStore = NULL;
+    return pTemp;
+}
+
+//=================================================================================================
+// 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_solver_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/satSolver_old.h b/src/sat/bsat/satSolver_old.h
new file mode 100644
index 00000000..4c577b1e
--- /dev/null
+++ b/src/sat/bsat/satSolver_old.h
@@ -0,0 +1,210 @@
+/**************************************************************************************************
+MiniSat -- Copyright (c) 2005, Niklas Sorensson
+http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko
+
+#ifndef satSolver_h
+#define satSolver_h
+
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+
+#include "satVec.h"
+#include "satMem.h"
+
+ABC_NAMESPACE_HEADER_START
+
+//#define USE_FLOAT_ACTIVITY
+
+//=================================================================================================
+// Public interface:
+
+struct sat_solver_t;
+typedef struct sat_solver_t sat_solver;
+
+extern sat_solver* sat_solver_new(void);
+extern void        sat_solver_delete(sat_solver* s);
+
+extern int         sat_solver_addclause(sat_solver* s, lit* begin, lit* end);
+extern int         sat_solver_simplify(sat_solver* s);
+extern int         sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal);
+extern void        sat_solver_rollback( sat_solver* s );
+
+extern int         sat_solver_nvars(sat_solver* s);
+extern int         sat_solver_nclauses(sat_solver* s);
+extern int         sat_solver_nconflicts(sat_solver* s);
+
+extern void        sat_solver_setnvars(sat_solver* s,int n);
+
+extern void        Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars );
+extern void        Sat_SolverPrintStats( FILE * pFile, sat_solver * p );
+extern int *       Sat_SolverGetModel( sat_solver * p, int * pVars, int nVars );
+extern void        Sat_SolverDoubleClauses( sat_solver * p, int iVar );
+
+// trace recording
+extern void        Sat_SolverTraceStart( sat_solver * pSat, char * pName );
+extern void        Sat_SolverTraceStop( sat_solver * pSat );
+extern void        Sat_SolverTraceWrite( sat_solver * pSat, int * pBeg, int * pEnd, int fRoot );
+
+// clause storage
+extern void        sat_solver_store_alloc( sat_solver * s );
+extern void        sat_solver_store_write( sat_solver * s, char * pFileName );
+extern void        sat_solver_store_free( sat_solver * s );
+extern void        sat_solver_store_mark_roots( sat_solver * s );
+extern void        sat_solver_store_mark_clauses_a( sat_solver * s );
+extern void *      sat_solver_store_release( sat_solver * s ); 
+
+//=================================================================================================
+// Solver representation:
+
+struct clause_t;
+typedef struct clause_t clause;
+
+struct sat_solver_t
+{
+    int      size;          // nof variables
+    int      cap;           // size of varmaps
+    int      qhead;         // Head index of queue.
+    int      qtail;         // Tail index of queue.
+
+    // clauses
+    vecp     clauses;       // List of problem constraints. (contains: clause*)
+    vecp     learnts;       // List of learnt clauses. (contains: clause*)
+
+    // activities
+#ifdef USE_FLOAT_ACTIVITY
+    double   var_inc;       // Amount to bump next variable with.
+    double   var_decay;     // INVERSE decay factor for variable activity: stores 1/decay. 
+    float    cla_inc;       // Amount to bump next clause with.
+    float    cla_decay;     // INVERSE decay factor for clause activity: stores 1/decay.
+    double*  activity;      // A heuristic measurement of the activity of a variable.
+#else
+    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.
+#endif
+
+    vecp*    wlists;        // 
+    lbool*   assigns;       // Current values of variables.
+    int*     orderpos;      // Index in variable order.
+    clause** reasons;       //
+    int*     levels;        //
+    lit*     trail;
+    char*    polarity;
+
+    clause*  binary;        // A temporary binary clause
+    lbool*   tags;          //
+    veci     tagged;        // (contains: var)
+    veci     stack;         // (contains: var)
+
+    veci     order;         // Variable order. (heap) (contains: var)
+    veci     trail_lim;     // Separator indices for different decision levels in 'trail'. (contains: int)
+    veci     model;         // If problem is solved, this vector contains the model (contains: lbool).
+    veci     conf_final;    // If problem is unsatisfiable (possibly under assumptions),
+                            // this vector represent the final conflict clause expressed in the assumptions.
+
+    int      root_level;    // Level of first proper decision.
+    int      simpdb_assigns;// Number of top-level assignments at last 'simplifyDB()'.
+    int      simpdb_props;  // Number of propagations before next 'simplifyDB()'.
+    double   random_seed;
+    double   progress_estimate;
+    int      verbosity;     // Verbosity level. 0=silent, 1=some progress report, 2=everything
+
+    stats_t    stats;
+
+    ABC_INT64_T   nConfLimit;    // external limit on the number of conflicts
+    ABC_INT64_T   nInsLimit;     // external limit on the number of implications
+    int           nRuntimeLimit; // external limit on runtime
+
+    veci     act_vars;      // variables whose activity has changed
+    double*  factors;       // the activity factors
+    int      nRestarts;     // the number of local restarts
+    int      nCalls;        // the number of local restarts
+    int      nCalls2;        // the number of local restarts
+ 
+    Sat_MmStep_t * pMem;
+
+    int      fSkipSimplify; // set to one to skip simplification of the clause database
+    int      fNotUseRandom; // do not allow random decisions with a fixed probability
+
+    int *    pGlobalVars;   // for experiments with global vars during interpolation
+    // clause store
+    void *   pStore;
+    int      fSolved;
+
+    // trace recording
+    FILE *   pFile;
+    int      nClauses;
+    int      nRoots;
+
+    veci     temp_clause;    // temporary storage for a CNF clause
+};
+
+static int sat_solver_var_value( sat_solver* s, int v ) 
+{
+    assert( s->model.ptr != NULL && v < s->size );
+    return (int)(s->model.ptr[v] == l_True);
+}
+static int sat_solver_var_literal( sat_solver* s, int v ) 
+{
+    assert( s->model.ptr != NULL && v < s->size );
+    return toLitCond( v, s->model.ptr[v] != l_True );
+}
+static void sat_solver_act_var_clear(sat_solver* s) 
+{
+    int i;
+    for (i = 0; i < s->size; i++)
+        s->activity[i] = 0.0;
+    s->var_inc = 1.0;
+}
+static void sat_solver_compress(sat_solver* s) 
+{
+    if ( s->qtail != s->qhead )
+    {
+        int RetValue = sat_solver_simplify(s);
+        assert( RetValue != 0 );
+    }
+}
+
+static int sat_solver_final(sat_solver* s, int ** ppArray)
+{
+    *ppArray = s->conf_final.ptr;
+    return s->conf_final.size;
+}
+
+static int sat_solver_set_runtime_limit(sat_solver* s, int Limit)
+{
+    int nRuntimeLimit = s->nRuntimeLimit;
+    s->nRuntimeLimit = Limit;
+    return nRuntimeLimit;
+}
+
+static int sat_solver_set_random(sat_solver* s, int fNotUseRandom)
+{
+    int fNotUseRandomOld = s->fNotUseRandom;
+    s->fNotUseRandom = fNotUseRandom;
+    return fNotUseRandomOld;
+}
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c
index 17a9ba4a..5e809172 100644
--- a/src/sat/bsat/satUtil.c
+++ b/src/sat/bsat/satUtil.c
@@ -58,6 +58,7 @@ static void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, int fIncreme
 ***********************************************************************/
 void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars )
 {
+/*
     FILE * pFile;
     void ** pClauses;
     int nClauses, i;
@@ -110,6 +111,7 @@ void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBe
 
     fprintf( pFile, "\n" );
     fclose( pFile );
+*/
 }   
 
 /**Function*************************************************************
@@ -273,6 +275,7 @@ int * Sat_Solver2GetModel( sat_solver2 * p, int * pVars, int nVars )
 ***********************************************************************/
 void Sat_SolverDoubleClauses( sat_solver * p, int iVar )
 {
+/*
     clause * pClause;
     lit Lit, * pLits;
     int RetValue, nClauses, nVarsOld, nLitsOld, nLits, c, v;
@@ -305,6 +308,7 @@ void Sat_SolverDoubleClauses( sat_solver * p, int iVar )
         for ( v = 0; v < nLits; v++ )
             pLits[v] -= nLitsOld;
     }
+*/
 }
 
 
diff --git a/src/sat/bsat/vecRec.h b/src/sat/bsat/vecRec.h
index d81cc631..fd0cc242 100644
--- a/src/sat/bsat/vecRec.h
+++ b/src/sat/bsat/vecRec.h
@@ -66,6 +66,9 @@ struct Vec_Rec_t_
     for ( c = 1; c <= p->nChunks; c++ )                \
         for ( s = 0; p->pChunks[c][s] && ((Handle) = (((c)<<16)|(s))); s += Size, assert(s < p->Mask) )
 
+#define Vec_RecForEachEntryStart( p, Size, Handle, c, s, hStart )   \
+    for ( c = Vec_RecChunk(hStart), s = Vec_RecShift(hStart); c <= p->nChunks; c++, s = 0 )                \
+        for ( ; p->pChunks[c][s] && ((Handle) = (((c)<<16)|(s))); s += Size, assert(s < p->Mask) )
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -97,6 +100,22 @@ static inline Vec_Rec_t * Vec_RecAlloc()
     p->pChunks[1][0] = 0;
     return p;
 }
+static inline void Vec_RecAlloc_( Vec_Rec_t * p )
+{
+//    Vec_Rec_t * p;
+//    p = ABC_CALLOC( Vec_Rec_t, 1 );
+    memset( p, 0, sizeof(Vec_Rec_t) );
+    p->LogSize       = 15; // chunk size = 2^15 ints = 128 Kb
+    p->Mask          = (1 << p->LogSize) - 1;
+    p->hCurrent      = (1 << 16);
+    p->nChunks       = 1;
+    p->nChunksAlloc  = 16;
+    p->pChunks       = ABC_CALLOC( int *, p->nChunksAlloc );
+    p->pChunks[0]    = NULL;
+    p->pChunks[1]    = ABC_ALLOC( int, (1 << 16) );
+    p->pChunks[1][0] = 0;
+//    return p;
+}
 
 /**Function*************************************************************
 
@@ -239,6 +258,14 @@ static inline void Vec_RecFree( Vec_Rec_t * p )
     ABC_FREE( p->pChunks );
     ABC_FREE( p );
 }
+static inline void Vec_RecFree_( Vec_Rec_t * p )
+{
+    int i;
+    for ( i = 0; i < p->nChunksAlloc; i++ )
+        ABC_FREE( p->pChunks[i] );
+    ABC_FREE( p->pChunks );
+//    ABC_FREE( p );
+}
 
 /**Function*************************************************************