Started experiments with a new solver.

16 files changed, 2092 insertions, 113 deletions

diff --git a/abclib.dsp b/abclib.dsp
index 4c722dd1..6bc62da1 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -1275,6 +1275,14 @@ SOURCE=.\src\sat\bsat\satSolver.h
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\sat\bsat\satSolver2.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\bsat\satSolver2.h
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\sat\bsat\satStore.c
 # End Source File
 # Begin Source File
diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c
index 837ca2c2..85311229 100644
--- a/src/aig/cnf/cnfMan.c
+++ b/src/aig/cnf/cnfMan.c
@@ -20,6 +20,7 @@
 
 #include "cnf.h"
 #include "satSolver.h"
+#include "satSolver2.h"
 #include "zlib.h"
 
 ABC_NAMESPACE_IMPL_START
@@ -416,6 +417,98 @@ void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit )
 
 /**Function*************************************************************
 
+  Synopsis    [Writes CNF into a file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void * Cnf_DataWriteIntoSolver2( Cnf_Dat_t * p, int nFrames, int fInit )
+{
+    sat_solver2 * pSat;
+    int i, f, status;
+    assert( nFrames > 0 );
+    pSat = sat_solver2_new();
+    sat_solver2_setnvars( pSat, p->nVars * nFrames );
+    for ( i = 0; i < p->nClauses; i++ )
+    {
+        if ( !sat_solver2_addclause( pSat, p->pClauses[i], p->pClauses[i+1] ) )
+        {
+            sat_solver2_delete( pSat );
+            return NULL;
+        }
+    }
+    if ( nFrames > 1 )
+    {
+        Aig_Obj_t * pObjLo, * pObjLi;
+        int nLitsAll, * pLits, Lits[2];
+        nLitsAll = 2 * p->nVars;
+        pLits = p->pClauses[0];
+        for ( f = 1; f < nFrames; f++ )
+        {
+            // add equality of register inputs/outputs for different timeframes
+            Aig_ManForEachLiLoSeq( p->pMan, pObjLi, pObjLo, i )
+            {
+                Lits[0] = (f-1)*nLitsAll + toLitCond( p->pVarNums[pObjLi->Id], 0 );
+                Lits[1] =  f   *nLitsAll + toLitCond( p->pVarNums[pObjLo->Id], 1 );
+                if ( !sat_solver2_addclause( pSat, Lits, Lits + 2 ) )
+                {
+                    sat_solver2_delete( pSat );
+                    return NULL;
+                }
+                Lits[0]++;
+                Lits[1]--;
+                if ( !sat_solver2_addclause( pSat, Lits, Lits + 2 ) )
+                {
+                    sat_solver2_delete( pSat );
+                    return NULL;
+                }
+            }
+            // add clauses for the next timeframe
+            for ( i = 0; i < p->nLiterals; i++ )
+                pLits[i] += nLitsAll;
+            for ( i = 0; i < p->nClauses; i++ )
+            {
+                if ( !sat_solver2_addclause( pSat, p->pClauses[i], p->pClauses[i+1] ) )
+                {
+                    sat_solver2_delete( pSat );
+                    return NULL;
+                }
+            }
+        }
+        // return literals to their original state
+        nLitsAll = (f-1) * nLitsAll;
+        for ( i = 0; i < p->nLiterals; i++ )
+            pLits[i] -= nLitsAll;
+    }
+    if ( fInit )
+    {
+        Aig_Obj_t * pObjLo;
+        int Lits[1];
+        Aig_ManForEachLoSeq( p->pMan, pObjLo, i )
+        {
+            Lits[0] = toLitCond( p->pVarNums[pObjLo->Id], 1 );
+            if ( !sat_solver2_addclause( pSat, Lits, Lits + 1 ) )
+            {
+                sat_solver2_delete( pSat );
+                return NULL;
+            }
+        }
+    }
+    status = sat_solver2_simplify(pSat);
+    if ( status == 0 )
+    {
+        sat_solver2_delete( pSat );
+        return NULL;
+    }
+    return pSat;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Adds the OR-clause.]
 
   Description []
@@ -453,6 +546,34 @@ int Cnf_DataWriteOrClause( void * p, Cnf_Dat_t * pCnf )
   SeeAlso     []
 
 ***********************************************************************/
+int Cnf_DataWriteOrClause2( void * p, Cnf_Dat_t * pCnf )
+{
+    sat_solver2 * pSat = (sat_solver2 *)p;
+    Aig_Obj_t * pObj;
+    int i, * pLits;
+    pLits = ABC_ALLOC( int, Aig_ManPoNum(pCnf->pMan) );
+    Aig_ManForEachPo( pCnf->pMan, pObj, i )
+        pLits[i] = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
+    if ( !sat_solver2_addclause( pSat, pLits, pLits + Aig_ManPoNum(pCnf->pMan) ) )
+    {
+        ABC_FREE( pLits );
+        return 0;
+    }
+    ABC_FREE( pLits );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds the OR-clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Cnf_DataWriteAndClauses( void * p, Cnf_Dat_t * pCnf )
 {
     sat_solver * pSat = (sat_solver *)p;
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index a0073ca1..ea362bdf 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -286,7 +286,7 @@ static inline int          Fra_ImpCreate( int Left, int Right )
 ////////////////////////////////////////////////////////////////////////
 
 /*=== fraCec.c ========================================================*/
-extern int                 Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fVerbose );
+extern int                 Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose );
 extern int                 Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose );
 extern int                 Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose );
 /*=== fraClass.c ========================================================*/
diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c
index 037e6c70..1c36ea62 100644
--- a/src/aig/fra/fraCec.c
+++ b/src/aig/fra/fraCec.c
@@ -20,6 +20,7 @@
 
 #include "fra.h"
 #include "cnf.h"
+#include "satSolver2.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -43,111 +44,223 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fVerbose )
+int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose )
 {
-    sat_solver * pSat;
-    Cnf_Dat_t * pCnf;
-    int status, RetValue, clk = clock();
-    Vec_Int_t * vCiIds;
+    if ( fNewSolver )
+    {
+        extern void * Cnf_DataWriteIntoSolver2( Cnf_Dat_t * p, int nFrames, int fInit );
+        extern int    Cnf_DataWriteOrClause2( void * pSat, Cnf_Dat_t * pCnf );
 
-    assert( Aig_ManRegNum(pMan) == 0 );
-    pMan->pData = NULL;
+        sat_solver2 * pSat;
+        Cnf_Dat_t * pCnf;
+        int status, RetValue, clk = clock();
+        Vec_Int_t * vCiIds;
 
-    // derive CNF
-    pCnf = Cnf_Derive( pMan, Aig_ManPoNum(pMan) );
-//    pCnf = Cnf_DeriveSimple( pMan, Aig_ManPoNum(pMan) );
+        assert( Aig_ManRegNum(pMan) == 0 );
+        pMan->pData = NULL;
 
-    if ( fFlipBits ) 
-        Cnf_DataTranformPolarity( pCnf, 0 );
+        // derive CNF
+        pCnf = Cnf_Derive( pMan, Aig_ManPoNum(pMan) );
+    //    pCnf = Cnf_DeriveSimple( pMan, Aig_ManPoNum(pMan) );
 
-    // convert into SAT solver
-    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
-    if ( pSat == NULL )
-    {
+        if ( fFlipBits ) 
+            Cnf_DataTranformPolarity( pCnf, 0 );
+
+        // convert into SAT solver
+        pSat = (sat_solver2 *)Cnf_DataWriteIntoSolver2( pCnf, 1, 0 );
+        if ( pSat == NULL )
+        {
+            Cnf_DataFree( pCnf );
+            return 1;
+        }
+
+
+        if ( fAndOuts )
+        {
+            // assert each output independently
+            if ( !Cnf_DataWriteAndClauses( pSat, pCnf ) )
+            {
+                sat_solver2_delete( pSat );
+                Cnf_DataFree( pCnf );
+                return 1;
+            }
+        }
+        else
+        {
+            // add the OR clause for the outputs
+            if ( !Cnf_DataWriteOrClause2( pSat, pCnf ) )
+            {
+                sat_solver2_delete( pSat );
+                Cnf_DataFree( pCnf );
+                return 1;
+            }
+        }
+        vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan );
         Cnf_DataFree( pCnf );
-        return 1;
-    }
 
 
-    if ( fAndOuts )
-    {
-        // assert each output independently
-        if ( !Cnf_DataWriteAndClauses( pSat, pCnf ) )
+        printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver2_nvars(pSat), sat_solver2_nclauses(pSat) );
+        ABC_PRT( "Time", clock() - clk );
+
+        // simplify the problem
+        clk = clock();
+        status = sat_solver2_simplify(pSat);
+        printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver2_nvars(pSat), sat_solver2_nclauses(pSat) );
+        ABC_PRT( "Time", clock() - clk );
+        if ( status == 0 )
         {
-            sat_solver_delete( pSat );
-            Cnf_DataFree( pCnf );
+            Vec_IntFree( vCiIds );
+            sat_solver2_delete( pSat );
+    //        printf( "The problem is UNSATISFIABLE after simplification.\n" );
             return 1;
         }
+
+        // solve the miter
+        clk = clock();
+        if ( fVerbose )
+            pSat->verbosity = 1;
+        status = sat_solver2_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+        if ( status == l_Undef )
+        {
+    //        printf( "The problem timed out.\n" );
+            RetValue = -1;
+        }
+        else if ( status == l_True )
+        {
+    //        printf( "The problem is SATISFIABLE.\n" );
+            RetValue = 0;
+        }
+        else if ( status == l_False )
+        {
+    //        printf( "The problem is UNSATISFIABLE.\n" );
+            RetValue = 1;
+        }
+        else
+            assert( 0 );
+
+    //    Abc_Print( 1, "The number of conflicts = %6d.  ", (int)pSat->stats.conflicts );
+    //    Abc_PrintTime( 1, "Solving time", clock() - clk );
+ 
+        // if the problem is SAT, get the counterexample
+        if ( status == l_True )
+        {
+            pMan->pData = Sat_Solver2GetModel( pSat, vCiIds->pArray, vCiIds->nSize );
+        }
+        // free the sat_solver2
+//        if ( fVerbose )
+            Sat_Solver2PrintStats( stdout, pSat );
+    //sat_solver2_store_write( pSat, "trace.cnf" );
+    //sat_solver2_store_free( pSat );
+        sat_solver2_delete( pSat );
+        Vec_IntFree( vCiIds );
+        return RetValue;
     }
     else
     {
-        // add the OR clause for the outputs
-        if ( !Cnf_DataWriteOrClause( pSat, pCnf ) )
+        sat_solver * pSat;
+        Cnf_Dat_t * pCnf;
+        int status, RetValue, clk = clock();
+        Vec_Int_t * vCiIds;
+
+        assert( Aig_ManRegNum(pMan) == 0 );
+        pMan->pData = NULL;
+
+        // derive CNF
+        pCnf = Cnf_Derive( pMan, Aig_ManPoNum(pMan) );
+    //    pCnf = Cnf_DeriveSimple( pMan, Aig_ManPoNum(pMan) );
+
+        if ( fFlipBits ) 
+            Cnf_DataTranformPolarity( pCnf, 0 );
+
+        // convert into SAT solver
+        pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+        if ( pSat == NULL )
         {
-            sat_solver_delete( pSat );
             Cnf_DataFree( pCnf );
             return 1;
         }
-    }
-    vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan );
-    Cnf_DataFree( pCnf );
 
 
-//    printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
-//    ABC_PRT( "Time", clock() - clk );
+        if ( fAndOuts )
+        {
+            // assert each output independently
+            if ( !Cnf_DataWriteAndClauses( pSat, pCnf ) )
+            {
+                sat_solver_delete( pSat );
+                Cnf_DataFree( pCnf );
+                return 1;
+            }
+        }
+        else
+        {
+            // add the OR clause for the outputs
+            if ( !Cnf_DataWriteOrClause( pSat, pCnf ) )
+            {
+                sat_solver_delete( pSat );
+                Cnf_DataFree( pCnf );
+                return 1;
+            }
+        }
+        vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan );
+        Cnf_DataFree( pCnf );
 
