Clone of the main SAT solver to eneable independent work.

2 files changed, 2921 insertions, 0 deletions

diff --git a/src/sat/bsat/satSolver3.c b/src/sat/bsat/satSolver3.c
new file mode 100644
index 00000000..b61ce96c
--- /dev/null
+++ b/src/sat/bsat/satSolver3.c
@@ -0,0 +1,2299 @@
+/**************************************************************************************************
+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 "satSolver3.h"
+
+ABC_NAMESPACE_IMPL_START
+
+#define SAT_USE_ANALYZE_FINAL
+
+//=================================================================================================
+// Debug:
+
+//#define VERBOSEDEBUG
+
+// For derivation output (verbosity level 2)
+#define L_IND    "%-*d"
+#define L_ind    sat_solver3_dl(s)*2+2,sat_solver3_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); }
+
+
+//=================================================================================================
+// 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_solver3* s, int v)            { return s->levels[v];   }
+static inline int     var_value     (sat_solver3* s, int v)            { return s->assigns[v];  }
+static inline int     var_polar     (sat_solver3* s, int v)            { return s->polarity[v]; }
+
+static inline void    var_set_level (sat_solver3* s, int v, int lev)   { s->levels[v] = lev;    }
+static inline void    var_set_value (sat_solver3* s, int v, int val)   { s->assigns[v] = val;   }
+static inline void    var_set_polar (sat_solver3* s, int v, int pol)   { s->polarity[v] = pol;  }
+
+// variable tags
+static inline int     var_tag       (sat_solver3* s, int v)            { return s->tags[v]; }
+static inline void    var_set_tag   (sat_solver3* 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_solver3* 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_solver3* 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_solver3_get_var_value(sat_solver3* 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;
+}
+
+//=================================================================================================
+// Simple helpers:
+
+static inline int      sat_solver3_dl(sat_solver3* s)                { return veci_size(&s->trail_lim); }
+static inline veci*    sat_solver3_read_wlist(sat_solver3* s, lit l) { return &s->wlists[l];            }
+
+//=================================================================================================
+// Variable order functions:
+
+static inline void order_update(sat_solver3* 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_solver3* s, int v) 
+{
+}
+
+static inline void order_unassigned(sat_solver3* 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_solver3* s, float random_var_freq) // selectvar
+{
+    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 (var_value(s, next) == varX)
+            return next;
+    }
+    // Activity based decision:
+    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;
+        }
+        if (var_value(s, next) == varX)
+            return next;
+    }
+    return var_Undef;
+}
+
+void sat_solver3_set_var_activity(sat_solver3* s, int * pVars, int nVars) 
+{
+    int i;
+    assert( s->VarActType == 1 );
+    for (i = 0; i < s->size; i++)
+        s->activity[i] = 0;
+    s->var_inc = Abc_Dbl2Word(1);
+    for ( i = 0; i < nVars; i++ )
+    {
+        int iVar = pVars ? pVars[i] : i;
+        s->activity[iVar] = Abc_Dbl2Word(nVars-i);
+        order_update( s, iVar );
+    }
+}
+
+//=================================================================================================
+// variable activities
+
+static inline void solver_init_activities(sat_solver3* s)  
+{
+    // variable activities
+    s->VarActType             = 0;
+    if ( s->VarActType == 0 )
+    {
+        s->var_inc            = (1 <<  5);
+        s->var_decay          = -1;
+    }
+    else if ( s->VarActType == 1 )
+    {
+        s->var_inc            = Abc_Dbl2Word(1.0);
+        s->var_decay          = Abc_Dbl2Word(1.0 / 0.95);
+    }
+    else if ( s->VarActType == 2 )
+    {
+        s->var_inc            = Xdbl_FromDouble(1.0);
+        s->var_decay          = Xdbl_FromDouble(1.0 / 0.950);
+    }
+    else assert(0);
+
+    // clause activities
+    s->ClaActType             = 0;
+    if ( s->ClaActType == 0 )
+    {
+        s->cla_inc            = (1 << 11);
+        s->cla_decay          = -1;
+    }
+    else
+    {
+        s->cla_inc            = 1;
+        s->cla_decay          = (float)(1 / 0.999);
+    }
+}
+
+static inline void act_var_rescale(sat_solver3* s)  
+{
+    if ( s->VarActType == 0 )
+    {
+        word* activity = s->activity;
+        int i;
+        for (i = 0; i < s->size; i++)
+            activity[i] >>= 19;
+        s->var_inc >>= 19;
+        s->var_inc = Abc_MaxInt( (unsigned)s->var_inc, (1<<4) );
+    }
+    else if ( s->VarActType == 1 )
+    {
+        double* activity = (double*)s->activity;
+        int i;
+        for (i = 0; i < s->size; i++)
+            activity[i] *= 1e-100;
+        s->var_inc = Abc_Dbl2Word( Abc_Word2Dbl(s->var_inc) * 1e-100 );
+        //printf( "Rescaling var activity...\n" ); 
+    }
+    else if ( s->VarActType == 2 )
+    {
+        xdbl * activity = s->activity;
+        int i;
+        for (i = 0; i < s->size; i++)
+            activity[i] = Xdbl_Div( activity[i], 200 ); // activity[i] / 2^200
+        s->var_inc = Xdbl_Div( s->var_inc, 200 ); 
+    }
+    else assert(0);
+}
+static inline void act_var_bump(sat_solver3* s, int v) 
+{
+    if ( s->VarActType == 0 )
+    {
+        s->activity[v] += s->var_inc;
+        if ((unsigned)s->activity[v] & 0x80000000)
+            act_var_rescale(s);
+        if (s->orderpos[v] != -1)
+            order_update(s,v);
+    }
+    else if ( s->VarActType == 1 )
+    {
+        double act = Abc_Word2Dbl(s->activity[v]) + Abc_Word2Dbl(s->var_inc);
+        s->activity[v] = Abc_Dbl2Word(act);
+        if (act > 1e100)
+            act_var_rescale(s);
+        if (s->orderpos[v] != -1)
+            order_update(s,v);
+    }
+    else if ( s->VarActType == 2 )
+    {
+        s->activity[v] = Xdbl_Add( s->activity[v], s->var_inc );
+        if (s->activity[v] > ABC_CONST(0x014c924d692ca61b))
+            act_var_rescale(s);
+        if (s->orderpos[v] != -1)
+            order_update(s,v);
+    }
+    else assert(0);
+}
+static inline void act_var_bump_global(sat_solver3* s, int v) 
+{
+    if ( !s->pGlobalVars || !s->pGlobalVars[v] )
+        return;
+    if ( s->VarActType == 0 )
+    {
+        s->activity[v] += (int)((unsigned)s->var_inc * 3);
+        if (s->activity[v] & 0x80000000)
+            act_var_rescale(s);
+        if (s->orderpos[v] != -1)
+            order_update(s,v);
+    }
+    else if ( s->VarActType == 1 )
+    {
+        double act = Abc_Word2Dbl(s->activity[v]) + Abc_Word2Dbl(s->var_inc) * 3.0;
+        s->activity[v] = Abc_Dbl2Word(act);
+        if ( act > 1e100)
+            act_var_rescale(s);
+        if (s->orderpos[v] != -1)
+            order_update(s,v);
+    }
+    else if ( s->VarActType == 2 )
+    {
+        s->activity[v] = Xdbl_Add( s->activity[v], Xdbl_Mul(s->var_inc, Xdbl_FromDouble(3.0)) );
+        if (s->activity[v] > ABC_CONST(0x014c924d692ca61b))
+            act_var_rescale(s);
+        if (s->orderpos[v] != -1)
+            order_update(s,v);
+    }
+    else assert( 0 );
+}
+static inline void act_var_bump_factor(sat_solver3* s, int v) 
+{
+    if ( !s->factors )
+        return;
+    if ( s->VarActType == 0 )
+    {
+        s->activity[v] += (int)((unsigned)s->var_inc * (float)s->factors[v]);
+        if (s->activity[v] & 0x80000000)
+            act_var_rescale(s);
+        if (s->orderpos[v] != -1)
+            order_update(s,v);
+    }
+    else if ( s->VarActType == 1 )
+    {
+        double act = Abc_Word2Dbl(s->activity[v]) + Abc_Word2Dbl(s->var_inc) * s->factors[v];
+        s->activity[v] = Abc_Dbl2Word(act);
+        if ( act > 1e100)
+            act_var_rescale(s);
+        if (s->orderpos[v] != -1)
+            order_update(s,v);
+    }
+    else if ( s->VarActType == 2 )
+    {
+        s->activity[v] = Xdbl_Add( s->activity[v], Xdbl_Mul(s->var_inc, Xdbl_FromDouble(s->factors[v])) );
+        if (s->activity[v] > ABC_CONST(0x014c924d692ca61b))
+            act_var_rescale(s);
+        if (s->orderpos[v] != -1)
+            order_update(s,v);
+    }
+    else assert( 0 );
+}
+
+static inline void act_var_decay(sat_solver3* s)    
+{ 
+    if ( s->VarActType == 0 )
+        s->var_inc += (s->var_inc >>  4); 
+    else if ( s->VarActType == 1 )
+        s->var_inc = Abc_Dbl2Word( Abc_Word2Dbl(s->var_inc) * Abc_Word2Dbl(s->var_decay) );
+    else if ( s->VarActType == 2 )
+        s->var_inc = Xdbl_Mul(s->var_inc, s->var_decay); 
+    else assert(0);
+}
+
+// clause activities
+static inline void act_clause_rescale(sat_solver3* s) 
+{
+    if ( s->ClaActType == 0 )
+    {
+        unsigned* activity = (unsigned *)veci_begin(&s->act_clas);
+        int i;
+        for (i = 0; i < veci_size(&s->act_clas); i++)
+            activity[i] >>= 14;
+        s->cla_inc >>= 14;
+        s->cla_inc = Abc_MaxInt( s->cla_inc, (1<<10) );
+    }
+    else
+    {
+        float* activity = (float *)veci_begin(&s->act_clas);
+        int i;
+        for (i = 0; i < veci_size(&s->act_clas); i++)
+            activity[i] *= (float)1e-20;
+        s->cla_inc *= (float)1e-20;
+    }
+}
+static inline void act_clause_bump(sat_solver3* s, clause *c) 
+{
+    if ( s->ClaActType == 0 )
+    {
+        unsigned* act = (unsigned *)veci_begin(&s->act_clas) + c->lits[c->size];
+        *act += s->cla_inc;
+        if ( *act & 0x80000000 )
+            act_clause_rescale(s);
+    }
+    else
+    {
+        float* act = (float *)veci_begin(&s->act_clas) + c->lits[c->size];
+        *act += s->cla_inc;
+        if (*act > 1e20) 
+            act_clause_rescale(s);
+    }
+}
+static inline void act_clause_decay(sat_solver3* s)    
+{ 
+    if ( s->ClaActType == 0 )
+        s->cla_inc += (s->cla_inc >> 10);
+    else
+        s->cla_inc *= s->cla_decay;
+}
+
+
+//=================================================================================================
+// 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);
+    }
+}
+
+//=================================================================================================
+// Clause functions:
+
+static inline int sat_clause_compute_lbd( sat_solver3* s, clause* c )
+{
+    int i, lev, minl = 0, lbd = 0;
+    for (i = 0; i < (int)c->size; i++)
+    {
+        lev = var_level(s, lit_var(c->lits[i]));
+        if ( !(minl & (1 << (lev & 31))) )
+        {
+            minl |= 1 << (lev & 31);
+            lbd++;
+//            printf( "%d ", lev );
+        }
+    }
+//    printf( " -> %d\n", lbd );
+    return lbd;
+}
+
+/* pre: size > 1 && no variable occurs twice
+ */
+int sat_solver3_clause_new(sat_solver3* s, lit* begin, lit* end, int learnt)
+{
+    int fUseBinaryClauses = 1;
+    int size;
+    clause* c;
+    int h;
+
+    assert(end - begin > 1);
+    assert(learnt >= 0 && learnt < 2);
+    size           = end - begin;
+
+    // do not allocate memory for the two-literal problem clause
+    if ( fUseBinaryClauses && size == 2 && !learnt )
+    {
+        veci_push(sat_solver3_read_wlist(s,lit_neg(begin[0])),(clause_from_lit(begin[1])));
+        veci_push(sat_solver3_read_wlist(s,lit_neg(begin[1])),(clause_from_lit(begin[0])));
+        s->stats.clauses++;
+        s->stats.clauses_literals += size;
+        return 0;
+    }
+
+    // create new clause
+//    h = Vec_SetAppend( &s->Mem, NULL, size + learnt + 1 + 1 ) << 1;
+    h = Sat_MemAppend( &s->Mem, begin, size, learnt, 0 );
+    assert( !(h & 1) );
+    if ( s->hLearnts == -1 && learnt )
+        s->hLearnts = h;
+    if (learnt)
+    {
+        c = clause_read( s, h );
+        c->lbd = sat_clause_compute_lbd( s, c );
+        assert( clause_id(c) == veci_size(&s->act_clas) );
+//        veci_push(&s->learned, h);
+//        act_clause_bump(s,clause_read(s, h));
+        if ( s->ClaActType == 0 )
+            veci_push(&s->act_clas, (1<<10));
+        else
+            veci_push(&s->act_clas, s->cla_inc);
+        s->stats.learnts++;
+        s->stats.learnts_literals += size;
+    }
+    else
+    {
+        s->stats.clauses++;
+        s->stats.clauses_literals += size;
+    }
+
+    assert(begin[0] >= 0);
+    assert(begin[0] < s->size*2);
+    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);
+
+    //veci_push(sat_solver3_read_wlist(s,lit_neg(begin[0])),c);
+    //veci_push(sat_solver3_read_wlist(s,lit_neg(begin[1])),c);
+    veci_push(sat_solver3_read_wlist(s,lit_neg(begin[0])),(size > 2 ? h : clause_from_lit(begin[1])));
+    veci_push(sat_solver3_read_wlist(s,lit_neg(begin[1])),(size > 2 ? h : clause_from_lit(begin[0])));
+
+    return h;
+}
+
+
+//=================================================================================================
+// Minor (solver) functions:
+
+static inline int sat_solver3_enqueue(sat_solver3* s, lit l, int from)
+{
+    int v  = lit_var(l);
+    if ( s->pFreqs[v] == 0 )
+//    {
+        s->pFreqs[v] = 1;
+//        s->nVarUsed++;
+//    }
+
+#ifdef VERBOSEDEBUG
+    printf(L_IND"enqueue("L_LIT")\n", L_ind, L_lit(l));
+#endif
+    if (var_value(s, v) != varX)
+        return var_value(s, v) == lit_sign(l);
+    else{
+/*
+        if ( s->pCnfFunc )
+        {
+            if ( lit_sign(l) )
+            {
+                if ( (s->loads[v] & 1) == 0 )
+                {
+                    s->loads[v] ^= 1;
+                    s->pCnfFunc( s->pCnfMan, l );
+                }
+            }
+            else
+            {
+                if ( (s->loads[v] & 2) == 0 )
+                {
+                    s->loads[v] ^= 2;
+                    s->pCnfFunc( s->pCnfMan, l );
+                }
+            }
+        }
+*/
+        // New fact -- store it.
+#ifdef VERBOSEDEBUG
+        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_solver3_dl(s));
+        s->reasons[v] = from;
+        s->trail[s->qtail++] = l;
+        order_assigned(s, v);
+        return true;
+    }
+}
+
+
+static inline int sat_solver3_decision(sat_solver3* s, lit l){
+    assert(s->qtail == s->qhead);
+    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_solver3_enqueue(s,l,0);
+}
+
+
+static void sat_solver3_canceluntil(sat_solver3* s, int level) {
+    int      bound;
+    int      lastLev;
+    int      c;
+    
+    if (sat_solver3_dl(s) <= level)
+        return;
+
+    assert( veci_size(&s->trail_lim) > 0 );
+    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(s->trail[c]);
+        var_set_value(s, x, varX);
+        s->reasons[x] = 0;
+        if ( c < lastLev )
+            var_set_polar( s, x, !lit_sign(s->trail[c]) );
+    }
+    //printf( "\n" );
+
+    for (c = s->qhead-1; c >= bound; c--)
+        order_unassigned(s,lit_var(s->trail[c]));
+
+    s->qhead = s->qtail = bound;
+    veci_resize(&s->trail_lim,level);
+}
+
+static void sat_solver3_canceluntil_rollback(sat_solver3* s, int NewBound) {
+    int      c, x;
+   
+    assert( sat_solver3_dl(s) == 0 );
+    assert( s->qtail == s->qhead );
+    assert( s->qtail >= NewBound );
+
+    for (c = s->qtail-1; c >= NewBound; c--) 
+    {
+        x = lit_var(s->trail[c]);
+        var_set_value(s, x, varX);
+        s->reasons[x] = 0;
+    }
+
+    for (c = s->qhead-1; c >= NewBound; c--)
+        order_unassigned(s,lit_var(s->trail[c]));
+
+    s->qhead = s->qtail = NewBound;
+}
+
+static void sat_solver3_record(sat_solver3* s, veci* cls)
+{
+    lit*    begin = veci_begin(cls);
+    lit*    end   = begin + veci_size(cls);
+    int     h     = (veci_size(cls) > 1) ? sat_solver3_clause_new(s,begin,end,1) : 0;
+    sat_solver3_enqueue(s,*begin,h);
+    assert(veci_size(cls) > 0);
+    if ( h == 0 )
+        veci_push( &s->unit_lits, *begin );
+
+/*
+    if (h != 0) {
+        act_clause_bump(s,clause_read(s, h));
+        s->stats.learnts++;
+        s->stats.learnts_literals += veci_size(cls);
+    }
+*/
+}
+
+int sat_solver3_count_assigned(sat_solver3* s)
+{
+    // count top-level assignments
+    int i, Count = 0;
+    assert(sat_solver3_dl(s) == 0);
+    for ( i = 0; i < s->size; i++ )
+        if (var_value(s, i) != varX)
+            Count++;
+    return Count;
+}
+
+static double sat_solver3_progress(sat_solver3* s)
+{
+    int     i;
+    double  progress = 0;
+    double  F        = 1.0 / s->size;
+    for (i = 0; i < s->size; i++)
+        if (var_value(s, i) != varX)
+            progress += pow(F, var_level(s, i));
+    return progress / s->size;
+}
+
+//=================================================================================================
+// Major methods:
+
+static int sat_solver3_lit_removable(sat_solver3* s, int x, int minl)
+{
+    int      top     = veci_size(&s->tagged);
+
+    assert(s->reasons[x] != 0);
+    veci_resize(&s->stack,0);
+    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);
+                    var_set_tag(s, v, 1);
+                }else{
+                    solver2_clear_tags(s, top);
+                    return 0;
+                }
+            }
+        }else{
+            clause* c = clause_read(s, s->reasons[v]);
+            lit* lits = clause_begin(c);
+            int  i;
+            for (i = 1; i < clause_size(c); i++){
+                int v = lit_var(lits[i]);
+                if (!var_tag(s,v) && var_level(s, v)){
+                    if (s->reasons[v] != 0 && ((1 << (var_level(s, v) & 31)) & minl)){
+                        veci_push(&s->stack,lit_var(lits[i]));
+                        var_set_tag(s, v, 1);
+                    }else{
+                        solver2_clear_tags(s, top);
+                        return 0;
+                    }
+                }
+            }
+        }
+    }
+    return 1;
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  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_solver3_analyze_final(sat_solver3* 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 )
+        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 (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 (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{
+                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 (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 (var_level(s, lit_var(lits[j])) > 0)
+                            var_set_tag(s, lit_var(lits[j]), 1);
+                }
+            }
+        }
+    }
+    solver2_clear_tags(s,0);
+}
+
+#endif
+
+static void sat_solver3_analyze(sat_solver3* s, int h, veci* learnt)
+{
+    lit*     trail   = s->trail;
+    int      cnt     = 0;
+    lit      p       = lit_Undef;
+    int      ind     = s->qtail-1;
+    lit*     lits;
+    int      i, j, minl;
+    veci_push(learnt,lit_Undef);
+    do{
+        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_solver3_dl(s))
+                    cnt++;
+                else
+                    veci_push(learnt,clause_read_lit(h));
+            }
+        }else{
+            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++){
+                int x = lit_var(lits[j]);
+                if (var_tag(s, x) == 0 && var_level(s, x) > 0){
+                    var_set_tag(s, x, 1);
+                    act_var_bump(s,x);
+                    // bump variables propaged by the LBD=2 clause
+//                    if ( s->reasons[x] && clause_read(s, s->reasons[x])->lbd <= 2 )
+//                        act_var_bump(s,x);
+                    if (var_level(s,x) == sat_solver3_dl(s))
+                        cnt++;
+                    else
+                        veci_push(learnt,lits[j]);
+                }
+            }
+        }
+
+        while ( !var_tag(s, lit_var(trail[ind--])) );
+
+        p = trail[ind+1];
+        h = s->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 = var_level(s, lit_var(lits[i]));
+        minl    |= 1 << (lev & 31);
+    }
+
+    // simplify (full)
+    for (i = j = 1; i < veci_size(learnt); i++){
+        if (s->reasons[lit_var(lits[i])] == 0 || !sat_solver3_lit_removable(s,lit_var(lits[i]),minl))
+            lits[j++] = lits[i];
+    }
+
+    // update size of learnt + statistics
+    veci_resize(learnt,j);
+    s->stats.tot_literals += j;
+
+
+    // clear tags
+    solver2_clear_tags(s,0);
+
+#ifdef DEBUG
+    for (i = 0; i < s->size; i++)
+        assert(!var_tag(s, i));
+#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   = var_level(s, lit_var(lits[1]));
+        lit tmp;
+
+        for (i = 2; i < veci_size(learnt); i++)
+            if (var_level(s, lit_var(lits[i])) > max){
+                max   = var_level(s, 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 ? var_level(s, lit_var(lits[1])) : 0;
+        printf(" } at level %d\n", lev);
+    }
+#endif
+}
+
+//#define TEST_CNF_LOAD
+
+int sat_solver3_propagate(sat_solver3* s)
+{
+    int     hConfl = 0;
+    lit*    lits;
+    lit false_lit;
+
+    //printf("sat_solver3_propagate\n");
+    while (hConfl == 0 && s->qtail - s->qhead > 0){
+        lit p = s->trail[s->qhead++];
+
+#ifdef TEST_CNF_LOAD
+        int v = lit_var(p);
+        if ( s->pCnfFunc )
+        {
+            if ( lit_sign(p) )
+            {
+                if ( (s->loads[v] & 1) == 0 )
+                {
+                    s->loads[v] ^= 1;
+                    s->pCnfFunc( s->pCnfMan, p );
+                }
+            }
+            else
+            {
+                if ( (s->loads[v] & 2) == 0 )
+                {
+                    s->loads[v] ^= 2;
+                    s->pCnfFunc( s->pCnfMan, p );
+                }
+            }
+        }
+        {
+#endif
+
+        veci* ws    = sat_solver3_read_wlist(s,p);
+        int*  begin = veci_begin(ws);
+        int*  end   = begin + veci_size(ws);
+        int*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);
+                if (var_value(s, lit_var(Lit)) == lit_sign(Lit)){
+                    *j++ = *i++;
+                    continue;
+                }
+
+                *j++ = *i;
+                if (!sat_solver3_enqueue(s,clause_read_lit(*i),clause_from_lit(p))){
+                    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{
+
+                clause* c = clause_read(s,*i);
+                lits = clause_begin(c);
+
+                // 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);
+
+                // If 0th watch is true, then clause is already satisfied.
+                if (var_value(s, lit_var(lits[0])) == lit_sign(lits[0]))
+                    *j++ = *i;
+                else{
+                    // Look for new watch:
+                    lit* stop = lits + clause_size(c);
+                    lit* k;
+                    for (k = lits + 2; k < stop; k++){
+                        if (var_value(s, lit_var(*k)) != !lit_sign(*k)){
+                            lits[1] = *k;
+                            *k = false_lit;
+                            veci_push(sat_solver3_read_wlist(s,lit_neg(lits[1])),*i);
+                            goto next; }
+                    }
+
+                    *j++ = *i;
+                    // Clause is unit under assignment:
+                    if ( c->lrn )
+                        c->lbd = sat_clause_compute_lbd(s, c);
+                    if (!sat_solver3_enqueue(s,lits[0], *i)){
+                        hConfl = *i++;
+                        // Copy the remaining watches:
+                        while (i < end)
+                            *j++ = *i++;
+                    }
+                }
+            }
+        next:
+            i++;
+        }
+
+        s->stats.inspects += j - veci_begin(ws);
+        veci_resize(ws,j - veci_begin(ws));
+#ifdef TEST_CNF_LOAD
+        }
+#endif
+    }
+
+    return hConfl;
+}
+
+//=================================================================================================
+// External solver functions:
+
+sat_solver3* sat_solver3_new(void)
+{
+    sat_solver3* s = (sat_solver3*)ABC_CALLOC( char, sizeof(sat_solver3));
+
+//    Vec_SetAlloc_(&s->Mem, 15);
+    Sat_MemAlloc_(&s->Mem, 17);
+    s->hLearnts = -1;
+    s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0, 0 );
+    s->binary = clause_read( s, s->hBinary );
+
+    s->nLearntStart = LEARNT_MAX_START_DEFAULT;  // starting learned clause limit
+    s->nLearntDelta = LEARNT_MAX_INCRE_DEFAULT;  // delta of learned clause limit
+    s->nLearntRatio = LEARNT_MAX_RATIO_DEFAULT;  // ratio of learned clause limit
+    s->nLearntMax   = s->nLearntStart;
+
+    // initialize vectors
+    veci_new(&s->order);
+    veci_new(&s->trail_lim);
+    veci_new(&s->tagged);
+//    veci_new(&s->learned);
+    veci_new(&s->act_clas);
+    veci_new(&s->stack);
+//    veci_new(&s->model);
+    veci_new(&s->unit_lits);
+    veci_new(&s->temp_clause);
+    veci_new(&s->conf_final);
+
+    // initialize arrays
+    s->wlists    = 0;
+    s->activity  = 0;
+    s->orderpos  = 0;
+    s->reasons   = 0;
+    s->trail     = 0;
+
+    // initialize other vars
+    s->size                   = 0;
+    s->cap                    = 0;
+    s->qhead                  = 0;
+    s->qtail                  = 0;
+
+    solver_init_activities(s);
+    veci_new(&s->act_vars);
+
+    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;
+    return s;
+}
+
+sat_solver3* zsat_solver3_new_seed(double seed)
+{
+    sat_solver3* s = (sat_solver3*)ABC_CALLOC( char, sizeof(sat_solver3));
+
+//    Vec_SetAlloc_(&s->Mem, 15);
+    Sat_MemAlloc_(&s->Mem, 15);
+    s->hLearnts = -1;
+    s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0, 0 );
+    s->binary = clause_read( s, s->hBinary );
+
+    s->nLearntStart = LEARNT_MAX_START_DEFAULT;  // starting learned clause limit
+    s->nLearntDelta = LEARNT_MAX_INCRE_DEFAULT;  // delta of learned clause limit
+    s->nLearntRatio = LEARNT_MAX_RATIO_DEFAULT;  // ratio of learned clause limit
+    s->nLearntMax   = s->nLearntStart;
+
+    // initialize vectors
+    veci_new(&s->order);
+    veci_new(&s->trail_lim);
+    veci_new(&s->tagged);
+//    veci_new(&s->learned);
+    veci_new(&s->act_clas);
+    veci_new(&s->stack);
+//    veci_new(&s->model);
+    veci_new(&s->unit_lits);
+    veci_new(&s->temp_clause);
+    veci_new(&s->conf_final);
+
+    // initialize arrays
+    s->wlists    = 0;
+    s->activity  = 0;
+    s->orderpos  = 0;
+    s->reasons   = 0;
+    s->trail     = 0;
+
+    // initialize other vars
+    s->size                   = 0;
+    s->cap                    = 0;
+    s->qhead                  = 0;
+    s->qtail                  = 0;
+
+    solver_init_activities(s);
+    veci_new(&s->act_vars);
+
+    s->root_level             = 0;
+//    s->simpdb_assigns         = 0;
+//    s->simpdb_props           = 0;
+    s->random_seed            = seed;
+    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;
+    return s;
+}
+
+void sat_solver3_setnvars(sat_solver3* s,int n)
+{
+    int var;
+
+    if (s->cap < n){
+        int old_cap = s->cap;
+        while (s->cap < n) s->cap = s->cap*2+1;
+        if ( s->cap < 50000 )
+            s->cap = 50000;
+
+        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);
+        s->loads     = ABC_REALLOC(char,   s->loads,    s->cap);
+        s->activity  = ABC_REALLOC(word,   s->activity, s->cap);
+        s->activity2 = ABC_REALLOC(word,   s->activity2,s->cap);
+        s->pFreqs    = ABC_REALLOC(char,   s->pFreqs,   s->cap);
+
+        if ( s->factors )
+        s->factors   = ABC_REALLOC(double, s->factors,  s->cap);
+        s->orderpos  = ABC_REALLOC(int,    s->orderpos, s->cap);
+        s->reasons   = ABC_REALLOC(int,    s->reasons,  s->cap);
+        s->trail     = ABC_REALLOC(lit,    s->trail,    s->cap);
+        s->model     = ABC_REALLOC(int,    s->model,    s->cap);
+        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 )
+            veci_new(&s->wlists[2*var]);
+        if ( s->wlists[2*var+1].ptr == NULL )
+            veci_new(&s->wlists[2*var+1]);
+
+        if ( s->VarActType == 0 )
+            s->activity[var] = (1<<10);
+        else if ( s->VarActType == 1 )
+            s->activity[var] = 0;
+        else if ( s->VarActType == 2 )
+            s->activity[var] = 0;
+        else assert(0);
+
+        s->pFreqs[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->loads   [var] = 0;
+        s->orderpos[var] = veci_size(&s->order);
+        s->reasons [var] = 0;
+        s->model   [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_solver3_delete(sat_solver3* s)
+{
+//    Vec_SetFree_( &s->Mem );
+    Sat_MemFree_( &s->Mem );
+
+    // delete vectors
+    veci_delete(&s->order);
+    veci_delete(&s->trail_lim);
+    veci_delete(&s->tagged);
+//    veci_delete(&s->learned);
+    veci_delete(&s->act_clas);
+    veci_delete(&s->stack);
+//    veci_delete(&s->model);
+    veci_delete(&s->act_vars);
+    veci_delete(&s->unit_lits);
+    veci_delete(&s->pivot_vars);
+    veci_delete(&s->temp_clause);
+    veci_delete(&s->conf_final);
+
+    // delete arrays
+    if (s->reasons != 0){
+        int i;
+        for (i = 0; i < s->cap*2; 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->loads    );
+        ABC_FREE(s->activity );
+        ABC_FREE(s->activity2);
+        ABC_FREE(s->pFreqs   );
+        ABC_FREE(s->factors  );
+        ABC_FREE(s->orderpos );
+        ABC_FREE(s->reasons  );
+        ABC_FREE(s->trail    );
+        ABC_FREE(s->model    );
+    }
+
+    ABC_FREE(s);
+}
+
+void sat_solver3_restart( sat_solver3* s )
+{
+    int i;
+    Sat_MemRestart( &s->Mem );
+    s->hLearnts = -1;
+    s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0, 0 );
+    s->binary = clause_read( s, s->hBinary );
+
+    veci_resize(&s->trail_lim, 0);
+    veci_resize(&s->order, 0);
+    for ( i = 0; i < s->size*2; i++ )
+        s->wlists[i].size = 0;
+
+    s->nDBreduces = 0;
+
+    // initialize other vars
+    s->size                   = 0;
+//    s->cap                    = 0;
+    s->qhead                  = 0;
+    s->qtail                  = 0;
+
+
+    // variable activities
+    solver_init_activities(s);
+    veci_resize(&s->act_clas, 0);
+
+
+    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;
+}
+
+void zsat_solver3_restart_seed( sat_solver3* s, double seed )
+{
+    int i;
+    Sat_MemRestart( &s->Mem );
+    s->hLearnts = -1;
+    s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0, 0 );
+    s->binary = clause_read( s, s->hBinary );
+
+    veci_resize(&s->trail_lim, 0);
+    veci_resize(&s->order, 0);
+    for ( i = 0; i < s->size*2; i++ )
+        s->wlists[i].size = 0;
+
+    s->nDBreduces = 0;
+
+    // initialize other vars
+    s->size                   = 0;
+//    s->cap                    = 0;
+    s->qhead                  = 0;
+    s->qtail                  = 0;
+
+    solver_init_activities(s);
+    veci_resize(&s->act_clas, 0);
+
+    s->root_level             = 0;
+//    s->simpdb_assigns         = 0;
+//    s->simpdb_props           = 0;
+    s->random_seed            = seed;
+    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;
+}
+
+// returns memory in bytes used by the SAT solver
+double sat_solver3_memory( sat_solver3* s )
+{
+    int i;
+    double Mem = sizeof(sat_solver3);
+    for (i = 0; i < s->cap*2; i++)
+        Mem += s->wlists[i].cap * sizeof(int);
+    Mem += s->cap * sizeof(veci);     // ABC_FREE(s->wlists   );
+    Mem += s->cap * sizeof(int);      // ABC_FREE(s->levels   );
+    Mem += s->cap * sizeof(char);     // ABC_FREE(s->assigns  );
+    Mem += s->cap * sizeof(char);     // ABC_FREE(s->polarity );
+    Mem += s->cap * sizeof(char);     // ABC_FREE(s->tags     );
+    Mem += s->cap * sizeof(char);     // ABC_FREE(s->loads    );
+    Mem += s->cap * sizeof(word);     // ABC_FREE(s->activity );
+    if ( s->activity2 )
+    Mem += s->cap * sizeof(word);     // ABC_FREE(s->activity );
+    if ( s->factors )
+    Mem += s->cap * sizeof(double);   // ABC_FREE(s->factors  );
+    Mem += s->cap * sizeof(int);      // ABC_FREE(s->orderpos );
+    Mem += s->cap * sizeof(int);      // ABC_FREE(s->reasons  );
+    Mem += s->cap * sizeof(lit);      // ABC_FREE(s->trail    );
+    Mem += s->cap * sizeof(int);      // ABC_FREE(s->model    );
+
+    Mem += s->order.cap * sizeof(int);
+    Mem += s->trail_lim.cap * sizeof(int);
+    Mem += s->tagged.cap * sizeof(int);
+//    Mem += s->learned.cap * sizeof(int);
+    Mem += s->stack.cap * sizeof(int);
+    Mem += s->act_vars.cap * sizeof(int);
+    Mem += s->unit_lits.cap * sizeof(int);
+    Mem += s->act_clas.cap * sizeof(int);
+    Mem += s->temp_clause.cap * sizeof(int);
+    Mem += s->conf_final.cap * sizeof(int);
+    Mem += Sat_MemMemoryAll( &s->Mem );
+    return Mem;
+}
+
+int sat_solver3_simplify(sat_solver3* s)
+{
+    assert(sat_solver3_dl(s) == 0);
+    if (sat_solver3_propagate(s) != 0)
+        return false;
+    return true;
+}
+
+void sat_solver3_reducedb(sat_solver3* s)
+{
+    static abctime TimeTotal = 0;
+    abctime clk = Abc_Clock();
+    Sat_Mem_t * pMem = &s->Mem;
+    int nLearnedOld = veci_size(&s->act_clas);
+    int * act_clas = veci_begin(&s->act_clas);
+    int * pPerm, * pArray, * pSortValues, nCutoffValue;
+    int i, k, j, Id, Counter, CounterStart, nSelected;
+    clause * c;
+
+    assert( s->nLearntMax > 0 );
+    assert( nLearnedOld == Sat_MemEntryNum(pMem, 1) );
+    assert( nLearnedOld == (int)s->stats.learnts );
+
+    s->nDBreduces++;
+
+    //printf( "Calling reduceDB with %d learned clause limit.\n", s->nLearntMax );
+    s->nLearntMax = s->nLearntStart + s->nLearntDelta * s->nDBreduces;
+//    return;
+
+    // create sorting values
+    pSortValues = ABC_ALLOC( int, nLearnedOld );
+    Sat_MemForEachLearned( pMem, c, i, k )
+    {
+        Id = clause_id(c);
+//        pSortValues[Id] = act[Id];
+        if ( s->ClaActType == 0 )
+            pSortValues[Id] = ((7 - Abc_MinInt(c->lbd, 7)) << 28) | (act_clas[Id] >> 4);
+        else
+            pSortValues[Id] = ((7 - Abc_MinInt(c->lbd, 7)) << 28);// | (act_clas[Id] >> 4);
+        assert( pSortValues[Id] >= 0 );
+    }
+
+    // preserve 1/20 of last clauses
+    CounterStart  = nLearnedOld - (s->nLearntMax / 20);
+
+    // preserve 3/4 of most active clauses
+    nSelected = nLearnedOld*s->nLearntRatio/100;
+
+    // find non-decreasing permutation
+    pPerm = Abc_MergeSortCost( pSortValues, nLearnedOld );
+    assert( pSortValues[pPerm[0]] <= pSortValues[pPerm[nLearnedOld-1]] );
+    nCutoffValue = pSortValues[pPerm[nLearnedOld-nSelected]];
+    ABC_FREE( pPerm );
+//    ActCutOff = ABC_INFINITY;
+
+    // mark learned clauses to remove
+    Counter = j = 0;
+    Sat_MemForEachLearned( pMem, c, i, k )
+    {
+        assert( c->mark == 0 );
+        if ( Counter++ > CounterStart || clause_size(c) < 3 || pSortValues[clause_id(c)] > nCutoffValue || s->reasons[lit_var(c->lits[0])] == Sat_MemHand(pMem, i, k) )
+            act_clas[j++] = act_clas[clause_id(c)];
+        else // delete
+        {
+            c->mark = 1;
+            s->stats.learnts_literals -= clause_size(c);
+            s->stats.learnts--;
+        }
+    }
+    assert( s->stats.learnts == (unsigned)j );
+    assert( Counter == nLearnedOld );
+    veci_resize(&s->act_clas,j);
+    ABC_FREE( pSortValues );
+
+    // update ID of each clause to be its new handle
+    Counter = Sat_MemCompactLearned( pMem, 0 );
+    assert( Counter == (int)s->stats.learnts );
+
+    // update reasons
+    for ( i = 0; i < s->size; i++ )
+    {
+        if ( !s->reasons[i] ) // no reason
+            continue;
+        if ( clause_is_lit(s->reasons[i]) ) // 2-lit clause
+            continue;
+        if ( !clause_learnt_h(pMem, s->reasons[i]) ) // problem clause
+            continue;
+        c = clause_read( s, s->reasons[i] );
+        assert( c->mark == 0 );
+        s->reasons[i] = clause_id(c); // updating handle here!!!
+    }
+
+    // update watches
+    for ( i = 0; i < s->size*2; i++ )
+    {
+        pArray = veci_begin(&s->wlists[i]);
+        for ( j = k = 0; k < veci_size(&s->wlists[i]); k++ )
+        {
+            if ( clause_is_lit(pArray[k]) ) // 2-lit clause
+                pArray[j++] = pArray[k];
+            else if ( !clause_learnt_h(pMem, pArray[k]) ) // problem clause
+                pArray[j++] = pArray[k];
+            else 
+            {
+                c = clause_read(s, pArray[k]);
+                if ( !c->mark ) // useful learned clause
+                   pArray[j++] = clause_id(c); // updating handle here!!!
+            }
+        }
+        veci_resize(&s->wlists[i],j);
+    }
+
+    // perform final move of the clauses
+    Counter = Sat_MemCompactLearned( pMem, 1 );
+    assert( Counter == (int)s->stats.learnts );
+
+    // report the results
+    TimeTotal += Abc_Clock() - clk;
+    if ( s->fVerbose )
+    {
+    Abc_Print(1, "reduceDB: Keeping %7d out of %7d clauses (%5.2f %%)  ",
+        s->stats.learnts, nLearnedOld, 100.0 * s->stats.learnts / nLearnedOld );
+    Abc_PrintTime( 1, "Time", TimeTotal );
+    }
+}
+
+
+// reverses to the previously bookmarked point
+void sat_solver3_rollback( sat_solver3* s )
+{
+    Sat_Mem_t * pMem = &s->Mem;
+    int i, k, j;
+    static int Count = 0;
+    Count++;
+    assert( s->iVarPivot >= 0 && s->iVarPivot <= s->size );
+    assert( s->iTrailPivot >= 0 && s->iTrailPivot <= s->qtail );
+    // reset implication queue
+    sat_solver3_canceluntil_rollback( s, s->iTrailPivot );
+    // update order 
+    if ( s->iVarPivot < s->size )
+    { 
+        if ( s->activity2 )
+        {
+            s->var_inc = s->var_inc2;
+            memcpy( s->activity, s->activity2, sizeof(word) * s->iVarPivot );
+        }
+        veci_resize(&s->order, 0);
+        for ( i = 0; i < s->iVarPivot; i++ )
+        {
+            if ( var_value(s, i) != varX )
+                continue;
+            s->orderpos[i] = veci_size(&s->order);
+            veci_push(&s->order,i);
+            order_update(s, i);
+        }
+    }
+    // compact watches
+    for ( i = 0; i < s->iVarPivot*2; i++ )
+    {
+        cla* pArray = veci_begin(&s->wlists[i]);
+        for ( j = k = 0; k < veci_size(&s->wlists[i]); k++ )
+        {
+            if ( clause_is_lit(pArray[k]) )
+            {
+                if ( clause_read_lit(pArray[k]) < s->iVarPivot*2 )
+                    pArray[j++] = pArray[k];
+            }
+            else if ( Sat_MemClauseUsed(pMem, pArray[k]) )
+                pArray[j++] = pArray[k];
+        }
+        veci_resize(&s->wlists[i],j);
+    }
+    // reset watcher lists
+    for ( i = 2*s->iVarPivot; i < 2*s->size; i++ )
+        s->wlists[i].size = 0;
+
+    // reset clause counts
+    s->stats.clauses = pMem->BookMarkE[0];
+    s->stats.learnts = pMem->BookMarkE[1];
+    // rollback clauses
+    Sat_MemRollBack( pMem );
+
+    // resize learned arrays
+    veci_resize(&s->act_clas,  s->stats.learnts);
+
+    // initialize other vars
+    s->size = s->iVarPivot;
+    if ( s->size == 0 )
+    {
+    //    s->size                   = 0;
+    //    s->cap                    = 0;
+        s->qhead                  = 0;
+        s->qtail                  = 0;
+
+        solver_init_activities(s);
+
+        s->root_level             = 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;
+
+        // initialize rollback
+        s->iVarPivot              =  0; // the pivot for variables
+        s->iTrailPivot            =  0; // the pivot for trail
+        s->hProofPivot            =  1; // the pivot for proof records
+    }
+}
+
+
+int sat_solver3_addclause(sat_solver3* s, lit* begin, lit* end)
+{
+    int fVerbose = 0;
+    lit *i,*j;
+    int maxvar;
+    lit last;
+    assert( begin < end );
+    if ( fVerbose )
+    {
+        for ( i = begin; i < end; i++ )
+            printf( "%s%d ", (*i)&1 ? "!":"", (*i)>>1 );
+        printf( "\n" );
+    }
+
+    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 );
+
+    // 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_solver3_setnvars(s,maxvar+1);
+
+    // 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) ? -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 && var_value(s, lit_var(*i)) == varX)
+            last = *j++ = *i;
+    }
+//    j = i;
+
+    if (j == begin)          // empty clause
+        return false;
+
+    if (j - begin == 1) // unit clause
+        return sat_solver3_enqueue(s,*begin,0);
+
+    // create new clause
+    sat_solver3_clause_new(s,begin,j,0);
+    return true;
+}
+
+static 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);
+} 
+
+static void luby_test()
+{
+    int i;
+    for ( i = 0; i < 20; i++ )
+        printf( "%d ", (int)luby(2,i) );
+    printf( "\n" );
+}
+
+static lbool sat_solver3_search(sat_solver3* s, ABC_INT64_T nof_conflicts)
+{
+//    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_solver3_dl(s));
+
+    s->nRestarts++;
+    s->stats.starts++;
+//    s->var_decay = (float)(1 / var_decay   );  // move this to sat_solver3_new()
+//    s->cla_decay = (float)(1 / clause_decay);  // move this to sat_solver3_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 (;;){
+        int hConfl = sat_solver3_propagate(s);
+        if (hConfl != 0){
+            // CONFLICT
+            int blevel;
+
+#ifdef VERBOSEDEBUG
+            printf(L_IND"**CONFLICT**\n", L_ind);
+#endif
+            s->stats.conflicts++; conflictC++;
+            if (sat_solver3_dl(s) == s->root_level){
+#ifdef SAT_USE_ANALYZE_FINAL
+                sat_solver3_analyze_final(s, hConfl, 0);
+#endif
+                veci_delete(&learnt_clause);
+                return l_False;
+            }
+
+            veci_resize(&learnt_clause,0);
+            sat_solver3_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_solver3_canceluntil(s,blevel);
+            sat_solver3_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 ) 
+                var_set_level(s, lit_var(learnt_clause.ptr[0]), 0);
+#endif
+            act_var_decay(s);
+            act_clause_decay(s);
+
+        }else{
+            // NO CONFLICT
+            int next;
+
+            // Reached bound on number of conflicts:
+            if ( (!s->fNoRestarts && nof_conflicts >= 0 && conflictC >= nof_conflicts) || (s->nRuntimeLimit && (s->stats.conflicts & 63) == 0 && Abc_Clock() > s->nRuntimeLimit)){
+                s->progress_estimate = sat_solver3_progress(s);
+                sat_solver3_canceluntil(s,s->root_level);
+                veci_delete(&learnt_clause);
+                return l_Undef; }
+
+            // Reached bound on number of conflicts:
+            if ( (s->nConfLimit && s->stats.conflicts > s->nConfLimit) ||
+                 (s->nInsLimit  && s->stats.propagations > s->nInsLimit) )
+            {
+                s->progress_estimate = sat_solver3_progress(s);
+                sat_solver3_canceluntil(s,s->root_level);
+                veci_delete(&learnt_clause);
+                return l_Undef; 
+            }
+
+            // Simplify the set of problem clauses:
+            if (sat_solver3_dl(s) == 0 && !s->fSkipSimplify)
+                sat_solver3_simplify(s);
+
+            // Reduce the set of learnt clauses:
+//            if (s->nLearntMax && veci_size(&s->learned) - s->qtail >= s->nLearntMax)
+            if (s->nLearntMax && veci_size(&s->act_clas) >= s->nLearntMax)
+                sat_solver3_reducedb(s);
+
+            // New variable decision:
+            s->stats.decisions++;
+            next = order_select(s,(float)random_var_freq);
+
+            if (next == var_Undef){
+                // Model found:
+                int i;
+                for (i = 0; i < s->size; i++)
+                    s->model[i] = (var_value(s,i)==var1 ? l_True : l_False);
+                sat_solver3_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 ( var_polar(s, next) ) // positive polarity
+                sat_solver3_decision(s,toLit(next));
+            else
+                sat_solver3_decision(s,lit_neg(toLit(next)));
+        }
+    }
+
+    return l_Undef; // cannot happen
+}
+
+// internal call to the SAT solver
+int sat_solver3_solve_internal(sat_solver3* s)
+{
+    lbool status = l_Undef;
+    int restart_iter = 0;
+    veci_resize(&s->unit_lits, 0);
+    s->nCalls++;
+
+    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){
+        ABC_INT64_T nof_conflicts;
+        double Ratio = (s->stats.learnts == 0)? 0.0 :
+            s->stats.learnts_literals / (double)s->stats.learnts;
+        if ( s->nRuntimeLimit && Abc_Clock() > 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)0, 
+                (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++) );
+        status = sat_solver3_search(s, nof_conflicts);
+        // quit the loop if reached an external limit
+        if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit )
+            break;
+        if ( s->nInsLimit  && s->stats.propagations > s->nInsLimit )
+            break;
+        if ( s->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit )
+            break;
+    }
+    if (s->verbosity >= 1)
+        printf("==============================================================================\n");
+
+    sat_solver3_canceluntil(s,s->root_level);
+    return status;
+}
+
+// pushing one assumption to the stack of assumptions
+int sat_solver3_push(sat_solver3* s, int p)
+{
+    assert(lit_var(p) < s->size);
+    veci_push(&s->trail_lim,s->qtail);
+    s->root_level++;
+    if (!sat_solver3_enqueue(s,p,0))
+    {
+        int h = s->reasons[lit_var(p)];
+        if (h)
+        {
+            if (clause_is_lit(h))
+            {
+                (clause_begin(s->binary))[1] = lit_neg(p);
+                (clause_begin(s->binary))[0] = clause_read_lit(h);
+                h = s->hBinary;
+            }
+            sat_solver3_analyze_final(s, h, 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 (var_level(s, lit_var(p)) > 0)
+                veci_push(&s->conf_final, p);
+        }
+        //sat_solver3_canceluntil(s, 0);
+        return false; 
+    }
+    else
+    {
+        int fConfl = sat_solver3_propagate(s);
+        if (fConfl){
+            sat_solver3_analyze_final(s, fConfl, 0);
+            //assert(s->conf_final.size > 0);
+            //sat_solver3_canceluntil(s, 0);
+            return false; }
+    }
+    return true;
+}
+
+// removing one assumption from the stack of assumptions
+void sat_solver3_pop(sat_solver3* s)
+{
+    assert( sat_solver3_dl(s) > 0 );
+    sat_solver3_canceluntil(s, --s->root_level);
+}
+
+void sat_solver3_set_resource_limits(sat_solver3* s, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
+{
+    // set the external limits
+    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;
+}
+
+int sat_solver3_solve(sat_solver3* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
+{
+    lbool status;
+    lit * i;
+    if ( s->fSolved )
+        return l_False;
+
+    if ( s->fVerbose )
+        printf( "Running SAT solver with parameters %d and %d and %d.\n", s->nLearntStart, s->nLearntDelta, s->nLearntRatio );
+
+    sat_solver3_set_resource_limits( s, nConfLimit, nInsLimit, nConfLimitGlobal, nInsLimitGlobal );
+
+#ifdef SAT_USE_ANALYZE_FINAL
+    // Perform assumptions:
+    s->root_level = 0;
+    for ( i = begin; i < end; i++ )
+        if ( !sat_solver3_push(s, *i) )
+        {
+            sat_solver3_canceluntil(s,0);
+            s->root_level = 0;
+            return l_False;
+        }
+    assert(s->root_level == sat_solver3_dl(s));
+#else
+    //printf("solve: "); printlits(begin, end); printf("\n");
+    for (i = begin; i < end; i++){
+//        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 varX: // l_Undef
+            sat_solver3_decision(s, *i);
+            if (sat_solver3_propagate(s) == 0)
+                break;
+            // fallthrough
+        case var0: // l_False 
+            sat_solver3_canceluntil(s, 0);
+            return l_False;
+        }
+    }
+    s->root_level = sat_solver3_dl(s);
+#endif
+
+    status = sat_solver3_solve_internal(s);
+
+    sat_solver3_canceluntil(s,0);
+    s->root_level = 0;
+    return status;
+}
+
+// This LEXSAT procedure should be called with a set of literals (pLits, nLits),
+// which defines both (1) variable order, and (2) assignment to begin search from.
+// It retuns the LEXSAT assigment that is the same or larger than the given one.
+// (It assumes that there is no smaller assignment than the one given!)
+// The resulting assignment is returned in the same set of literals (pLits, nLits).
+// It pushes/pops assumptions internally and will undo them before terminating.
+int sat_solver3_solve_lexsat( sat_solver3* s, int * pLits, int nLits )
+{
+    int i, iLitFail = -1;
+    lbool status;
+    assert( nLits > 0 );
+    // help the SAT solver by setting desirable polarity
+    sat_solver3_set_literal_polarity( s, pLits, nLits );
+    // check if there exists a satisfying assignment
+    status = sat_solver3_solve_internal( s );
+    if ( status != l_True ) // no assignment
+        return status;
+    // there is at least one satisfying assignment
+    assert( status == l_True );
+    // find the first mismatching literal
+    for ( i = 0; i < nLits; i++ )
+        if ( pLits[i] != sat_solver3_var_literal(s, Abc_Lit2Var(pLits[i])) )
+            break;
+    if ( i == nLits ) // no mismatch - the current assignment is the minimum one!
+        return l_True;
+    // mismatch happens in literal i
+    iLitFail = i;
+    // create assumptions up to this literal (as in pLits) - including this literal!
+    for ( i = 0; i <= iLitFail; i++ )
+        if ( !sat_solver3_push(s, pLits[i]) ) // can become UNSAT while adding the last assumption
+            break;
+    if ( i < iLitFail + 1 ) // the solver became UNSAT while adding assumptions
+        status = l_False;
+    else // solve under the assumptions
+        status = sat_solver3_solve_internal( s );
+    if ( status == l_True )
+    {
+        // we proved that there is a sat assignment with literal (iLitFail) having polarity as in pLits
+        // continue solving recursively
+        if ( iLitFail + 1 < nLits )
+            status = sat_solver3_solve_lexsat( s, pLits + iLitFail + 1, nLits - iLitFail - 1 );
+    }
+    else if ( status == l_False )
+    {
+        // we proved that there is no assignment with iLitFail having polarity as in pLits
+        assert( Abc_LitIsCompl(pLits[iLitFail]) ); // literal is 0 
+        // (this assert may fail only if there is a sat assignment smaller than one originally given in pLits)
+        // now we flip this literal (make it 1), change the last assumption
+        // and contiue looking for the 000...0-assignment of other literals
+        sat_solver3_pop( s );
+        pLits[iLitFail] = Abc_LitNot(pLits[iLitFail]);
+        if ( !sat_solver3_push(s, pLits[iLitFail]) )
+            printf( "sat_solver3_solve_lexsat(): A satisfying assignment should exist.\n" ); // because we know that the problem is satisfiable
+        // update other literals to be 000...0
+        for ( i = iLitFail + 1; i < nLits; i++ )
+            pLits[i] = Abc_LitNot( Abc_LitRegular(pLits[i]) );
+        // continue solving recursively
+        if ( iLitFail + 1 < nLits )
+            status = sat_solver3_solve_lexsat( s, pLits + iLitFail + 1, nLits - iLitFail - 1 );
+        else
+            status = l_True;
+    }
+    // undo the assumptions
+    for ( i = iLitFail; i >= 0; i-- )
+        sat_solver3_pop( s );
+    return status;
+}
+
+// This procedure is called on a set of assumptions to minimize their number.
+// The procedure relies on the fact that the current set of assumptions is UNSAT.  
+// It receives and returns SAT solver without assumptions. It returns the number 
+// of assumptions after minimization. The set of assumptions is returned in pLits.
+int sat_solver3_minimize_assumptions( sat_solver3* s, int * pLits, int nLits, int nConfLimit )
+{
+    int i, k, nLitsL, nLitsR, nResL, nResR;
+    if ( nLits == 1 )
+    {
+        // since the problem is UNSAT, we will try to solve it without assuming the last literal
+        // if the result is UNSAT, the last literal can be dropped; otherwise, it is needed
+        int status = l_False;
+        int Temp = s->nConfLimit; 
+        s->nConfLimit = nConfLimit;
+        status = sat_solver3_solve_internal( s );
+        s->nConfLimit = Temp;
+        return (int)(status != l_False); // return 1 if the problem is not UNSAT
+    }
+    assert( nLits >= 2 );
+    nLitsL = nLits / 2;
+    nLitsR = nLits - nLitsL;
+    // assume the left lits
+    for ( i = 0; i < nLitsL; i++ )
+        if ( !sat_solver3_push(s, pLits[i]) )
+        {
+            for ( k = i; k >= 0; k-- )
+                sat_solver3_pop(s);
+            return sat_solver3_minimize_assumptions( s, pLits, i+1, nConfLimit );
+        }
+    // solve for the right lits
+    nResL = sat_solver3_minimize_assumptions( s, pLits + nLitsL, nLitsR, nConfLimit );
+    for ( i = 0; i < nLitsL; i++ )
+        sat_solver3_pop(s);
+    // swap literals
+//    assert( nResL <= nLitsL );
+//    for ( i = 0; i < nResL; i++ )
+//        ABC_SWAP( int, pLits[i], pLits[nLitsL+i] );
+    veci_resize( &s->temp_clause, 0 );
+    for ( i = 0; i < nLitsL; i++ )
+        veci_push( &s->temp_clause, pLits[i] );
+    for ( i = 0; i < nResL; i++ )
+        pLits[i] = pLits[nLitsL+i];
+    for ( i = 0; i < nLitsL; i++ )
+        pLits[nResL+i] = veci_begin(&s->temp_clause)[i];
+    // assume the right lits
+    for ( i = 0; i < nResL; i++ )
+        if ( !sat_solver3_push(s, pLits[i]) )
+        {
+            for ( k = i; k >= 0; k-- )
+                sat_solver3_pop(s);
+            return sat_solver3_minimize_assumptions( s, pLits, i+1, nConfLimit );
+        }
+    // solve for the left lits
+    nResR = sat_solver3_minimize_assumptions( s, pLits + nResL, nLitsL, nConfLimit );
+    for ( i = 0; i < nResL; i++ )
+        sat_solver3_pop(s);
+    return nResL + nResR;
+}
+
+// This is a specialized version of the above procedure with several custom changes:
+// - makes sure that at least one of the marked literals is preserved in the clause
+// - sets literals to zero when they do not have to be used
+// - sets literals to zero for disproved variables
+int sat_solver3_minimize_assumptions2( sat_solver3* s, int * pLits, int nLits, int nConfLimit )
+{
+    int i, k, nLitsL, nLitsR, nResL, nResR;
+    if ( nLits == 1 )
+    {
+        // since the problem is UNSAT, we will try to solve it without assuming the last literal
+        // if the result is UNSAT, the last literal can be dropped; otherwise, it is needed
+        int RetValue = 1, LitNot = Abc_LitNot(pLits[0]);
+        int status = l_False;
+        int Temp = s->nConfLimit; 
+        s->nConfLimit = nConfLimit;
+
+        RetValue = sat_solver3_push( s, LitNot ); assert( RetValue );
+        status = sat_solver3_solve_internal( s );
+        sat_solver3_pop( s );
+
+        // if the problem is UNSAT, add clause
+        if ( status == l_False )
+        {
+            RetValue = sat_solver3_addclause( s, &LitNot, &LitNot+1 );
+            assert( RetValue );
+        }
+
+        s->nConfLimit = Temp;
+        return (int)(status != l_False); // return 1 if the problem is not UNSAT
+    }
+    assert( nLits >= 2 );
+    nLitsL = nLits / 2;
+    nLitsR = nLits - nLitsL;
+    // assume the left lits
+    for ( i = 0; i < nLitsL; i++ )
+        if ( !sat_solver3_push(s, pLits[i]) )
+        {
+            for ( k = i; k >= 0; k-- )
+                sat_solver3_pop(s);
+
+            // add clauses for these literal
+            for ( k = i+1; k > nLitsL; k++ )
+            {
+                int LitNot = Abc_LitNot(pLits[i]);
+                int RetValue = sat_solver3_addclause( s, &LitNot, &LitNot+1 );
+                assert( RetValue );
+            }
+
+            return sat_solver3_minimize_assumptions2( s, pLits, i+1, nConfLimit );
+        }
+    // solve for the right lits
+    nResL = sat_solver3_minimize_assumptions2( s, pLits + nLitsL, nLitsR, nConfLimit );
+    for ( i = 0; i < nLitsL; i++ )
+        sat_solver3_pop(s);
+    // swap literals
+//    assert( nResL <= nLitsL );
+    veci_resize( &s->temp_clause, 0 );
+    for ( i = 0; i < nLitsL; i++ )
+        veci_push( &s->temp_clause, pLits[i] );
+    for ( i = 0; i < nResL; i++ )
+        pLits[i] = pLits[nLitsL+i];
+    for ( i = 0; i < nLitsL; i++ )
+        pLits[nResL+i] = veci_begin(&s->temp_clause)[i];
+    // assume the right lits
+    for ( i = 0; i < nResL; i++ )
+        if ( !sat_solver3_push(s, pLits[i]) )
+        {
+            for ( k = i; k >= 0; k-- )
+                sat_solver3_pop(s);
+
+            // add clauses for these literal
+            for ( k = i+1; k > nResL; k++ )
+            {
+                int LitNot = Abc_LitNot(pLits[i]);
+                int RetValue = sat_solver3_addclause( s, &LitNot, &LitNot+1 );
+                assert( RetValue );
+            }
+
+            return sat_solver3_minimize_assumptions2( s, pLits, i+1, nConfLimit );
+        }
+    // solve for the left lits
+    nResR = sat_solver3_minimize_assumptions2( s, pLits + nResL, nLitsL, nConfLimit );
+    for ( i = 0; i < nResL; i++ )
+        sat_solver3_pop(s);
+    return nResL + nResR;
+}
+
+
+
+int sat_solver3_nvars(sat_solver3* s)
+{
+    return s->size;
+}
+
+
+int sat_solver3_nclauses(sat_solver3* s)
+{
+    return s->stats.clauses;
+}
+
+
+int sat_solver3_nconflicts(sat_solver3* s)
+{
+    return (int)s->stats.conflicts;
+}
+
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/bsat/satSolver3.h b/src/sat/bsat/satSolver3.h
new file mode 100644
index 00000000..2d2e7ded
--- /dev/null
+++ b/src/sat/bsat/satSolver3.h
@@ -0,0 +1,622 @@
+/**************************************************************************************************
+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 ABC__sat__bsat__satSolver3_h
+#define ABC__sat__bsat__satSolver3_h
+
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+
+#include "satVec.h"
+#include "satClause.h"
+#include "misc/util/utilDouble.h"
+
+ABC_NAMESPACE_HEADER_START
+
+//=================================================================================================
+// Public interface:
+
+struct sat_solver3_t;
+typedef struct sat_solver3_t sat_solver3;
+
+extern sat_solver3* sat_solver3_new(void);
+extern sat_solver3* zsat_solver3_new_seed(double seed);
+extern void        sat_solver3_delete(sat_solver3* s);
+
+extern int         sat_solver3_addclause(sat_solver3* s, lit* begin, lit* end);
+extern int         sat_solver3_clause_new(sat_solver3* s, lit* begin, lit* end, int learnt);
+extern int         sat_solver3_simplify(sat_solver3* s);
+extern int         sat_solver3_solve(sat_solver3* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal);
+extern int         sat_solver3_solve_internal(sat_solver3* s);
+extern int         sat_solver3_solve_lexsat(sat_solver3* s, int * pLits, int nLits);
+extern int         sat_solver3_minimize_assumptions( sat_solver3* s, int * pLits, int nLits, int nConfLimit );
+extern int         sat_solver3_minimize_assumptions2( sat_solver3* s, int * pLits, int nLits, int nConfLimit );
+extern int         sat_solver3_push(sat_solver3* s, int p);
+extern void        sat_solver3_pop(sat_solver3* s);
+extern void        sat_solver3_set_resource_limits(sat_solver3* s, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal);
+extern void        sat_solver3_restart( sat_solver3* s );
+extern void        zsat_solver3_restart_seed( sat_solver3* s, double seed );
+extern void        sat_solver3_rollback( sat_solver3* s );
+
+extern int         sat_solver3_nvars(sat_solver3* s);
+extern int         sat_solver3_nclauses(sat_solver3* s);
+extern int         sat_solver3_nconflicts(sat_solver3* s);
+extern double      sat_solver3_memory(sat_solver3* s);
+extern int         sat_solver3_count_assigned(sat_solver3* s);
+
+extern void        sat_solver3_setnvars(sat_solver3* s,int n);
+extern int         sat_solver3_get_var_value(sat_solver3* s, int v);
+extern void        sat_solver3_set_var_activity(sat_solver3* s, int * pVars, int nVars);
+
+extern void        sat_solver3WriteDimacs( sat_solver3 * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars );
+extern void        sat_solver3PrintStats( FILE * pFile, sat_solver3 * p );
+extern int *       sat_solver3GetModel( sat_solver3 * p, int * pVars, int nVars );
+extern void        sat_solver3DoubleClauses( sat_solver3 * p, int iVar );
+
+// trace recording
+extern void        sat_solver3TraceStart( sat_solver3 * pSat, char * pName );
+extern void        sat_solver3TraceStop( sat_solver3 * pSat );
+extern void        sat_solver3TraceWrite( sat_solver3 * pSat, int * pBeg, int * pEnd, int fRoot );
+
+// clause storage
+extern void        sat_solver3_store_alloc( sat_solver3 * s );
+extern void        sat_solver3_store_write( sat_solver3 * s, char * pFileName );
+extern void        sat_solver3_store_free( sat_solver3 * s );
+extern void        sat_solver3_store_mark_roots( sat_solver3 * s );
+extern void        sat_solver3_store_mark_clauses_a( sat_solver3 * s );
+extern void *      sat_solver3_store_release( sat_solver3 * s ); 
+
+//=================================================================================================
+// Solver representation:
+
+//struct clause_t;
+//typedef struct clause_t clause;
+
+struct varinfo_t;
+typedef struct varinfo_t varinfo;
+
+struct sat_solver3_t
+{
+    int         size;          // nof variables
+    int         cap;           // size of varmaps
+    int         qhead;         // Head index of queue.
+    int         qtail;         // Tail index of queue.
+
+    // clauses
+    Sat_Mem_t   Mem;
+    int         hLearnts;      // the first learnt clause
+    int         hBinary;       // the special binary clause
+    clause *    binary;
+    veci*       wlists;        // watcher lists
+
+    // rollback
+    int         iVarPivot;     // the pivot for variables
+    int         iTrailPivot;   // the pivot for trail
+    int         hProofPivot;   // the pivot for proof records
+
+    // activities
+    int         VarActType;
+    int         ClaActType;
+    word        var_inc;       // Amount to bump next variable with.
+    word        var_inc2;      // Amount to bump next variable with.
+    word        var_decay;     // INVERSE decay factor for variable activity: stores 1/decay. 
+    word*       activity;      // A heuristic measurement of the activity of a variable.
+    word*       activity2;     // backup variable activity
+    unsigned    cla_inc;       // Amount to bump next clause with.
+    unsigned    cla_decay;     // INVERSE decay factor for clause activity: stores 1/decay.
+    veci        act_clas;      // contain clause activities
+
+    char *      pFreqs;        // how many times this variable was assigned a value
+    int         nVarUsed;
+
+//    varinfo *   vi;            // variable information
+    int*        levels;        //
+    char*       assigns;       // Current values of variables.
+    char*       polarity;      //
+    char*       tags;          //
+    char*       loads;         //
+
+    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).
+    int *       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
+    int         fVerbose;
+
+    stats_t     stats;
+    int         nLearntMax;    // max number of learned clauses
+    int         nLearntStart;  // starting learned clause limit
+    int         nLearntDelta;  // delta of learned clause limit
+    int         nLearntRatio;  // ratio percentage of learned clauses
+    int         nDBreduces;    // number of DB reductions
+
+    ABC_INT64_T nConfLimit;    // external limit on the number of conflicts
+    ABC_INT64_T nInsLimit;     // external limit on the number of implications
+    abctime     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
+    veci        unit_lits;     // variables whose activity has changed
+    veci        pivot_vars;    // pivot variables
+
+    int         fSkipSimplify; // set to one to skip simplification of the clause database
+    int         fNotUseRandom; // do not allow random decisions with a fixed probability
+    int         fNoRestarts;   // disables periodic restarts
+
+    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
+
+    // CNF loading
+    void *      pCnfMan;           // external CNF manager
+    int(*pCnfFunc)(void * p, int); // external callback
+};
+
+static inline clause * clause_read( sat_solver3 * s, cla h )          
+{ 
+    return Sat_MemClauseHand( &s->Mem, h );      
+}
+
+static int sat_solver3_var_value( sat_solver3* s, int v )
+{
+    assert( v >= 0 && v < s->size );
+    return (int)(s->model[v] == l_True);
+}
+static int sat_solver3_var_literal( sat_solver3* s, int v )
+{
+    assert( v >= 0 && v < s->size );
+    return toLitCond( v, s->model[v] != l_True );
+}
+static void sat_solver3_act_var_clear(sat_solver3* s) 
+{
+    int i;
+    if ( s->VarActType == 0 )
+    {
+        for (i = 0; i < s->size; i++)
+            s->activity[i] = (1 << 10);
+        s->var_inc = (1 << 5);
+    }
+    else if ( s->VarActType == 1 )
+    {
+        for (i = 0; i < s->size; i++)
+            s->activity[i] = 0;
+        s->var_inc = 1;
+    }
+    else if ( s->VarActType == 2 )
+    {
+        for (i = 0; i < s->size; i++)
+            s->activity[i] = Xdbl_Const1();
+        s->var_inc = Xdbl_Const1();
+    }
+    else assert(0);
+}
+static void sat_solver3_compress(sat_solver3* s) 
+{
+    if ( s->qtail != s->qhead )
+    {
+        int RetValue = sat_solver3_simplify(s);
+        assert( RetValue != 0 );
+        (void) RetValue;
+    }
+}
+static void sat_solver3_delete_p( sat_solver3 ** ps )
+{
+    if ( *ps )
+        sat_solver3_delete( *ps );
+    *ps = NULL;
+}
+static void sat_solver3_clean_polarity(sat_solver3* s, int * pVars, int nVars )
+{
+    int i;
+    for ( i = 0; i < nVars; i++ )
+        s->polarity[pVars[i]] = 0;
+}
+static void sat_solver3_set_polarity(sat_solver3* s, int * pVars, int nVars )
+{
+    int i;
+    for ( i = 0; i < s->size; i++ )
+        s->polarity[i] = 0;
+    for ( i = 0; i < nVars; i++ )
+        s->polarity[pVars[i]] = 1;
+}
+static void sat_solver3_set_literal_polarity(sat_solver3* s, int * pLits, int nLits )
+{
+    int i;
+    for ( i = 0; i < nLits; i++ )
+        s->polarity[Abc_Lit2Var(pLits[i])] = !Abc_LitIsCompl(pLits[i]);
+}
+
+static int sat_solver3_final(sat_solver3* s, int ** ppArray)
+{
+    *ppArray = s->conf_final.ptr;
+    return s->conf_final.size;
+}
+
+static abctime sat_solver3_set_runtime_limit(sat_solver3* s, abctime Limit)
+{
+    abctime nRuntimeLimit = s->nRuntimeLimit;
+    s->nRuntimeLimit = Limit;
+    return nRuntimeLimit;
+}
+
+static int sat_solver3_set_random(sat_solver3* s, int fNotUseRandom)
+{
+    int fNotUseRandomOld = s->fNotUseRandom;
+    s->fNotUseRandom = fNotUseRandom;
+    return fNotUseRandomOld;
+}
+
+static inline void sat_solver3_bookmark(sat_solver3* s)
+{
+    assert( s->qhead == s->qtail );
+    s->iVarPivot    = s->size;
+    s->iTrailPivot  = s->qhead;
+    Sat_MemBookMark( &s->Mem );
+    if ( s->activity2 )
+    {
+        s->var_inc2 = s->var_inc;
+        memcpy( s->activity2, s->activity, sizeof(word) * s->iVarPivot );
+    }
+}
+static inline void sat_solver3_set_pivot_variables( sat_solver3* s, int * pPivots, int nPivots )
+{
+    s->pivot_vars.cap = nPivots;
+    s->pivot_vars.size = nPivots;
+    s->pivot_vars.ptr = pPivots;
+}
+static inline int sat_solver3_count_usedvars(sat_solver3* s)
+{
+    int i, nVars = 0;
+    for ( i = 0; i < s->size; i++ )
+        if ( s->pFreqs[i] )
+        {
+            s->pFreqs[i] = 0;
+            nVars++;
+        }
+    return nVars;
+}
+
+static inline int sat_solver3_add_const( sat_solver3 * pSat, int iVar, int fCompl )
+{
+    lit Lits[1];
+    int Cid;
+    assert( iVar >= 0 );
+
+    Lits[0] = toLitCond( iVar, fCompl );
+    Cid = sat_solver3_addclause( pSat, Lits, Lits + 1 );
+    assert( Cid );
+    return 1;
+}
+static inline int sat_solver3_add_buffer( sat_solver3 * pSat, int iVarA, int iVarB, int fCompl )
+{
+    lit Lits[2];
+    int Cid;
+    assert( iVarA >= 0 && iVarB >= 0 );
+
+    Lits[0] = toLitCond( iVarA, 0 );
+    Lits[1] = toLitCond( iVarB, !fCompl );
+    Cid = sat_solver3_addclause( pSat, Lits, Lits + 2 );
+    if ( Cid == 0 )
+        return 0;
+    assert( Cid );
+
+    Lits[0] = toLitCond( iVarA, 1 );
+    Lits[1] = toLitCond( iVarB, fCompl );
+    Cid = sat_solver3_addclause( pSat, Lits, Lits + 2 );
+    if ( Cid == 0 )
+        return 0;
+    assert( Cid );
+    return 2;
+}
+static inline int sat_solver3_add_buffer_enable( sat_solver3 * pSat, int iVarA, int iVarB, int iVarEn, int fCompl )
+{
+    lit Lits[3];
+    int Cid;
+    assert( iVarA >= 0 && iVarB >= 0 && iVarEn >= 0 );
+
+    Lits[0] = toLitCond( iVarA, 0 );
+    Lits[1] = toLitCond( iVarB, !fCompl );
+    Lits[2] = toLitCond( iVarEn, 1 );
+    Cid = sat_solver3_addclause( pSat, Lits, Lits + 3 );
+    assert( Cid );
+
+    Lits[0] = toLitCond( iVarA, 1 );
+    Lits[1] = toLitCond( iVarB, fCompl );
+    Lits[2] = toLitCond( iVarEn, 1 );
+    Cid = sat_solver3_addclause( pSat, Lits, Lits + 3 );
+    assert( Cid );
+    return 2;
+}
+static inline int sat_solver3_add_and( sat_solver3 * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fCompl )
+{
+    lit Lits[3];
+    int Cid;
+
+    Lits[0] = toLitCond( iVar, !fCompl );
+    Lits[1] = toLitCond( iVar0, fCompl0 );
+    Cid = sat_solver3_addclause( pSat, Lits, Lits + 2 );
+    assert( Cid );
+
+    Lits[0] = toLitCond( iVar, !fCompl );
+    Lits[1] = toLitCond( iVar1, fCompl1 );
+    Cid = sat_solver3_addclause( pSat, Lits, Lits + 2 );
+    assert( Cid );
+
+    Lits[0] = toLitCond( iVar, fCompl );
+    Lits[1] = toLitCond( iVar0, !fCompl0 );
+    Lits[2] = toLitCond( iVar1, !fCompl1 );
+    Cid = sat_solver3_addclause( pSat, Lits, Lits + 3 );
+    assert( Cid );
+    return 3;
+}
+static inline int sat_solver3_add_xor( sat_solver3 * pSat, int iVarA, int iVarB, int iVarC, int fCompl )
+{
+    lit Lits[3];
+    int Cid;
+    assert( iVarA >= 0 && iVarB >= 0 && iVarC >= 0 );
+
+    Lits[0] = toLitCond( iVarA, !fCompl );
+    Lits[1] = toLitCond( iVarB, 1 );
+    Lits[2] = toLitCond( iVarC, 1 );
+    Cid = sat_solver3_addclause( pSat, Lits, Lits + 3 );
+    assert( Cid );
+
+    Lits[0] = toLitCond( iVarA, !fCompl );
+    Lits[1] = toLitCond( iVarB, 0 );
+    Lits[2] = toLitCond( iVarC, 0 );
+    Cid = sat_solver3_addclause( pSat, Lits, Lits + 3 );
+    assert( Cid );
+
+    Lits[0] = toLitCond( iVarA, fCompl );
+    Lits[1] = toLitCond( iVarB, 1 );
+    Lits[2] = toLitCond( iVarC, 0 );
+    Cid = sat_solver3_addclause( pSat, Lits, Lits + 3 );
+    assert( Cid );
+
+    Lits[0] = toLitCond( iVarA, fCompl );
+    Lits[1] = toLitCond( iVarB, 0 );
+    Lits[2] = toLitCond( iVarC, 1 );
+    Cid = sat_solver3_addclause( pSat, Lits, Lits + 3 );
+    assert( Cid );
+    return 4;
+}
+static inline int sat_solver3_add_mux( sat_solver3 * pSat, int iVarZ, int iVarC, int iVarT, int iVarE, int iComplC, int iComplT, int iComplE, int iComplZ )
+{
+    lit Lits[3];
+    int Cid;
+    assert( iVarC >= 0 && iVarT >= 0 && iVarE >= 0 && iVarZ >= 0 );
+
+    Lits[0] = toLitCond( iVarC, 1 ^ iComplC );
+    Lits[1] = toLitCond( iVarT, 1 ^ iComplT );
+    Lits[2] = toLitCond( iVarZ, 0 );
+    Cid = sat_solver3_addclause( pSat, Lits, Lits + 3 );
+    assert( Cid );
+
+    Lits[0] = toLitCond( iVarC, 1 ^ iComplC );
+    Lits[1] = toLitCond( iVarT, 0 ^ iComplT );
+    Lits[2] = toLitCond( iVarZ, 1 ^ iComplZ );
+    Cid = sat_solver3_addclause( pSat, Lits, Lits + 3 );
+    assert( Cid );
+
+    Lits[0] = toLitCond( iVarC, 0 ^ iComplC );
+    Lits[1] = toLitCond( iVarE, 1 ^ iComplE );
+    Lits[2] = toLitCond( iVarZ, 0 ^ iComplZ );
+    Cid = sat_solver3_addclause( pSat, Lits, Lits + 3 );
+    assert( Cid );
+
+    Lits[0] = toLitCond( iVarC, 0 ^ iComplC );
+    Lits[1] = toLitCond( iVarE, 0 ^ iComplE );
+    Lits[2] = toLitCond( iVarZ, 1 ^ iComplZ );
+    Cid = sat_solver3_addclause( pSat, Lits, Lits + 3 );
+    assert( Cid );
+
+    if ( iVarT == iVarE )
+        return 4;
+
+    Lits[0] = toLitCond( iVarT, 0 ^ iComplT );
+    Lits[1] = toLitCond( iVarE, 0 ^ iComplE );
+    Lits[2] = toLitCond( iVarZ, 1 ^ iComplZ );
+    Cid = sat_solver3_addclause( pSat, Lits, Lits + 3 );
+    assert( Cid );
+
+    Lits[0] = toLitCond( iVarT, 1 ^ iComplT );
+    Lits[1] = toLitCond( iVarE, 1 ^ iComplE );
+    Lits[2] = toLitCond( iVarZ, 0 ^ iComplZ );
+    Cid = sat_solver3_addclause( pSat, Lits, Lits + 3 );
+    assert( Cid );
+    return 6;
+}
+static inline int sat_solver3_add_mux41( sat_solver3 * pSat, int iVarZ, int iVarC0, int iVarC1, int iVarD0, int iVarD1, int iVarD2, int iVarD3 )
+{
+    lit Lits[4];
+    int Cid;
+    assert( iVarC0 >= 0 && iVarC1 >= 0 && iVarD0 >= 0 && iVarD1 >= 0 && iVarD2 >= 0 && iVarD3 >= 0 && iVarZ >= 0 );
+
+    Lits[0] = toLitCond( iVarD0, 1 );
+    Lits[1] = toLitCond( iVarC0, 0 );
+    Lits[2] = toLitCond( iVarC1, 0 );
+    Lits[3] = toLitCond( iVarZ,  0 );
+    Cid = sat_solver3_addclause( pSat, Lits, Lits + 4 );
+    assert( Cid );
+
+    Lits[0] = toLitCond( iVarD1, 1 );
+    Lits[1] = toLitCond( iVarC0, 1 );
+    Lits[2] = toLitCond( iVarC1, 0 );
+    Lits[3] = toLitCond( iVarZ,  0 );
+    Cid = sat_solver3_addclause( pSat, Lits, Lits + 4 );
+    assert( Cid );
+
+    Lits[0] = toLitCond( iVarD2, 1 );
+    Lits[1] = toLitCond( iVarC0, 0 );
+    Lits[2] = toLitCond( iVarC1, 1 );
+    Lits[3] = toLitCond( iVarZ,  0 );
+    Cid = sat_solver3_addclause( pSat, Lits, Lits + 4 );
+    assert( Cid );
+
+    Lits[0] = toLitCond( iVarD3, 1 );
+    Lits[1] = toLitCond( iVarC0, 1 );
+    Lits[2] = toLitCond( iVarC1, 1 );
+    Lits[3] = toLitCond( iVarZ,  0 );
+    Cid = sat_solver3_addclause( pSat, Lits, Lits + 4 );
+    assert( Cid );
+
+
+    Lits[0] = toLitCond( iVarD0, 0 );
+    Lits[1] = toLitCond( iVarC0, 0 );
+    Lits[2] = toLitCond( iVarC1, 0 );
+    Lits[3] = toLitCond( iVarZ,  1 );
+    Cid = sat_solver3_addclause( pSat, Lits, Lits + 4 );
+    assert( Cid );
+
+    Lits[0] = toLitCond( iVarD1, 0 );
+    Lits[1] = toLitCond( iVarC0, 1 );
+    Lits[2] = toLitCond( iVarC1, 0 );
+    Lits[3] = toLitCond( iVarZ,  1 );
+    Cid = sat_solver3_addclause( pSat, Lits, Lits + 4 );
+    assert( Cid );
+
+    Lits[0] = toLitCond( iVarD2, 0 );
+    Lits[1] = toLitCond( iVarC0, 0 );
+    Lits[2] = toLitCond( iVarC1, 1 );
+    Lits[3] = toLitCond( iVarZ,  1 );
+    Cid = sat_solver3_addclause( pSat, Lits, Lits + 4 );
+    assert( Cid );
+
+    Lits[0] = toLitCond( iVarD3, 0 );
+    Lits[1] = toLitCond( iVarC0, 1 );
+    Lits[2] = toLitCond( iVarC1, 1 );
+    Lits[3] = toLitCond( iVarZ,  1 );
+    Cid = sat_solver3_addclause( pSat, Lits, Lits + 4 );
+    assert( Cid );
+    return 8;
+}
+static inline int sat_solver3_add_xor_and( sat_solver3 * pSat, int iVarF, int iVarA, int iVarB, int iVarC )
+{
+    // F = (a (+) b) * c
+    lit Lits[4];
+    int Cid;
+    assert( iVarF >= 0 && iVarA >= 0 && iVarB >= 0 && iVarC >= 0 );
+
+    Lits[0] = toLitCond( iVarF, 1 );
+    Lits[1] = toLitCond( iVarA, 1 );
+    Lits[2] = toLitCond( iVarB, 1 );
+    Cid = sat_solver3_addclause( pSat, Lits, Lits + 3 );
+    assert( Cid );
+
+    Lits[0] = toLitCond( iVarF, 1 );
+    Lits[1] = toLitCond( iVarA, 0 );
+    Lits[2] = toLitCond( iVarB, 0 );
+    Cid = sat_solver3_addclause( pSat, Lits, Lits + 3 );
+    assert( Cid );
+
+    Lits[0] = toLitCond( iVarF, 1 );
+    Lits[1] = toLitCond( iVarC, 0 );
+    Cid = sat_solver3_addclause( pSat, Lits, Lits + 2 );
+    assert( Cid );
+
+    Lits[0] = toLitCond( iVarF, 0 );
+    Lits[1] = toLitCond( iVarA, 1 );
+    Lits[2] = toLitCond( iVarB, 0 );
+    Lits[3] = toLitCond( iVarC, 1 );
+    Cid = sat_solver3_addclause( pSat, Lits, Lits + 4 );
+    assert( Cid );
+
+    Lits[0] = toLitCond( iVarF, 0 );
+    Lits[1] = toLitCond( iVarA, 0 );
+    Lits[2] = toLitCond( iVarB, 1 );
+    Lits[3] = toLitCond( iVarC, 1 );
+    Cid = sat_solver3_addclause( pSat, Lits, Lits + 4 );
+    assert( Cid );
+    return 5;
+}
+static inline int sat_solver3_add_constraint( sat_solver3 * pSat, int iVar, int iVar2, int fCompl )
+{
+    lit Lits[2];
+    int Cid;
+    assert( iVar >= 0 );
+
+    Lits[0] = toLitCond( iVar, fCompl );
+    Lits[1] = toLitCond( iVar2, 0 );
+    Cid = sat_solver3_addclause( pSat, Lits, Lits + 2 );
+    assert( Cid );
+
+    Lits[0] = toLitCond( iVar, fCompl );
+    Lits[1] = toLitCond( iVar2, 1 );
+    Cid = sat_solver3_addclause( pSat, Lits, Lits + 2 );
+    assert( Cid );
+    return 2;
+}
+
+static inline int sat_solver3_add_half_sorter( sat_solver3 * pSat, int iVarA, int iVarB, int iVar0, int iVar1 )
+{
+    lit Lits[3];
+    int Cid;
+
+    Lits[0] = toLitCond( iVarA, 0 );
+    Lits[1] = toLitCond( iVar0, 1 );
+    Cid = sat_solver3_addclause( pSat, Lits, Lits + 2 );
+    assert( Cid );
+
+    Lits[0] = toLitCond( iVarA, 0 );
+    Lits[1] = toLitCond( iVar1, 1 );
+    Cid = sat_solver3_addclause( pSat, Lits, Lits + 2 );
+    assert( Cid );
+
+    Lits[0] = toLitCond( iVarB, 0 );
+    Lits[1] = toLitCond( iVar0, 1 );
+    Lits[2] = toLitCond( iVar1, 1 );
+    Cid = sat_solver3_addclause( pSat, Lits, Lits + 3 );
+    assert( Cid );
+    return 3;
+}
+
+
+ABC_NAMESPACE_HEADER_END
+
+#endif