Proof-logging in the updated solver.

5 files changed, 481 insertions, 216 deletions

diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index ff5e6e3d..f500b46b 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -113,8 +113,8 @@ extern void *      sat_solver_store_release( sat_solver * s );
 //=================================================================================================
 // Solver representation:
 
-//struct clause_t;
-//typedef struct clause_t clause;
+struct clause_t;
+typedef struct clause_t clause;
 
 struct sat_solver_t
 {
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index 5cb62cf6..405e4367 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -38,7 +38,7 @@ ABC_NAMESPACE_IMPL_START
 
 // For derivation output (verbosity level 2)
 #define L_IND    "%-*d"
-#define L_ind    sat_solver2_dlevel(s)*3+3,sat_solver2_dlevel(s)
+#define L_ind    solver2_dlevel(s)*3+3,solver2_dlevel(s)
 #define L_LIT    "%sx%d"
 #define L_lit(p) lit_sign(p)?"~":"", (lit_var(p))
 static void printlits(lit* begin, lit* end)
@@ -65,6 +65,8 @@ 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:
@@ -80,46 +82,88 @@ static const int varX  = 3;
 
 struct varinfo_t
 {
-    unsigned val    :  2; 
-    unsigned pol    :  1;
-    unsigned mark   :  1;
-    unsigned tag    :  3;
-    unsigned lev    : 25;
+    unsigned val    :  2;  // variable value 
+    unsigned pol    :  1;  // last polarity
+    unsigned tag    :  3;  // conflict analysis tags
+    unsigned lev    : 26;  // variable level
 };
 
-static inline int     var_value     (sat_solver2 * s, int v)            { return s->vi[v].val;                          }
-static inline int     var_polar     (sat_solver2 * s, int v)            { return s->vi[v].pol;                          }
-static inline int     var_tag       (sat_solver2 * s, int v)            { return s->vi[v].tag;                          }
-static inline int     var_mark      (sat_solver2 * s, int v)            { return s->vi[v].mark;                         }
-static inline int     var_level     (sat_solver2 * s, int v)            { return s->vi[v].lev;                          }
+static inline int     var_value     (sat_solver2* s, int v)            { return s->vi[v].val;                          }
+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_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;                          }
+static inline void    var_set_tag   (sat_solver2* s, int v, int tag)   { 
+    assert( tag > 0 && tag < 16 );
+    if ( s->vi[v].tag == 0 )
+        veci_push( &s->tagged, v );
+    s->vi[v].tag = tag;                           
+}
+static inline void    var_add_tag   (sat_solver2* s, int v, int tag)   { 
+    assert( tag > 0 && tag < 16 );
+    if ( s->vi[v].tag == 0 )
+        veci_push( &s->tagged, v );
+    s->vi[v].tag |= tag;                           
+}
+static inline void    solver2_clear_tags(sat_solver2* s, int start)    { 
+    int i, * tagged = veci_begin(&s->tagged);
+    for (i = start; i < veci_size(&s->tagged); i++)
+        s->vi[tagged[i]].tag = 0;
+    veci_resize(&s->tagged,start);
+}
 
-static inline void    var_set_value (sat_solver2 * s, int v, int val )  { s->vi[v].val = val;                           }
-static inline void    var_set_polar (sat_solver2 * s, int v, int pol )  { s->vi[v].pol = pol;                           }
-static inline void    var_set_tag   (sat_solver2 * s, int v, int tag )  { s->vi[v].tag = tag;                           }
-static inline void    var_set_mark  (sat_solver2 * s, int v, int mark)  { s->vi[v].mark = mark;                         }
-static inline void    var_set_level (sat_solver2 * s, int v, int lev )  { s->vi[v].lev = lev;                           }
+// level marks
+static inline int     var_lev_mark (sat_solver2* s, int v)             { 
+    return (veci_begin(&s->trail_lim)[var_level(s,v)] & 0x80000000) > 0;   
+}
+static inline void    var_lev_set_mark (sat_solver2* s, int v)         { 
+    int level = var_level(s,v);
+    assert( level < veci_size(&s->trail_lim) );
+    veci_begin(&s->trail_lim)[level] |= 0x80000000;
+    veci_push(&s->mark_levels, level);
+}
+static inline void    solver2_clear_marks(sat_solver2* s)              { 
+    int i, * mark_levels = veci_begin(&s->mark_levels);
+    for (i = 0; i < veci_size(&s->mark_levels); i++)
+        veci_begin(&s->trail_lim)[mark_levels[i]] &= 0x7FFFFFFF;
+    veci_resize(&s->mark_levels,0);
+}
+
+// other inlines
+//static inline int     var_reason    (sat_solver2* s, int v)            { return (s->reasons[v]&1) ? 0 : s->reasons[v];                   } 
+//static inline int     lit_reason    (sat_solver2* s, int l)            { return (s->reasons[lit_var(l)&1]) ? 0 : s->reasons[lit_var(l)]; } 
+static inline int     var_reason    (sat_solver2* s, int v)            { return s->reasons[v]; } 
+static inline int     lit_reason    (sat_solver2* s, int l)            { return s->reasons[lit_var(l)]; } 
 
 //=================================================================================================
 // Clause datatype + minor functions:
 
-struct clause_t // should have even number of entries!
+typedef struct satset_t satset;
+struct satset_t // should have even number of entries!
 {
     unsigned learnt :  1;
-    unsigned fMark  :  1;
-    unsigned fPartA :  1;
-    unsigned fRefed :  1;
-    unsigned nLits  : 28;
+    unsigned mark   :  1;
+    unsigned partA  :  1;
+    unsigned nLits  : 29;
     int      Id;
-    lit lits[0];
+    lit      pLits[0];
 };
 
-static inline lit*    clause_begin  (clause* c)                  { return c->lits;                                 }
-static inline int     clause_learnt (clause* c)                  { return c->learnt;                               }
-static inline int     clause_nlits  (clause* c)                  { return c->nLits;                                }
-static inline int     clause_size   (int nLits)                  { return sizeof(clause)/4 + nLits + (nLits & 1);  }
+static inline lit*    clause_begin  (satset* c)                  { return c->pLits;                                }
+static inline int     clause_learnt (satset* c)                  { return c->learnt;                               }
+static inline int     clause_nlits  (satset* c)                  { return c->nLits;                                }
+static inline int     clause_size   (int nLits)                  { return sizeof(satset)/4 + nLits + (nLits & 1);  }
 