-    // simplify the problem
-    clk = clock();
-    status = sat_solver_simplify(pSat);
-//    printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
-//    ABC_PRT( "Time", clock() - clk );
-    if ( status == 0 )
-    {
-        Vec_IntFree( vCiIds );
-        sat_solver_delete( pSat );
-//        printf( "The problem is UNSATISFIABLE after simplification.\n" );
-        return 1;
-    }
 
-    // solve the miter
-    clk = clock();
-    if ( fVerbose )
-        pSat->verbosity = 1;
-    status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-    if ( status == l_Undef )
-    {
-//        printf( "The problem timed out.\n" );
-        RetValue = -1;
-    }
-    else if ( status == l_True )
-    {
-//        printf( "The problem is SATISFIABLE.\n" );
-        RetValue = 0;
-    }
-    else if ( status == l_False )
-    {
-//        printf( "The problem is UNSATISFIABLE.\n" );
-        RetValue = 1;
-    }
-    else
-        assert( 0 );
+    //    printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
+    //    ABC_PRT( "Time", clock() - clk );
+
+        // simplify the problem
+        clk = clock();
+        status = sat_solver_simplify(pSat);
+    //    printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
+    //    ABC_PRT( "Time", clock() - clk );
+        if ( status == 0 )
+        {
+            Vec_IntFree( vCiIds );
+            sat_solver_delete( pSat );
+    //        printf( "The problem is UNSATISFIABLE after simplification.\n" );
+            return 1;
+        }
 
-//    Abc_Print( 1, "The number of conflicts = %6d.  ", (int)pSat->stats.conflicts );
-//    Abc_PrintTime( 1, "Solving time", clock() - clk );
+        // solve the miter
+        clk = clock();
+        if ( fVerbose )
+            pSat->verbosity = 1;
+        status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+        if ( status == l_Undef )
+        {
+    //        printf( "The problem timed out.\n" );
+            RetValue = -1;
+        }
+        else if ( status == l_True )
+        {
+    //        printf( "The problem is SATISFIABLE.\n" );
+            RetValue = 0;
+        }
+        else if ( status == l_False )
+        {
+    //        printf( "The problem is UNSATISFIABLE.\n" );
+            RetValue = 1;
+        }
+        else
+            assert( 0 );
+
+    //    Abc_Print( 1, "The number of conflicts = %6d.  ", (int)pSat->stats.conflicts );
+    //    Abc_PrintTime( 1, "Solving time", clock() - clk );
  
-    // if the problem is SAT, get the counterexample
-    if ( status == l_True )
-    {
-        pMan->pData = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
+        // if the problem is SAT, get the counterexample
+        if ( status == l_True )
+        {
+            pMan->pData = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
+        }
+        // free the sat_solver
+//        if ( fVerbose )
+            Sat_SolverPrintStats( stdout, pSat );
+    //sat_solver_store_write( pSat, "trace.cnf" );
+    //sat_solver_store_free( pSat );
+        sat_solver_delete( pSat );
+        Vec_IntFree( vCiIds );
+        return RetValue;
     }
-    // free the sat_solver
-    if ( fVerbose )
-        Sat_SolverPrintStats( stdout, pSat );
-//sat_solver_store_write( pSat, "trace.cnf" );
-//sat_solver_store_free( pSat );
-    sat_solver_delete( pSat );
-    Vec_IntFree( vCiIds );
-    return RetValue;
 }
 
 /**Function*************************************************************
@@ -187,7 +300,7 @@ int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose )
 
     // if SAT only, solve without iteration
 clk = clock();
-    RetValue = Fra_FraigSat( pAig, (ABC_INT64_T)2*nBTLimitStart, (ABC_INT64_T)0, 1, 0, 0 );
+    RetValue = Fra_FraigSat( pAig, (ABC_INT64_T)2*nBTLimitStart, (ABC_INT64_T)0, 1, 0, 0, 0 );
     if ( fVerbose )
     {
         printf( "Initial SAT:      Nodes = %6d.  ", Aig_ManNodeNum(pAig) );
@@ -255,7 +368,7 @@ ABC_PRT( "Time", clock() - clk );
     if ( RetValue == -1 )
     {
 clk = clock();
-        RetValue = Fra_FraigSat( pAig, (ABC_INT64_T)nBTLimitLast, (ABC_INT64_T)0, 1, 0, 0 );
+        RetValue = Fra_FraigSat( pAig, (ABC_INT64_T)nBTLimitLast, (ABC_INT64_T)0, 1, 0, 0, 0 );
         if ( fVerbose )
         {
             printf( "Final SAT:            Nodes = %6d.  ", Aig_ManNodeNum(pAig) );
diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c
index 221593a1..00148451 100644
--- a/src/aig/gia/giaAig.c
+++ b/src/aig/gia/giaAig.c
@@ -568,11 +568,11 @@ void Gia_ManSeqCleanupClasses( Gia_Man_t * p, int fConst, int fEquiv, int fVerbo
 ***********************************************************************/
 int Gia_ManSolveSat( Gia_Man_t * p )
 {
-//    extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fVerbose );
+//    extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose );
     Aig_Man_t * pNew;
     int RetValue, clk = clock();
     pNew = Gia_ManToAig( p, 0 );
-    RetValue = Fra_FraigSat( pNew, 10000000, 0, 1, 1, 0 );
+    RetValue = Fra_FraigSat( pNew, 10000000, 0, 1, 1, 0, 0 );
     if ( RetValue == 0 )
     {
         Gia_Obj_t * pObj;
diff --git a/src/aig/int/intContain.c b/src/aig/int/intContain.c
index 4cc8577e..d4af0ae8 100644
--- a/src/aig/int/intContain.c
+++ b/src/aig/int/intContain.c
@@ -57,7 +57,7 @@ int Inter_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld )
         pAigTemp = Fra_FraigEquivence( pMiter, 1000000, 1 );
         RetValue = Fra_FraigMiterStatus( pAigTemp );
         Aig_ManStop( pAigTemp );
-//        RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0 );
+//        RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0, 0 );
     }
     assert( RetValue != -1 );
     Aig_ManStop( pMiter );
@@ -88,7 +88,7 @@ int Inter_ManCheckEquivalence( Aig_Man_t * pNew, Aig_Man_t * pOld )
         pAigTemp = Fra_FraigEquivence( pMiter, 1000000, 1 );
         RetValue = Fra_FraigMiterStatus( pAigTemp );
         Aig_ManStop( pAigTemp );
-//        RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0 );
+//        RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0, 0 );
     }
     assert( RetValue != -1 );
     Aig_ManStop( pMiter );
diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c
index 87209ca3..b53805b4 100644
--- a/src/aig/ivy/ivyFraig.c
+++ b/src/aig/ivy/ivyFraig.c
@@ -2907,14 +2907,14 @@ printf( "***************\n" );
 ***********************************************************************/
 int Ivy_FraigCheckCone( Ivy_FraigMan_t * pGlo, Ivy_Man_t * p, Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2, int nConfLimit )
 {
-    extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fVerbose );
+    extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose );
     Vec_Int_t * vLeaves;
     Aig_Man_t * pMan;
     Aig_Obj_t * pObj;
     int i, RetValue;
     vLeaves  = Vec_IntAlloc( 100 );
     pMan     = Ivy_FraigExtractCone( p, pObj1, pObj2, vLeaves );
-    RetValue = Fra_FraigSat( pMan, nConfLimit, 0, 0, 0, 1 ); 
+    RetValue = Fra_FraigSat( pMan, nConfLimit, 0, 0, 0, 0, 1 ); 
     if ( RetValue == 0 )
     {
         int Counter = 0;
diff --git a/src/aig/saig/saigGlaPba.c b/src/aig/saig/saigGlaPba.c
index 50f6fce8..5834db76 100644
--- a/src/aig/saig/saigGlaPba.c
+++ b/src/aig/saig/saigGlaPba.c
@@ -558,6 +558,7 @@ Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in
     Aig_Gla2Man_t * p;
     Vec_Int_t * vCore, * vResult;
     int nTimeToStop = time(NULL) + TimeLimit;
+    int clk, clk2 = clock();
     assert( Saig_ManPoNum(pAig) == 1 );
 
     Abc_Clock(0,1); 
@@ -570,6 +571,7 @@ Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in
     }
 
     // start the solver
+    clk = clock();
     Abc_Clock(1,1); 
     p = Aig_Gla2ManStart( pAig, nStart, nFramesMax, fVerbose );
     if ( !Aig_Gla2CreateSatSolver( p ) )
@@ -579,13 +581,15 @@ Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in
         return NULL;
     }
     sat_solver_set_random( p->pSat, fSkipRand );
-    p->timePre += (Abc_Clock(1,0)/ABC_CPS)*CLOCKS_PER_SEC;
+//    p->timePre += (Abc_Clock(1,0)/ABC_CPS)*CLOCKS_PER_SEC;
+    p->timePre += clock() - clk;
 
     // set runtime limit
     if ( TimeLimit )
         sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
 
     // compute UNSAT core
+    clk = clock();
     Abc_Clock(1,1); 
     vCore = Saig_AbsSolverUnsatCore( p->pSat, nConfLimit, fVerbose, NULL );
     if ( vCore == NULL )
@@ -593,8 +597,10 @@ Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in
         Aig_Gla2ManStop( p );
         return NULL;
     }
-    p->timeSat += (Abc_Clock(1,0)/ABC_CPS)*CLOCKS_PER_SEC;
-    p->timeTotal = (Abc_Clock(0,0)/ABC_CPS)*CLOCKS_PER_SEC;
+//    p->timeSat += (Abc_Clock(1,0)/ABC_CPS)*CLOCKS_PER_SEC;
+//    p->timeTotal = (Abc_Clock(0,0)/ABC_CPS)*CLOCKS_PER_SEC;
+    p->timeSat += clock() - clk;
+    p->timeTotal += clock() - clk2;
 
     // print stats
     if ( fVerbose )
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 32ed17eb..ac0f26dd 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -17038,7 +17038,7 @@ int Abc_CommandDCec( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fPartition;
     int fMiter;
 
-    extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fVerbose );
+    extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose );
     extern int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int fPartition, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -17143,7 +17143,7 @@ int Abc_CommandDCec( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // perform equivalence checking
     if ( fSat && fMiter )
-        Abc_NtkDSat( pNtk1, nConfLimit, nInsLimit, 0, 0, fVerbose );
+        Abc_NtkDSat( pNtk1, nConfLimit, nInsLimit, 0, 0, 0, fVerbose );
     else
         Abc_NtkDarCec( pNtk1, pNtk2, nConfLimit, fPartition, fVerbose );
 
@@ -18250,20 +18250,22 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     int RetValue;
     int fAlignPol;
     int fAndOuts;
+    int fNewSolver;
     int fVerbose;
     int nConfLimit;
     int nInsLimit;
     int clk;
 
-    extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fVerbose );
+    extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose );
     // set defaults
     fAlignPol  = 0;
     fAndOuts   = 0;
+    fNewSolver = 0;
     fVerbose   = 0;
     nConfLimit = 100000;   
     nInsLimit  = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CIpavh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CIpanvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -18295,6 +18297,9 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'a':
             fAndOuts ^= 1;
             break;