-static inline clause* get_clause    (sat_solver2* s, int c)      { return (clause *)(s->pMemArray + c);            }
-static inline cla     clause_id     (sat_solver2* s, clause* c)  { return (cla)((int *)c - s->pMemArray);          }
+static inline satset* get_clause    (sat_solver2* s, int c)      { return c ? (satset*)(veci_begin(&s->clauses) + c) : NULL;  }
+static inline cla     clause_id     (sat_solver2* s, satset* c)  { return (cla)((int *)c - veci_begin(&s->clauses));          }
+
+static inline satset* var_unit_clause(sat_solver2* s, int v)           { return (s->reasons[v]&1) ? get_clause(s, s->reasons[v] >> 1) : NULL;  } 
+static inline void    var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(i && !s->reasons[v]); s->reasons[v] = (i << 1) | 1;            } 
 
 #define sat_solver_foreach_clause( s, c, i )  \
     for ( i = 16; (i < s->nMemSize) && (((c) = get_clause(s, i)), 1); i += clause_size(c->nLits) )
@@ -127,17 +171,55 @@ static inline cla     clause_id     (sat_solver2* s, clause* c)  { return (cla)(
     for ( i = s->iLearnt; (i < s->nMemSize) && (((c) = get_clause(s, i)), 1); i += clause_size(c->nLits) )
 
 //=================================================================================================
+// Proof logging:
+
+static inline void proof_chain_start( sat_solver2* s, satset* c )
+{
+    if ( s->fProofLogging )
+    {
+        s->iStartChain = veci_size(&s->proof_clas);
+        veci_push(&s->proof_clas, 0);
+        veci_push(&s->proof_clas, 0);
+        veci_push(&s->proof_clas, c->learnt ? veci_begin(&s->claProofs)[c->Id] : clause_id(s,c) ^ 1 );
+        veci_push(&s->proof_vars, 0);
+        veci_push(&s->proof_vars, 0);
+        veci_push(&s->proof_vars, 0);
+    }
+}
+
+static inline void proof_chain_resolve( sat_solver2* s, satset* c, int Var )
+{
+    if ( s->fProofLogging && c )
+    {
+        veci_push(&s->proof_clas, c->learnt ? veci_begin(&s->claProofs)[c->Id] : clause_id(s,c) ^ 1 );
+        veci_push(&s->proof_vars, Var);
+    }
+}
+
+static inline void proof_chain_stop( sat_solver2* s )
+{
+    if ( s->fProofLogging )
+    {
+        satset* c = (satset*)(veci_begin(&s->proof_clas) + s->iStartChain);
+        assert( s->iStartChain > 0 && s->iStartChain < veci_size(&s->proof_clas) );
+        c->nLits = veci_size(&s->proof_clas) - s->iStartChain - 2;
+        s->iStartChain = 0;
+//        printf( "%d ", c->nLits );
+    }
+}
+
+//=================================================================================================
 // Simple helpers:
 
-static inline int     sat_solver2_dlevel(sat_solver2* s)            { return veci_size(&s->trail_lim); }
-static inline veci*   sat_solver2_read_wlist(sat_solver2* s, lit l) { return &s->wlists[l]; }
+static inline int     solver2_dlevel(sat_solver2* s)       { return veci_size(&s->trail_lim); }
+static inline veci*   solver2_wlist(sat_solver2* s, lit l) { return &s->wlists[l];            }
 
 //=================================================================================================
 // Clause functions:
 
 static int clause_new(sat_solver2* s, lit* begin, lit* end, int learnt)
 {
-    clause* c;
+    satset* c;
     int i, Cid, nLits = end - begin;
     assert(nLits > 1);
     assert(begin[0] >= 0);
@@ -145,44 +227,43 @@ static int clause_new(sat_solver2* s, lit* begin, lit* end, int learnt)
     assert(lit_var(begin[0]) < s->size);
     assert(lit_var(begin[1]) < s->size);
     // add memory if needed
-    if ( s->nMemSize + clause_size(nLits) > s->nMemAlloc )
+    if ( veci_size(&s->clauses) + clause_size(nLits) > s->clauses.cap )
     {
-        int nMemAlloc = s->nMemAlloc ? s->nMemAlloc * 2 : (1 << 24);
-        s->pMemArray  = ABC_REALLOC( int, s->pMemArray, nMemAlloc );
-        memset( s->pMemArray + s->nMemAlloc, 0, sizeof(int) * (nMemAlloc - s->nMemAlloc) );
-        printf( "Reallocing from %d to %d...\n", s->nMemAlloc, nMemAlloc );
-        s->nMemAlloc = nMemAlloc;
-        s->nMemSize = Abc_MaxInt( s->nMemSize, 16 ); 
+        int nMemAlloc = s->clauses.cap ? 2 * s->clauses.cap : (1 << 20);
+        s->clauses.ptr = ABC_REALLOC( int, veci_begin(&s->clauses), nMemAlloc );
+        memset( veci_begin(&s->clauses) + s->clauses.cap, 0, sizeof(int) * (nMemAlloc - s->clauses.cap) );
+//        printf( "Reallocing from %d to %d...\n", s->clauses.cap, nMemAlloc );
+        s->clauses.cap = nMemAlloc;
+        s->clauses.size = Abc_MaxInt( veci_size(&s->clauses), 2 ); 
     }
     // create clause
-    c = (clause*)(s->pMemArray + s->nMemSize);
+    c = (satset*)(veci_begin(&s->clauses) + veci_size(&s->clauses));
     c->learnt = learnt;
     c->nLits  = nLits;
     for (i = 0; i < nLits; i++)
-        c->lits[i] = begin[i];
+        c->pLits[i] = begin[i];
     // assign clause ID
     if ( learnt )
     {
         c->Id = s->stats.learnts + 1;
         assert( c->Id == veci_size(&s->claActs) );
         veci_push(&s->claActs, 0);
+        //veci_push(&s->claProof, 0);
     }
     else
-    {
-        c->Id = -(s->stats.clauses + 1);
-    }
+        c->Id = s->stats.clauses + 1;
 
     // extend storage
-    Cid = s->nMemSize;
-    s->nMemSize += clause_size(nLits);
-    if ( s->nMemSize > s->nMemAlloc )
+    Cid = veci_size(&s->clauses);
+    s->clauses.size += clause_size(nLits);
+    if ( veci_size(&s->clauses) > s->clauses.cap )
         printf( "Out of memory!!!\n" );
-    assert( s->nMemSize <= s->nMemAlloc );
+    assert( veci_size(&s->clauses) <= s->clauses.cap );
     assert(((ABC_PTRUINT_T)c & 7) == 0);
 
     // watch the clause
-    veci_push(sat_solver2_read_wlist(s,lit_neg(begin[0])),clause_id(s,c));
-    veci_push(sat_solver2_read_wlist(s,lit_neg(begin[1])),clause_id(s,c));
+    veci_push(solver2_wlist(s,lit_neg(begin[0])),clause_id(s,c));
+    veci_push(solver2_wlist(s,lit_neg(begin[1])),clause_id(s,c));
 
     // remember the last one and first learnt
     s->iLast = Cid;
@@ -284,56 +365,85 @@ static inline int  order_select(sat_solver2* s, float random_var_freq) // select
 //=================================================================================================
 // Activity functions:
 
-static inline void act_var_rescale(sat_solver2* s) {
-    unsigned* activity = s->activity;
-    int i, clk = clock();
-    static int Total = 0;
+#ifdef USE_FLOAT_ACTIVITY
+
+static inline void act_var_rescale(sat_solver2* s)  {
+    double* activity = s->activity;
+    int i;
     for (i = 0; i < s->size; i++)
-        activity[i] >>= 19;
-    s->var_inc >>= 19;
-//    assert( s->var_inc > 15 );
-    s->var_inc = Abc_MaxInt( s->var_inc, (1<<4) );
-//    printf( "Rescaling... Var inc = %5d  Conf = %10d ", s->var_inc,  s->stats.conflicts );
-    Total += clock() - clk;
-//    Abc_PrintTime( 1, "Time", Total );
+        activity[i] *= 1e-100;
+    s->var_inc *= 1e-100;
 }
+static inline void act_clause_rescale(sat_solver2* s) {
+    static int Total = 0;
+    float * claActs = (float *)veci_begin(&s->claActs);
+    int i, clk = clock();
+    for (i = 0; i < veci_size(&s->claActs); i++)
+        claActs[i] *= (float)1e-20;
+    s->cla_inc *= (float)1e-20;
 
+    printf( "Rescaling...   Cla inc = %10.3f  Conf = %10d   ", s->cla_inc,  s->stats.conflicts );
+    Total += clock() - clk;
+    Abc_PrintTime( 1, "Time", Total );
+}
 static inline void act_var_bump(sat_solver2* s, int v) {
-    static int Counter = 0;
     s->activity[v] += s->var_inc;
-    if (s->activity[v] & 0x80000000)
+    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_solver2* s, satset*c) {
+    float * claActs = (float *)veci_begin(&s->claActs);
+    assert( c->Id < veci_size(&s->claActs) );
+    claActs[c->Id] += s->cla_inc;
+    if (claActs[c->Id] > (float)1e20) 
+        act_clause_rescale(s);
+}
+static inline void act_var_decay(sat_solver2* s)    { s->var_inc *= s->var_decay; }
+static inline void act_clause_decay(sat_solver2* s) { s->cla_inc *= s->cla_decay; }
 
-//static inline void act_var_decay(sat_solver2* s) { s->var_inc *= s->var_decay; }
-static inline void act_var_decay(sat_solver2* s) { s->var_inc += (s->var_inc >> 4); }
+#else
 
+static inline void act_var_rescale(sat_solver2* 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_solver2* s) {
     static int Total = 0;
     int i, clk = clock();
-    unsigned * tagged = (unsigned *)veci_begin(&s->claActs);
+    unsigned * claActs = (unsigned *)veci_begin(&s->claActs);
     for (i = 1; i < veci_size(&s->claActs); i++)
-        tagged[i] >>= 14;
+        claActs[i] >>= 14;
     s->cla_inc >>= 14;
-//    assert( s->cla_inc > (1<<10)-1 );
     s->cla_inc = Abc_MaxInt( s->cla_inc, (1<<10) );
-    printf( "Rescaling... Cla inc = %5d  Conf = %10d   ", s->cla_inc,  s->stats.conflicts );
+
+    printf( "Rescaling...   Cla inc = %5d  Conf = %10d   ", s->cla_inc,  s->stats.conflicts );
     Total += clock() - clk;
     Abc_PrintTime( 1, "Time", Total );
 }
-
-static inline void act_clause_bump(sat_solver2* s, clause *c) {
+static inline void act_var_bump(sat_solver2* 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_clause_bump(sat_solver2* s, satset*c) {
+    unsigned * claActs = (unsigned *)veci_begin(&s->claActs);
     assert( c->Id > 0 && c->Id < veci_size(&s->claActs) );
-    ((unsigned *)veci_begin(&s->claActs))[c->Id] += s->cla_inc;
-    if (((unsigned *)veci_begin(&s->claActs))[c->Id] & 0x80000000) 
+    claActs[c->Id] += s->cla_inc;
+    if (claActs[c->Id] & 0x80000000) 
         act_clause_rescale(s);
 }
-
-//static inline void act_clause_decay(sat_solver2* s) { s->cla_inc *= s->cla_decay; }
+static inline void act_var_decay(sat_solver2* s)    { s->var_inc += (s->var_inc >>  4); }
 static inline void act_clause_decay(sat_solver2* s) { s->cla_inc += (s->cla_inc >> 10); }
 
+#endif
 
 //=================================================================================================
 // Minor (solver) functions:
@@ -352,7 +462,7 @@ static inline int enqueue(sat_solver2* s, lit l, int from)
         printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(l));
 #endif
         var_set_value( s, v, lit_sign(l) );
-        var_set_level( s, v, sat_solver2_dlevel(s) );
+        var_set_level( s, v, solver2_dlevel(s) );
         s->reasons[v] = from;
         s->trail[s->qtail++] = l;
         order_assigned(s, v);
@@ -377,7 +487,7 @@ static void sat_solver2_canceluntil(sat_solver2* s, int level) {
     int      lastLev;
     int      c, x;
    
-    if (sat_solver2_dlevel(s) <= level)
+    if (solver2_dlevel(s) <= level)
         return;
 
     trail   = s->trail;
@@ -440,7 +550,7 @@ static double sat_solver2_progress(sat_solver2* s)
 |    stores the result in 'out_conflict'.
 |________________________________________________________________________________________________@*/
 /*
-void Solver::analyzeFinal(Clause* confl, bool skip_first)
+void Solver::analyzeFinal(satset* confl, bool skip_first)
 {
     // -- NOTE! This code is relatively untested. Please report bugs!
     conflict.clear();
@@ -481,102 +591,166 @@ void Solver::analyzeFinal(Clause* confl, bool skip_first)
 
 #ifdef SAT_USE_ANALYZE_FINAL
 
-static void sat_solver2_analyze_final(sat_solver2* s, clause* conf, int skip_first)
+static void sat_solver2_analyze_final(sat_solver2* s, satset* conf, int skip_first)
 {
-    int* tagged;
-    int i, j, start;
+    int i, j, start, x;
     veci_resize(&s->conf_final,0);
     if ( s->root_level == 0 )
         return;
     assert( veci_size(&s->tagged) == 0 );
     for (i = skip_first ? 1 : 0; i < clause_nlits(conf); i++)
     {
-        int x = lit_var(clause_begin(conf)[i]);
+        x = lit_var(clause_begin(conf)[i]);
         if ( var_level(s,x) )
-        {
             var_set_tag(s, x, 1);
-            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->vi[x].tag == 1){
-            if (s->reasons[x] == 0){
-                assert( var_level(s,x) );
-                veci_push(&s->conf_final,lit_neg(s->trail[i]));
-            }else{
-                clause* c = get_clause(s, s->reasons[x]);
+        x = lit_var(s->trail[i]);
+        if (var_tag(s,x)){
+            satset* c = get_clause(s, var_reason(s,x));
+            if (c){
                 int* lits = clause_begin(c);
                 for (j = 1; j < clause_nlits(c); j++)
                     if ( var_level(s,lit_var(lits[j])) )
-                    {
                         var_set_tag(s, lit_var(lits[j]), 1);
-                        veci_push(&s->tagged,lit_var(lits[j]));
-                    }
+            }else {
+                assert( var_level(s,x) );
+                veci_push(&s->conf_final,lit_neg(s->trail[i]));
             }
         }
     }
-    tagged = veci_begin(&s->tagged);
-    for (i = 0; i < veci_size(&s->tagged); i++)
-        var_set_tag(s, tagged[i], 0);
-    veci_resize(&s->tagged,0);
+    solver2_clear_tags(s,0);
 }
 
 #endif
 
 
-static int sat_solver2_lit_removable(sat_solver2* s, lit l, int minl)
+static int sat_solver2_lit_removable_rec(sat_solver2* s, int v)
 {
-    clause* c;
-    lit* lits;
-    int i, j, v, top = veci_size(&s->tagged);
-    assert(lit_var(l) >= 0 && lit_var(l) < s->size);
-    assert(s->reasons[lit_var(l)] != 0);
+    // tag[0]: True if original conflict clause literal.
+    // tag[1]: Processed by this procedure
+    // tag[2]: 0=non-removable, 1=removable
+
+    satset* c;
+    int i, x;
+
+    // skip visited
+    if (var_tag(s,v) & 2)
+        return (var_tag(s,v) & 4) > 0;
+
+    // skip decisions on a wrong level
+    c = get_clause(s, var_reason(s,v));
+    if ( c == NULL ){
+        var_add_tag(s,v,2);
+        return 0;
+    }
+
+    for ( i = 1; i < (int)c->nLits; i++ ){
+        x = lit_var(c->pLits[i]);
+        if (var_tag(s,x) & 1)
+            sat_solver2_lit_removable_rec(s, x);
+        else{
+            if (var_level(s,x) == 0 || var_tag(s,x) == 6) continue;     // -- 'x' checked before, found to be removable (or belongs to the toplevel)
+            if (var_tag(s,x) == 2 || !var_lev_mark(s,x) || !sat_solver2_lit_removable_rec(s, x))
+            {  // -- 'x' checked before, found NOT to be removable, or it belongs to a wrong level, or cannot be removed
+                var_add_tag(s,v,2); 
+                return 0; 
+            }
+        }
+    }
+//    if (pfl && visit[p0] & 1){
+//        result.push(p0); }
+    var_add_tag(s,v,6);
+    return 1;
+}
+
+static int sat_solver2_lit_removable(sat_solver2* s, int x)
+{
+    satset* c;
+    int i, top;
+    if ( !var_reason(s,x) )
+        return 0;
+    if ( var_tag(s,x) & 2 )
+    {
+        assert( var_tag(s,x) & 1 );
+        return 1;
+    }
+    top = veci_size(&s->tagged);
     veci_resize(&s->stack,0);
-    veci_push(&s->stack,lit_var(l));
-    while (veci_size(&s->stack) > 0)
+    veci_push(&s->stack, x << 1);
+    while (veci_size(&s->stack))
     {
-        v = veci_begin(&s->stack)[veci_size(&s->stack)-1];
-        assert(v >= 0 && v < s->size);
-        veci_resize(&s->stack,veci_size(&s->stack)-1);
-        assert(s->reasons[v] != 0);
-        c = get_clause(s, s->reasons[v]);
-        lits = clause_begin(c);
-        for (i = 1; i < clause_nlits(c); i++){
-            int v = lit_var(lits[i]);
-            if (s->vi[v].tag == 0 && var_level(s,v)){
-                if (s->reasons[v] != 0 && ((1 << (var_level(s,v) & 31)) & minl)){
-                    veci_push(&s->stack,lit_var(lits[i]));
-                    var_set_tag(s, v, 1);
-                    veci_push(&s->tagged,v);
-                }else{
-                    int* tagged = veci_begin(&s->tagged);
-                    for (j = top; j < veci_size(&s->tagged); j++)
-                        var_set_tag(s, tagged[j], 0);
-                    veci_resize(&s->tagged,top);
-                    return false;
-                }
+        x = veci_pop(&s->stack);
+        if ( s->fProofLogging ){
+            if ( x & 1 ){
+                if ( var_tag(s,x >> 1) & 1 )
+                    veci_push(&s->min_lit_order, x >> 1 );
+                continue;
             }
+            veci_push(&s->stack, x ^ 1 );
+        }
+        x >>= 1;
+        c = get_clause(s, var_reason(s,x));
+        for (i = 1; i < (int)c->nLits; i++){
+            x = lit_var(c->pLits[i]);
+            if (var_tag(s,x) || !var_level(s,x))
+                continue;
+            if (!var_reason(s,x) || !var_lev_mark(s,x)){
+                solver2_clear_tags(s, top);
+                return 0;
+            }
+            veci_push(&s->stack, x << 1);
+            var_set_tag(s, x, 2);
         }
     }
-    return true;
+    return 1;
 }
 
-static void sat_solver2_analyze(sat_solver2* s, clause* c, veci* learnt)
+static void sat_solver2_logging_order(sat_solver2* s, int x)
 {
-    lit*     trail   = s->trail;
-    int      cnt     = 0;
-    lit      p       = lit_Undef;
-    int      ind     = s->qtail-1;
-    lit*     lits;
-    int      i, j, minl;
-    int*     tagged;
-    assert( veci_size(&s->tagged) == 0 );
+    satset* c;
+    int i;
+    if ( (var_tag(s,x) & 4) )
+        return;
+    var_add_tag(s, x, 4);
+    veci_resize(&s->stack,0);
+    veci_push(&s->stack,x << 1);
+    while (veci_size(&s->stack))
+    {
+        x = veci_pop(&s->stack);
+        if ( x & 1 ){
+            veci_push(&s->min_step_order, x >> 1 );
+            continue;
+        }
+        veci_push(&s->stack, x ^ 1 );
+        x >>= 1;
+        c = get_clause(s, var_reason(s,x));
+//        if ( !c )
+//            printf( "sat_solver2_logging_order(): Error in conflict analysis!!!\n" );
+        for (i = 1; i < (int)c->nLits; i++){
+            x = lit_var(c->pLits[i]);
+            if ( !var_level(s,x) || (var_tag(s,x) & 1) )
+                continue;
+            veci_push(&s->stack, x << 1);
+            var_add_tag(s, x, 4);
+        }
+    }
+}
 
+static void sat_solver2_analyze(sat_solver2* s, satset* c, veci* learnt)
+{
+    int  cnt     = 0;
+    lit  p       = lit_Undef;
+    int  x, ind  = s->qtail-1;
+    lit* lits,* vars, i, j, k;
+    assert( veci_size(&s->tagged) == 0 );
+    // tag[0] - visited by conflict analysis (afterwards: literals of the learned clause)
+    // tag[1] - visited by sat_solver2_lit_removable() with success
+    // tag[2] - visited by sat_solver2_logging_order()
+/*
+    proof_chain_start( s, c );
     veci_push(learnt,lit_Undef);
-
     do{
         assert(c != 0);
         if (clause_learnt(c))
@@ -588,46 +762,107 @@ static void sat_solver2_analyze(sat_solver2* s, clause* c, veci* learnt)
             assert(lit_var(q) >= 0 && lit_var(q) < s->size);
             if (!var_tag(s, lit_var(q)) && var_level(s,lit_var(q))){
                 var_set_tag(s, lit_var(q), 1);
-                veci_push(&s->tagged,lit_var(q));
                 act_var_bump(s,lit_var(q));
-                if (var_level(s,lit_var(q)) == sat_solver2_dlevel(s))
+                if (var_level(s,lit_var(q)) == solver2_dlevel(s))
                     cnt++;
                 else
                     veci_push(learnt,q);
             }
         }
 
-        while (!var_tag(s, lit_var(trail[ind--])));
+        while (!var_tag(s, lit_var(s->trail[ind--])));
 
-        p = trail[ind+1];
-        c = get_clause(s, s->reasons[lit_var(p)]);
+        p = s->trail[ind+1];
+        c = get_clause(s, lit_reason(s,p));
         cnt--;
 
     }while (cnt > 0);
+    *veci_begin(learnt) = lit_neg(p);
+*/
 
+    proof_chain_start( s, c );
+    veci_push(learnt,lit_Undef);
+    while ( 1 ){
+        assert(c != 0);
+        if (clause_learnt(c))
+            act_clause_bump(s,c);
+        for ( j = (int)(p != lit_Undef); j < (int)c->nLits; j++){
+            x = lit_var(c->pLits[j]);
+            assert(x >= 0 && x < s->size);
+            if ( var_tag(s, x) )
+                continue;
+            if ( var_level(s,x) == 0 )
+            {
+                proof_chain_resolve( s, var_unit_clause(s, x), x );
+                continue;
+            }
+            var_set_tag(s, x, 1);
+            act_var_bump(s,x);
+            if (var_level(s,x) == solver2_dlevel(s))
+                cnt++;
+            else
+                veci_push(learnt,c->pLits[j]);
+        }
+
+        while (!var_tag(s, lit_var(s->trail[ind--])));
+
+        p = s->trail[ind+1];
+        c = get_clause(s, lit_reason(s,p));
+        cnt--;
+        if ( cnt == 0 )
+            break;
+        proof_chain_resolve( s, c, lit_var(p) );
+    }
     *veci_begin(learnt) = lit_neg(p);
 
+    // mark levels
+    assert( veci_size(&s->mark_levels) == 0 );
     lits = veci_begin(learnt);
-    minl = 0;
     for (i = 1; i < veci_size(learnt); i++)
-        minl |= 1 << (var_level(s,lit_var(lits[i])) & 31);
+        var_lev_set_mark(s, lit_var(lits[i]));
 
     // simplify (full)
+    veci_resize(&s->min_lit_order, 0);
     for (i = j = 1; i < veci_size(learnt); i++){
-        if (s->reasons[lit_var(lits[i])] == 0 || !sat_solver2_lit_removable(s,lits[i],minl))
+//        if (!sat_solver2_lit_removable_rec(s,lit_var(lits[i]))) // changed to vars!!!
+        if (!sat_solver2_lit_removable( s,lit_var(lits[i])) )
             lits[j++] = lits[i];
+    } 
+
+    // record the proof
+    if ( s->fProofLogging )
+    {
+        // collect additional clauses to resolve
+        veci_resize(&s->min_step_order, 0);
+        vars = veci_begin(&s->min_lit_order);
+        for (i = 0; i < veci_size(&s->min_lit_order); i++)
+            sat_solver2_logging_order( s, vars[i] );
+
+        // add them in the reverse order
+        vars = veci_begin(&s->min_step_order);
+        for (i = veci_size(&s->min_step_order); i > 0; ) { i--;
+            c = get_clause(s, var_reason(s,vars[i]));
+            proof_chain_resolve( s, c, vars[i] );
+            for ( k = 1; k < (int)c->nLits; k++ )
+            {
+                x = lit_var(c->pLits[k]);
+                if ( var_level(s,x) == 0 )
+                    proof_chain_resolve( s, var_unit_clause(s, x), x );
+            }
+        }
+        proof_chain_stop( s );
     }
 
+    // unmark levels
+    solver2_clear_marks( s );
+
     // update size of learnt + statistics
     s->stats.max_literals += veci_size(learnt);
     veci_resize(learnt,j);
     s->stats.tot_literals += j;
 
     // clear tags
-    tagged = veci_begin(&s->tagged);
-    for (i = 0; i < veci_size(&s->tagged); i++)
-        var_set_tag(s, tagged[i], 0);
-    veci_resize(&s->tagged,0);
+    solver2_clear_tags(s,0);
 
 #ifdef DEBUG
     for (i = 0; i < s->size; i++)
@@ -660,16 +895,16 @@ static void sat_solver2_analyze(sat_solver2* s, clause* c, veci* learnt)
 #endif
 }
 
-clause* sat_solver2_propagate(sat_solver2* s)
+satset* sat_solver2_propagate(sat_solver2* s)
 {
-    clause * c, * confl  = NULL;
+    satset* c, * confl  = NULL;
     veci* ws;
     lit* lits, false_lit, p, * stop, * k;
     cla* begin,* end, *i, *j;
 
     while (confl == 0 && s->qtail - s->qhead > 0){
         p  = s->trail[s->qhead++];
-        ws = sat_solver2_read_wlist(s,p);
+        ws = solver2_wlist(s,p);
         begin = (cla*)veci_begin(ws);
         end   = begin + veci_size(ws);
 
@@ -703,7 +938,7 @@ clause* sat_solver2_propagate(sat_solver2* s)
                         if (var_value(s, lit_var(*k)) != !lit_sign(*k)){
                             lits[1] = *k;
                             *k = false_lit;
-                            veci_push(sat_solver2_read_wlist(s,lit_neg(lits[1])),*i);
+                            veci_push(solver2_wlist(s,lit_neg(lits[1])),*i);
                             goto next; }
                     }
 
@@ -729,14 +964,14 @@ next:       i++;
 
 
 
-static void clause_remove(sat_solver2* s, clause* c)
+static void clause_remove(sat_solver2* s, satset* c)
 {
     lit* lits = clause_begin(c);
     assert(lit_neg(lits[0]) < s->size*2);
     assert(lit_neg(lits[1]) < s->size*2);
 
-    veci_remove(sat_solver2_read_wlist(s,lit_neg(lits[0])),clause_id(s,c));
-    veci_remove(sat_solver2_read_wlist(s,lit_neg(lits[1])),clause_id(s,c));
+    veci_remove(solver2_wlist(s,lit_neg(lits[0])),clause_id(s,c));
+    veci_remove(solver2_wlist(s,lit_neg(lits[1])),clause_id(s,c));
 
     if (clause_learnt(c)){
         s->stats.learnts--;
@@ -748,11 +983,11 @@ static void clause_remove(sat_solver2* s, clause* c)
 }
 
 
-static lbool clause_simplify(sat_solver2* s, clause* c)
+static lbool clause_simplify(sat_solver2* s, satset* c)
 {
     lit*   lits   = clause_begin(c);
     int i;
-    assert(sat_solver2_dlevel(s) == 0);
+    assert(solver2_dlevel(s) == 0);
     for (i = 0; i < clause_nlits(c); i++){
         if (var_value(s, lit_var(lits[i])) == lit_sign(lits[i]))
             return l_True;
@@ -764,7 +999,7 @@ int sat_solver2_simplify(sat_solver2* s)
 {
 //    int type;
     int Counter = 0;
-    assert(sat_solver2_dlevel(s) == 0);
+    assert(solver2_dlevel(s) == 0);
     if (sat_solver2_propagate(s) != 0)
         return false;
     if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0)
@@ -775,8 +1010,8 @@ int sat_solver2_simplify(sat_solver2* s)
         int*  cls = (int*)veci_begin(cs);
         int i, j;
         for (j = i = 0; i < veci_size(cs); i++){
-            clause * c = get_clause(s,cls[i]);
-            if (s->reasons[lit_var(*clause_begin(c))] != cls[i] &&
+            satset* c = get_clause(s,cls[i]);
+            if (lit_reason(s,*clause_begin(c)) != cls[i] &&
                 clause_simplify(s,c) == l_True)
                 clause_remove(s,c), Counter++;
             else
@@ -794,7 +1029,8 @@ int sat_solver2_simplify(sat_solver2* s)
  
 void sat_solver2_reducedb(sat_solver2* s)
 {
-    clause * c;
+/*
+    satset* c;
     cla Cid;
     int clk = clock();
 
@@ -814,10 +1050,10 @@ void sat_solver2_reducedb(sat_solver2* s)
         sat_solver_foreach_learnt( s, c, Cid )
         {
             assert( c->Id == k );
-            c->fMark = 0;
-            if ( clause_nlits(c) > 2 && s->reasons[lit_var(*clause_begin(c))] != Cid && (k < nLearnts/2 || pActs[k] < extra_lim) )
+            c->mark = 0;
+            if ( clause_nlits(c) > 2 && lit_reason(s,*clause_begin(c)) != Cid && (k < nLearnts/2 || pActs[k] < extra_lim) )
             {
-                c->fMark = 1;
+                c->mark = 1;
                 Counter++;
             }
             k++;
@@ -826,28 +1062,25 @@ printf( "ReduceDB removed %10d clauses (out of %10d)... Cutoff = %8d  ", Counter
 Abc_PrintTime( 1, "Time", clock() - clk );
     }
     ABC_FREE( pPerm );
+*/
 }
 
 
 static lbool sat_solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts, ABC_INT64_T * nof_learnts)
 {
-    double  var_decay       = 0.95;
-    double  clause_decay    = 0.999;
     double  random_var_freq = s->fNotUseRandom ? 0.0 : 0.02;
-//    s->var_decay = (float)(1 / var_decay   );
-//    s->cla_decay = (float)(1 / clause_decay);
 
     ABC_INT64_T  conflictC       = 0;
     veci    learnt_clause;
 
-    assert(s->root_level == sat_solver2_dlevel(s));
+    assert(s->root_level == solver2_dlevel(s));
 
     s->stats.starts++;
     veci_resize(&s->model,0);
     veci_new(&learnt_clause);
 
     for (;;){
-        clause* confl = sat_solver2_propagate(s);
+        satset* confl = sat_solver2_propagate(s);
         if (confl != 0){
             // CONFLICT
             int blevel;
@@ -856,7 +1089,7 @@ static lbool sat_solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts, ABC_I
             printf(L_IND"**CONFLICT**\n", L_ind);
 #endif
             s->stats.conflicts++; conflictC++;
-            if (sat_solver2_dlevel(s) == s->root_level){
+            if (solver2_dlevel(s) == s->root_level){
 #ifdef SAT_USE_ANALYZE_FINAL
                 sat_solver2_analyze_final(s, confl, 0);
 #endif
@@ -901,7 +1134,7 @@ static lbool sat_solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts, ABC_I
                 return l_Undef; 
             }
 
-//            if (sat_solver2_dlevel(s) == 0 && !s->fSkipSimplify)
+//            if (solver2_dlevel(s) == 0 && !s->fSkipSimplify)
                 // Simplify the set of problem clauses:
 //                sat_solver2_simplify(s);
 
@@ -951,7 +1184,7 @@ static lbool sat_solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts, ABC_I
 
 sat_solver2* sat_solver2_new(void)
 {
-    sat_solver2 * s = (sat_solver2 *)ABC_CALLOC( char, sizeof(sat_solver2) );
+    sat_solver2* s = (sat_solver2 *)ABC_CALLOC( char, sizeof(sat_solver2) );
 
     // initialize vectors
     veci_new(&s->order);
@@ -961,20 +1194,32 @@ sat_solver2* sat_solver2_new(void)
     veci_new(&s->model);
     veci_new(&s->temp_clause);
     veci_new(&s->conf_final);
-    veci_new(&s->claActs);
-    veci_new(&s->claProofs);
-    veci_push(&s->claActs,   -1);
-    veci_push(&s->claProofs, -1);
+    veci_new(&s->mark_levels);
+    veci_new(&s->min_lit_order); 
+    veci_new(&s->min_step_order);
+    veci_new(&s->proof_clas); veci_push(&s->proof_clas, -1);
+    veci_new(&s->proof_vars); veci_push(&s->proof_vars, -1);
+    veci_new(&s->claActs);    veci_push(&s->claActs,    -1);
+    veci_new(&s->claProofs);  veci_push(&s->claProofs,  -1);
 
     // initialize other
     s->iLearnt                = -1; // the first learnt clause 
     s->iLast                  = -1; // the last learnt clause 
+#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);
-    s->var_inc                = (1 << 5);
+#endif
     s->random_seed            = 91648253;
+    s->fProofLogging          =  1;
     return s;
 }
 
+
 void sat_solver2_setnvars(sat_solver2* s,int n)
 {
     int var;
@@ -985,10 +1230,14 @@ 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->activity  = ABC_REALLOC(unsigned, s->activity, s->cap);
         s->orderpos  = ABC_REALLOC(int,      s->orderpos, s->cap);
         s->reasons   = ABC_REALLOC(cla,      s->reasons,  s->cap);
         s->trail     = ABC_REALLOC(lit,      s->trail,    s->cap);
+#ifdef USE_FLOAT_ACTIVITY
+        s->activity  = ABC_REALLOC(double,   s->activity, s->cap);
+#else
+        s->activity  = ABC_REALLOC(unsigned, s->activity, s->cap);
+#endif
     }
 
     for (var = s->size; var < n; var++){
@@ -1008,7 +1257,9 @@ void sat_solver2_setnvars(sat_solver2* s,int n)
 
 void sat_solver2_delete(sat_solver2* s)
 {
-    ABC_FREE(s->pMemArray);
+    // report statistics
+    assert( veci_size(&s->proof_clas) == veci_size(&s->proof_vars) );
+    printf( "Used %6.2f Mb for proof-logging.\n", 8.0 * veci_size(&s->proof_clas) / (1<<20) );
 
     // delete vectors
     veci_delete(&s->order);
@@ -1018,8 +1269,14 @@ void sat_solver2_delete(sat_solver2* s)
     veci_delete(&s->model);
     veci_delete(&s->temp_clause);
     veci_delete(&s->conf_final);
+    veci_delete(&s->mark_levels);
+    veci_delete(&s->min_lit_order);
+    veci_delete(&s->min_step_order);
+    veci_delete(&s->proof_clas);
+    veci_delete(&s->proof_vars);
     veci_delete(&s->claActs);
     veci_delete(&s->claProofs);
+    veci_delete(&s->clauses);
 
     // delete arrays
     if (s->vi != 0){
@@ -1029,10 +1286,10 @@ void sat_solver2_delete(sat_solver2* s)
                 veci_delete(&s->wlists[i]);
         ABC_FREE(s->wlists   );
         ABC_FREE(s->vi       );
-        ABC_FREE(s->activity );
         ABC_FREE(s->orderpos );
         ABC_FREE(s->reasons  );
         ABC_FREE(s->trail    );
+        ABC_FREE(s->activity );
     }
     ABC_FREE(s);
 }
@@ -1162,7 +1419,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
             return l_False;
         }
     }
-    s->root_level = sat_solver2_dlevel(s);
+    s->root_level = solver2_dlevel(s);
 
 #endif
 
@@ -1175,7 +1432,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
         if (!assume(p)){
             GClause r = reason[var(p)];
             if (r != GClause_NULL){
-                Clause* confl;
+                satset* confl;
                 if (r.isLit()){
                     confl = propagate_tmpbin;
                     (*confl)[1] = ~p;
@@ -1189,7 +1446,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
                 conflict.push(~p);
             cancelUntil(0);
             return false; }
-        Clause* confl = propagate();
+        satset* confl = propagate();
         if (confl != NULL){
             analyzeFinal(confl), assert(conflict.size() > 0);
             cancelUntil(0);
@@ -1208,10 +1465,10 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
         veci_push(&s->trail_lim,s->qtail);
         if (!enqueue(s,p,0))
         {
-            clause * r = get_clause(s, s->reasons[lit_var(p)]);
+            satset* r = get_clause(s, lit_reason(s,p));
             if (r != NULL)
             {
-                clause* confl = r;
+                satset* confl = r;
                 sat_solver2_analyze_final(s, confl, 1);
                 veci_push(&s->conf_final, lit_neg(p));
             }
@@ -1225,7 +1482,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
         }
         else
         {
-            clause* confl = sat_solver2_propagate(s);
+            satset* confl = sat_solver2_propagate(s);
             if (confl != NULL){
                 sat_solver2_analyze_final(s, confl, 0);
                 assert(s->conf_final.size > 0);
@@ -1233,7 +1490,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
                 return l_False; }
         }
     }
-    assert(s->root_level == sat_solver2_dlevel(s));
+    assert(s->root_level == solver2_dlevel(s));
 #endif
 
 //    s->nCalls2++;
diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h
index a5ed85b3..937972a6 100644
--- a/src/sat/bsat/satSolver2.h
+++ b/src/sat/bsat/satSolver2.h
@@ -32,7 +32,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 ABC_NAMESPACE_HEADER_START
 
-
+//#define USE_FLOAT_ACTIVITY
 
 //=================================================================================================
 // Public interface:
@@ -70,9 +70,6 @@ extern void *      sat_solver2_store_release( sat_solver2 * s );
 //=================================================================================================
 // Solver representation:
 
-//struct clause_t;
-//typedef struct clause_t clause;
-
 struct varinfo_t;
 typedef struct varinfo_t varinfo;
 
@@ -91,21 +88,26 @@ struct sat_solver2_t
     int           verbosity;     // Verbosity level. 0=silent, 1=some progress report, 2=everything
     int           fNotUseRandom; // do not allow random decisions with a fixed probability
 //    int           fSkipSimplify; // set to one to skip simplification of the clause database
+    int           fProofLogging; // enable proof-logging
 
     // clauses
+    veci          clauses;       // clause memory
+    veci*         wlists;        // watcher lists (for each literal)
     int           iLearnt;       // the first learnt clause 
     int           iLast;         // the last learnt clause 
-    veci*         wlists;        // watcher lists (for each literal)
-
-    // clause memory
-    int *         pMemArray;
-    int           nMemAlloc;
-    int           nMemSize;
 
     // 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
     veci          claActs;       // clause activities
     veci          claProofs;     // clause proofs
 
@@ -123,6 +125,15 @@ struct sat_solver2_t
     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.
+    veci          mark_levels;   // temporary storage for labeled levels
+    veci          min_lit_order; // ordering of removable literals
+    veci          min_step_order;// ordering of resolution steps
+
+    // proof logging
+    veci          proof_clas;    // sequence of proof clauses
+    veci          proof_vars;    // sequence of proof variables 
+    int           iStartChain;   // beginning of the chain
+
     // statistics
     stats_t       stats;
     ABC_INT64_T   nConfLimit;    // external limit on the number of conflicts
diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c
index ab9641bb..99a09081 100644
--- a/src/sat/bsat/satUtil.c
+++ b/src/sat/bsat/satUtil.c
@@ -169,16 +169,15 @@ void Sat_SolverPrintStats( FILE * pFile, sat_solver * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Sat_Solver2PrintStats( FILE * pFile, sat_solver2 * p )
+void Sat_Solver2PrintStats( FILE * pFile, sat_solver2 * s )
 {
-//    printf( "calls         : %10d (%d)\n", (int)p->nCalls, (int)p->nCalls2 );
-    printf( "starts        : %10d\n", (int)p->stats.starts );
-    printf( "conflicts     : %10d\n", (int)p->stats.conflicts );
-    printf( "decisions     : %10d\n", (int)p->stats.decisions );
-    printf( "propagations  : %10d\n", (int)p->stats.propagations );
-//    printf( "inspects      : %10d\n", (int)p->stats.inspects );
-//    printf( "inspects2     : %10d\n", (int)p->stats.inspects2 );
-    printf( "memory        : %10d\n", p->nMemSize );
+    printf( "starts        : %10d\n", (int)s->stats.starts );
+    printf( "conflicts     : %10d\n", (int)s->stats.conflicts );
+    printf( "decisions     : %10d\n", (int)s->stats.decisions );
+    printf( "propagations  : %10d\n", (int)s->stats.propagations );
+//    printf( "inspects      : %10d\n", (int)s->stats.inspects );
+//    printf( "inspects2     : %10d\n", (int)s->stats.inspects2 );
+    printf( "memory        : %10d\n", veci_size(&s->clauses) );
 }
 
 /**Function*************************************************************
diff --git a/src/sat/bsat/satVec.h b/src/sat/bsat/satVec.h
index aeca3059..1f63ba1e 100644
--- a/src/sat/bsat/satVec.h
+++ b/src/sat/bsat/satVec.h
@@ -44,7 +44,8 @@ static inline void veci_new (veci* v) {
 static inline void   veci_delete (veci* v)          { ABC_FREE(v->ptr);   }
 static inline int*   veci_begin  (veci* v)          { return v->ptr;  }
 static inline int    veci_size   (veci* v)          { return v->size; }
-static inline void   veci_resize (veci* v, int k)   { v->size = k;    } // only safe to shrink !!
+static inline void   veci_resize (veci* v, int k)   { assert(k <= v->size); v->size = k;         } // only safe to shrink !!
+static inline int    veci_pop    (veci* v)          { assert(v->size); return v->ptr[--v->size]; }
 static inline void   veci_push   (veci* v, int e)
 {
     if (v->size == v->cap) {
@@ -82,7 +83,7 @@ static inline void vecp_new (vecp* v) {
 static inline void   vecp_delete (vecp* v)          { ABC_FREE(v->ptr);   }
 static inline void** vecp_begin  (vecp* v)          { return v->ptr;  }
 static inline int    vecp_size   (vecp* v)          { return v->size; }
-static inline void   vecp_resize (vecp* v, int   k) { v->size = k;    } // only safe to shrink !!
+static inline void   vecp_resize (vecp* v, int   k) { assert(k <= v->size); v->size = k;    } // only safe to shrink !!
 static inline void   vecp_push   (vecp* v, void* e)
 {
     if (v->size == v->cap) {
@@ -143,9 +144,6 @@ struct stats_t
 };
 typedef struct stats_t stats_t;
 
-struct clause_t;
-typedef struct clause_t clause;
-
 ABC_NAMESPACE_HEADER_END
 
 #endif