+        case 'n':
+            fNewSolver ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -18329,7 +18334,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     clk = clock();
-    RetValue = Abc_NtkDSat( pNtk, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, fAlignPol, fAndOuts, fVerbose );
+    RetValue = Abc_NtkDSat( pNtk, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, fAlignPol, fAndOuts, fNewSolver, fVerbose );
     // verify that the pattern is correct
     if ( RetValue == 0 && Abc_NtkPoNum(pNtk) == 1 )
     {
@@ -18351,13 +18356,14 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: dsat [-C num] [-I num] [-pavh]\n" );
+    Abc_Print( -2, "usage: dsat [-C num] [-I num] [-panvh]\n" );
     Abc_Print( -2, "\t         solves the combinational miter using SAT solver MiniSat-1.14\n" );
     Abc_Print( -2, "\t         derives CNF from the current network and leave it unchanged\n" );
     Abc_Print( -2, "\t-C num : limit on the number of conflicts [default = %d]\n",    nConfLimit );
     Abc_Print( -2, "\t-I num : limit on the number of inspections [default = %d]\n", nInsLimit );
     Abc_Print( -2, "\t-p     : alighn polarity of SAT variables [default = %s]\n", fAlignPol? "yes": "no" );  
     Abc_Print( -2, "\t-a     : toggle ANDing/ORing of miter outputs [default = %s]\n", fAndOuts? "ANDing": "ORing" );  
+    Abc_Print( -2, "\t-n     : toggle using new solver [default = %s]\n", fNewSolver? "yes": "no" );  
     Abc_Print( -2, "\t-v     : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index dc090791..0bfd515e 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1240,7 +1240,7 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName, int fFastAlgo,
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fVerbose )
+int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose )
 {
     Aig_Man_t * pMan;
     int RetValue;//, clk = clock();
@@ -1248,7 +1248,7 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit
     assert( Abc_NtkLatchNum(pNtk) == 0 );
 //    assert( Abc_NtkPoNum(pNtk) == 1 );
     pMan = Abc_NtkToDar( pNtk, 0, 0 );
-    RetValue = Fra_FraigSat( pMan, nConfLimit, nInsLimit, fAlignPol, fAndOuts, fVerbose ); 
+    RetValue = Fra_FraigSat( pMan, nConfLimit, nInsLimit, fAlignPol, fAndOuts, fNewSolver, fVerbose ); 
     pNtk->pModel = (int *)pMan->pData, pMan->pData = NULL;
     Aig_ManStop( pMan );
     return RetValue;
@@ -1910,7 +1910,7 @@ int Abc_NtkDarBmcInter_int( Aig_Man_t * pMan, Inter_ManParams_t * pPars, Aig_Man
             if ( Aig_ManRegNum(pTemp) == 0 )
             {
                 pTemp->pSeqModel = NULL;
-                RetValue = Fra_FraigSat( pTemp, pPars->nBTLimit, 0, 0, 0, 0 ); 
+                RetValue = Fra_FraigSat( pTemp, pPars->nBTLimit, 0, 0, 0, 0, 0 ); 
                 if ( pTemp->pData )
                     pTemp->pSeqModel = Abc_CexCreate( Aig_ManRegNum(pMan), Saig_ManPiNum(pMan), (int *)pTemp->pData, 0, i, 1 );
 //                pNtk->pModel = pTemp->pData, pTemp->pData = NULL;
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index 52ac5192..28ff0ee6 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -30,7 +30,7 @@ ABC_NAMESPACE_IMPL_START
 
 extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
 extern void   Aig_ManStop( Aig_Man_t * pMan );
-//extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fVerbose );
+//extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose );
 extern Ivy_Obj_t * Dec_GraphToNetworkIvy( Ivy_Man_t * pMan, Dec_Graph_t * pGraph );
 extern void Ivy_CutComputeAll( Ivy_Man_t * p, int nInputs );
 
@@ -532,7 +532,7 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
     // if SAT only, solve without iteration
 //    RetValue = Abc_NtkMiterSat( pNtk, 2*(ABC_INT64_T)pParams->nMiteringLimitStart, (ABC_INT64_T)0, 0, NULL, NULL );
     pMan2 = Abc_NtkToDar( pNtk, 0, 0 );
-    RetValue = Fra_FraigSat( pMan2, (ABC_INT64_T)pParams->nMiteringLimitStart, (ABC_INT64_T)0, 1, 0, 0 ); 
+    RetValue = Fra_FraigSat( pMan2, (ABC_INT64_T)pParams->nMiteringLimitStart, (ABC_INT64_T)0, 1, 0, 0, 0 ); 
     pNtk->pModel = (int *)pMan2->pData, pMan2->pData = NULL;
     Aig_ManStop( pMan2 );
 //    pNtk->pModel = Aig_ManReleaseData( pMan2 );
@@ -582,7 +582,7 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
             Ioa_WriteAiger( pMan2, pFileName, 0, 0 );
             printf( "Intermediate reduced miter is written into file \"%s\".\n", pFileName );
         }
-        RetValue = Fra_FraigSat( pMan2, pParams->nMiteringLimitLast, 0, 0, 0, pParams->fVerbose ); 
+        RetValue = Fra_FraigSat( pMan2, pParams->nMiteringLimitLast, 0, 0, 0, 0, pParams->fVerbose ); 
         pNtk->pModel = (int *)pMan2->pData, pMan2->pData = NULL;
         Aig_ManStop( pMan2 );
     }
diff --git a/src/base/abci/abcQbf.c b/src/base/abci/abcQbf.c
index 90cc0146..e6395ef3 100644
--- a/src/base/abci/abcQbf.c
+++ b/src/base/abci/abcQbf.c
@@ -41,7 +41,7 @@ static void Abc_NtkVectorClearVars( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues, int
 static void Abc_NtkVectorPrintPars( Vec_Int_t * vPiValues, int nPars );
 static void Abc_NtkVectorPrintVars( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues, int nPars );
 
-extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fVerbose );
+extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -101,7 +101,7 @@ void Abc_NtkQbf( Abc_Ntk_t * pNtk, int nPars, int nItersMax, int fVerbose )
         // solve the synthesis instance
 clkS = clock();
 //        RetValue = Abc_NtkMiterSat( pNtkSyn, 0, 0, 0, NULL, NULL );
-        RetValue = Abc_NtkDSat( pNtkSyn, (ABC_INT64_T)0, (ABC_INT64_T)0, 1, 0, 0 );
+        RetValue = Abc_NtkDSat( pNtkSyn, (ABC_INT64_T)0, (ABC_INT64_T)0, 1, 0, 0, 0 );
 clkS = clock() - clkS;
         if ( RetValue == 0 )
             Abc_NtkModelToVector( pNtkSyn, vPiValues );
diff --git a/src/sat/bsat/module.make b/src/sat/bsat/module.make
index 4bc6eca7..4f633df4 100644
--- a/src/sat/bsat/module.make
+++ b/src/sat/bsat/module.make
@@ -4,6 +4,7 @@ SRC +=  src/sat/bsat/satMem.c \
     src/sat/bsat/satInterB.c \
     src/sat/bsat/satInterP.c \
     src/sat/bsat/satSolver.c \
+    src/sat/bsat/satSolver2.c \
     src/sat/bsat/satStore.c \
     src/sat/bsat/satTrace.c \
     src/sat/bsat/satUtil.c
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
new file mode 100644
index 00000000..81e26cb8
--- /dev/null
+++ b/src/sat/bsat/satSolver2.c
@@ -0,0 +1,1482 @@
+/**************************************************************************************************
+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 "satSolver2.h"
+
+ABC_NAMESPACE_IMPL_START
+
+#define SAT_USE_ANALYZE_FINAL
+
+//#define SAT_USE_SYSTEM_MEMORY_MANAGEMENT
+
+//=================================================================================================
+// Debug:
+
+//#define VERBOSEDEBUG
+
+// For derivation output (verbosity level 2)
+#define L_IND    "%-*d"
+#define L_ind    sat_solver2_dlevel(s)*3+3,sat_solver2_dlevel(s)
+#define L_LIT    "%sx%d"
+#define L_lit(p) lit_sign(p)?"~":"", (lit_var(p))
+static void printlits(lit* begin, lit* end)
+{
+    int i;
+    for (i = 0; i < end - begin; i++)
+        printf(L_LIT" ",L_lit(begin[i]));
+}
+
+//=================================================================================================
+// Random numbers:
+
+
+// Returns a random float 0 <= x < 1. Seed must never be 0.
+static inline double drand(double* seed) {
+    int q;
+    *seed *= 1389796;
+    q = (int)(*seed / 2147483647);
+    *seed -= (double)q * 2147483647;
+    return *seed / 2147483647; }
+
+
+// Returns a random integer 0 <= x < size. Seed must never be 0.
+static inline int irand(double* seed, int size) {
+    return (int)(drand(seed) * size); }
+
+
+//=================================================================================================
+// Predeclarations:
+
+static void sat_solver2_sort(void** array, int size, int(*comp)(const void *, const void *));
+
+//=================================================================================================
+// Clause datatype + minor functions:
+
+struct clause_t
+{
+    int size_learnt;
+    unsigned act;
+    lit lits[0];
+};
+
+static inline int      clause_size    (clause* c)              { return c->size_learnt >> 1;           }
+static inline int      clause_learnt  (clause* c)              { return c->size_learnt & 1;            }
+static inline lit*     clause_begin   (clause* c)              { return c->lits;                       }
+
+static inline clause * get_clause     (sat_solver2* s, int c)  { return (clause *)(s->pMemArray + c);  }
+
+//=================================================================================================
+// Simple helpers:
+
+static inline int     sat_solver2_dlevel(sat_solver2* s)            { return veci_size(&s->trail_lim); }
+static inline vecp*   sat_solver2_read_wlist(sat_solver2* s, lit l) { return &s->wlists[l]; }
+static inline void    vecp_remove(vecp* v, void* e)
+{
+    void** ws = vecp_begin(v);
+    int    j  = 0;
+    for (; ws[j] != e  ; j++);
+    assert(j < vecp_size(v));
+    for (; j < vecp_size(v)-1; j++) ws[j] = ws[j+1];
+    vecp_resize(v,vecp_size(v)-1);
+}
+
+//=================================================================================================
+// Variable order functions:
+
+static inline void order_update(sat_solver2* 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_solver2* s, int v) 
+{
+}
+
+static inline void order_unassigned(sat_solver2* 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);
+    }
+}
+
+static inline int  order_select(sat_solver2* s, float random_var_freq) // selectvar
+{
+    int*      heap     = veci_begin(&s->order);
+    int*      orderpos = s->orderpos;
+    lbool*    values   = s->assigns;
+
+    // Random decision:
+    if (drand(&s->random_seed) < random_var_freq){
+        int next = irand(&s->random_seed,s->size);
+        assert(next >= 0 && next < s->size);
+        if (values[next] == l_Undef)
+            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){
+            unsigned act   = s->activity[x];
+            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 (act >= s->activity[heap[child]])
+                    break;
+
+                heap[i]           = heap[child];
+                orderpos[heap[i]] = i;
+                i                 = child;
+                child             = 2 * child + 1;
+            }
+            heap[i]           = x;
+            orderpos[heap[i]] = i;
+        }
+
+//printf( "-%d ", next );
+        if (values[next] == l_Undef)
+            return next;
+    }
+
+    return var_Undef;
+}
+
+//=================================================================================================
+// Activity functions:
+
+static inline void act_var_rescale(sat_solver2* s) {
+    unsigned* activity = s->activity;
+    int i, clk = clock();
+    static int Total = 0;
+    for (i = 0; i < s->size; i++)
+        activity[i] >>= 20;
+    s->var_inc >>= 20;
+//    assert( s->var_inc > 15 );
+
+    s->cla_inc = Abc_MaxInt( s->cla_inc, (1<<4) );
+//    printf( "Rescaling... Var inc = %5d  Conf = %10d ", s->var_inc,  s->stats.conflicts );
+    Total += clock() - clk;
+//    Abc_PrintTime( 1, "Time", Total );
+}
+
+static inline void act_var_bump(sat_solver2* s, int v) {
+    static int Counter = 0;
+    s->activity[v] += s->var_inc;
+    if (s->activity[v] & 0x80000000)
+        act_var_rescale(s);
+    if (s->orderpos[v] != -1)
+        order_update(s,v);
+}
+
+//static inline void act_var_decay(sat_solver2* s) { s->var_inc *= s->var_decay; }
+static inline void act_var_decay(sat_solver2* s) { s->var_inc += (s->var_inc >> 4); }
+
+static inline void act_clause_rescale(sat_solver2* s) {
+    clause** cs = (clause**)vecp_begin(&s->learnts);
+    int i, clk = clock();
+    static int Total = 0;
+
+    for (i = 0; i < vecp_size(&s->learnts); i++)
+        cs[i]->act >>= 14;
+    s->cla_inc >>= 14;
+
+//    assert( s->cla_inc > (1<<10)-1 );
+    s->cla_inc = Abc_MaxInt( s->cla_inc, (1<<10) );
+
+    printf( "Rescaling... Cla inc = %5d  Conf = %10d   ", s->cla_inc,  s->stats.conflicts );
+    Total += clock() - clk;
+    Abc_PrintTime( 1, "Time", Total );
+}
+
+
+static inline void act_clause_bump(sat_solver2* s, clause *c) {
+    c->act += s->cla_inc;
+    if (c->act & 0x80000000) 
+        act_clause_rescale(s);
+}
+
+//static inline void act_clause_decay(sat_solver2* s) { s->cla_inc *= s->cla_decay; }
+static inline void act_clause_decay(sat_solver2* s) { s->cla_inc += (s->cla_inc >> 10); }
+
+//=================================================================================================
+// Clause functions:
+
+/* pre: size > 1 && no variable occurs twice
+ */
+static clause* clause_new(sat_solver2* s, lit* begin, lit* end, int learnt)
+{
+    int size;
+    clause* c;
+    int i;
+
+    assert(end - begin > 1);
+    assert(learnt >= 0 && learnt < 2);
+    size           = end - begin;
+
+    //    c              = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
+#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
+    c = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit) * size);
+#else
+//    c = (clause*)Sat_MmStepEntryFetch( s->pMem, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float) );
+    if ( s->nMemSize + (int)sizeof(clause)/4 + size > s->nMemAlloc )
+    {
+        int nMemAlloc = s->nMemAlloc ? s->nMemAlloc * 2 : (1 << 24);
+        s->pMemArray  = ABC_REALLOC( int, s->pMemArray, nMemAlloc );
+        memset( s->pMemArray + s->nMemAlloc, 0, sizeof(int) * (nMemAlloc - s->nMemAlloc) );
+        printf( "Reallocing from %d to %d...\n", s->nMemAlloc, nMemAlloc );
+        s->nMemAlloc = nMemAlloc;
+        s->nMemSize = Abc_MaxInt( s->nMemSize, 16 ); 
+    }
+    c = (clause*)(s->pMemArray + s->nMemSize);
+    s->nMemSize += sizeof(clause)/4 + size;
+    if ( s->nMemSize > s->nMemAlloc )
+        printf( "Out of memory!!!\n" );
+    assert( s->nMemSize <= s->nMemAlloc );
+#endif
+
+    c->size_learnt = (size << 1) | learnt;
+    assert(((ABC_PTRUINT_T)c & 1) == 0);
+
+    c->act = 0;
+    for (i = 0; i < size; i++)
+        c->lits[i] = begin[i];
+
+    assert(begin[0] >= 0);
+    assert(begin[0] < s->size*2);
+    assert(begin[1] >= 0);
+    assert(begin[1] < s->size*2);
+
+    assert(lit_neg(begin[0]) < s->size*2);
+    assert(lit_neg(begin[1]) < s->size*2);
+
+    vecp_push(sat_solver2_read_wlist(s,lit_neg(begin[0])),(void*)c);
+    vecp_push(sat_solver2_read_wlist(s,lit_neg(begin[1])),(void*)c);
+    return c;
+}
+
+
+static void clause_remove(sat_solver2* s, clause* c)
+{
+    lit* lits = clause_begin(c);
+    assert(lit_neg(lits[0]) < s->size*2);
+    assert(lit_neg(lits[1]) < s->size*2);
+
+    vecp_remove(sat_solver2_read_wlist(s,lit_neg(lits[0])),(void*)c);
+    vecp_remove(sat_solver2_read_wlist(s,lit_neg(lits[1])),(void*)c);
+
+    if (clause_learnt(c)){
+        s->stats.learnts--;
+        s->stats.learnts_literals -= clause_size(c);
+    }else{
+        s->stats.clauses--;
+        s->stats.clauses_literals -= clause_size(c);
+    }
+
+#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
+    ABC_FREE(c);
+#else
+//    Sat_MmStepEntryRecycle( s->pMem, (char *)c, sizeof(clause) + sizeof(lit) * clause_size(c) + clause_learnt(c) * sizeof(float) );
+#endif
+}
+
+
+static lbool clause_simplify(sat_solver2* s, clause* c)
+{
+    lit*   lits   = clause_begin(c);
+    lbool* values = s->assigns;
+    int i;
+
+    assert(sat_solver2_dlevel(s) == 0);
+
+    for (i = 0; i < clause_size(c); i++){
+        lbool sig = !lit_sign(lits[i]); sig += sig - 1;
+        if (values[lit_var(lits[i])] == sig)
+            return l_True;
+    }
+    return l_False;
+}
+
+//=================================================================================================
+// Minor (solver) functions:
+
+void sat_solver2_setnvars(sat_solver2* s,int n)
+{
+    int var;
+
+    if (s->cap < n){
+
+        while (s->cap < n) s->cap = s->cap*2+1;
+
+        s->wlists    = ABC_REALLOC(vecp,   s->wlists,   s->cap*2);
+//        s->activity  = ABC_REALLOC(double, s->activity, s->cap);
+        s->activity  = ABC_REALLOC(unsigned, s->activity, s->cap);
+//        s->factors   = ABC_REALLOC(double, s->factors,  s->cap);
+        s->assigns   = ABC_REALLOC(lbool,  s->assigns,  s->cap);
+        s->orderpos  = ABC_REALLOC(int,    s->orderpos, s->cap);
+        s->reasons   = ABC_REALLOC(clause*,s->reasons,  s->cap);
+        s->levels    = ABC_REALLOC(int,    s->levels,   s->cap);
+        s->tags      = ABC_REALLOC(lbool,  s->tags,     s->cap);
+        s->trail     = ABC_REALLOC(lit,    s->trail,    s->cap);
+        s->polarity  = ABC_REALLOC(char,   s->polarity, s->cap);
+    }
+
+    for (var = s->size; var < n; var++){
+        vecp_new(&s->wlists[2*var]);
+        vecp_new(&s->wlists[2*var+1]);
+        s->activity [var] = (1<<10);
+//        s->factors  [var] = 0;
+        s->assigns  [var] = l_Undef;
+        s->orderpos [var] = veci_size(&s->order);
+        s->reasons  [var] = (clause*)0;
+        s->levels   [var] = 0;
+        s->tags     [var] = l_Undef;
+        s->polarity [var] = 0;
+        
+        /* does not hold because variables enqueued at top level will not be reinserted in the heap
+           assert(veci_size(&s->order) == var); 
+         */
+        veci_push(&s->order,var);
+        order_update(s, var);
+    }
+
+    s->size = n > s->size ? n : s->size;
+}
+
+
+static inline int enqueue(sat_solver2* s, lit l, clause* from)
+{
+    lbool* values = s->assigns;
+    int    v      = lit_var(l);
+    lbool  val    = values[v];
+#ifdef VERBOSEDEBUG
+    printf(L_IND"enqueue("L_LIT")\n", L_ind, L_lit(l));
+#endif
+
+    lbool sig = !lit_sign(l); sig += sig - 1;
+    if (val != l_Undef){
+        return val == sig;
+    }else{
+        // New fact -- store it.
+#ifdef VERBOSEDEBUG
+        printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(l));
+#endif
+        int*     levels  = s->levels;
+        clause** reasons = s->reasons;
+
+        values [v] = sig;
+        levels [v] = sat_solver2_dlevel(s);
+        reasons[v] = from;
+        s->trail[s->qtail++] = l;
+
+        order_assigned(s, v);
+        return true;
+    }
+}
+
+
+static inline int assume(sat_solver2* s, lit l){
+    assert(s->qtail == s->qhead);
+    assert(s->assigns[lit_var(l)] == l_Undef);
+#ifdef VERBOSEDEBUG
+    printf(L_IND"assume("L_LIT")\n", L_ind, L_lit(l));
+#endif
+    veci_push(&s->trail_lim,s->qtail);
+    return enqueue(s,l,(clause*)0);
+}
+
+
+static void sat_solver2_canceluntil(sat_solver2* s, int level) {
+    lit*     trail;   
+    lbool*   values;  
+    clause** reasons; 
+    int      bound;
+    int      lastLev;
+    int      c;
+    
+    if (sat_solver2_dlevel(s) <= level)
+        return;
+
+    trail   = s->trail;
+    values  = s->assigns;
+    reasons = s->reasons;
+    bound   = (veci_begin(&s->trail_lim))[level];
+    lastLev = (veci_begin(&s->trail_lim))[veci_size(&s->trail_lim)-1];
+
+    ////////////////////////////////////////
+    // added to cancel all assignments
+//    if ( level == -1 )
+//        bound = 0;
+    ////////////////////////////////////////
+
+    for (c = s->qtail-1; c >= bound; c--) {
+        int     x  = lit_var(trail[c]);
+        values [x] = l_Undef;
+        reasons[x] = (clause*)0;
+        if ( c < lastLev )
+            s->polarity[x] = !lit_sign(trail[c]);
+    }
+
+    for (c = s->qhead-1; c >= bound; c--)
+        order_unassigned(s,lit_var(trail[c]));
+
+    s->qhead = s->qtail = bound;
+    veci_resize(&s->trail_lim,level);
+}
+
+static void sat_solver2_record(sat_solver2* s, veci* cls)
+{
+    lit*    begin = veci_begin(cls);
+    lit*    end   = begin + veci_size(cls);
+    clause* c     = (veci_size(cls) > 1) ? clause_new(s,begin,end,1) : (clause*)0;
+    enqueue(s,*begin,c);
+
+    assert(veci_size(cls) > 0);
+
+    if (c != 0) {
+        vecp_push(&s->learnts,c);
+        act_clause_bump(s,c);
+        s->stats.learnts++;
+        s->stats.learnts_literals += veci_size(cls);
+    }
+}
+
+
+static double sat_solver2_progress(sat_solver2* s)
+{
+    lbool*  values = s->assigns;
+    int*    levels = s->levels;
+    int     i;
+
+    double  progress = 0;
+    double  F        = 1.0 / s->size;
+    for (i = 0; i < s->size; i++)
+        if (values[i] != l_Undef)
+            progress += pow(F, levels[i]);
+    return progress / s->size;
+}
+
+//=================================================================================================
+// Major methods:
+
+static int sat_solver2_lit_removable(sat_solver2* s, lit l, int minl)
+{
+    lbool*   tags    = s->tags;
+    clause** reasons = s->reasons;
+    int*     levels  = s->levels;
+    int      top     = veci_size(&s->tagged);
+
+    assert(lit_var(l) >= 0 && lit_var(l) < s->size);
+    assert(reasons[lit_var(l)] != 0);
+    veci_resize(&s->stack,0);
+    veci_push(&s->stack,lit_var(l));
+
+    while (veci_size(&s->stack) > 0){
+        clause* c;
+        int v = veci_begin(&s->stack)[veci_size(&s->stack)-1];
+        assert(v >= 0 && v < s->size);
+        veci_resize(&s->stack,veci_size(&s->stack)-1);
+        assert(reasons[v] != 0);
+        c    = reasons[v];
+
+        {
+        lit*    lits = clause_begin(c);
+        int     i, j;
+
+        for (i = 1; i < clause_size(c); i++){
+            int v = lit_var(lits[i]);
+            if (tags[v] == l_Undef && levels[v] != 0){
+                if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){
+
+                    veci_push(&s->stack,lit_var(lits[i]));
+                    tags[v] = l_True;
+                    veci_push(&s->tagged,v);
+                }else{
+                    int* tagged = veci_begin(&s->tagged);
+                    for (j = top; j < veci_size(&s->tagged); j++)
+                        tags[tagged[j]] = l_Undef;
+                    veci_resize(&s->tagged,top);
+                    return false;
+                }
+            }
+        }
+        }
+    }
+
+    return true;
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  analyzeFinal : (p : Lit)  ->  [void]
+|  
+|  Description:
+|    Specialized analysis procedure to express the final conflict in terms of assumptions.
+|    Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and
+|    stores the result in 'out_conflict'.
+|________________________________________________________________________________________________@*/
+/*
+void Solver::analyzeFinal(Clause* confl, bool skip_first)
+{
+    // -- NOTE! This code is relatively untested. Please report bugs!
+    conflict.clear();
+    if (root_level == 0) return;
+
+    vec<char>& seen  = analyze_seen;
+    for (int i = skip_first ? 1 : 0; i < confl->size(); i++){
+        Var x = var((*confl)[i]);
+        if (level[x] > 0)
+            seen[x] = 1;
+    }
+
+    int start = (root_level >= trail_lim.size()) ? trail.size()-1 : trail_lim[root_level];
+    for (int i = start; i >= trail_lim[0]; i--){
+        Var     x = var(trail[i]);
+        if (seen[x]){
+            GClause r = reason[x];
+            if (r == GClause_NULL){
+                assert(level[x] > 0);
+                conflict.push(~trail[i]);
+            }else{
+                if (r.isLit()){
+                    Lit p = r.lit();
+                    if (level[var(p)] > 0)
+                        seen[var(p)] = 1;
+                }else{
+                    Clause& c = *r.clause();
+                    for (int j = 1; j < c.size(); j++)
+                        if (level[var(c[j])] > 0)
+                            seen[var(c[j])] = 1;
+                }
+            }
+            seen[x] = 0;
+        }
+    }
+}
+*/
+
+#ifdef SAT_USE_ANALYZE_FINAL
+
+static void sat_solver2_analyze_final(sat_solver2* s, clause* conf, int skip_first)
+{
+    int i, j, start;
+    veci_resize(&s->conf_final,0);
+    if ( s->root_level == 0 )
+        return;
+    assert( veci_size(&s->tagged) == 0 );
+//    assert( s->tags[lit_var(p)] == l_Undef );
+//    s->tags[lit_var(p)] = l_True;
+    for (i = skip_first ? 1 : 0; i < clause_size(conf); i++)
+    {
+        int x = lit_var(clause_begin(conf)[i]);
+        if (s->levels[x] > 0)
+        {
+            s->tags[x] = l_True;
+            veci_push(&s->tagged,x);
+        }
+    }
+
+    start = (s->root_level >= veci_size(&s->trail_lim))? s->qtail-1 : (veci_begin(&s->trail_lim))[s->root_level];
+    for (i = start; i >= (veci_begin(&s->trail_lim))[0]; i--){
+        int x = lit_var(s->trail[i]);
+        if (s->tags[x] == l_True){
+            if (s->reasons[x] == NULL){
+                assert(s->levels[x] > 0);
+                veci_push(&s->conf_final,lit_neg(s->trail[i]));
+            }else{
+                clause* c = s->reasons[x];
+                {
+                    int* lits = clause_begin(c);
+                    for (j = 1; j < clause_size(c); j++)
+                        if (s->levels[lit_var(lits[j])] > 0)
+                        {
+                            s->tags[lit_var(lits[j])] = l_True;
+                            veci_push(&s->tagged,lit_var(lits[j]));
+                        }
+                }
+            }
+        }
+    }
+    for (i = 0; i < veci_size(&s->tagged); i++)
+        s->tags[veci_begin(&s->tagged)[i]] = l_Undef;
+    veci_resize(&s->tagged,0);
+}
+
+#endif
+
+
+static void sat_solver2_analyze(sat_solver2* s, clause* c, veci* learnt)
+{
+    lit*     trail   = s->trail;
+    lbool*   tags    = s->tags;
+    clause** reasons = s->reasons;
+    int*     levels  = s->levels;
+    int      cnt     = 0;
+    lit      p       = lit_Undef;
+    int      ind     = s->qtail-1;
+    lit*     lits;
+    int      i, j, minl;
+    int*     tagged;
+
+    veci_push(learnt,lit_Undef);
+
+    do{
+        assert(c != 0);
+        if (clause_learnt(c))
+            act_clause_bump(s,c);
+
+        lits = clause_begin(c);
+        //printlits(lits,lits+clause_size(c)); printf("\n");
+        for (j = (p == lit_Undef ? 0 : 1); j < clause_size(c); j++){
+            lit q = lits[j];
+            assert(lit_var(q) >= 0 && lit_var(q) < s->size);
+            if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){
+                tags[lit_var(q)] = l_True;
+                veci_push(&s->tagged,lit_var(q));
+                act_var_bump(s,lit_var(q));
+                if (levels[lit_var(q)] == sat_solver2_dlevel(s))
+                    cnt++;
+                else
+                    veci_push(learnt,q);
+            }
+        }
+
+        while (tags[lit_var(trail[ind--])] == l_Undef);
+
+        p = trail[ind+1];
+        c = reasons[lit_var(p)];
+        cnt--;
+
+    }while (cnt > 0);
+
+    *veci_begin(learnt) = lit_neg(p);
+
+    lits = veci_begin(learnt);
+    minl = 0;
+    for (i = 1; i < veci_size(learnt); i++){
+        int lev = levels[lit_var(lits[i])];
+        minl    |= 1 << (lev & 31);
+    }
+
+    // simplify (full)
+    for (i = j = 1; i < veci_size(learnt); i++){
+        if (reasons[lit_var(lits[i])] == 0 || !sat_solver2_lit_removable(s,lits[i],minl))
+            lits[j++] = lits[i];
+    }
+
+    // update size of learnt + statistics
+    s->stats.max_literals += veci_size(learnt);
+    veci_resize(learnt,j);
+    s->stats.tot_literals += j;
+
+    // clear tags
+    tagged = veci_begin(&s->tagged);
+    for (i = 0; i < veci_size(&s->tagged); i++)
+        tags[tagged[i]] = l_Undef;
+    veci_resize(&s->tagged,0);
+
+#ifdef DEBUG
+    for (i = 0; i < s->size; i++)
+        assert(tags[i] == l_Undef);
+#endif
+
+#ifdef VERBOSEDEBUG
+    printf(L_IND"Learnt {", L_ind);
+    for (i = 0; i < veci_size(learnt); i++) printf(" "L_LIT, L_lit(lits[i]));
+#endif
+    if (veci_size(learnt) > 1){
+        int max_i = 1;
+        int max   = levels[lit_var(lits[1])];
+        lit tmp;
+
+        for (i = 2; i < veci_size(learnt); i++)
+            if (levels[lit_var(lits[i])] > max){
+                max   = levels[lit_var(lits[i])];
+                max_i = i;
+            }
+
+        tmp         = lits[1];
+        lits[1]     = lits[max_i];
+        lits[max_i] = tmp;
+    }
+#ifdef VERBOSEDEBUG
+    {
+        int lev = veci_size(learnt) > 1 ? levels[lit_var(lits[1])] : 0;
+        printf(" } at level %d\n", lev);
+    }
+#endif
+}
+
+
+clause* sat_solver2_propagate(sat_solver2* s)
+{
+    lbool*  values = s->assigns;
+    clause* confl  = (clause*)0;
+    lit*    lits;
+
+    //printf("sat_solver2_propagate\n");
+    while (confl == 0 && s->qtail - s->qhead > 0){
+        lit  p  = s->trail[s->qhead++];
+        vecp* ws = sat_solver2_read_wlist(s,p);
+        clause **begin = (clause**)vecp_begin(ws);
+        clause **end   = begin + vecp_size(ws);
+        clause **i, **j;
+
+        s->stats.propagations++;
+        s->simpdb_props--;
+
+        //printf("checking lit %d: "L_LIT"\n", veci_size(ws), L_lit(p));
+        for (i = j = begin; i < end; ){
+        {
+            lit false_lit;
+            lbool sig;
+
+            lits = clause_begin(*i);
+
+            // Make sure the false literal is data[1]:
+            false_lit = lit_neg(p);
+            if (lits[0] == false_lit){
+                lits[0] = lits[1];
+                lits[1] = false_lit;
+            }
+            assert(lits[1] == false_lit);
+            //printf("checking clause: "); printlits(lits, lits+clause_size(*i)); printf("\n");
+
+            // If 0th watch is true, then clause is already satisfied.
+            sig = !lit_sign(lits[0]); sig += sig - 1;
+            if (values[lit_var(lits[0])] == sig){
+                *j++ = *i;
+            }else{
+                // Look for new watch:
+                lit* stop = lits + clause_size(*i);
+                lit* k;
+                for (k = lits + 2; k < stop; k++){
+                    lbool sig = lit_sign(*k); sig += sig - 1;
+                    if (values[lit_var(*k)] != sig){
+                        lits[1] = *k;
+                        *k = false_lit;
+                        vecp_push(sat_solver2_read_wlist(s,lit_neg(lits[1])),*i);
+                        goto next; }
+                }
+
+                *j++ = *i;
+                // Clause is unit under assignment:
+                if (!enqueue(s,lits[0], *i)){
+                    confl = *i++;
+                    // Copy the remaining watches:
+//                        s->stats.inspects2 += end - i;
+                    while (i < end)
+                        *j++ = *i++;
+                }
+            }
+        }
+        next:
+            i++;
+        }
+
+        s->stats.inspects += j - (clause**)vecp_begin(ws);
+        vecp_resize(ws,j - (clause**)vecp_begin(ws));
+    }
+
+    return confl;
+}
+
+static int clause_cmp (const void* x, const void* y) {
+//    return clause_size((clause*)x) > 2 && (clause_size((clause*)y) == 2 || clause_activity((clause*)x) < clause_activity((clause*)y)) ? -1 : 1; }
+    return clause_size((clause*)x) > 2 && (clause_size((clause*)y) == 2 || ((clause*)x)->act < ((clause*)y)->act) ? -1 : 1; }
+
+void sat_solver2_reducedb(sat_solver2* s)
+{
+    int Counter = 0;
+    int      i, j;
+    unsigned extra_lim;
+    double   extra_limD = (double)s->cla_inc / vecp_size(&s->learnts); // Remove any clause below this activity
+    clause** learnts = (clause**)vecp_begin(&s->learnts);
+    clause** reasons = s->reasons;
+
+    if ( extra_limD < 1.0 )
+        extra_lim = 1;
+    else
+        extra_lim = (int)extra_limD;
+
+    sat_solver2_sort(vecp_begin(&s->learnts), vecp_size(&s->learnts), &clause_cmp);
+
+    for (i = j = 0; i < vecp_size(&s->learnts) / 2; i++){
+//        printf( "%d ", learnts[i]->act );
+//    for (i = j = 0; i < vecp_size(&s->learnts) / 4; i++){
+        if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i])
+            clause_remove(s,learnts[i]), Counter++;
+        else
+            learnts[j++] = learnts[i];
+    }
+    for (; i < vecp_size(&s->learnts); i++){
+//        if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i] && clause_activity(learnts[i]) < extra_lim)
+        if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i] && learnts[i]->act < extra_lim)
+            clause_remove(s,learnts[i]), Counter++;
+        else
+            learnts[j++] = learnts[i];
+    }
+printf( "Reduction removed %10d clauses (out of %10d)... Value = %d\n", Counter, vecp_size(&s->learnts), extra_lim );
+
+    //printf("reducedb deleted %d\n", vecp_size(&s->learnts) - j);
+
+
+    vecp_resize(&s->learnts,j);
+}
+
+static lbool sat_solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts, ABC_INT64_T * nof_learnts)
+{
+    int*    levels          = s->levels;
+    double  var_decay       = 0.95;
+    double  clause_decay    = 0.999;
+    double  random_var_freq = s->fNotUseRandom ? 0.0 : 0.02;
+//    s->var_decay = (float)(1 / var_decay   );
+//    s->cla_decay = (float)(1 / clause_decay);
+
+    ABC_INT64_T  conflictC       = 0;
+    veci    learnt_clause;
+
+    assert(s->root_level == sat_solver2_dlevel(s));
+
+    s->stats.starts++;
+    veci_resize(&s->model,0);
+    veci_new(&learnt_clause);
+
+    for (;;){
+        clause* confl = sat_solver2_propagate(s);
+        if (confl != 0){
+            // CONFLICT
+            int blevel;
+
+#ifdef VERBOSEDEBUG
+            printf(L_IND"**CONFLICT**\n", L_ind);
+#endif
+            s->stats.conflicts++; conflictC++;
+            if (sat_solver2_dlevel(s) == s->root_level){
+#ifdef SAT_USE_ANALYZE_FINAL
+                sat_solver2_analyze_final(s, confl, 0);
+#endif
+                veci_delete(&learnt_clause);
+                return l_False;
+            }
+
+            veci_resize(&learnt_clause,0);
+            sat_solver2_analyze(s, confl, &learnt_clause);
+            blevel = veci_size(&learnt_clause) > 1 ? levels[lit_var(veci_begin(&learnt_clause)[1])] : s->root_level;
+            blevel = s->root_level > blevel ? s->root_level : blevel;
+            sat_solver2_canceluntil(s,blevel);
+            sat_solver2_record(s,&learnt_clause);
+#ifdef SAT_USE_ANALYZE_FINAL
+//            if (learnt_clause.size() == 1) level[var(learnt_clause[0])] = 0;    // (this is ugly (but needed for 'analyzeFinal()') -- in future versions, we will backtrack past the 'root_level' and redo the assumptions)
+            if ( learnt_clause.size == 1 ) s->levels[lit_var(learnt_clause.ptr[0])] = 0;
+#endif
+            act_var_decay(s);
+            act_clause_decay(s);
+
+        }else{
+            // NO CONFLICT
+            int next;
+
+            if (nof_conflicts >= 0 && conflictC >= nof_conflicts){
+                // Reached bound on number of conflicts:
+                s->progress_estimate = sat_solver2_progress(s);
+                sat_solver2_canceluntil(s,s->root_level);
+                veci_delete(&learnt_clause);
+                return l_Undef; }
+
+            if ( (s->nConfLimit && s->stats.conflicts > s->nConfLimit) ||
+//                 (s->nInsLimit  && s->stats.inspects  > s->nInsLimit) )
+                 (s->nInsLimit  && s->stats.propagations > s->nInsLimit) )
+            {
+                // Reached bound on number of conflicts:
+                s->progress_estimate = sat_solver2_progress(s);
+                sat_solver2_canceluntil(s,s->root_level);
+                veci_delete(&learnt_clause);
+                return l_Undef; 
+            }
+
+//            if (sat_solver2_dlevel(s) == 0 && !s->fSkipSimplify)
+                // Simplify the set of problem clauses:
+//                sat_solver2_simplify(s);
+
+            if (*nof_learnts >= 0 && vecp_size(&s->learnts) - s->qtail >= *nof_learnts)
+            {
+                // Reduce the set of learnt clauses:
+                sat_solver2_reducedb(s);
+                *nof_learnts = *nof_learnts * 12 / 10; //*= 1.1;
+            }
+
+            // New variable decision:
+            s->stats.decisions++;
+            next = order_select(s,(float)random_var_freq);
+
+            if (next == var_Undef){
+                // Model found:
+                lbool* values = s->assigns;
+                int i;
+                veci_resize(&s->model, 0);
+                for (i = 0; i < s->size; i++) 
+                    veci_push(&s->model,(int)values[i]);
+                sat_solver2_canceluntil(s,s->root_level);
+                veci_delete(&learnt_clause);
+
+                /*
+                veci apa; veci_new(&apa);
+                for (i = 0; i < s->size; i++) 
+                    veci_push(&apa,(int)(s->model.ptr[i] == l_True ? toLit(i) : lit_neg(toLit(i))));
+                printf("model: "); printlits((lit*)apa.ptr, (lit*)apa.ptr + veci_size(&apa)); printf("\n");
+                veci_delete(&apa);
+                */
+
+                return l_True;
+            }
+
+            if ( s->polarity[next] ) // positive polarity
+                assume(s,toLit(next));
+            else
+                assume(s,lit_neg(toLit(next)));
+        }
+    }
+
+    return l_Undef; // cannot happen
+}
+
+//=================================================================================================
+// External solver functions:
+
+sat_solver2* sat_solver2_new(void)
+{
+    sat_solver2* s = (sat_solver2*)ABC_ALLOC( char, sizeof(sat_solver2));
+    memset( s, 0, sizeof(sat_solver2) );
+
+    // initialize vectors
+    vecp_new(&s->clauses);
+    vecp_new(&s->learnts);
+    veci_new(&s->order);
+    veci_new(&s->trail_lim);
+    veci_new(&s->tagged);
+    veci_new(&s->stack);
+    veci_new(&s->model);
+//    veci_new(&s->act_vars);
+    veci_new(&s->temp_clause);
+    veci_new(&s->conf_final);
+
+    // initialize arrays
+    s->wlists    = 0;
+    s->activity  = 0;
+//    s->factors   = 0;
+    s->assigns   = 0;
+    s->orderpos  = 0;
+    s->reasons   = 0;
+    s->levels    = 0;
+    s->tags      = 0;
+    s->trail     = 0;
+
+
+    // initialize other vars
+    s->size                   = 0;
+    s->cap                    = 0;
+    s->qhead                  = 0;
+    s->qtail                  = 0;
+    s->cla_inc                = (1 << 11);
+    s->var_inc                = (1 << 5);
+//    s->cla_decay              = 1;
+//    s->var_decay              = 1;
+    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.max_literals     = 0;
+    s->stats.tot_literals     = 0;
+
+    return s;
+}
+
+
+void sat_solver2_delete(sat_solver2* s)
+{
+
+#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
+    int i;
+    for (i = 0; i < vecp_size(&s->clauses); i++)
+        ABC_FREE(vecp_begin(&s->clauses)[i]);
+    for (i = 0; i < vecp_size(&s->learnts); i++)
+        ABC_FREE(vecp_begin(&s->learnts)[i]);
+#endif
+    ABC_FREE(s->pMemArray);
+
+    // delete vectors
+    vecp_delete(&s->clauses);
+    vecp_delete(&s->learnts);
+    veci_delete(&s->order);
+    veci_delete(&s->trail_lim);
+    veci_delete(&s->tagged);
+    veci_delete(&s->stack);
+    veci_delete(&s->model);
+//    veci_delete(&s->act_vars);
+    veci_delete(&s->temp_clause);
+    veci_delete(&s->conf_final);
+    ABC_FREE(s->binary);
+
+    // delete arrays
+    if (s->wlists != 0){
+        int i;
+        for (i = 0; i < s->size*2; i++)
+            vecp_delete(&s->wlists[i]);
+
+        // if one is different from null, all are
+        ABC_FREE(s->wlists   );
+        ABC_FREE(s->activity );
+//        ABC_FREE(s->factors  );
+        ABC_FREE(s->assigns  );
+        ABC_FREE(s->orderpos );
+        ABC_FREE(s->reasons  );
+        ABC_FREE(s->levels   );
+        ABC_FREE(s->trail    );
+        ABC_FREE(s->tags     );
+        ABC_FREE(s->polarity );
+    }
+
+//    sat_solver2_store_free(s);
+    ABC_FREE(s);
+}
+
+
+int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end)
+{
+    clause * c;
+    lit *i,*j;
+    int maxvar;
+    lbool* values;
+    lit last;
+
+    veci_resize( &s->temp_clause, 0 );
+    for ( i = begin; i < end; i++ )
+        veci_push( &s->temp_clause, *i );
+    begin = veci_begin( &s->temp_clause );
+    end = begin + veci_size( &s->temp_clause );
+
+    if (begin == end) 
+        return false;
+
+    //printlits(begin,end); printf("\n");
+    // insertion sort
+    maxvar = lit_var(*begin);
+    for (i = begin + 1; i < end; i++){
+        lit l = *i;
+        maxvar = lit_var(l) > maxvar ? lit_var(l) : maxvar;
+        for (j = i; j > begin && *(j-1) > l; j--)
+            *j = *(j-1);
+        *j = l;
+    }
+    sat_solver2_setnvars(s,maxvar+1);
+//    sat_solver2_setnvars(s, lit_var(*(end-1))+1 );
+
+    //printlits(begin,end); printf("\n");
+    values = s->assigns;
+
+    // delete duplicates
+    last = lit_Undef;
+    for (i = j = begin; i < end; i++){
+        //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]));
+        lbool sig = !lit_sign(*i); sig += sig - 1;
+        if (*i == lit_neg(last) || sig == values[lit_var(*i)])
+            return true;   // tautology
+        else if (*i != last && values[lit_var(*i)] == l_Undef)
+            last = *j++ = *i;
+    }
+
+    //printf("final: "); printlits(begin,j); printf("\n");
+
+    if (j == begin)          // empty clause
+        return false;
+
+    if (j - begin == 1) // unit clause
+        return enqueue(s,*begin,(clause*)0);
+
+    // create new clause
+    c = clause_new(s,begin,j,0);
+    if ( c )
+        vecp_push( &s->clauses,c );
+
+    s->stats.clauses++;
+    s->stats.clauses_literals += j - begin;
+
+    return true;
+}
+
+
+int sat_solver2_simplify(sat_solver2* s)
+{
+    clause** reasons;
+    int type;
+    int Counter = 0;
+
+    assert(sat_solver2_dlevel(s) == 0);
+
+    if (sat_solver2_propagate(s) != 0)
+        return false;
+
+    if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0)
+        return true;
+
+    reasons = s->reasons;
+    for (type = 0; type < 2; type++){
+        vecp*    cs  = type ? &s->learnts : &s->clauses;
+        clause** cls = (clause**)vecp_begin(cs);
+
+        int i, j;
+        for (j = i = 0; i < vecp_size(cs); i++){
+            if (reasons[lit_var(*clause_begin(cls[i]))] != cls[i] &&
+                clause_simplify(s,cls[i]) == l_True)
+                clause_remove(s,cls[i]), Counter++;
+            else
+                cls[j++] = cls[i];
+        }
+        vecp_resize(cs,j);
+    }
+//printf( "Simplification removed %d clauses (out of %d)...\n", Counter, s->stats.clauses );
+
+    s->simpdb_assigns = s->qhead;
+    // (shouldn't depend on 'stats' really, but it will do for now)
+    s->simpdb_props   = (int)(s->stats.clauses_literals + s->stats.learnts_literals);
+
+    return true;
+}
+
+double luby2(double y, int x)
+{
+    int size, seq;
+    for (size = 1, seq = 0; size < x+1; seq++, size = 2*size + 1);
+    while (size-1 != x){
+        size = (size-1) >> 1;
+        seq--;
+        x = x % size;
+    }
+    return pow(y, (double)seq);
+} 
+
+void luby2_test()
+{
+    int i;
+    for ( i = 0; i < 20; i++ )
+        printf( "%d ", (int)luby2(2,i) );
+    printf( "\n" );
+}
+
+int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
+{
+    int restart_iter = 0;
+    ABC_INT64_T  nof_conflicts;
+    ABC_INT64_T  nof_learnts   = sat_solver2_nclauses(s) / 3;
+    lbool   status        = l_Undef;
+    lbool*  values        = s->assigns;
+    lit*    i;
+
+    // set the external limits
+//    s->nCalls++;
+//    s->nRestarts  = 0;
+    s->nConfLimit = 0;
+    s->nInsLimit  = 0;
+    if ( nConfLimit )
+        s->nConfLimit = s->stats.conflicts + nConfLimit;
+    if ( nInsLimit )
+//        s->nInsLimit = s->stats.inspects + nInsLimit;
+        s->nInsLimit = s->stats.propagations + nInsLimit;
+    if ( nConfLimitGlobal && (s->nConfLimit == 0 || s->nConfLimit > nConfLimitGlobal) )
+        s->nConfLimit = nConfLimitGlobal;
+    if ( nInsLimitGlobal && (s->nInsLimit == 0 || s->nInsLimit > nInsLimitGlobal) )
+        s->nInsLimit = nInsLimitGlobal;
+
+#ifndef SAT_USE_ANALYZE_FINAL
+
+    //printf("solve: "); printlits(begin, end); printf("\n");
+    for (i = begin; i < end; i++){
+        switch (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]){
+        case 1: // l_True: 
+            break;
+        case 0: // l_Undef
+            assume(s, *i);
+            if (sat_solver2_propagate(s) == NULL)
+                break;
+            // fallthrough
+        case -1: // l_False 
+            sat_solver2_canceluntil(s, 0);
+            return l_False;
+        }
+    }
+    s->root_level = sat_solver2_dlevel(s);
+
+#endif
+
+/*
+    // Perform assumptions:
+    root_level = assumps.size();
+    for (int i = 0; i < assumps.size(); i++){
+        Lit p = assumps[i];
+        assert(var(p) < nVars());
+        if (!assume(p)){
+            GClause r = reason[var(p)];
+            if (r != GClause_NULL){
+                Clause* confl;
+                if (r.isLit()){
+                    confl = propagate_tmpbin;
+                    (*confl)[1] = ~p;
+                    (*confl)[0] = r.lit();
+                }else
+                    confl = r.clause();
+                analyzeFinal(confl, true);
+                conflict.push(~p);
+            }else
+                conflict.clear(),
+                conflict.push(~p);
+            cancelUntil(0);
+            return false; }
+        Clause* confl = propagate();
+        if (confl != NULL){
+            analyzeFinal(confl), assert(conflict.size() > 0);
+            cancelUntil(0);
+            return false; }
+    }
+    assert(root_level == decisionLevel());
+*/
+
+#ifdef SAT_USE_ANALYZE_FINAL
+    // Perform assumptions:
+    s->root_level = end - begin;
+    for ( i = begin; i < end; i++ )
+    {
+        lit p = *i;
+        assert(lit_var(p) < s->size);
+        veci_push(&s->trail_lim,s->qtail);
+        if (!enqueue(s,p,(clause*)0))
+        {
+            clause * r = s->reasons[lit_var(p)];
+            if (r != NULL)
+            {
+                clause* confl = r;
+                sat_solver2_analyze_final(s, confl, 1);
+                veci_push(&s->conf_final, lit_neg(p));
+            }
+            else
+            {
+                veci_resize(&s->conf_final,0);
+                veci_push(&s->conf_final, lit_neg(p));
+            }
+            sat_solver2_canceluntil(s, 0);
+            return l_False; 
+        }
+        else
+        {
+            clause* confl = sat_solver2_propagate(s);
+            if (confl != NULL){
+                sat_solver2_analyze_final(s, confl, 0);
+                assert(s->conf_final.size > 0);
+                sat_solver2_canceluntil(s, 0);
+                return l_False; }
+        }
+    }
+    assert(s->root_level == sat_solver2_dlevel(s));
+#endif
+
+//    s->nCalls2++;
+
+    if (s->verbosity >= 1){
+        printf("==================================[MINISAT]===================================\n");
+        printf("| Conflicts |     ORIGINAL     |              LEARNT              | Progress |\n");
+        printf("|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |\n");
+        printf("==============================================================================\n");
+    }
+
+    while (status == l_Undef){
+//        int nConfs = 0;
+        double Ratio = (s->stats.learnts == 0)? 0.0 :
+            s->stats.learnts_literals / (double)s->stats.learnts;
+        if ( s->nRuntimeLimit && time(NULL) > s->nRuntimeLimit )
+            break;
+
+        if (s->verbosity >= 1)
+        {
+            printf("| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %6.3f %% |\n", 
+                (double)s->stats.conflicts,
+                (double)s->stats.clauses, 
+                (double)s->stats.clauses_literals,
+                (double)nof_learnts, 
+                (double)s->stats.learnts, 
+                (double)s->stats.learnts_literals,
+                Ratio,
+                s->progress_estimate*100);
+            fflush(stdout);
+        }
+        nof_conflicts = (ABC_INT64_T)( 100 * luby2(2, restart_iter++) );
+//printf( "%d ", (int)nof_conflicts );
+//        nConfs = s->stats.conflicts;
+        status = sat_solver2_search(s, nof_conflicts, &nof_learnts);
+//        if ( status == l_True )
+//            printf( "%d ", s->stats.conflicts - nConfs );
+
+//        nof_conflicts = nof_conflicts * 3 / 2; //*= 1.5;
+//printf( "%d ", s->stats.conflicts  );
+        // quit the loop if reached an external limit
+        if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit )
+        {
+//            printf( "Reached the limit on the number of conflicts (%d).\n", s->nConfLimit );
+            break;
+        }
+//        if ( s->nInsLimit  && s->stats.inspects > s->nInsLimit )
+        if ( s->nInsLimit  && s->stats.propagations > s->nInsLimit )
+        {
+//            printf( "Reached the limit on the number of implications (%d).\n", s->nInsLimit );
+            break;
+        }
+        if ( s->nRuntimeLimit && time(NULL) > s->nRuntimeLimit )
+            break;
+    }
+//printf( "\n" );
+    if (s->verbosity >= 1)
+        printf("==============================================================================\n");
+
+    sat_solver2_canceluntil(s,0);
+    return status;
+}
+
+
+int sat_solver2_nvars(sat_solver2* s)
+{
+    return s->size;
+}
+
+
+int sat_solver2_nclauses(sat_solver2* s)
+{
+    return vecp_size(&s->clauses);
+}
+
+
+int sat_solver2_nconflicts(sat_solver2* s)
+{
+    return (int)s->stats.conflicts;
+}
+
+//=================================================================================================
+// Sorting functions (sigh):
+
+static inline void selectionsort(void** array, int size, int(*comp)(const void *, const void *))
+{
+    int     i, j, best_i;
+    void*   tmp;
+
+    for (i = 0; i < size-1; i++){
+        best_i = i;
+        for (j = i+1; j < size; j++){
+            if (comp(array[j], array[best_i]) < 0)
+                best_i = j;
+        }
+        tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp;
+    }
+}
+
+
+static void sortrnd(void** array, int size, int(*comp)(const void *, const void *), double* seed)
+{
+    if (size <= 15)
+        selectionsort(array, size, comp);
+
+    else{
+        void*       pivot = array[irand(seed, size)];
+        void*       tmp;
+        int         i = -1;
+        int         j = size;
+
+        for(;;){
+            do i++; while(comp(array[i], pivot)<0);
+            do j--; while(comp(pivot, array[j])<0);
+
+            if (i >= j) break;
+
+            tmp = array[i]; array[i] = array[j]; array[j] = tmp;
+        }
+
+        sortrnd(array    , i     , comp, seed);
+        sortrnd(&array[i], size-i, comp, seed);
+    }
+}
+
+void sat_solver2_sort(void** array, int size, int(*comp)(const void *, const void *))
+{
+//    int i;
+    double seed = 91648253;
+    sortrnd(array,size,comp,&seed);
+//    for ( i = 1; i < size; i++ )
+//        assert(comp(array[i-1], array[i])<0);
+}
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h
new file mode 100644
index 00000000..94cf0d63
--- /dev/null
+++ b/src/sat/bsat/satSolver2.h
@@ -0,0 +1,194 @@
+/**************************************************************************************************
+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 satSolver2_h
+#define satSolver2_h
+
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+
+#include "satVec.h"
+
+ABC_NAMESPACE_HEADER_START
+
+
+
+//=================================================================================================
+// Public interface:
+
+struct sat_solver2_t;
+typedef struct sat_solver2_t sat_solver2;
+
+extern sat_solver2* sat_solver2_new(void);
+extern void        sat_solver2_delete(sat_solver2* s);
+
+extern int         sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end);
+extern int         sat_solver2_simplify(sat_solver2* s);
+extern int         sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal);
+
+extern int         sat_solver2_nvars(sat_solver2* s);
+extern int         sat_solver2_nclauses(sat_solver2* s);
+extern int         sat_solver2_nconflicts(sat_solver2* s);
+
+extern void        sat_solver2_setnvars(sat_solver2* s,int n);
+
+extern void        Sat_Solver2WriteDimacs( sat_solver2 * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars );
+extern void        Sat_Solver2PrintStats( FILE * pFile, sat_solver2 * p );
+extern int *       Sat_Solver2GetModel( sat_solver2 * p, int * pVars, int nVars );
+extern void        Sat_Solver2DoubleClauses( sat_solver2 * p, int iVar );
+
+// trace recording
+extern void        sat_solver2TraceStart( sat_solver2 * pSat, char * pName );
+extern void        sat_solver2TraceStop( sat_solver2 * pSat );
+extern void        sat_solver2TraceWrite( sat_solver2 * pSat, int * pBeg, int * pEnd, int fRoot );
+
+// clause storage
+extern void        sat_solver2_store_alloc( sat_solver2 * s );
+extern void        sat_solver2_store_write( sat_solver2 * s, char * pFileName );
+extern void        sat_solver2_store_free( sat_solver2 * s );
+extern void        sat_solver2_store_mark_roots( sat_solver2 * s );
+extern void        sat_solver2_store_mark_clauses_a( sat_solver2 * s );
+extern void *      sat_solver2_store_release( sat_solver2 * s ); 
+
+//=================================================================================================
+// Solver representation:
+
+struct clause_t;
+typedef struct clause_t clause;
+
+struct sat_solver2_t
+{
+    int      size;          // nof variables
+    int      cap;           // size of varmaps
+    int      qhead;         // Head index of queue.
+    int      qtail;         // Tail index of queue.
+
+    // clauses
+    vecp     clauses;       // List of problem constraints. (contains: clause*)
+    vecp     learnts;       // List of learnt clauses. (contains: clause*)
+
+    // activities
+//    double   var_inc;       // Amount to bump next variable with.
+//    double   var_decay;     // INVERSE decay factor for variable activity: stores 1/decay. 
+    int      var_inc;
+//    int      var_decay;
+
+//    float    cla_inc;       // Amount to bump next clause with.
+    int      cla_inc;       // Amount to bump next clause with.
+//    float    cla_decay;     // INVERSE decay factor for clause activity: stores 1/decay.
+
+    vecp*    wlists;        // 
+//    double*  activity;      // A heuristic measurement of the activity of a variable.
+    unsigned*activity;      // A heuristic measurement of the activity of a variable.
+    lbool*   assigns;       // Current values of variables.
+    int*     orderpos;      // Index in variable order.
+    clause** reasons;       //
+    int*     levels;        //
+    lit*     trail;
+    char*    polarity;
+
+    clause*  binary;        // A temporary binary clause
+    lbool*   tags;          //
+    veci     tagged;        // (contains: var)
+    veci     stack;         // (contains: var)
+
+    veci     order;         // Variable order. (heap) (contains: var)
+    veci     trail_lim;     // Separator indices for different decision levels in 'trail'. (contains: int)
+    veci     model;         // If problem is solved, this vector contains the model (contains: lbool).
+    veci     conf_final;    // If problem is unsatisfiable (possibly under assumptions),
+                            // this vector represent the final conflict clause expressed in the assumptions.
+
+    int      root_level;    // Level of first proper decision.
+    int      simpdb_assigns;// Number of top-level assignments at last 'simplifyDB()'.
+    int      simpdb_props;  // Number of propagations before next 'simplifyDB()'.
+    double   random_seed;
+    double   progress_estimate;
+    int      verbosity;     // Verbosity level. 0=silent, 1=some progress report, 2=everything
+
+    stats_t    stats;
+
+    ABC_INT64_T   nConfLimit;    // external limit on the number of conflicts
+    ABC_INT64_T   nInsLimit;     // external limit on the number of implications
+    int           nRuntimeLimit; // external limit on runtime
+
+    // clause memory
+    int *    pMemArray;
+    int      nMemAlloc;
+    int      nMemSize;
+
+//    int      fSkipSimplify; // set to one to skip simplification of the clause database
+    int      fNotUseRandom; // do not allow random decisions with a fixed probability
+
+    veci     temp_clause;    // temporary storage for a CNF clause
+};
+
+static int sat_solver2_var_value( sat_solver2* s, int v ) 
+{
+    assert( s->model.ptr != NULL && v < s->size );
+    return (int)(s->model.ptr[v] == l_True);
+}
+static int sat_solver2_var_literal( sat_solver2* s, int v ) 
+{
+    assert( s->model.ptr != NULL && v < s->size );
+    return toLitCond( v, s->model.ptr[v] != l_True );
+}
+static void sat_solver2_act_var_clear(sat_solver2* s) 
+{
+    int i;
+    for (i = 0; i < s->size; i++)
+        s->activity[i] = 0;//.0;
+    s->var_inc = 1.0;
+}
+static void sat_solver2_compress(sat_solver2* s) 
+{
+    if ( s->qtail != s->qhead )
+    {
+        int RetValue = sat_solver2_simplify(s);
+        assert( RetValue != 0 );
+    }
+}
+
+static int sat_solver2_final(sat_solver2* s, int ** ppArray)
+{
+    *ppArray = s->conf_final.ptr;
+    return s->conf_final.size;
+}
+
+static int sat_solver2_set_runtime_limit(sat_solver2* s, int Limit)
+{
+    int nRuntimeLimit = s->nRuntimeLimit;
+    s->nRuntimeLimit = Limit;
+    return nRuntimeLimit;
+}
+
+static int sat_solver2_set_random(sat_solver2* s, int fNotUseRandom)
+{
+    int fNotUseRandomOld = s->fNotUseRandom;
+    s->fNotUseRandom = fNotUseRandom;
+    return fNotUseRandomOld;
+}
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c
index 0ce40acd..c8569606 100644
--- a/src/sat/bsat/satUtil.c
+++ b/src/sat/bsat/satUtil.c
@@ -21,6 +21,7 @@
 #include <stdio.h>
 #include <assert.h>
 #include "satSolver.h"
+#include "satSolver2.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -148,13 +149,36 @@ void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, int fIncrement )
 ***********************************************************************/
 void Sat_SolverPrintStats( FILE * pFile, sat_solver * p )
 {
-//    printf( "calls         : %8d (%d)\n", (int)p->nCalls, (int)p->nCalls2 );
-    printf( "starts        : %8d\n", (int)p->stats.starts );
-    printf( "conflicts     : %8d\n", (int)p->stats.conflicts );
-    printf( "decisions     : %8d\n", (int)p->stats.decisions );
-    printf( "propagations  : %8d\n", (int)p->stats.propagations );
-    printf( "inspects      : %8d\n", (int)p->stats.inspects );
-//    printf( "inspects2     : %8d\n", (int)p->stats.inspects2 );
+//    printf( "calls         : %10d (%d)\n", (int)p->nCalls, (int)p->nCalls2 );
+    printf( "starts        : %10d\n", (int)p->stats.starts );
+    printf( "conflicts     : %10d\n", (int)p->stats.conflicts );
+    printf( "decisions     : %10d\n", (int)p->stats.decisions );
+    printf( "propagations  : %10d\n", (int)p->stats.propagations );
+    printf( "inspects      : %10d\n", (int)p->stats.inspects );
+//    printf( "inspects2     : %10d\n", (int)p->stats.inspects2 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the given clause in a file in DIMACS format.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sat_Solver2PrintStats( FILE * pFile, sat_solver2 * p )
+{
+//    printf( "calls         : %10d (%d)\n", (int)p->nCalls, (int)p->nCalls2 );
+    printf( "starts        : %10d\n", (int)p->stats.starts );
+    printf( "conflicts     : %10d\n", (int)p->stats.conflicts );
+    printf( "decisions     : %10d\n", (int)p->stats.decisions );
+    printf( "propagations  : %10d\n", (int)p->stats.propagations );
+    printf( "inspects      : %10d\n", (int)p->stats.inspects );
+//    printf( "inspects2     : %10d\n", (int)p->stats.inspects2 );
+    printf( "memory        : %10d\n", p->nMemSize );
 }
 
 /**Function*************************************************************
@@ -183,6 +207,30 @@ int * Sat_SolverGetModel( sat_solver * p, int * pVars, int nVars )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns a counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int * Sat_Solver2GetModel( sat_solver2 * p, int * pVars, int nVars )
+{
+    int * pModel;
+    int i;
+    pModel = ABC_CALLOC( int, nVars+1 );
+    for ( i = 0; i < nVars; i++ )
+    {
+        assert( pVars[i] >= 0 && pVars[i] < p->size );
+        pModel[i] = (int)(p->model.ptr[pVars[i]] == l_True);
+    }
+    return pModel;    
+}
+
+/**Function*************************************************************
+
   Synopsis    [Duplicates all clauses, complements unit clause of the given var.]
 
   Description []