Version abc71001

17 files changed, 5429 insertions, 0 deletions

diff --git a/src/sat/msat/module.make b/src/sat/msat/module.make
new file mode 100644
index 00000000..0dadfbe1
--- /dev/null
+++ b/src/sat/msat/module.make
@@ -0,0 +1,13 @@
+SRC +=  src/sat/msat/msatActivity.c \
+    src/sat/msat/msatClause.c \
+    src/sat/msat/msatClauseVec.c \
+    src/sat/msat/msatMem.c \
+    src/sat/msat/msatOrderJ.c \
+    src/sat/msat/msatQueue.c \
+    src/sat/msat/msatRead.c \
+    src/sat/msat/msatSolverApi.c \
+    src/sat/msat/msatSolverCore.c \
+    src/sat/msat/msatSolverIo.c \
+    src/sat/msat/msatSolverSearch.c \
+    src/sat/msat/msatSort.c \
+    src/sat/msat/msatVec.c
diff --git a/src/sat/msat/msat.h b/src/sat/msat/msat.h
new file mode 100644
index 00000000..53353ba6
--- /dev/null
+++ b/src/sat/msat/msat.h
@@ -0,0 +1,172 @@
+/**CFile****************************************************************
+
+  FileName    [msat.h]
+
+  PackageName [A C version of SAT solver MINISAT, originally developed 
+  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of 
+  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
+
+  Synopsis    [External definitions of the solver.]
+
+  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 1, 2004.]
+
+  Revision    [$Id: msat.h,v 1.6 2004/05/12 06:30:20 satrajit Exp $]
+
+***********************************************************************/
+
+#ifndef __MSAT_H__
+#define __MSAT_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    STRUCTURE DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+#ifdef bool
+#undef bool
+#endif
+
+#ifndef __MVTYPES_H__
+typedef int  bool;
+#endif
+
+typedef struct Msat_Solver_t_      Msat_Solver_t;
+
+// the vector of intergers and of clauses
+typedef struct Msat_IntVec_t_      Msat_IntVec_t;
+typedef struct Msat_ClauseVec_t_   Msat_ClauseVec_t;
+typedef struct Msat_VarHeap_t_     Msat_VarHeap_t;
+
+// the return value of the solver
+typedef enum { MSAT_FALSE = -1, MSAT_UNKNOWN = 0, MSAT_TRUE = 1 } Msat_Type_t;
+
+// representation of variables and literals
+// the literal (l) is the variable (v) and the sign (s)
+// s = 0 the variable is positive
+// s = 1 the variable is negative
+#define MSAT_VAR2LIT(v,s) (2*(v)+(s)) 
+#define MSAT_LITNOT(l)    ((l)^1)
+#define MSAT_LITSIGN(l)   ((l)&1)     
+#define MSAT_LIT2VAR(l)   ((l)>>1)
+
+////////////////////////////////////////////////////////////////////////
+///                       GLOBAL VARIABLES                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                       MACRO DEFINITIONS                          ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DECLARATIONS                        ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== satRead.c ============================================================*/
+extern bool             Msat_SolverParseDimacs( FILE * pFile, Msat_Solver_t ** p, int fVerbose );
+/*=== satSolver.c ===========================================================*/
+// adding vars, clauses, simplifying the database, and solving
+extern bool             Msat_SolverAddVar( Msat_Solver_t * p, int Level );
+extern bool             Msat_SolverAddClause( Msat_Solver_t * p, Msat_IntVec_t * pLits );
+extern bool             Msat_SolverSimplifyDB( Msat_Solver_t * p );
+extern bool             Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * pVecAssumps, int nBackTrackLimit, int nTimeLimit );
+// printing stats, assignments, and clauses
+extern void             Msat_SolverPrintStats( Msat_Solver_t * p );
+extern void             Msat_SolverPrintAssignment( Msat_Solver_t * p );
+extern void             Msat_SolverPrintClauses( Msat_Solver_t * p );
+extern void             Msat_SolverWriteDimacs( Msat_Solver_t * p, char * pFileName );
+// access to the solver internal data
+extern int              Msat_SolverReadVarNum( Msat_Solver_t * p );
+extern int              Msat_SolverReadClauseNum( Msat_Solver_t * p );
+extern int              Msat_SolverReadVarAllocNum( Msat_Solver_t * p );
+extern int *            Msat_SolverReadAssignsArray( Msat_Solver_t * p );
+extern int *            Msat_SolverReadModelArray( Msat_Solver_t * p );
+extern unsigned         Msat_SolverReadTruth( Msat_Solver_t * p );
+extern int              Msat_SolverReadBackTracks( Msat_Solver_t * p );
+extern int              Msat_SolverReadInspects( Msat_Solver_t * p );
+extern void             Msat_SolverSetVerbosity( Msat_Solver_t * p, int fVerbose );
+extern void             Msat_SolverSetProofWriting( Msat_Solver_t * p, int fProof );
+extern void             Msat_SolverSetVarTypeA( Msat_Solver_t * p, int Var );
+extern void             Msat_SolverSetVarMap( Msat_Solver_t * p, Msat_IntVec_t * vVarMap );
+extern void             Msat_SolverMarkLastClauseTypeA( Msat_Solver_t * p );
+extern void             Msat_SolverMarkClausesStart( Msat_Solver_t * p );
+extern float *          Msat_SolverReadFactors( Msat_Solver_t * p );
+// returns the solution after incremental solving
+extern int              Msat_SolverReadSolutions( Msat_Solver_t * p );
+extern int *            Msat_SolverReadSolutionsArray( Msat_Solver_t * p );
+extern Msat_ClauseVec_t *  Msat_SolverReadAdjacents( Msat_Solver_t * p );
+extern Msat_IntVec_t *  Msat_SolverReadConeVars( Msat_Solver_t * p );
+extern Msat_IntVec_t *  Msat_SolverReadVarsUsed( Msat_Solver_t * p );
+/*=== satSolverSearch.c ===========================================================*/
+extern void             Msat_SolverRemoveLearned( Msat_Solver_t * p );
+extern void             Msat_SolverRemoveMarked( Msat_Solver_t * p );
+/*=== satSolverApi.c ===========================================================*/
+// allocation, cleaning, and freeing the solver
+extern Msat_Solver_t *  Msat_SolverAlloc( int nVars, double dClaInc, double dClaDecay, double dVarInc, double dVarDecay, bool fVerbose );
+extern void             Msat_SolverResize( Msat_Solver_t * pMan, int nVarsAlloc );
+extern void             Msat_SolverClean( Msat_Solver_t * p, int nVars );
+extern void             Msat_SolverPrepare( Msat_Solver_t * pSat, Msat_IntVec_t * vVars );
+extern void             Msat_SolverFree( Msat_Solver_t * p );
+/*=== satVec.c ===========================================================*/
+extern Msat_IntVec_t *  Msat_IntVecAlloc( int nCap );
+extern Msat_IntVec_t *  Msat_IntVecAllocArray( int * pArray, int nSize );
+extern Msat_IntVec_t *  Msat_IntVecAllocArrayCopy( int * pArray, int nSize );
+extern Msat_IntVec_t *  Msat_IntVecDup( Msat_IntVec_t * pVec );
+extern Msat_IntVec_t *  Msat_IntVecDupArray( Msat_IntVec_t * pVec );
+extern void             Msat_IntVecFree( Msat_IntVec_t * p );
+extern void             Msat_IntVecFill( Msat_IntVec_t * p, int nSize, int Entry );
+extern int *            Msat_IntVecReleaseArray( Msat_IntVec_t * p );
+extern int *            Msat_IntVecReadArray( Msat_IntVec_t * p );
+extern int              Msat_IntVecReadSize( Msat_IntVec_t * p );
+extern int              Msat_IntVecReadEntry( Msat_IntVec_t * p, int i );
+extern int              Msat_IntVecReadEntryLast( Msat_IntVec_t * p );
+extern void             Msat_IntVecWriteEntry( Msat_IntVec_t * p, int i, int Entry );
+extern void             Msat_IntVecGrow( Msat_IntVec_t * p, int nCapMin );
+extern void             Msat_IntVecShrink( Msat_IntVec_t * p, int nSizeNew );
+extern void             Msat_IntVecClear( Msat_IntVec_t * p );
+extern void             Msat_IntVecPush( Msat_IntVec_t * p, int Entry );
+extern int              Msat_IntVecPushUnique( Msat_IntVec_t * p, int Entry );
+extern void             Msat_IntVecPushUniqueOrder( Msat_IntVec_t * p, int Entry, int fIncrease );
+extern int              Msat_IntVecPop( Msat_IntVec_t * p );
+extern void             Msat_IntVecSort( Msat_IntVec_t * p, int fReverse );
+/*=== satHeap.c ===========================================================*/
+extern Msat_VarHeap_t * Msat_VarHeapAlloc();
+extern void             Msat_VarHeapSetActivity( Msat_VarHeap_t * p, double * pActivity );
+extern void             Msat_VarHeapStart( Msat_VarHeap_t * p, int * pVars, int nVars, int nVarsAlloc );
+extern void             Msat_VarHeapGrow( Msat_VarHeap_t * p, int nSize );
+extern void             Msat_VarHeapStop( Msat_VarHeap_t * p );
+extern void             Msat_VarHeapPrint( FILE * pFile, Msat_VarHeap_t * p );
+extern void             Msat_VarHeapCheck( Msat_VarHeap_t * p );
+extern void             Msat_VarHeapCheckOne( Msat_VarHeap_t * p, int iVar );
+extern int              Msat_VarHeapContainsVar( Msat_VarHeap_t * p, int iVar );
+extern void             Msat_VarHeapInsert( Msat_VarHeap_t * p, int iVar );  
+extern void             Msat_VarHeapUpdate( Msat_VarHeap_t * p, int iVar );  
+extern void             Msat_VarHeapDelete( Msat_VarHeap_t * p, int iVar );  
+extern double           Msat_VarHeapReadMaxWeight( Msat_VarHeap_t * p );
+extern int              Msat_VarHeapCountNodes( Msat_VarHeap_t * p, double WeightLimit );  
+extern int              Msat_VarHeapReadMax( Msat_VarHeap_t * p );  
+extern int              Msat_VarHeapGetMax( Msat_VarHeap_t * p );  
+ 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/msat/msatActivity.c b/src/sat/msat/msatActivity.c
new file mode 100644
index 00000000..1cd795bd
--- /dev/null
+++ b/src/sat/msat/msatActivity.c
@@ -0,0 +1,160 @@
+/**CFile****************************************************************
+
+  FileName    [msatActivity.c]
+
+  PackageName [A C version of SAT solver MINISAT, originally developed 
+  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of 
+  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
+
+  Synopsis    [Procedures controlling activity of variables and clauses.]
+
+  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 1, 2004.]
+
+  Revision    [$Id: msatActivity.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "msatInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_SolverVarBumpActivity( Msat_Solver_t * p, Msat_Lit_t Lit )
+{
+    Msat_Var_t Var;
+    if ( p->dVarDecay < 0 ) // (negative decay means static variable order -- don't bump)
+        return;
+    Var = MSAT_LIT2VAR(Lit);
+    p->pdActivity[Var] += p->dVarInc;
+//    p->pdActivity[Var] += p->dVarInc * p->pFactors[Var];
+    if ( p->pdActivity[Var] > 1e100 )
+        Msat_SolverVarRescaleActivity( p );
+    Msat_OrderUpdate( p->pOrder, Var );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_SolverVarDecayActivity( Msat_Solver_t * p )
+{
+    if ( p->dVarDecay >= 0 )
+        p->dVarInc *= p->dVarDecay;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Divide all variable activities by 1e100.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_SolverVarRescaleActivity( Msat_Solver_t * p )
+{
+    int i;
+    for ( i = 0; i < p->nVars; i++ )
+        p->pdActivity[i] *= 1e-100;
+    p->dVarInc *= 1e-100;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_SolverClaBumpActivity( Msat_Solver_t * p, Msat_Clause_t * pC )
+{
+    float Activ;
+    Activ = Msat_ClauseReadActivity(pC);
+    if ( Activ + p->dClaInc > 1e20 )
+    {
+        Msat_SolverClaRescaleActivity( p );
+        Activ = Msat_ClauseReadActivity( pC );
+    }
+    Msat_ClauseWriteActivity( pC, Activ + (float)p->dClaInc );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_SolverClaDecayActivity( Msat_Solver_t * p )
+{
+    p->dClaInc *= p->dClaDecay;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Divide all constraint activities by 1e20.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_SolverClaRescaleActivity( Msat_Solver_t * p )
+{
+    Msat_Clause_t ** pLearned;
+    int nLearned, i;
+    float Activ;
+    nLearned = Msat_ClauseVecReadSize( p->vLearned );
+    pLearned = Msat_ClauseVecReadArray( p->vLearned );
+    for ( i = 0; i < nLearned; i++ )
+    {
+        Activ = Msat_ClauseReadActivity( pLearned[i] );
+        Msat_ClauseWriteActivity( pLearned[i], Activ * (float)1e-20 );
+    }
+    p->dClaInc *= 1e-20;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/msat/msatClause.c b/src/sat/msat/msatClause.c
new file mode 100644
index 00000000..2ba8cd32
--- /dev/null
+++ b/src/sat/msat/msatClause.c
@@ -0,0 +1,529 @@
+/**CFile****************************************************************
+
+  FileName    [msatClause.c]
+
+  PackageName [A C version of SAT solver MINISAT, originally developed 
+  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of 
+  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
+
+  Synopsis    [Procedures working with SAT clauses.]
+
+  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 1, 2004.]
+
+  Revision    [$Id: msatClause.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "msatInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+struct Msat_Clause_t_
+{
+    int           Num;              // unique number of the clause
+    unsigned      fLearned   :  1;  // 1 if the clause is learned
+    unsigned      fMark      :  1;  // used to mark visited clauses during proof recording
+    unsigned      fTypeA     :  1;  // used to mark clauses belonging to A for interpolant computation
+    unsigned      nSize      : 14;  // the number of literals in the clause
+    unsigned      nSizeAlloc : 15;  // the number of bytes allocated for the clause
+    Msat_Lit_t     pData[0];
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a new clause.]
+
+  Description [Returns FALSE if top-level conflict detected (must be handled); 
+  TRUE otherwise. 'pClause_out' may be set to NULL if clause is already 
+  satisfied by the top-level assignment.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearned, Msat_Clause_t ** pClause_out )
+{
+    int * pAssigns = Msat_SolverReadAssignsArray(p);
+    Msat_ClauseVec_t ** pvWatched;
+    Msat_Clause_t * pC;
+    int * pLits;
+    int nLits, i, j;
+    int nBytes;
+    Msat_Var_t Var;
+    bool Sign;
+
+    *pClause_out = NULL;
+
+    nLits = Msat_IntVecReadSize(vLits);
+    pLits = Msat_IntVecReadArray(vLits);
+
+    if ( !fLearned ) 
+    {
+        int * pSeen = Msat_SolverReadSeenArray( p );
+        int nSeenId;
+        assert( Msat_SolverReadDecisionLevel(p) == 0 );
+        // sorting literals makes the code trace-equivalent 
+        // with to the original C++ solver
+        Msat_IntVecSort( vLits, 0 );
+        // increment the counter of seen twice
+        nSeenId = Msat_SolverIncrementSeenId( p );
+        nSeenId = Msat_SolverIncrementSeenId( p );
+        // nSeenId - 1 stands for negative
+        // nSeenId     stands for positive
+        // Remove false literals
+
+        // there is a bug here!!!!
+        // when the same var in opposite polarities is given, it drops one polarity!!!
+
+        for ( i = j = 0; i < nLits; i++ ) {
+            // get the corresponding variable
+            Var  = MSAT_LIT2VAR(pLits[i]);
+            Sign = MSAT_LITSIGN(pLits[i]); // Sign=0 for positive
+            // check if we already saw this variable in the this clause
+            if ( pSeen[Var] >= nSeenId - 1 )
+            {
+                if ( (pSeen[Var] != nSeenId) == Sign ) // the same lit
+                    continue;
+                return 1; // two opposite polarity lits -- don't add the clause
+            }
+            // mark the variable as seen
+            pSeen[Var] = nSeenId - !Sign;
+
+            // analize the value of this literal
+            if ( pAssigns[Var] != MSAT_VAR_UNASSIGNED )
+            {
+                if ( pAssigns[Var] == pLits[i] )
+                    return 1;  // the clause is always true -- don't add anything
+                // the literal has no impact - skip it
+                continue;
+            }
+            // otherwise, add this literal to the clause
+            pLits[j++] = pLits[i];
+        }
+        Msat_IntVecShrink( vLits, j );
+        nLits = j;
+/*
+        // the problem with this code is that performance is very
+        // sensitive to the ordering of adjacency lits
+        // the best ordering requires fanins first, next fanouts
+        // this ordering is more convenient to make from FRAIG
+
+        // create the adjacency information
+        if ( nLits > 2 )
+        {
+            Msat_Var_t VarI, VarJ;
+            Msat_IntVec_t * pAdjI, * pAdjJ;
+
+            for ( i = 0; i < nLits; i++ )
+            {
+                VarI = MSAT_LIT2VAR(pLits[i]);
+                pAdjI = (Msat_IntVec_t *)p->vAdjacents->pArray[VarI];
+
+                for ( j = i+1; j < nLits; j++ )
+                {
+                    VarJ = MSAT_LIT2VAR(pLits[j]);
+                    pAdjJ = (Msat_IntVec_t *)p->vAdjacents->pArray[VarJ];
+
+                    Msat_IntVecPushUniqueOrder( pAdjI, VarJ, 1 );
+                    Msat_IntVecPushUniqueOrder( pAdjJ, VarI, 1 );
+                }
+            }
+        }
+*/
+    }
+    // 'vLits' is now the (possibly) reduced vector of literals.
+    if ( nLits == 0 )
+        return 0;
+    if ( nLits == 1 )
+        return Msat_SolverEnqueue( p, pLits[0], NULL );
+
+    // Allocate clause:
+//    nBytes = sizeof(unsigned)*(nLits + 1 + (int)fLearned);
+    nBytes = sizeof(unsigned)*(nLits + 2 + (int)fLearned);
+#ifdef USE_SYSTEM_MEMORY_MANAGEMENT
+    pC = (Msat_Clause_t *)ALLOC( char, nBytes );
+#else
+    pC = (Msat_Clause_t *)Msat_MmStepEntryFetch( Msat_SolverReadMem(p), nBytes );
+#endif
+    pC->Num        = p->nClauses++;
+    pC->fTypeA     = 0;
+    pC->fMark      = 0;
+    pC->fLearned   = fLearned;
+    pC->nSize      = nLits;
+    pC->nSizeAlloc = nBytes;
+    memcpy( pC->pData, pLits, sizeof(int)*nLits );
+
+    // For learnt clauses only:
+    if ( fLearned )
+    {
+        int * pLevel = Msat_SolverReadDecisionLevelArray( p );
+        int iLevelMax, iLevelCur, iLitMax;
+
+        // Put the second watch on the literal with highest decision level:
+        iLitMax = 1;
+        iLevelMax = pLevel[ MSAT_LIT2VAR(pLits[1]) ];
+        for ( i = 2; i < nLits; i++ )
+        {
+            iLevelCur = pLevel[ MSAT_LIT2VAR(pLits[i]) ];
+            assert( iLevelCur != -1 );
+            if ( iLevelMax < iLevelCur )
+            // this is very strange - shouldn't it be???
+            // if ( iLevelMax > iLevelCur )
+                iLevelMax = iLevelCur, iLitMax = i;
+        }
+        pC->pData[1]       = pLits[iLitMax];
+        pC->pData[iLitMax] = pLits[1];
+
+        // Bumping:
+        // (newly learnt clauses should be considered active)
+        Msat_ClauseWriteActivity( pC, 0.0 );
+        Msat_SolverClaBumpActivity( p, pC ); 
+//        if ( nLits < 20 )
+        for ( i = 0; i < nLits; i++ )
+        {
+            Msat_SolverVarBumpActivity( p, pLits[i] );
+//            Msat_SolverVarBumpActivity( p, pLits[i] );
+//            p->pFreq[ MSAT_LIT2VAR(pLits[i]) ]++;
+        }
+    }
+
+    // Store clause:
+    pvWatched = Msat_SolverReadWatchedArray( p );
+    Msat_ClauseVecPush( pvWatched[ MSAT_LITNOT(pC->pData[0]) ], pC );
+    Msat_ClauseVecPush( pvWatched[ MSAT_LITNOT(pC->pData[1]) ], pC );
+    *pClause_out = pC;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocates the clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_ClauseFree( Msat_Solver_t * p, Msat_Clause_t * pC, bool fRemoveWatched )
+{
+    if ( fRemoveWatched )
+    {
+        Msat_Lit_t Lit;
+        Msat_ClauseVec_t ** pvWatched;
+        pvWatched = Msat_SolverReadWatchedArray( p );
+        Lit = MSAT_LITNOT( pC->pData[0] );
+        Msat_ClauseRemoveWatch( pvWatched[Lit], pC );
+        Lit = MSAT_LITNOT( pC->pData[1] );
+        Msat_ClauseRemoveWatch( pvWatched[Lit], pC ); 
+    }
+
+#ifdef USE_SYSTEM_MEMORY_MANAGEMENT
+    free( pC );
+#else
+    Msat_MmStepEntryRecycle( Msat_SolverReadMem(p), (char *)pC, pC->nSizeAlloc );
+#endif
+
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Access the data field of the clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool  Msat_ClauseReadLearned( Msat_Clause_t * pC )  {  return pC->fLearned; }
+int   Msat_ClauseReadSize( Msat_Clause_t * pC )     {  return pC->nSize;    }
+int * Msat_ClauseReadLits( Msat_Clause_t * pC )     {  return pC->pData;    }
+bool  Msat_ClauseReadMark( Msat_Clause_t * pC )     {  return pC->fMark;    }
+int   Msat_ClauseReadNum( Msat_Clause_t * pC )      {  return pC->Num;      }
+bool  Msat_ClauseReadTypeA( Msat_Clause_t * pC )    {  return pC->fTypeA;    }
+
+void  Msat_ClauseSetMark( Msat_Clause_t * pC, bool fMark )   {  pC->fMark = fMark;   }
+void  Msat_ClauseSetNum( Msat_Clause_t * pC, int Num )       {  pC->Num = Num;       }
+void  Msat_ClauseSetTypeA( Msat_Clause_t * pC, bool fTypeA ) {  pC->fTypeA = fTypeA; }
+
+/**Function*************************************************************
+
+  Synopsis    [Checks whether the learned clause is locked.]
+
+  Description [The clause may be locked if it is the reason of a
+  recent conflict. Such clause cannot be removed from the database.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Msat_ClauseIsLocked( Msat_Solver_t * p, Msat_Clause_t * pC )
+{
+    Msat_Clause_t ** pReasons = Msat_SolverReadReasonArray( p );
+    return (bool)(pReasons[MSAT_LIT2VAR(pC->pData[0])] == pC);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reads the activity of the given clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Msat_ClauseReadActivity( Msat_Clause_t * pC )
+{
+    return *((float *)(pC->pData + pC->nSize));
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the activity of the clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_ClauseWriteActivity( Msat_Clause_t * pC, float Num )
+{
+    *((float *)(pC->pData + pC->nSize)) = Num;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Propages the assignment.]
+
+  Description [The literal that has become true (Lit) is given to this 
+  procedure. The array of current variable assignments is given for
+  efficiency. The output literal (pLit_out) can be the second watched
+  literal (if TRUE is returned) or the conflict literal (if FALSE is 
+  returned). This messy interface is used to improve performance.
+  This procedure accounts for ~50% of the runtime of the solver.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Msat_ClausePropagate( Msat_Clause_t * pC, Msat_Lit_t Lit, int * pAssigns, Msat_Lit_t * pLit_out )
+{
+    // make sure the false literal is pC->pData[1]
+    Msat_Lit_t LitF = MSAT_LITNOT(Lit);
+    if ( pC->pData[0] == LitF )
+         pC->pData[0] = pC->pData[1], pC->pData[1] = LitF;
+    assert( pC->pData[1] == LitF );
+    // if the 0-th watch is true, clause is already satisfied
+    if ( pAssigns[MSAT_LIT2VAR(pC->pData[0])] == pC->pData[0] )
+        return 1; 
+    // look for a new watch
+    if ( pC->nSize > 2 )
+    {
+        int i;
+        for ( i = 2; i < (int)pC->nSize; i++ )
+            if ( pAssigns[MSAT_LIT2VAR(pC->pData[i])] != MSAT_LITNOT(pC->pData[i]) )
+            {
+                pC->pData[1] = pC->pData[i], pC->pData[i] = LitF;
+                *pLit_out = MSAT_LITNOT(pC->pData[1]);
+                return 1; 
+            }
+    }
+    // clause is unit under assignment
+    *pLit_out = pC->pData[0];
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Simplifies the clause.]
+
+  Description [Assumes everything has been propagated! (esp. watches 
+  in clauses are NOT unsatisfied)]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Msat_ClauseSimplify( Msat_Clause_t * pC, int * pAssigns )
+{
+    Msat_Var_t Var;
+    int i, j;
+    for ( i = j = 0; i < (int)pC->nSize; i++ )
+    {
+        Var = MSAT_LIT2VAR(pC->pData[i]);
+        if ( pAssigns[Var] == MSAT_VAR_UNASSIGNED )
+        {
+            pC->pData[j++] = pC->pData[i];
+            continue;
+        }
+        if ( pAssigns[Var] == pC->pData[i] )
+            return 1;
+        // otherwise, the value of the literal is false
+        // make sure, this literal is not watched
+        assert( i >= 2 );
+    }
+    // if the size has changed, update it and move activity
+    if ( j < (int)pC->nSize )
+    {
+        float Activ = Msat_ClauseReadActivity(pC);
+        pC->nSize = j;
+        Msat_ClauseWriteActivity(pC, Activ);
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes reason of conflict in the given clause.]
+
+  Description [If the literal is unassigned, finds the reason by 
+  complementing literals in the given cluase (pC). If the literal is
+  assigned, makes sure that this literal is the first one in the clause
+  and computes the complement of all other literals in the clause.
+  Returns the reason in the given array (vLits_out). If the clause is
+  learned, bumps its activity.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_ClauseCalcReason( Msat_Solver_t * p, Msat_Clause_t * pC, Msat_Lit_t Lit, Msat_IntVec_t * vLits_out )
+{
+    int i;
+    // clear the reason
+    Msat_IntVecClear( vLits_out );
+    assert( Lit == MSAT_LIT_UNASSIGNED || Lit == pC->pData[0] );
+    for ( i = (Lit != MSAT_LIT_UNASSIGNED); i < (int)pC->nSize; i++ )
+    {
+        assert( Msat_SolverReadAssignsArray(p)[MSAT_LIT2VAR(pC->pData[i])] == MSAT_LITNOT(pC->pData[i]) );
+        Msat_IntVecPush( vLits_out, MSAT_LITNOT(pC->pData[i]) );
+    }
+    if ( pC->fLearned ) 
+        Msat_SolverClaBumpActivity( p, pC );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes the given clause from the watched list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_ClauseRemoveWatch( Msat_ClauseVec_t * vClauses, Msat_Clause_t * pC )
+{
+    Msat_Clause_t ** pClauses;
+    int nClauses, i;
+    nClauses = Msat_ClauseVecReadSize( vClauses );
+    pClauses = Msat_ClauseVecReadArray( vClauses );
+    for ( i = 0; pClauses[i] != pC; i++ )
+        assert( i < nClauses );
+    for (      ; i < nClauses - 1; i++ )
+        pClauses[i] = pClauses[i+1];
+    Msat_ClauseVecPop( vClauses );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the given clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_ClausePrint( Msat_Clause_t * pC )
+{
+    int i;
+    if ( pC == NULL )
+        printf( "NULL pointer" );
+    else 
+    {
+        if ( pC->fLearned )
+            printf( "Act = %.4f  ", Msat_ClauseReadActivity(pC) );
+        for ( i = 0; i < (int)pC->nSize; i++ )
+            printf( " %s%d", ((pC->pData[i]&1)? "-": ""),  pC->pData[i]/2 + 1 );
+    }
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the given clause in a file in DIMACS format.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_ClauseWriteDimacs( FILE * pFile, Msat_Clause_t * pC, bool fIncrement )
+{
+    int i;
+    for ( i = 0; i < (int)pC->nSize; i++ )
+        fprintf( pFile, "%s%d ", ((pC->pData[i]&1)? "-": ""),  pC->pData[i]/2 + (int)(fIncrement>0) );
+    if ( fIncrement )
+        fprintf( pFile, "0" );
+    fprintf( pFile, "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the given clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_ClausePrintSymbols( Msat_Clause_t * pC )
+{
+    int i;
+    if ( pC == NULL )
+        printf( "NULL pointer" );
+    else 
+    {
+//        if ( pC->fLearned )
+//            printf( "Act = %.4f  ", Msat_ClauseReadActivity(pC) );
+        for ( i = 0; i < (int)pC->nSize; i++ )
+            printf(" "L_LIT, L_lit(pC->pData[i]));
+    }
+    printf( "\n" );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/msat/msatClauseVec.c b/src/sat/msat/msatClauseVec.c
new file mode 100644
index 00000000..04691cf2
--- /dev/null
+++ b/src/sat/msat/msatClauseVec.c
@@ -0,0 +1,232 @@
+/**CFile****************************************************************
+
+  FileName    [msatClauseVec.c]
+
+  PackageName [A C version of SAT solver MINISAT, originally developed 
+  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of 
+  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
+
+  Synopsis    [Procedures working with arrays of SAT clauses.]
+
+  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 1, 2004.]
+
+  Revision    [$Id: msatClauseVec.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "msatInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates a vector with the given capacity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Msat_ClauseVec_t * Msat_ClauseVecAlloc( int nCap )
+{
+    Msat_ClauseVec_t * p;
+    p = ALLOC( Msat_ClauseVec_t, 1 );
+    if ( nCap > 0 && nCap < 16 )
+        nCap = 16;
+    p->nSize  = 0;
+    p->nCap   = nCap;
+    p->pArray = p->nCap? ALLOC( Msat_Clause_t *, p->nCap ) : NULL;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_ClauseVecFree( Msat_ClauseVec_t * p )
+{
+    FREE( p->pArray );
+    FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Msat_Clause_t ** Msat_ClauseVecReadArray( Msat_ClauseVec_t * p )
+{
+    return p->pArray;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Msat_ClauseVecReadSize( Msat_ClauseVec_t * p )
+{
+    return p->nSize;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resizes the vector to the given capacity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_ClauseVecGrow( Msat_ClauseVec_t * p, int nCapMin )
+{
+    if ( p->nCap >= nCapMin )
+        return;
+    p->pArray = REALLOC( Msat_Clause_t *, p->pArray, nCapMin ); 
+    p->nCap   = nCapMin;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_ClauseVecShrink( Msat_ClauseVec_t * p, int nSizeNew )
+{
+    assert( p->nSize >= nSizeNew );
+    p->nSize = nSizeNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_ClauseVecClear( Msat_ClauseVec_t * p )
+{
+    p->nSize = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_ClauseVecPush( Msat_ClauseVec_t * p, Msat_Clause_t * Entry )
+{
+    if ( p->nSize == p->nCap )
+    {
+        if ( p->nCap < 16 )
+            Msat_ClauseVecGrow( p, 16 );
+        else
+            Msat_ClauseVecGrow( p, 2 * p->nCap );
+    }
+    p->pArray[p->nSize++] = Entry;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Msat_Clause_t * Msat_ClauseVecPop( Msat_ClauseVec_t * p )
+{
+    return p->pArray[--p->nSize];
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_ClauseVecWriteEntry( Msat_ClauseVec_t * p, int i, Msat_Clause_t * Entry )
+{
+    assert( i >= 0 && i < p->nSize );
+    p->pArray[i] = Entry;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Msat_Clause_t * Msat_ClauseVecReadEntry( Msat_ClauseVec_t * p, int i )
+{
+    assert( i >= 0 && i < p->nSize );
+    return p->pArray[i];
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/msat/msatInt.h b/src/sat/msat/msatInt.h
new file mode 100644
index 00000000..03903abe
--- /dev/null
+++ b/src/sat/msat/msatInt.h
@@ -0,0 +1,306 @@
+/**CFile****************************************************************
+
+  FileName    [msatInt.c]
+
+  PackageName [A C version of SAT solver MINISAT, originally developed 
+  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of 
+  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
+
+  Synopsis    [Internal definitions of the solver.]
+
+  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 1, 2004.]
+
+  Revision    [$Id: msatInt.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __MSAT_INT_H__
+#define __MSAT_INT_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+//#include "leaks.h"       
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+#include <time.h>
+#include <math.h>
+#include "msat.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    STRUCTURE DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+#ifdef _MSC_VER
+typedef __int64     int64;
+#else
+typedef long long   int64;
+#endif
+
+// outputs the runtime in seconds
+#define PRT(a,t) \
+    printf( "%s = ", (a) ); printf( "%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC) )
+
+// memory management macros
+#define ALLOC(type, num)    \
+    ((type *) malloc(sizeof(type) * (num)))
+#define REALLOC(type, obj, num)    \
+    ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
+        ((type *) malloc(sizeof(type) * (num))))
+#define FREE(obj)        \
+    ((obj) ? (free((char *)(obj)), (obj) = 0) : 0)
+
+// By default, custom memory management is used
+// which guarantees constant time allocation/deallocation 
+// for SAT clauses and other frequently modified objects.
+// For debugging, it is possible use system memory management
+// directly. In which case, uncomment the macro below.
+//#define USE_SYSTEM_MEMORY_MANAGEMENT 
+
+// internal data structures
+typedef struct Msat_Clause_t_      Msat_Clause_t;
+typedef struct Msat_Queue_t_       Msat_Queue_t;
+typedef struct Msat_Order_t_       Msat_Order_t;
+// memory managers (duplicated from Extra for stand-aloneness)
+typedef struct Msat_MmFixed_t_     Msat_MmFixed_t;    
+typedef struct Msat_MmFlex_t_      Msat_MmFlex_t;     
+typedef struct Msat_MmStep_t_      Msat_MmStep_t;     
+// variables and literals
+typedef int                       Msat_Lit_t;  
+typedef int                       Msat_Var_t;  
+// the type of return value
+#define MSAT_VAR_UNASSIGNED (-1)
+#define MSAT_LIT_UNASSIGNED (-2)
+#define MSAT_ORDER_UNKNOWN  (-3)
+
+// printing the search tree
+#define L_IND      "%-*d"
+#define L_ind      Msat_SolverReadDecisionLevel(p)*3+3,Msat_SolverReadDecisionLevel(p)
+#define L_LIT      "%s%d"
+#define L_lit(Lit) MSAT_LITSIGN(Lit)?"-":"", MSAT_LIT2VAR(Lit)+1
+
+typedef struct Msat_SolverStats_t_ Msat_SolverStats_t;
+struct Msat_SolverStats_t_
+{
+    int64   nStarts;        // the number of restarts
+    int64   nDecisions;     // the number of decisions
+    int64   nPropagations;  // the number of implications
+    int64   nInspects;      // the number of times clauses are vising while watching them
+    int64   nConflicts;     // the number of conflicts
+    int64   nSuccesses;     // the number of sat assignments found
+};
+
+typedef struct Msat_SearchParams_t_ Msat_SearchParams_t;
+struct Msat_SearchParams_t_
+{
+    double  dVarDecay;
+    double  dClaDecay;
+};
+
+// sat solver data structure visible through all the internal files
+struct Msat_Solver_t_
+{
+    int                 nClauses;    // the total number of clauses
+    int                 nClausesStart; // the number of clauses before adding
+    Msat_ClauseVec_t *  vClauses;    // problem clauses
+    Msat_ClauseVec_t *  vLearned;    // learned clauses
+    double              dClaInc;     // Amount to bump next clause with.
+    double              dClaDecay;   // INVERSE decay factor for clause activity: stores 1/decay.
+
+    double *            pdActivity;  // A heuristic measurement of the activity of a variable.
+    float *             pFactors;    // the multiplicative factors of variable activity
+    double              dVarInc;     // Amount to bump next variable with.
+    double              dVarDecay;   // INVERSE decay factor for variable activity: stores 1/decay. Use negative value for static variable order.
+    Msat_Order_t *      pOrder;      // Keeps track of the decision variable order.
+
+    Msat_ClauseVec_t ** pvWatched;   // 'pvWatched[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
+    Msat_Queue_t *      pQueue;      // Propagation queue.
+
+    int                 nVars;       // the current number of variables
+    int                 nVarsAlloc;  // the maximum allowed number of variables
+    int *               pAssigns;    // The current assignments (literals or MSAT_VAR_UNKOWN)
+    int *               pModel;      // The satisfying assignment
+    Msat_IntVec_t *     vTrail;      // List of assignments made. 
+    Msat_IntVec_t *     vTrailLim;   // Separator indices for different decision levels in 'trail'.
+    Msat_Clause_t **    pReasons;    // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none.
+    int *               pLevel;      // 'level[var]' is the decision level at which assignment was made. 
+    int                 nLevelRoot;  // Level of first proper decision.
+
+    double              dRandSeed;   // For the internal random number generator (makes solver deterministic over different platforms). 
+
+    bool                fVerbose;    // the verbosity flag
+    double              dProgress;   // Set by 'search()'.
+
+    // the variable cone and variable connectivity
+    Msat_IntVec_t *     vConeVars;
+    Msat_IntVec_t *     vVarsUsed;
+    Msat_ClauseVec_t *  vAdjacents;
+
+    // internal data used during conflict analysis
+    int *               pSeen;       // time when a lit was seen for the last time
+    int                 nSeenId;     // the id of current seeing
+    Msat_IntVec_t *     vReason;     // the temporary array of literals
+    Msat_IntVec_t *     vTemp;       // the temporary array of literals
+    int *               pFreq;       // the number of times each var participated in conflicts
+
+    // the memory manager
+    Msat_MmStep_t *     pMem;
+
+    // statistics
+    Msat_SolverStats_t  Stats;
+    int                 nTwoLits;
+    int                 nTwoLitsL;
+    int                 nClausesInit;
+    int                 nClausesAlloc;
+    int                 nClausesAllocL;
+    int                 nBackTracks;
+};
+
+struct Msat_ClauseVec_t_
+{
+    Msat_Clause_t **    pArray;
+    int                 nSize;
+    int                 nCap;
+};
+
+struct Msat_IntVec_t_
+{
+    int *               pArray;
+    int                 nSize;
+    int                 nCap;
+};
+
+////////////////////////////////////////////////////////////////////////
+///                       GLOBAL VARIABLES                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                       MACRO DEFINITIONS                          ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DECLARATIONS                        ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== satActivity.c ===========================================================*/
+extern void                Msat_SolverVarDecayActivity( Msat_Solver_t * p );
+extern void                Msat_SolverVarRescaleActivity( Msat_Solver_t * p );
+extern void                Msat_SolverClaDecayActivity( Msat_Solver_t * p );
+extern void                Msat_SolverClaRescaleActivity( Msat_Solver_t * p );
+/*=== satSolverApi.c ===========================================================*/
+extern Msat_Clause_t *     Msat_SolverReadClause( Msat_Solver_t * p, int Num );
+/*=== satSolver.c ===========================================================*/
+extern int                 Msat_SolverReadDecisionLevel( Msat_Solver_t * p );
+extern int *               Msat_SolverReadDecisionLevelArray( Msat_Solver_t * p );
+extern Msat_Clause_t **    Msat_SolverReadReasonArray( Msat_Solver_t * p );
+extern Msat_Type_t         Msat_SolverReadVarValue( Msat_Solver_t * p, Msat_Var_t Var );
+extern Msat_ClauseVec_t *  Msat_SolverReadLearned( Msat_Solver_t * p );
+extern Msat_ClauseVec_t ** Msat_SolverReadWatchedArray( Msat_Solver_t * p );
+extern int *               Msat_SolverReadSeenArray( Msat_Solver_t * p );
+extern int                 Msat_SolverIncrementSeenId( Msat_Solver_t * p );
+extern Msat_MmStep_t *     Msat_SolverReadMem( Msat_Solver_t * p );
+extern void                Msat_SolverClausesIncrement( Msat_Solver_t * p );
+extern void                Msat_SolverClausesDecrement( Msat_Solver_t * p );
+extern void                Msat_SolverClausesIncrementL( Msat_Solver_t * p );
+extern void                Msat_SolverClausesDecrementL( Msat_Solver_t * p );
+extern void                Msat_SolverVarBumpActivity( Msat_Solver_t * p, Msat_Lit_t Lit );
+extern void                Msat_SolverClaBumpActivity( Msat_Solver_t * p, Msat_Clause_t * pC );
+extern bool                Msat_SolverEnqueue( Msat_Solver_t * p, Msat_Lit_t Lit, Msat_Clause_t * pC );
+extern double              Msat_SolverProgressEstimate( Msat_Solver_t * p );
+/*=== satSolverSearch.c ===========================================================*/
+extern bool                Msat_SolverAssume( Msat_Solver_t * p, Msat_Lit_t Lit );
+extern Msat_Clause_t *     Msat_SolverPropagate( Msat_Solver_t * p );
+extern void                Msat_SolverCancelUntil( Msat_Solver_t * p, int Level );
+extern Msat_Type_t         Msat_SolverSearch( Msat_Solver_t * p, int nConfLimit, int nLearnedLimit, int nBackTrackLimit, Msat_SearchParams_t * pPars );
+/*=== satQueue.c ===========================================================*/
+extern Msat_Queue_t *      Msat_QueueAlloc( int nVars );
+extern void                Msat_QueueFree( Msat_Queue_t * p );
+extern int                 Msat_QueueReadSize( Msat_Queue_t * p );
+extern void                Msat_QueueInsert( Msat_Queue_t * p, int Lit );
+extern int                 Msat_QueueExtract( Msat_Queue_t * p );
+extern void                Msat_QueueClear( Msat_Queue_t * p );
+/*=== satOrder.c ===========================================================*/
+extern Msat_Order_t *      Msat_OrderAlloc( Msat_Solver_t * pSat );
+extern void                Msat_OrderSetBounds( Msat_Order_t * p, int nVarsMax );
+extern void                Msat_OrderClean( Msat_Order_t * p, Msat_IntVec_t * vCone );
+extern int                 Msat_OrderCheck( Msat_Order_t * p );
+extern void                Msat_OrderFree( Msat_Order_t * p );
+extern int                 Msat_OrderVarSelect( Msat_Order_t * p );
+extern void                Msat_OrderVarAssigned( Msat_Order_t * p, int Var );
+extern void                Msat_OrderVarUnassigned( Msat_Order_t * p, int Var );
+extern void                Msat_OrderUpdate( Msat_Order_t * p, int Var );
+/*=== satClause.c ===========================================================*/
+extern bool                Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearnt, Msat_Clause_t ** pClause_out );
+extern Msat_Clause_t *     Msat_ClauseCreateFake( Msat_Solver_t * p, Msat_IntVec_t * vLits );
+extern Msat_Clause_t *     Msat_ClauseCreateFakeLit( Msat_Solver_t * p, Msat_Lit_t Lit );
+extern bool                Msat_ClauseReadLearned( Msat_Clause_t * pC );
+extern int                 Msat_ClauseReadSize( Msat_Clause_t * pC );
+extern int *               Msat_ClauseReadLits( Msat_Clause_t * pC );
+extern bool                Msat_ClauseReadMark( Msat_Clause_t * pC );
+extern void                Msat_ClauseSetMark( Msat_Clause_t * pC, bool fMark );
+extern int                 Msat_ClauseReadNum( Msat_Clause_t * pC );
+extern void                Msat_ClauseSetNum( Msat_Clause_t * pC, int Num );
+extern bool                Msat_ClauseReadTypeA( Msat_Clause_t * pC );
+extern void                Msat_ClauseSetTypeA( Msat_Clause_t * pC, bool fTypeA );
+extern bool                Msat_ClauseIsLocked( Msat_Solver_t * p, Msat_Clause_t * pC );
+extern float               Msat_ClauseReadActivity( Msat_Clause_t * pC );
+extern void                Msat_ClauseWriteActivity( Msat_Clause_t * pC, float Num );
+extern void                Msat_ClauseFree( Msat_Solver_t * p, Msat_Clause_t * pC, bool fRemoveWatched );
+extern bool                Msat_ClausePropagate( Msat_Clause_t * pC, Msat_Lit_t Lit, int * pAssigns, Msat_Lit_t * pLit_out );
+extern bool                Msat_ClauseSimplify( Msat_Clause_t * pC, int * pAssigns );
+extern void                Msat_ClauseCalcReason( Msat_Solver_t * p, Msat_Clause_t * pC, Msat_Lit_t Lit, Msat_IntVec_t * vLits_out );
+extern void                Msat_ClauseRemoveWatch( Msat_ClauseVec_t * vClauses, Msat_Clause_t * pC );
+extern void                Msat_ClausePrint( Msat_Clause_t * pC );
+extern void                Msat_ClausePrintSymbols( Msat_Clause_t * pC );
+extern void                Msat_ClauseWriteDimacs( FILE * pFile, Msat_Clause_t * pC, bool fIncrement );
+extern unsigned            Msat_ClauseComputeTruth( Msat_Solver_t * p, Msat_Clause_t * pC );
+/*=== satSort.c ===========================================================*/
+extern void                Msat_SolverSortDB( Msat_Solver_t * p );
+/*=== satClauseVec.c ===========================================================*/
+extern Msat_ClauseVec_t *  Msat_ClauseVecAlloc( int nCap );
+extern void                Msat_ClauseVecFree( Msat_ClauseVec_t * p );
+extern Msat_Clause_t **    Msat_ClauseVecReadArray( Msat_ClauseVec_t * p );
+extern int                 Msat_ClauseVecReadSize( Msat_ClauseVec_t * p );
+extern void                Msat_ClauseVecGrow( Msat_ClauseVec_t * p, int nCapMin );
+extern void                Msat_ClauseVecShrink( Msat_ClauseVec_t * p, int nSizeNew );
+extern void                Msat_ClauseVecClear( Msat_ClauseVec_t * p );
+extern void                Msat_ClauseVecPush( Msat_ClauseVec_t * p, Msat_Clause_t * Entry );
+extern Msat_Clause_t *     Msat_ClauseVecPop( Msat_ClauseVec_t * p );
+extern void                Msat_ClauseVecWriteEntry( Msat_ClauseVec_t * p, int i, Msat_Clause_t * Entry );
+extern Msat_Clause_t *     Msat_ClauseVecReadEntry( Msat_ClauseVec_t * p, int i );
+
+/*=== satMem.c ===========================================================*/
+// fixed-size-block memory manager
+extern Msat_MmFixed_t *    Msat_MmFixedStart( int nEntrySize );
+extern void                Msat_MmFixedStop( Msat_MmFixed_t * p, int fVerbose );
+extern char *              Msat_MmFixedEntryFetch( Msat_MmFixed_t * p );
+extern void                Msat_MmFixedEntryRecycle( Msat_MmFixed_t * p, char * pEntry );
+extern void                Msat_MmFixedRestart( Msat_MmFixed_t * p );
+extern int                 Msat_MmFixedReadMemUsage( Msat_MmFixed_t * p );
+// flexible-size-block memory manager
+extern Msat_MmFlex_t *     Msat_MmFlexStart();
+extern void                Msat_MmFlexStop( Msat_MmFlex_t * p, int fVerbose );
+extern char *              Msat_MmFlexEntryFetch( Msat_MmFlex_t * p, int nBytes );
+extern int                 Msat_MmFlexReadMemUsage( Msat_MmFlex_t * p );
+// hierarchical memory manager
+extern Msat_MmStep_t *     Msat_MmStepStart( int nSteps );
+extern void                Msat_MmStepStop( Msat_MmStep_t * p, int fVerbose );
+extern char *              Msat_MmStepEntryFetch( Msat_MmStep_t * p, int nBytes );
+extern void                Msat_MmStepEntryRecycle( Msat_MmStep_t * p, char * pEntry, int nBytes );
+extern int                 Msat_MmStepReadMemUsage( Msat_MmStep_t * p );
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+#endif
diff --git a/src/sat/msat/msatMem.c b/src/sat/msat/msatMem.c
new file mode 100644
index 00000000..30bf4a96
--- /dev/null
+++ b/src/sat/msat/msatMem.c
@@ -0,0 +1,529 @@
+/**CFile****************************************************************
+
+  FileName    [msatMem.c]
+
+  PackageName [A C version of SAT solver MINISAT, originally developed 
+  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of 
+  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
+
+  Synopsis    [Memory managers borrowed from Extra.]
+
+  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 1, 2004.]
+
+  Revision    [$Id: msatMem.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "msatInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+struct Msat_MmFixed_t_
+{
+    // information about individual entries
+    int           nEntrySize;    // the size of one entry
+    int           nEntriesAlloc; // the total number of entries allocated
+    int           nEntriesUsed;  // the number of entries in use
+    int           nEntriesMax;   // the max number of entries in use
+    char *        pEntriesFree;  // the linked list of free entries
+
+    // this is where the memory is stored
+    int           nChunkSize;    // the size of one chunk
+    int           nChunksAlloc;  // the maximum number of memory chunks 
+    int           nChunks;       // the current number of memory chunks 
+    char **       pChunks;       // the allocated memory
+
+    // statistics
+    int           nMemoryUsed;   // memory used in the allocated entries
+    int           nMemoryAlloc;  // memory allocated
+};
+
+struct Msat_MmFlex_t_
+{
+    // information about individual entries
+    int           nEntriesUsed;  // the number of entries allocated
+    char *        pCurrent;      // the current pointer to free memory
+    char *        pEnd;          // the first entry outside the free memory
+
+    // this is where the memory is stored
+    int           nChunkSize;    // the size of one chunk
+    int           nChunksAlloc;  // the maximum number of memory chunks 
+    int           nChunks;       // the current number of memory chunks 
+    char **       pChunks;       // the allocated memory
+
+    // statistics
+    int           nMemoryUsed;   // memory used in the allocated entries
+    int           nMemoryAlloc;  // memory allocated
+};
+
+
+struct Msat_MmStep_t_
+{
+    int                nMems;    // the number of fixed memory managers employed
+    Msat_MmFixed_t **   pMems;    // memory managers: 2^1 words, 2^2 words, etc
+    int                nMapSize; // the size of the memory array
+    Msat_MmFixed_t **   pMap;     // maps the number of bytes into its memory manager
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates memory pieces of fixed size.]
+
+  Description [The size of the chunk is computed as the minimum of
+  1024 entries and 64K. Can only work with entry size at least 4 byte long.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Msat_MmFixed_t * Msat_MmFixedStart( int nEntrySize )
+{
+    Msat_MmFixed_t * p;
+
+    p = ALLOC( Msat_MmFixed_t, 1 );
+    memset( p, 0, sizeof(Msat_MmFixed_t) );
+
+    p->nEntrySize    = nEntrySize;
+    p->nEntriesAlloc = 0;
+    p->nEntriesUsed  = 0;
+    p->pEntriesFree  = NULL;
+
+    if ( nEntrySize * (1 << 10) < (1<<16) )
+        p->nChunkSize = (1 << 10);
+    else
+        p->nChunkSize = (1<<16) / nEntrySize;
+    if ( p->nChunkSize < 8 )
+        p->nChunkSize = 8;
+
+    p->nChunksAlloc  = 64;
+    p->nChunks       = 0;
+    p->pChunks       = ALLOC( char *, p->nChunksAlloc );
+
+    p->nMemoryUsed   = 0;
+    p->nMemoryAlloc  = 0;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_MmFixedStop( Msat_MmFixed_t * p, int fVerbose )
+{
+    int i;
+    if ( p == NULL )
+        return;
+    if ( fVerbose )
+    {
+        printf( "Fixed memory manager: Entry = %5d. Chunk = %5d. Chunks used = %5d.\n",
+            p->nEntrySize, p->nChunkSize, p->nChunks );
+        printf( "   Entries used = %8d. Entries peak = %8d. Memory used = %8d. Memory alloc = %8d.\n",
+            p->nEntriesUsed, p->nEntriesMax, p->nEntrySize * p->nEntriesUsed, p->nMemoryAlloc );
+    }
+    for ( i = 0; i < p->nChunks; i++ )
+        free( p->pChunks[i] );
+    free( p->pChunks );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Msat_MmFixedEntryFetch( Msat_MmFixed_t * p )
+{
+    char * pTemp;
+    int i;
+
+    // check if there are still free entries
+    if ( p->nEntriesUsed == p->nEntriesAlloc )
+    { // need to allocate more entries
+        assert( p->pEntriesFree == NULL );
+        if ( p->nChunks == p->nChunksAlloc )
+        {
+            p->nChunksAlloc *= 2;
+            p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); 
+        }
+        p->pEntriesFree = ALLOC( char, p->nEntrySize * p->nChunkSize );
+        p->nMemoryAlloc += p->nEntrySize * p->nChunkSize;
+        // transform these entries into a linked list
+        pTemp = p->pEntriesFree;
+        for ( i = 1; i < p->nChunkSize; i++ )
+        {
+            *((char **)pTemp) = pTemp + p->nEntrySize;
+            pTemp += p->nEntrySize;
+        }
+        // set the last link
+        *((char **)pTemp) = NULL;
+        // add the chunk to the chunk storage
+        p->pChunks[ p->nChunks++ ] = p->pEntriesFree;
+        // add to the number of entries allocated
+        p->nEntriesAlloc += p->nChunkSize;
+    }
+    // incrememt the counter of used entries
+    p->nEntriesUsed++;
+    if ( p->nEntriesMax < p->nEntriesUsed )
+        p->nEntriesMax = p->nEntriesUsed;
+    // return the first entry in the free entry list
+    pTemp = p->pEntriesFree;
+    p->pEntriesFree = *((char **)pTemp);
+    return pTemp;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_MmFixedEntryRecycle( Msat_MmFixed_t * p, char * pEntry )
+{
+    // decrement the counter of used entries
+    p->nEntriesUsed--;
+    // add the entry to the linked list of free entries
+    *((char **)pEntry) = p->pEntriesFree;
+    p->pEntriesFree = pEntry;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description [Relocates all the memory except the first chunk.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_MmFixedRestart( Msat_MmFixed_t * p )
+{
+    int i;
+    char * pTemp;
+
+    // deallocate all chunks except the first one
+    for ( i = 1; i < p->nChunks; i++ )
+        free( p->pChunks[i] );
+    p->nChunks = 1;
+    // transform these entries into a linked list
+    pTemp = p->pChunks[0];
+    for ( i = 1; i < p->nChunkSize; i++ )
+    {
+        *((char **)pTemp) = pTemp + p->nEntrySize;
+        pTemp += p->nEntrySize;
+    }
+    // set the last link
+    *((char **)pTemp) = NULL;
+    // set the free entry list
+    p->pEntriesFree  = p->pChunks[0];
+    // set the correct statistics
+    p->nMemoryAlloc  = p->nEntrySize * p->nChunkSize;
+    p->nMemoryUsed   = 0;
+    p->nEntriesAlloc = p->nChunkSize;
+    p->nEntriesUsed  = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Msat_MmFixedReadMemUsage( Msat_MmFixed_t * p )
+{
+    return p->nMemoryAlloc;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates entries of flexible size.]
+
+  Description [Can only work with entry size at least 4 byte long.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Msat_MmFlex_t * Msat_MmFlexStart()
+{
+    Msat_MmFlex_t * p;
+
+    p = ALLOC( Msat_MmFlex_t, 1 );
+    memset( p, 0, sizeof(Msat_MmFlex_t) );
+
+    p->nEntriesUsed  = 0;
+    p->pCurrent      = NULL;
+    p->pEnd          = NULL;
+
+    p->nChunkSize    = (1 << 12);
+    p->nChunksAlloc  = 64;
+    p->nChunks       = 0;
+    p->pChunks       = ALLOC( char *, p->nChunksAlloc );
+
+    p->nMemoryUsed   = 0;
+    p->nMemoryAlloc  = 0;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_MmFlexStop( Msat_MmFlex_t * p, int fVerbose )
+{
+    int i;
+    if ( p == NULL )
+        return;
+    if ( fVerbose )
+    {
+        printf( "Flexible memory manager: Chunk size = %d. Chunks used = %d.\n",
+            p->nChunkSize, p->nChunks );
+        printf( "   Entries used = %d. Memory used = %d. Memory alloc = %d.\n",
+            p->nEntriesUsed, p->nMemoryUsed, p->nMemoryAlloc );
+    }
+    for ( i = 0; i < p->nChunks; i++ )
+        free( p->pChunks[i] );
+    free( p->pChunks );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Msat_MmFlexEntryFetch( Msat_MmFlex_t * p, int nBytes )
+{
+    char * pTemp;
+    // check if there are still free entries
+    if ( p->pCurrent == NULL || p->pCurrent + nBytes > p->pEnd )
+    { // need to allocate more entries
+        if ( p->nChunks == p->nChunksAlloc )
+        {
+            p->nChunksAlloc *= 2;
+            p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); 
+        }
+        if ( nBytes > p->nChunkSize )
+        {
+            // resize the chunk size if more memory is requested than it can give
+            // (ideally, this should never happen)
+            p->nChunkSize = 2 * nBytes;
+        }
+        p->pCurrent = ALLOC( char, p->nChunkSize );
+        p->pEnd     = p->pCurrent + p->nChunkSize;
+        p->nMemoryAlloc += p->nChunkSize;
+        // add the chunk to the chunk storage
+        p->pChunks[ p->nChunks++ ] = p->pCurrent;
+    }
+    assert( p->pCurrent + nBytes <= p->pEnd );
+    // increment the counter of used entries
+    p->nEntriesUsed++;
+    // keep track of the memory used
+    p->nMemoryUsed += nBytes;
+    // return the next entry
+    pTemp = p->pCurrent;
+    p->pCurrent += nBytes;
+    return pTemp;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Msat_MmFlexReadMemUsage( Msat_MmFlex_t * p )
+{
+    return p->nMemoryAlloc;
+}
+
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the hierarchical memory manager.]
+
+  Description [This manager can allocate entries of any size.
+  Iternally they are mapped into the entries with the number of bytes
+  equal to the power of 2. The smallest entry size is 8 bytes. The
+  next one is 16 bytes etc. So, if the user requests 6 bytes, he gets 
+  8 byte entry. If we asks for 25 bytes, he gets 32 byte entry etc.
+  The input parameters "nSteps" says how many fixed memory managers
+  are employed internally. Calling this procedure with nSteps equal
+  to 10 results in 10 hierarchically arranged internal memory managers, 
+  which can allocate up to 4096 (1Kb) entries. Requests for larger 
+  entries are handed over to malloc() and then free()ed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Msat_MmStep_t * Msat_MmStepStart( int nSteps )
+{
+    Msat_MmStep_t * p;
+    int i, k;
+    p = ALLOC( Msat_MmStep_t, 1 );
+    p->nMems = nSteps;
+    // start the fixed memory managers
+    p->pMems = ALLOC( Msat_MmFixed_t *, p->nMems );
+    for ( i = 0; i < p->nMems; i++ )
+        p->pMems[i] = Msat_MmFixedStart( (8<<i) );
+    // set up the mapping of the required memory size into the corresponding manager
+    p->nMapSize = (4<<p->nMems);
+    p->pMap = ALLOC( Msat_MmFixed_t *, p->nMapSize+1 );
+    p->pMap[0] = NULL;
+    for ( k = 1; k <= 4; k++ )
+        p->pMap[k] = p->pMems[0];
+    for ( i = 0; i < p->nMems; i++ )
+        for ( k = (4<<i)+1; k <= (8<<i); k++ )
+            p->pMap[k] = p->pMems[i];
+//for ( i = 1; i < 100; i ++ )
+//printf( "%10d: size = %10d\n", i, p->pMap[i]->nEntrySize );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the memory manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_MmStepStop( Msat_MmStep_t * p, int fVerbose )
+{
+    int i;
+    for ( i = 0; i < p->nMems; i++ )
+        Msat_MmFixedStop( p->pMems[i], fVerbose );
+    free( p->pMems );
+    free( p->pMap );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the entry.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Msat_MmStepEntryFetch( Msat_MmStep_t * p, int nBytes )
+{
+    if ( nBytes == 0 )
+        return NULL;
+    if ( nBytes > p->nMapSize )
+    {
+//        printf( "Allocating %d bytes.\n", nBytes );
+        return ALLOC( char, nBytes );
+    }
+    return Msat_MmFixedEntryFetch( p->pMap[nBytes] );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Recycles the entry.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_MmStepEntryRecycle( Msat_MmStep_t * p, char * pEntry, int nBytes )
+{
+    if ( nBytes == 0 )
+        return;
+    if ( nBytes > p->nMapSize )
+    {
+        free( pEntry );
+        return;
+    }
+    Msat_MmFixedEntryRecycle( p->pMap[nBytes], pEntry );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Msat_MmStepReadMemUsage( Msat_MmStep_t * p )
+{
+    int i, nMemTotal = 0;
+    for ( i = 0; i < p->nMems; i++ )
+        nMemTotal += p->pMems[i]->nMemoryAlloc;
+    return nMemTotal;
+}
diff --git a/src/sat/msat/msatOrderH.c b/src/sat/msat/msatOrderH.c
new file mode 100644
index 00000000..956e7fc6
--- /dev/null
+++ b/src/sat/msat/msatOrderH.c
@@ -0,0 +1,405 @@
+/**CFile****************************************************************
+
+  FileName    [msatOrder.c]
+
+  PackageName [A C version of SAT solver MINISAT, originally developed 
+  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of 
+  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
+
+  Synopsis    [The manager of variable assignment.]
+
+  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 1, 2004.]
+
+  Revision    [$Id: msatOrder.c,v 1.0 2005/05/30 1:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "msatInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// the variable package data structure
+struct Msat_Order_t_
+{
+    Msat_Solver_t *      pSat;         // the SAT solver 
+    Msat_IntVec_t *      vIndex;       // the heap
+    Msat_IntVec_t *      vHeap;        // the mapping of var num into its heap num
+};
+
+//The solver can communicate to the variable order the following parts:
+//- the array of current assignments (pSat->pAssigns)
+//- the array of variable activities (pSat->pdActivity)
+//- the array of variables currently in the cone (pSat->vConeVars)
+//- the array of arrays of variables adjucent to each(pSat->vAdjacents)
+
+#define HLEFT(i)               ((i)<<1)
+#define HRIGHT(i)             (((i)<<1)+1)
+#define HPARENT(i)             ((i)>>1)
+#define HCOMPARE(p, i, j)      ((p)->pSat->pdActivity[i] > (p)->pSat->pdActivity[j])
+#define HHEAP(p, i)            ((p)->vHeap->pArray[i])
+#define HSIZE(p)               ((p)->vHeap->nSize)
+#define HOKAY(p, i)            ((i) >= 0 && (i) < (p)->vIndex->nSize)
+#define HINHEAP(p, i)          (HOKAY(p, i) && (p)->vIndex->pArray[i] != 0)
+#define HEMPTY(p)              (HSIZE(p) == 1)
+
+static int Msat_HeapCheck_rec( Msat_Order_t * p, int i );
+static int Msat_HeapGetTop( Msat_Order_t * p );
+static void Msat_HeapInsert( Msat_Order_t * p, int n );
+static void Msat_HeapIncrease( Msat_Order_t * p, int n );
+static void Msat_HeapPercolateUp( Msat_Order_t * p, int i );
+static void Msat_HeapPercolateDown( Msat_Order_t * p, int i );
+
+extern int timeSelect;
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates the ordering structure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Msat_Order_t * Msat_OrderAlloc( Msat_Solver_t * pSat )
+{
+    Msat_Order_t * p;
+    p = ALLOC( Msat_Order_t, 1 );
+    memset( p, 0, sizeof(Msat_Order_t) );
+    p->pSat   = pSat;
+    p->vIndex = Msat_IntVecAlloc( 0 );
+    p->vHeap  = Msat_IntVecAlloc( 0 );
+    Msat_OrderSetBounds( p, pSat->nVarsAlloc );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the bound of the ordering structure.]
+
+  Description [Should be called whenever the SAT solver is resized.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_OrderSetBounds( Msat_Order_t * p, int nVarsMax )
+{
+    Msat_IntVecGrow( p->vIndex, nVarsMax );
+    Msat_IntVecGrow( p->vHeap, nVarsMax + 1 );
+    p->vIndex->nSize = nVarsMax;
+    p->vHeap->nSize = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Cleans the ordering structure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_OrderClean( Msat_Order_t * p, Msat_IntVec_t * vCone )
+{
+    int i;
+    for ( i = 0; i < p->vIndex->nSize; i++ )
+        p->vIndex->pArray[i] = 0;
+    for ( i = 0; i < vCone->nSize; i++ )
+    {
+        assert( i+1 < p->vHeap->nCap );
+        p->vHeap->pArray[i+1] = vCone->pArray[i];
+
+        assert( vCone->pArray[i] < p->vIndex->nSize );
+        p->vIndex->pArray[vCone->pArray[i]] = i+1;
+    }
+    p->vHeap->nSize = vCone->nSize + 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks that the J-boundary is okay.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Msat_OrderCheck( Msat_Order_t * p )
+{
+    return Msat_HeapCheck_rec( p, 1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the ordering structure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_OrderFree( Msat_Order_t * p )
+{
+    Msat_IntVecFree( p->vHeap );
+    Msat_IntVecFree( p->vIndex );
+    free( p );
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Selects the next variable to assign.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Msat_OrderVarSelect( Msat_Order_t * p )
+{
+    // Activity based decision:
+//    while (!heap.empty()){
+//        Var next = heap.getmin();
+//        if (toLbool(assigns[next]) == l_Undef)
+//            return next;
+//    }
+//    return var_Undef;
+
+    int Var;
+    int clk = clock();
+
+    while ( !HEMPTY(p) )
+    {
+        Var = Msat_HeapGetTop(p);
+        if ( (p)->pSat->pAssigns[Var] == MSAT_VAR_UNASSIGNED )
+        {
+//assert( Msat_OrderCheck(p) );
+timeSelect += clock() - clk;
+            return Var;
+        }
+    }
+    return MSAT_ORDER_UNKNOWN;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates J-boundary when the variable is assigned.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_OrderVarAssigned( Msat_Order_t * p, int Var )
+{
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates the order after a variable is unassigned.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_OrderVarUnassigned( Msat_Order_t * p, int Var )
+{
+//    if (!heap.inHeap(x))
+//        heap.insert(x);
+
+    int clk = clock();
+    if ( !HINHEAP(p,Var) )
+        Msat_HeapInsert( p, Var );
+timeSelect += clock() - clk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates the order after a variable changed weight.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_OrderUpdate( Msat_Order_t * p, int Var )
+{
+//    if (heap.inHeap(x))
+//        heap.increase(x);
+
+    int clk = clock();
+    if ( HINHEAP(p,Var) )
+        Msat_HeapIncrease( p, Var );
+timeSelect += clock() - clk;
+}
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Checks the heap property recursively.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Msat_HeapCheck_rec( Msat_Order_t * p, int i )
+{
+    return i >= HSIZE(p) ||
+        ( HPARENT(i) == 0 || !HCOMPARE(p, HHEAP(p, i), HHEAP(p, HPARENT(i))) ) &&
+        Msat_HeapCheck_rec( p, HLEFT(i) ) && Msat_HeapCheck_rec( p, HRIGHT(i) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Retrieves the minimum element.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Msat_HeapGetTop( Msat_Order_t * p )
+{
+    int Result, NewTop;
+    Result                    = HHEAP(p, 1);
+    NewTop                    = Msat_IntVecPop( p->vHeap );
+    p->vHeap->pArray[1]       = NewTop;
+    p->vIndex->pArray[NewTop] = 1;
+    p->vIndex->pArray[Result] = 0;
+    if ( p->vHeap->nSize > 1 )
+        Msat_HeapPercolateDown( p, 1 );
+    return Result;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts the new element.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_HeapInsert( Msat_Order_t * p, int n )
+{
+    assert( HOKAY(p, n) );
+    p->vIndex->pArray[n] = HSIZE(p);
+    Msat_IntVecPush( p->vHeap, n );
+    Msat_HeapPercolateUp( p, p->vIndex->pArray[n] );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts the new element.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_HeapIncrease( Msat_Order_t * p, int n )
+{
+    Msat_HeapPercolateUp( p, p->vIndex->pArray[n] );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Moves the entry up.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_HeapPercolateUp( Msat_Order_t * p, int i )
+{
+    int x = HHEAP(p, i);
+    while ( HPARENT(i) != 0 && HCOMPARE(p, x, HHEAP(p, HPARENT(i))) )
+    {
+        p->vHeap->pArray[i]            = HHEAP(p, HPARENT(i));
+        p->vIndex->pArray[HHEAP(p, i)] = i;
+        i                              = HPARENT(i);
+    }
+    p->vHeap->pArray[i]  = x;
+    p->vIndex->pArray[x] = i;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Moves the entry down.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_HeapPercolateDown( Msat_Order_t * p, int i )
+{
+    int x = HHEAP(p, i);
+    int Child;
+    while ( HLEFT(i) < HSIZE(p) )
+    {
+        if ( HRIGHT(i) < HSIZE(p) && HCOMPARE(p, HHEAP(p, HRIGHT(i)), HHEAP(p, HLEFT(i))) )
+            Child = HRIGHT(i);
+        else
+            Child = HLEFT(i);
+        if ( !HCOMPARE(p, HHEAP(p, Child), x) )
+            break;
+        p->vHeap->pArray[i]            = HHEAP(p, Child);
+        p->vIndex->pArray[HHEAP(p, i)] = i;
+        i                              = Child;
+    }
+    p->vHeap->pArray[i]  = x;
+    p->vIndex->pArray[x] = i;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/msat/msatOrderJ.c b/src/sat/msat/msatOrderJ.c
new file mode 100644
index 00000000..4db7ff7b
--- /dev/null
+++ b/src/sat/msat/msatOrderJ.c
@@ -0,0 +1,472 @@
+/**CFile****************************************************************
+
+  FileName    [msatOrder.c]
+
+  PackageName [A C version of SAT solver MINISAT, originally developed 
+  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of 
+  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
+
+  Synopsis    [The manager of variable assignment.]
+
+  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 1, 2004.]
+
+  Revision    [$Id: msatOrder.c,v 1.0 2005/05/30 1:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "msatInt.h"
+
+/* 
+The J-boundary (justification boundary) is defined as a set of unassigned 
+variables belonging to the cone of interest, such that for each of them,
+there exist an adjacent assigned variable in the cone of interest.
+*/
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Msat_OrderVar_t_  Msat_OrderVar_t;
+typedef struct Msat_OrderRing_t_ Msat_OrderRing_t;
+
+// the variable data structure
+struct Msat_OrderVar_t_
+{
+    Msat_OrderVar_t    * pNext;
+    Msat_OrderVar_t    * pPrev;
+    int                  Num;
+};
+
+// the ring of variables data structure (J-boundary)
+struct Msat_OrderRing_t_
+{
+    Msat_OrderVar_t    * pRoot; 
+    int                 nItems;
+};
+
+// the variable package data structure
+struct Msat_Order_t_
+{
+    Msat_Solver_t *      pSat;         // the SAT solver 
+    Msat_OrderVar_t *    pVars;        // the storage for variables
+    int                 nVarsAlloc;   // the number of variables allocated
+    Msat_OrderRing_t     rVars;        // the J-boundary as a ring of variables
+};
+
+//The solver can communicate to the variable order the following parts:
+//- the array of current assignments (pSat->pAssigns)
+//- the array of variable activities (pSat->pdActivity)
+//- the array of variables currently in the cone (pSat->vConeVars)
+//- the array of arrays of variables adjucent to each(pSat->vAdjacents)
+
+#define Msat_OrderVarIsInBoundary( p, i )   ((p)->pVars[i].pNext)
+#define Msat_OrderVarIsAssigned( p, i )     ((p)->pSat->pAssigns[i] != MSAT_VAR_UNASSIGNED)
+#define Msat_OrderVarIsUsedInCone( p, i )   ((p)->pSat->vVarsUsed->pArray[i])
+
+// iterator through the entries in J-boundary
+#define Msat_OrderRingForEachEntry( pRing, pVar, pNext )         \
+    for ( pVar = pRing,                                         \
+          pNext = pVar? pVar->pNext : NULL;                     \
+          pVar;                                                 \
+          pVar = (pNext != pRing)? pNext : NULL,                \
+          pNext = pVar? pVar->pNext : NULL )
+
+static void Msat_OrderRingAddLast( Msat_OrderRing_t * pRing, Msat_OrderVar_t * pVar );
+static void Msat_OrderRingRemove( Msat_OrderRing_t * pRing, Msat_OrderVar_t * pVar );
+
+extern int timeSelect;
+extern int timeAssign;
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates the ordering structure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Msat_Order_t * Msat_OrderAlloc( Msat_Solver_t * pSat )
+{
+    Msat_Order_t * p;
+    p = ALLOC( Msat_Order_t, 1 );
+    memset( p, 0, sizeof(Msat_Order_t) );
+    p->pSat = pSat;
+    Msat_OrderSetBounds( p, pSat->nVarsAlloc );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the bound of the ordering structure.]
+
+  Description [Should be called whenever the SAT solver is resized.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_OrderSetBounds( Msat_Order_t * p, int nVarsMax )
+{
+    int i;
+    // add variables if they are missing
+    if ( p->nVarsAlloc < nVarsMax )
+    {
+        p->pVars = REALLOC( Msat_OrderVar_t, p->pVars, nVarsMax );
+        for ( i = p->nVarsAlloc; i < nVarsMax; i++ )
+        {
+            p->pVars[i].pNext = p->pVars[i].pPrev = NULL;
+            p->pVars[i].Num = i;
+        }
+        p->nVarsAlloc = nVarsMax;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Cleans the ordering structure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_OrderClean( Msat_Order_t * p, Msat_IntVec_t * vCone )
+{
+    Msat_OrderVar_t * pVar, * pNext;
+    // quickly undo the ring
+    Msat_OrderRingForEachEntry( p->rVars.pRoot, pVar, pNext )
+        pVar->pNext = pVar->pPrev = NULL;
+    p->rVars.pRoot  = NULL;
+    p->rVars.nItems = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks that the J-boundary is okay.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Msat_OrderCheck( Msat_Order_t * p )
+{
+    Msat_OrderVar_t * pVar, * pNext;
+    Msat_IntVec_t * vRound;
+    int * pRound, nRound;
+    int * pVars, nVars, i, k;
+    int Counter = 0;
+
+    // go through all the variables in the boundary
+    Msat_OrderRingForEachEntry( p->rVars.pRoot, pVar, pNext )
+    {
+        assert( !Msat_OrderVarIsAssigned(p, pVar->Num) );
+        // go though all the variables in the neighborhood
+        // and check that it is true that there is least one assigned
+        vRound = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( p->pSat->vAdjacents, pVar->Num );
+        nRound = Msat_IntVecReadSize( vRound );
+        pRound = Msat_IntVecReadArray( vRound );
+        for ( i = 0; i < nRound; i++ )
+        {
+            if ( !Msat_OrderVarIsUsedInCone(p, pRound[i]) )
+                continue;
+            if ( Msat_OrderVarIsAssigned(p, pRound[i]) )
+                break;
+        }
+//        assert( i != nRound );
+//        if ( i == nRound )
+//            return 0;
+        if ( i == nRound )
+            Counter++;
+    }
+    if ( Counter > 0 )
+        printf( "%d(%d) ", Counter, p->rVars.nItems );
+
+    // we may also check other unassigned variables in the cone
+    // to make sure that if they are not in J-boundary, 
+    // then they do not have an assigned neighbor
+    nVars = Msat_IntVecReadSize( p->pSat->vConeVars );
+    pVars = Msat_IntVecReadArray( p->pSat->vConeVars );
+    for ( i = 0; i < nVars; i++ )
+    {
+        assert( Msat_OrderVarIsUsedInCone(p, pVars[i]) );
+        // skip assigned vars, vars in the boundary, and vars not used in the cone
+        if ( Msat_OrderVarIsAssigned(p, pVars[i]) || 
+             Msat_OrderVarIsInBoundary(p, pVars[i]) )
+            continue;
+        // make sure, it does not have assigned neighbors
+        vRound = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( p->pSat->vAdjacents, pVars[i] );
+        nRound = Msat_IntVecReadSize( vRound );
+        pRound = Msat_IntVecReadArray( vRound );
+        for ( k = 0; k < nRound; k++ )
+        {
+            if ( !Msat_OrderVarIsUsedInCone(p, pRound[k]) )
+                continue;
+            if ( Msat_OrderVarIsAssigned(p, pRound[k]) )
+                break;
+        }
+//        assert( k == nRound );
+//        if ( k != nRound )
+//            return 0;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the ordering structure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_OrderFree( Msat_Order_t * p )
+{
+    free( p->pVars );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Selects the next variable to assign.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Msat_OrderVarSelect( Msat_Order_t * p )
+{
+    Msat_OrderVar_t * pVar, * pNext, * pVarBest;
+    double * pdActs = p->pSat->pdActivity;
+    double dfActBest;
+//    int clk = clock();
+
+    pVarBest = NULL;
+    dfActBest = -1.0;
+    Msat_OrderRingForEachEntry( p->rVars.pRoot, pVar, pNext )
+    {
+        if ( dfActBest < pdActs[pVar->Num] )
+        {
+            dfActBest = pdActs[pVar->Num];
+            pVarBest  = pVar;
+        }
+    }
+//timeSelect += clock() - clk;
+//timeAssign += clock() - clk;
+
+//if ( pVarBest && pVarBest->Num % 1000 == 0 )
+//printf( "%d ", p->rVars.nItems );
+
+//    Msat_OrderCheck( p );
+    if ( pVarBest )
+    {
+        assert( Msat_OrderVarIsUsedInCone(p, pVarBest->Num) );
+        return pVarBest->Num;
+    }
+    return MSAT_ORDER_UNKNOWN;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates J-boundary when the variable is assigned.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_OrderVarAssigned( Msat_Order_t * p, int Var )
+{
+    Msat_IntVec_t * vRound;
+    int i;//, clk = clock();
+
+    // make sure the variable is in the boundary
+    assert( Var < p->nVarsAlloc );
+    // if it is not in the boundary (initial decision, random decision), do not remove
+    if ( Msat_OrderVarIsInBoundary( p, Var ) )
+        Msat_OrderRingRemove( &p->rVars, &p->pVars[Var] );
+    // add to the boundary those neighbors that are (1) unassigned, (2) not in boundary
+    // because for them we know that there is a variable (Var) which is assigned
+    vRound = (Msat_IntVec_t *)p->pSat->vAdjacents->pArray[Var];
+    for ( i = 0; i < vRound->nSize; i++ )
+    {
+        if ( !Msat_OrderVarIsUsedInCone(p, vRound->pArray[i]) )
+            continue;
+        if ( Msat_OrderVarIsAssigned(p, vRound->pArray[i]) )
+            continue;
+        if ( Msat_OrderVarIsInBoundary(p, vRound->pArray[i]) )
+            continue;
+        Msat_OrderRingAddLast( &p->rVars, &p->pVars[vRound->pArray[i]] );
+    }
+//timeSelect += clock() - clk;
+//    Msat_OrderCheck( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates the order after a variable is unassigned.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_OrderVarUnassigned( Msat_Order_t * p, int Var )
+{
+    Msat_IntVec_t * vRound, * vRound2;
+    int i, k;//, clk = clock();
+
+    // make sure the variable is not in the boundary
+    assert( Var < p->nVarsAlloc );
+    assert( !Msat_OrderVarIsInBoundary( p, Var ) );
+    // go through its neigbors - if one of them is assigned add this var
+    // add to the boundary those neighbors that are not there already
+    // this will also get rid of variable outside of the current cone
+    // because they are unassigned in Msat_SolverPrepare()
+    vRound = (Msat_IntVec_t *)p->pSat->vAdjacents->pArray[Var];
+    for ( i = 0; i < vRound->nSize; i++ )
+        if ( Msat_OrderVarIsAssigned(p, vRound->pArray[i]) ) 
+            break;
+    if ( i != vRound->nSize )
+        Msat_OrderRingAddLast( &p->rVars, &p->pVars[Var] );
+
+    // unassigning a variable may lead to its adjacents dropping from the boundary
+    for ( i = 0; i < vRound->nSize; i++ )
+        if ( Msat_OrderVarIsInBoundary(p, vRound->pArray[i]) )
+        { // the neighbor is in the J-boundary (and unassigned)
+            assert( !Msat_OrderVarIsAssigned(p, vRound->pArray[i]) );
+            vRound2 = (Msat_IntVec_t *)p->pSat->vAdjacents->pArray[vRound->pArray[i]];
+            // go through its neighbors and determine if there is at least one assigned
+            for ( k = 0; k < vRound2->nSize; k++ )
+                if ( Msat_OrderVarIsAssigned(p, vRound2->pArray[k]) ) 
+                    break;
+            if ( k == vRound2->nSize ) // there is no assigned vars, delete this one
+                Msat_OrderRingRemove( &p->rVars, &p->pVars[vRound->pArray[i]] );
+        }
+//timeSelect += clock() - clk;
+//    Msat_OrderCheck( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates the order after a variable changed weight.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_OrderUpdate( Msat_Order_t * p, int Var )
+{
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Adds node to the end of the ring.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_OrderRingAddLast( Msat_OrderRing_t * pRing, Msat_OrderVar_t * pVar )
+{
+//printf( "adding %d\n", pVar->Num );
+    // check that the node is not in a ring
+    assert( pVar->pPrev == NULL );
+    assert( pVar->pNext == NULL );
+    // if the ring is empty, make the node point to itself
+    pRing->nItems++;
+    if ( pRing->pRoot == NULL )
+    {
+        pRing->pRoot  = pVar;
+        pVar->pPrev  = pVar;
+        pVar->pNext  = pVar;
+        return;
+    }
+    // if the ring is not empty, add it as the last entry
+    pVar->pPrev = pRing->pRoot->pPrev;
+    pVar->pNext = pRing->pRoot;
+    pVar->pPrev->pNext = pVar;
+    pVar->pNext->pPrev = pVar;
+
+    // move the root so that it points to the new entry
+//    pRing->pRoot = pRing->pRoot->pPrev;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes the node from the ring.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_OrderRingRemove( Msat_OrderRing_t * pRing, Msat_OrderVar_t * pVar )
+{
+//printf( "removing %d\n", pVar->Num );
+    // check that the var is in a ring
+    assert( pVar->pPrev );
+    assert( pVar->pNext );
+    pRing->nItems--;
+    if ( pRing->nItems == 0 )
+    {
+        assert( pRing->pRoot == pVar );
+        pVar->pPrev = NULL;
+        pVar->pNext = NULL;
+        pRing->pRoot = NULL;
+        return;
+    }
+    // move the root if needed
+    if ( pRing->pRoot == pVar )
+        pRing->pRoot = pVar->pNext;
+    // move the root to the next entry after pVar
+    // this way all the additions to the list will be traversed first
+//    pRing->pRoot = pVar->pPrev;
+    // delete the node
+    pVar->pPrev->pNext = pVar->pNext;
+    pVar->pNext->pPrev = pVar->pPrev;
+    pVar->pPrev = NULL;
+    pVar->pNext = NULL;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/msat/msatQueue.c b/src/sat/msat/msatQueue.c
new file mode 100644
index 00000000..5938e042
--- /dev/null
+++ b/src/sat/msat/msatQueue.c
@@ -0,0 +1,157 @@
+/**CFile****************************************************************
+
+  FileName    [msatQueue.c]
+
+  PackageName [A C version of SAT solver MINISAT, originally developed 
+  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of 
+  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
+
+  Synopsis    [The manager of the assignment propagation queue.]
+
+  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 1, 2004.]
+
+  Revision    [$Id: msatQueue.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "msatInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+struct Msat_Queue_t_ 
+{
+    int         nVars;
+    int *       pVars;
+    int         iFirst;
+    int         iLast;
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates the variable propagation queue.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Msat_Queue_t * Msat_QueueAlloc( int nVars )
+{
+    Msat_Queue_t * p;
+    p = ALLOC( Msat_Queue_t, 1 );
+    memset( p, 0, sizeof(Msat_Queue_t) );
+    p->nVars  = nVars;
+    p->pVars  = ALLOC( int, nVars );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocate the variable propagation queue.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_QueueFree( Msat_Queue_t * p )
+{
+    free( p->pVars );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reads the queue size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Msat_QueueReadSize( Msat_Queue_t * p )
+{
+    return p->iLast - p->iFirst;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Insert an entry into the queue.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_QueueInsert( Msat_Queue_t * p, int Lit )
+{
+    if ( p->iLast == p->nVars )
+    {
+        int i;
+        assert( 0 );
+        for ( i = 0; i < p->iLast; i++ )
+            printf( "entry = %2d  lit = %2d  var = %2d \n", i, p->pVars[i], p->pVars[i]/2 );
+    }
+    assert( p->iLast < p->nVars );
+    p->pVars[p->iLast++] = Lit;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Extracts an entry from the queue.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Msat_QueueExtract( Msat_Queue_t * p )
+{
+    if ( p->iFirst == p->iLast )
+        return -1;
+    return p->pVars[p->iFirst++];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resets the queue.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_QueueClear( Msat_Queue_t * p )
+{
+    p->iFirst = 0;
+    p->iLast  = 0;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/msat/msatRead.c b/src/sat/msat/msatRead.c
new file mode 100644
index 00000000..738562ef
--- /dev/null
+++ b/src/sat/msat/msatRead.c
@@ -0,0 +1,268 @@
+/**CFile****************************************************************
+
+  FileName    [msatRead.c]
+
+  PackageName [A C version of SAT solver MINISAT, originally developed 
+  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of 
+  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
+
+  Synopsis    [The reader of the CNF formula in DIMACS format.]
+
+  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 1, 2004.]
+
+  Revision    [$Id: msatRead.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "msatInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static char * Msat_FileRead( FILE * pFile );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Read the file into the internal buffer.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Msat_FileRead( FILE * pFile )
+{
+    int nFileSize;
+    char * pBuffer;
+    // get the file size, in bytes
+    fseek( pFile, 0, SEEK_END );  
+    nFileSize = ftell( pFile );  
+    // move the file current reading position to the beginning
+    rewind( pFile ); 
+    // load the contents of the file into memory
+    pBuffer = ALLOC( char, nFileSize + 3 );
+    fread( pBuffer, nFileSize, 1, pFile );
+    // terminate the string with '\0'
+    pBuffer[ nFileSize + 0] = '\n';
+    pBuffer[ nFileSize + 1] = '\0';
+    return pBuffer;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void Msat_ReadWhitespace( char ** pIn ) 
+{
+    while ((**pIn >= 9 && **pIn <= 13) || **pIn == 32)
+        (*pIn)++; 
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void Msat_ReadNotWhitespace( char ** pIn ) 
+{
+    while ( !((**pIn >= 9 && **pIn <= 13) || **pIn == 32) )
+        (*pIn)++; 
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void skipLine( char ** pIn ) 
+{
+    while ( 1 )
+    {
+        if (**pIn == 0) 
+            return;
+        if (**pIn == '\n') 
+        { 
+            (*pIn)++; 
+            return; 
+        }
+        (*pIn)++; 
+    } 
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static int Msat_ReadInt( char ** pIn ) 
+{
+    int     val = 0;
+    bool    neg = 0;
+
+    Msat_ReadWhitespace( pIn );
+    if ( **pIn == '-' ) 
+        neg = 1, 
+        (*pIn)++;
+    else if ( **pIn == '+' ) 
+        (*pIn)++;
+    if ( **pIn < '0' || **pIn > '9' ) 
+        fprintf(stderr, "PARSE ERROR! Unexpected char: %c\n", **pIn), 
+        exit(1);
+    while ( **pIn >= '0' && **pIn <= '9' )
+        val = val*10 + (**pIn - '0'),
+        (*pIn)++;
+    return neg ? -val : val; 
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void Msat_ReadClause( char ** pIn, Msat_Solver_t * p, Msat_IntVec_t * pLits ) 
+{
+    int nVars = Msat_SolverReadVarNum( p );
+    int parsed_lit, var, sign;
+
+    Msat_IntVecClear( pLits );
+    while ( 1 )
+    {
+        parsed_lit = Msat_ReadInt(pIn);
+        if ( parsed_lit == 0 ) 
+            break;
+        var = abs(parsed_lit) - 1;
+        sign = (parsed_lit > 0);
+        if ( var >= nVars )
+        {
+            printf( "Variable %d is larger than the number of allocated variables (%d).\n", var+1, nVars );
+            exit(1);
+        }
+        Msat_IntVecPush( pLits, MSAT_VAR2LIT(var, !sign) );
+    }
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static bool Msat_ReadDimacs( char * pText, Msat_Solver_t ** pS, bool fVerbose ) 
+{
+    Msat_Solver_t * p;
+    Msat_IntVec_t * pLits;
+    char * pIn = pText;
+    int nVars, nClas;
+    while ( 1 )
+    {
+        Msat_ReadWhitespace( &pIn );
+        if ( *pIn == 0 )
+            break;
+        else if ( *pIn == 'c' )
+            skipLine( &pIn );
+        else if ( *pIn == 'p' )
+        {
+            pIn++;
+            Msat_ReadWhitespace( &pIn );
+            Msat_ReadNotWhitespace( &pIn );
+
+            nVars = Msat_ReadInt( &pIn );
+            nClas = Msat_ReadInt( &pIn );
+            skipLine( &pIn );
+            // start the solver
+            p = Msat_SolverAlloc( nVars, 1, 1, 1, 1, 0 ); 
+            Msat_SolverClean( p, nVars );
+            Msat_SolverSetVerbosity( p, fVerbose );
+            // allocate the vector
+            pLits = Msat_IntVecAlloc( nVars );
+        }
+        else
+        {
+            if ( p == NULL )
+            {
+                printf( "There is no parameter line.\n" );
+                exit(1);
+            }
+            Msat_ReadClause( &pIn, p, pLits );
+            if ( !Msat_SolverAddClause( p, pLits ) )
+                return 0;
+        }
+    }
+    Msat_IntVecFree( pLits );
+    *pS = p;
+    return Msat_SolverSimplifyDB( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the solver and reads the DIMAC file.]
+
+  Description [Returns FALSE upon immediate conflict.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Msat_SolverParseDimacs( FILE * pFile, Msat_Solver_t ** p, int fVerbose )
+{
+    char * pText;
+    bool Value;
+    pText = Msat_FileRead( pFile );
+    Value = Msat_ReadDimacs( pText, p, fVerbose );
+    free( pText );
+    return Value;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/msat/msatSolverApi.c b/src/sat/msat/msatSolverApi.c
new file mode 100644
index 00000000..ee3507a6
--- /dev/null
+++ b/src/sat/msat/msatSolverApi.c
@@ -0,0 +1,500 @@
+/**CFile****************************************************************
+
+  FileName    [msatSolverApi.c]
+
+  PackageName [A C version of SAT solver MINISAT, originally developed 
+  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of 
+  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
+
+  Synopsis    [APIs of the SAT solver.]
+
+  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 1, 2004.]
+
+  Revision    [$Id: msatSolverApi.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "msatInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Msat_SolverSetupTruthTables( unsigned uTruths[][2] );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Simple SAT solver APIs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int                Msat_SolverReadVarNum( Msat_Solver_t * p )                  { return p->nVars;      }
+int                Msat_SolverReadClauseNum( Msat_Solver_t * p )               { return p->nClauses;   }
+int                Msat_SolverReadVarAllocNum( Msat_Solver_t * p )             { return p->nVarsAlloc; }
+int                Msat_SolverReadDecisionLevel( Msat_Solver_t * p )           { return Msat_IntVecReadSize(p->vTrailLim); }
+int *              Msat_SolverReadDecisionLevelArray( Msat_Solver_t * p )      { return p->pLevel;     }
+Msat_Clause_t **    Msat_SolverReadReasonArray( Msat_Solver_t * p )            { return p->pReasons;   }
+Msat_Lit_t          Msat_SolverReadVarValue( Msat_Solver_t * p, Msat_Var_t Var ) { return p->pAssigns[Var]; }
+Msat_ClauseVec_t *  Msat_SolverReadLearned( Msat_Solver_t * p )                { return p->vLearned;   }
+Msat_ClauseVec_t ** Msat_SolverReadWatchedArray( Msat_Solver_t * p )           { return p->pvWatched;  }
+int *              Msat_SolverReadAssignsArray( Msat_Solver_t * p )            { return p->pAssigns;   }
+int *              Msat_SolverReadModelArray( Msat_Solver_t * p )              { return p->pModel;     }
+int                Msat_SolverReadBackTracks( Msat_Solver_t * p )              { return (int)p->Stats.nConflicts; }
+int                Msat_SolverReadInspects( Msat_Solver_t * p )                { return (int)p->Stats.nInspects;  }
+Msat_MmStep_t *     Msat_SolverReadMem( Msat_Solver_t * p )                    { return p->pMem;       }
+int *              Msat_SolverReadSeenArray( Msat_Solver_t * p )               { return p->pSeen;      }
+int                Msat_SolverIncrementSeenId( Msat_Solver_t * p )             { return ++p->nSeenId;  }
+void               Msat_SolverSetVerbosity( Msat_Solver_t * p, int fVerbose )  { p->fVerbose = fVerbose; }
+void               Msat_SolverClausesIncrement( Msat_Solver_t * p )            { p->nClausesAlloc++;   }
+void               Msat_SolverClausesDecrement( Msat_Solver_t * p )            { p->nClausesAlloc--;   }
+void               Msat_SolverClausesIncrementL( Msat_Solver_t * p )           { p->nClausesAllocL++;  }
+void               Msat_SolverClausesDecrementL( Msat_Solver_t * p )           { p->nClausesAllocL--;  }
+void               Msat_SolverMarkLastClauseTypeA( Msat_Solver_t * p )         { Msat_ClauseSetTypeA( Msat_ClauseVecReadEntry( p->vClauses, Msat_ClauseVecReadSize(p->vClauses)-1 ), 1 ); }
+void               Msat_SolverMarkClausesStart( Msat_Solver_t * p )            { p->nClausesStart = Msat_ClauseVecReadSize(p->vClauses); }
+float *            Msat_SolverReadFactors( Msat_Solver_t * p )                 { return p->pFactors;   }
+
+/**Function*************************************************************
+
+  Synopsis    [Reads the clause with the given number.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Msat_Clause_t * Msat_SolverReadClause( Msat_Solver_t * p, int Num )
+{
+    int nClausesP;
+    assert( Num < p->nClauses );
+    nClausesP = Msat_ClauseVecReadSize( p->vClauses );
+    if ( Num < nClausesP )
+        return Msat_ClauseVecReadEntry( p->vClauses, Num );
+    return Msat_ClauseVecReadEntry( p->vLearned, Num - nClausesP );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reads the clause with the given number.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Msat_ClauseVec_t *  Msat_SolverReadAdjacents( Msat_Solver_t * p )
+{
+    return p->vAdjacents;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reads the clause with the given number.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Msat_IntVec_t *  Msat_SolverReadConeVars( Msat_Solver_t * p )
+{
+    return p->vConeVars;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reads the clause with the given number.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Msat_IntVec_t *  Msat_SolverReadVarsUsed( Msat_Solver_t * p )
+{
+    return p->vVarsUsed;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates the solver.]
+
+  Description [After the solver is allocated, the procedure
+  Msat_SolverClean() should be called to set the number of variables.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Msat_Solver_t * Msat_SolverAlloc( int nVarsAlloc,
+    double dClaInc, double dClaDecay, 
+    double dVarInc, double dVarDecay, 
+    bool fVerbose )
+{
+    Msat_Solver_t * p;
+    int i;
+
+    assert(sizeof(Msat_Lit_t) == sizeof(unsigned));
+    assert(sizeof(float)     == sizeof(unsigned));
+
+    p = ALLOC( Msat_Solver_t, 1 );
+    memset( p, 0, sizeof(Msat_Solver_t) );
+
+    p->nVarsAlloc = nVarsAlloc;
+    p->nVars     = 0;
+
+    p->nClauses  = 0;
+    p->vClauses  = Msat_ClauseVecAlloc( 512 );
+    p->vLearned  = Msat_ClauseVecAlloc( 512 );
+
+    p->dClaInc   = dClaInc;
+    p->dClaDecay = dClaDecay;
+    p->dVarInc   = dVarInc;
+    p->dVarDecay = dVarDecay;
+
+    p->pdActivity = ALLOC( double, p->nVarsAlloc );
+    p->pFactors   = ALLOC( float, p->nVarsAlloc );
+    for ( i = 0; i < p->nVarsAlloc; i++ )
+    {
+        p->pdActivity[i] = 0.0;
+        p->pFactors[i]   = 1.0;
+    }
+
+    p->pAssigns  = ALLOC( int, p->nVarsAlloc ); 
+    p->pModel    = ALLOC( int, p->nVarsAlloc ); 
+    for ( i = 0; i < p->nVarsAlloc; i++ )
+        p->pAssigns[i] = MSAT_VAR_UNASSIGNED;
+//    p->pOrder    = Msat_OrderAlloc( p->pAssigns, p->pdActivity, p->nVarsAlloc );
+    p->pOrder    = Msat_OrderAlloc( p );
+
+    p->pvWatched = ALLOC( Msat_ClauseVec_t *, 2 * p->nVarsAlloc );
+    for ( i = 0; i < 2 * p->nVarsAlloc; i++ )
+        p->pvWatched[i] = Msat_ClauseVecAlloc( 16 );
+    p->pQueue    = Msat_QueueAlloc( p->nVarsAlloc );
+
+    p->vTrail    = Msat_IntVecAlloc( p->nVarsAlloc );
+    p->vTrailLim = Msat_IntVecAlloc( p->nVarsAlloc );
+    p->pReasons  = ALLOC( Msat_Clause_t *, p->nVarsAlloc );
+    memset( p->pReasons, 0, sizeof(Msat_Clause_t *) * p->nVarsAlloc );
+    p->pLevel = ALLOC( int, p->nVarsAlloc );
+    for ( i = 0; i < p->nVarsAlloc; i++ )
+        p->pLevel[i] = -1;
+    p->dRandSeed = 91648253;
+    p->fVerbose  = fVerbose;
+    p->dProgress = 0.0;
+//    p->pModel = Msat_IntVecAlloc( p->nVarsAlloc );
+    p->pMem = Msat_MmStepStart( 10 );
+
+    p->vConeVars   = Msat_IntVecAlloc( p->nVarsAlloc ); 
+    p->vAdjacents  = Msat_ClauseVecAlloc( p->nVarsAlloc );
+    for ( i = 0; i < p->nVarsAlloc; i++ )
+        Msat_ClauseVecPush( p->vAdjacents, (Msat_Clause_t *)Msat_IntVecAlloc(5) );
+    p->vVarsUsed   = Msat_IntVecAlloc( p->nVarsAlloc ); 
+    Msat_IntVecFill( p->vVarsUsed, p->nVarsAlloc, 1 );
+
+
+    p->pSeen     = ALLOC( int, p->nVarsAlloc );
+    memset( p->pSeen, 0, sizeof(int) * p->nVarsAlloc );
+    p->nSeenId   = 1;
+    p->vReason   = Msat_IntVecAlloc( p->nVarsAlloc );
+    p->vTemp     = Msat_IntVecAlloc( p->nVarsAlloc );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resizes the solver.]
+
+  Description [Assumes that the solver contains some clauses, and that 
+  it is currently between the calls. Resizes the solver to accomodate 
+  more variables.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_SolverResize( Msat_Solver_t * p, int nVarsAlloc )
+{
+    int nVarsAllocOld, i;
+
+    nVarsAllocOld = p->nVarsAlloc;
+    p->nVarsAlloc = nVarsAlloc;
+
+    p->pdActivity = REALLOC( double, p->pdActivity, p->nVarsAlloc );
+    p->pFactors   = REALLOC( float, p->pFactors, p->nVarsAlloc );
+    for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
+    {
+        p->pdActivity[i] = 0.0;
+        p->pFactors[i]   = 1.0;
+    }
+
+    p->pAssigns  = REALLOC( int, p->pAssigns, p->nVarsAlloc );
+    p->pModel    = REALLOC( int, p->pModel, p->nVarsAlloc );
+    for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
+        p->pAssigns[i] = MSAT_VAR_UNASSIGNED;
+
+//    Msat_OrderRealloc( p->pOrder, p->pAssigns, p->pdActivity, p->nVarsAlloc );
+    Msat_OrderSetBounds( p->pOrder, p->nVarsAlloc );
+
+    p->pvWatched = REALLOC( Msat_ClauseVec_t *, p->pvWatched, 2 * p->nVarsAlloc );
+    for ( i = 2 * nVarsAllocOld; i < 2 * p->nVarsAlloc; i++ )
+        p->pvWatched[i] = Msat_ClauseVecAlloc( 16 );
+
+    Msat_QueueFree( p->pQueue );
+    p->pQueue    = Msat_QueueAlloc( p->nVarsAlloc );
+
+    p->pReasons  = REALLOC( Msat_Clause_t *, p->pReasons, p->nVarsAlloc );
+    p->pLevel    = REALLOC( int, p->pLevel, p->nVarsAlloc );
+    for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
+    {
+        p->pReasons[i] = NULL;
+        p->pLevel[i] = -1;
+    }
+
+    p->pSeen     = REALLOC( int, p->pSeen, p->nVarsAlloc );
+    for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
+        p->pSeen[i] = 0;
+
+    Msat_IntVecGrow( p->vTrail, p->nVarsAlloc );
+    Msat_IntVecGrow( p->vTrailLim, p->nVarsAlloc );
+
+    // make sure the array of adjucents has room to store the variable numbers
+    for ( i = Msat_ClauseVecReadSize(p->vAdjacents); i < p->nVarsAlloc; i++ )
+        Msat_ClauseVecPush( p->vAdjacents, (Msat_Clause_t *)Msat_IntVecAlloc(5) );
+    Msat_IntVecFill( p->vVarsUsed, p->nVarsAlloc, 1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the solver.]
+
+  Description [Cleans the solver assuming that the problem will involve 
+  the given number of variables (nVars). This procedure is useful 
+  for many small (incremental) SAT problems, to prevent the solver
+  from being reallocated each time.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_SolverClean( Msat_Solver_t * p, int nVars )
+{
+    int i;
+    // free the clauses
+    int nClauses;
+    Msat_Clause_t ** pClauses;
+
+    assert( p->nVarsAlloc >= nVars );
+    p->nVars    = nVars;
+    p->nClauses = 0;
+
+    nClauses = Msat_ClauseVecReadSize( p->vClauses );
+    pClauses = Msat_ClauseVecReadArray( p->vClauses );
+    for ( i = 0; i < nClauses; i++ )
+        Msat_ClauseFree( p, pClauses[i], 0 );
+//    Msat_ClauseVecFree( p->vClauses );
+    Msat_ClauseVecClear( p->vClauses );
+
+    nClauses = Msat_ClauseVecReadSize( p->vLearned );
+    pClauses = Msat_ClauseVecReadArray( p->vLearned );
+    for ( i = 0; i < nClauses; i++ )
+        Msat_ClauseFree( p, pClauses[i], 0 );
+//    Msat_ClauseVecFree( p->vLearned );
+    Msat_ClauseVecClear( p->vLearned );
+
+//    FREE( p->pdActivity );
+    for ( i = 0; i < p->nVars; i++ )
+        p->pdActivity[i] = 0;
+
+//    Msat_OrderFree( p->pOrder );
+//    Msat_OrderClean( p->pOrder, p->nVars, NULL );
+    Msat_OrderSetBounds( p->pOrder, p->nVars );
+
+    for ( i = 0; i < 2 * p->nVars; i++ )
+//        Msat_ClauseVecFree( p->pvWatched[i] );
+        Msat_ClauseVecClear( p->pvWatched[i] );
+//    FREE( p->pvWatched );
+//    Msat_QueueFree( p->pQueue );
+    Msat_QueueClear( p->pQueue );
+
+//    FREE( p->pAssigns );
+    for ( i = 0; i < p->nVars; i++ )
+        p->pAssigns[i] = MSAT_VAR_UNASSIGNED;
+//    Msat_IntVecFree( p->vTrail );
+    Msat_IntVecClear( p->vTrail );
+//    Msat_IntVecFree( p->vTrailLim );
+    Msat_IntVecClear( p->vTrailLim );
+//    FREE( p->pReasons );
+    memset( p->pReasons, 0, sizeof(Msat_Clause_t *) * p->nVars );
+//    FREE( p->pLevel );
+    for ( i = 0; i < p->nVars; i++ )
+        p->pLevel[i] = -1;
+//    Msat_IntVecFree( p->pModel );
+//    Msat_MmStepStop( p->pMem, 0 );
+    p->dRandSeed = 91648253;
+    p->dProgress = 0.0;
+
+//    FREE( p->pSeen );
+    memset( p->pSeen, 0, sizeof(int) * p->nVars );
+    p->nSeenId = 1;
+//    Msat_IntVecFree( p->vReason );
+    Msat_IntVecClear( p->vReason );
+//    Msat_IntVecFree( p->vTemp );
+    Msat_IntVecClear( p->vTemp );
+//    printf(" The number of clauses remaining = %d (%d).\n", p->nClausesAlloc, p->nClausesAllocL );
+//    FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_SolverFree( Msat_Solver_t * p )
+{
+    int i;
+
+    // free the clauses
+    int nClauses;
+    Msat_Clause_t ** pClauses;
+//printf( "clauses = %d. learned = %d.\n", Msat_ClauseVecReadSize( p->vClauses ), 
+//                                         Msat_ClauseVecReadSize( p->vLearned ) );
+
+    nClauses = Msat_ClauseVecReadSize( p->vClauses );
+    pClauses = Msat_ClauseVecReadArray( p->vClauses );
+    for ( i = 0; i < nClauses; i++ )
+        Msat_ClauseFree( p, pClauses[i], 0 );
+    Msat_ClauseVecFree( p->vClauses );
+
+    nClauses = Msat_ClauseVecReadSize( p->vLearned );
+    pClauses = Msat_ClauseVecReadArray( p->vLearned );
+    for ( i = 0; i < nClauses; i++ )
+        Msat_ClauseFree( p, pClauses[i], 0 );
+    Msat_ClauseVecFree( p->vLearned );
+
+    FREE( p->pdActivity );
+    FREE( p->pFactors );
+    Msat_OrderFree( p->pOrder );
+
+    for ( i = 0; i < 2 * p->nVarsAlloc; i++ )
+        Msat_ClauseVecFree( p->pvWatched[i] );
+    FREE( p->pvWatched );
+    Msat_QueueFree( p->pQueue );
+
+    FREE( p->pAssigns );
+    FREE( p->pModel );
+    Msat_IntVecFree( p->vTrail );
+    Msat_IntVecFree( p->vTrailLim );
+    FREE( p->pReasons );
+    FREE( p->pLevel );
+
+    Msat_MmStepStop( p->pMem, 0 );
+
+    nClauses = Msat_ClauseVecReadSize( p->vAdjacents );
+    pClauses = Msat_ClauseVecReadArray( p->vAdjacents );
+    for ( i = 0; i < nClauses; i++ )
+        Msat_IntVecFree( (Msat_IntVec_t *)pClauses[i] );
+    Msat_ClauseVecFree( p->vAdjacents );
+    Msat_IntVecFree( p->vConeVars );
+    Msat_IntVecFree( p->vVarsUsed );
+
+    FREE( p->pSeen );
+    Msat_IntVecFree( p->vReason );
+    Msat_IntVecFree( p->vTemp );
+    FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the solver to run on a subset of variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_SolverPrepare( Msat_Solver_t * p, Msat_IntVec_t * vVars )
+{
+
+    int i;
+    // undo the previous data
+    for ( i = 0; i < p->nVarsAlloc; i++ )
+    {
+        p->pAssigns[i]   = MSAT_VAR_UNASSIGNED;
+        p->pReasons[i]   = NULL;
+        p->pLevel[i]     = -1;
+        p->pdActivity[i] = 0.0;
+    }
+
+    // set the new variable order
+    Msat_OrderClean( p->pOrder, vVars );
+
+    Msat_QueueClear( p->pQueue );
+    Msat_IntVecClear( p->vTrail );
+    Msat_IntVecClear( p->vTrailLim );
+    p->dProgress = 0.0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets up the truth tables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_SolverSetupTruthTables( unsigned uTruths[][2] )
+{
+    int m, v;
+    // set up the truth tables
+    for ( m = 0; m < 32; m++ )
+        for ( v = 0; v < 5; v++ )
+            if ( m & (1 << v) )
+                uTruths[v][0] |= (1 << m);
+    // make adjustments for the case of 6 variables
+    for ( v = 0; v < 5; v++ )
+        uTruths[v][1] = uTruths[v][0];
+    uTruths[5][0] = 0;
+    uTruths[5][1] = ~((unsigned)0);
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/msat/msatSolverCore.c b/src/sat/msat/msatSolverCore.c
new file mode 100644
index 00000000..f9fee73c
--- /dev/null
+++ b/src/sat/msat/msatSolverCore.c
@@ -0,0 +1,212 @@
+/**CFile****************************************************************
+
+  FileName    [msatSolverCore.c]
+
+  PackageName [A C version of SAT solver MINISAT, originally developed 
+  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of 
+  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
+
+  Synopsis    [The SAT solver core procedures.]
+
+  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 1, 2004.]
+
+  Revision    [$Id: msatSolverCore.c,v 1.2 2004/05/12 03:37:40 satrajit Exp $]
+
+***********************************************************************/
+
+#include "msatInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Adds one variable to the solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Msat_SolverAddVar( Msat_Solver_t * p, int Level )
+{
+    if ( p->nVars == p->nVarsAlloc )
+        Msat_SolverResize( p, 2 * p->nVarsAlloc );
+    p->pLevel[p->nVars] = Level;
+    p->nVars++;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds one clause to the solver's clause database.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Msat_SolverAddClause( Msat_Solver_t * p, Msat_IntVec_t * vLits )
+{
+    Msat_Clause_t * pC; 
+    bool Value;
+    Value = Msat_ClauseCreate( p, vLits, 0, &pC );
+    if ( pC != NULL )
+        Msat_ClauseVecPush( p->vClauses, pC );
+//    else if ( p->fProof )
+//        Msat_ClauseCreateFake( p, vLits );
+    return Value;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns search-space coverage. Not extremely reliable.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+double Msat_SolverProgressEstimate( Msat_Solver_t * p )
+{
+    double dProgress = 0.0;
+    double dF = 1.0 / p->nVars;
+    int i;
+    for ( i = 0; i < p->nVars; i++ )
+        if ( p->pAssigns[i] != MSAT_VAR_UNASSIGNED )
+            dProgress += pow( dF, p->pLevel[i] );
+    return dProgress / p->nVars;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints statistics about the solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_SolverPrintStats( Msat_Solver_t * p )
+{
+    printf("C solver (%d vars; %d clauses; %d learned):\n", 
+        p->nVars, Msat_ClauseVecReadSize(p->vClauses), Msat_ClauseVecReadSize(p->vLearned) );
+    printf("starts        : %lld\n", p->Stats.nStarts);
+    printf("conflicts     : %lld\n", p->Stats.nConflicts);
+    printf("decisions     : %lld\n", p->Stats.nDecisions);
+    printf("propagations  : %lld\n", p->Stats.nPropagations);
+    printf("inspects      : %lld\n", p->Stats.nInspects);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Top-level solve.]
+
+  Description [If using assumptions (non-empty 'assumps' vector), you must 
+  call 'simplifyDB()' first to see that no top-level conflict is present 
+  (which would put the solver in an undefined state. If the last argument
+  is given (vProj), the solver enumerates through the satisfying solutions,
+  which are projected on the variables listed in this array. Note that the
+  variables in the array may be complemented, in which case the derived
+  assignment for the variable is complemented.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTrackLimit, int nTimeLimit )
+{
+    Msat_SearchParams_t Params = { 0.95, 0.999 };
+    double nConflictsLimit, nLearnedLimit;
+    Msat_Type_t Status;
+    int timeStart = clock();
+    int64 nConflictsOld = p->Stats.nConflicts;
+    int64 nDecisionsOld = p->Stats.nDecisions;
+
+//    p->pFreq = ALLOC( int, p->nVarsAlloc );
+//    memset( p->pFreq, 0, sizeof(int) * p->nVarsAlloc );
+ 
+    if ( vAssumps )
+    {
+        int * pAssumps, nAssumps, i;
+
+        assert( Msat_IntVecReadSize(p->vTrailLim) == 0 );
+
+        nAssumps = Msat_IntVecReadSize( vAssumps );
+        pAssumps = Msat_IntVecReadArray( vAssumps );
+        for ( i = 0; i < nAssumps; i++ )
+        {
+            if ( !Msat_SolverAssume(p, pAssumps[i]) || Msat_SolverPropagate(p) )
+            {
+                Msat_QueueClear( p->pQueue );
+                Msat_SolverCancelUntil( p, 0 );
+                return MSAT_FALSE;
+            }
+        }
+    }
+    p->nLevelRoot   = Msat_SolverReadDecisionLevel(p);
+    p->nClausesInit = Msat_ClauseVecReadSize( p->vClauses );    
+    nConflictsLimit = 100;
+    nLearnedLimit   = Msat_ClauseVecReadSize(p->vClauses) / 3;
+    Status = MSAT_UNKNOWN;
+    p->nBackTracks = (int)p->Stats.nConflicts;
+    while ( Status == MSAT_UNKNOWN )
+    {
+        if ( p->fVerbose )
+            printf("Solving -- conflicts=%d   learnts=%d   progress=%.4f %%\n", 
+                (int)nConflictsLimit, (int)nLearnedLimit, p->dProgress*100);
+        Status = Msat_SolverSearch( p, (int)nConflictsLimit, (int)nLearnedLimit, nBackTrackLimit, &Params );
+        nConflictsLimit *= 1.5;
+        nLearnedLimit   *= 1.1;
+        // if the limit on the number of backtracks is given, quit the restart loop
+        if ( nBackTrackLimit > 0 && (int)p->Stats.nConflicts - p->nBackTracks > nBackTrackLimit )
+            break;
+        // if the runtime limit is exceeded, quit the restart loop
+        if ( nTimeLimit > 0 && clock() - timeStart >= nTimeLimit * CLOCKS_PER_SEC )
+            break;
+    }
+    Msat_SolverCancelUntil( p, 0 );
+    p->nBackTracks = (int)p->Stats.nConflicts - p->nBackTracks;
+/*
+    PRT( "True solver runtime", clock() - timeStart );
+    // print the statistics
+    {
+        int i, Counter = 0;
+        for ( i = 0; i < p->nVars; i++ )
+            if ( p->pFreq[i] > 0 )
+            {
+                printf( "%d ", p->pFreq[i] );
+                Counter++;
+            }
+        if ( Counter )
+            printf( "\n" );
+        printf( "Total = %d. Used = %d.  Decisions = %d. Imps = %d. Conflicts = %d. ", p->nVars, Counter, (int)p->Stats.nDecisions, (int)p->Stats.nPropagations, (int)p->Stats.nConflicts );
+        PRT( "Time", clock() - timeStart );
+    }
+*/
+    return Status;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/msat/msatSolverIo.c b/src/sat/msat/msatSolverIo.c
new file mode 100644
index 00000000..05b7f6a9
--- /dev/null
+++ b/src/sat/msat/msatSolverIo.c
@@ -0,0 +1,177 @@
+/**CFile****************************************************************
+
+  FileName    [msatSolverIo.c]
+
+  PackageName [A C version of SAT solver MINISAT, originally developed 
+  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of 
+  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
+
+  Synopsis    [Input/output of CNFs.]
+
+  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 1, 2004.]
+
+  Revision    [$Id: msatSolverIo.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "msatInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static char * Msat_TimeStamp();
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_SolverPrintAssignment( Msat_Solver_t * p )
+{
+    int i;
+    printf( "Current assignments are: \n" );
+    for ( i = 0; i < p->nVars; i++ )
+        printf( "%d", i % 10 );
+    printf( "\n" );
+    for ( i = 0; i < p->nVars; i++ )
+        if ( p->pAssigns[i] == MSAT_VAR_UNASSIGNED )
+            printf( "." );
+        else
+        {
+            assert( i == MSAT_LIT2VAR(p->pAssigns[i]) );
+            if ( MSAT_LITSIGN(p->pAssigns[i]) )
+                printf( "0" );
+            else 
+                printf( "1" );
+        }
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_SolverPrintClauses( Msat_Solver_t * p )
+{
+    Msat_Clause_t ** pClauses;
+    int nClauses, i;
+
+    printf( "Original clauses: \n" );
+    nClauses = Msat_ClauseVecReadSize( p->vClauses );
+    pClauses = Msat_ClauseVecReadArray( p->vClauses );
+    for ( i = 0; i < nClauses; i++ )
+    {
+        printf( "%3d: ", i );
+        Msat_ClausePrint( pClauses[i] );
+    }
+
+    printf( "Learned clauses: \n" );
+    nClauses = Msat_ClauseVecReadSize( p->vLearned );
+    pClauses = Msat_ClauseVecReadArray( p->vLearned );
+    for ( i = 0; i < nClauses; i++ )
+    {
+        printf( "%3d: ", i );
+        Msat_ClausePrint( pClauses[i] );
+    }
+
+    printf( "Variable activity: \n" );
+    for ( i = 0; i < p->nVars; i++ )
+        printf( "%3d : %.4f\n", i, p->pdActivity[i] );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_SolverWriteDimacs( Msat_Solver_t * p, char * pFileName )
+{
+    FILE * pFile;
+    Msat_Clause_t ** pClauses;
+    int nClauses, i;
+
+    nClauses = Msat_ClauseVecReadSize(p->vClauses) + Msat_ClauseVecReadSize(p->vLearned);
+    for ( i = 0; i < p->nVars; i++ )
+        nClauses += ( p->pLevel[i] == 0 );
+
+    pFile = fopen( pFileName, "wb" );
+    fprintf( pFile, "c Produced by Msat_SolverWriteDimacs() on %s\n", Msat_TimeStamp() );
+    fprintf( pFile, "p cnf %d %d\n", p->nVars, nClauses );
+
+    nClauses = Msat_ClauseVecReadSize( p->vClauses );
+    pClauses = Msat_ClauseVecReadArray( p->vClauses );
+    for ( i = 0; i < nClauses; i++ )
+        Msat_ClauseWriteDimacs( pFile, pClauses[i], 1 );
+
+    nClauses = Msat_ClauseVecReadSize( p->vLearned );
+    pClauses = Msat_ClauseVecReadArray( p->vLearned );
+    for ( i = 0; i < nClauses; i++ )
+        Msat_ClauseWriteDimacs( pFile, pClauses[i], 1 );
+
+    // write zero-level assertions
+    for ( i = 0; i < p->nVars; i++ )
+        if ( p->pLevel[i] == 0 )
+            fprintf( pFile, "%s%d 0\n", ((p->pAssigns[i]&1)? "-": ""), i + 1 );
+
+    fprintf( pFile, "\n" );
+    fclose( pFile );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the time stamp.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Msat_TimeStamp()
+{
+    static char Buffer[100];
+    time_t ltime;
+    char * TimeStamp;
+    // get the current time
+    time( &ltime );
+    TimeStamp = asctime( localtime( &ltime ) );
+    TimeStamp[ strlen(TimeStamp) - 1 ] = 0;
+    strcpy( Buffer, TimeStamp );
+    return Buffer;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/msat/msatSolverSearch.c b/src/sat/msat/msatSolverSearch.c
new file mode 100644
index 00000000..11a6540c
--- /dev/null
+++ b/src/sat/msat/msatSolverSearch.c
@@ -0,0 +1,629 @@
+/**CFile****************************************************************
+
+  FileName    [msatSolverSearch.c]
+
+  PackageName [A C version of SAT solver MINISAT, originally developed 
+  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of 
+  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
+
+  Synopsis    [The search part of the solver.]
+
+  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 1, 2004.]
+
+  Revision    [$Id: msatSolverSearch.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "msatInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void            Msat_SolverUndoOne( Msat_Solver_t * p );
+static void            Msat_SolverCancel( Msat_Solver_t * p );
+static Msat_Clause_t * Msat_SolverRecord( Msat_Solver_t * p, Msat_IntVec_t * vLits );
+static void            Msat_SolverAnalyze( Msat_Solver_t * p, Msat_Clause_t * pC, Msat_IntVec_t * vLits_out, int * pLevel_out );
+static void            Msat_SolverReduceDB( Msat_Solver_t * p );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Makes the next assumption (Lit).]
+
+  Description [Returns FALSE if immediate conflict.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Msat_SolverAssume( Msat_Solver_t * p, Msat_Lit_t Lit )
+{
+    assert( Msat_QueueReadSize(p->pQueue) == 0 );
+    if ( p->fVerbose )
+        printf(L_IND"assume("L_LIT")\n", L_ind, L_lit(Lit));
+    Msat_IntVecPush( p->vTrailLim, Msat_IntVecReadSize(p->vTrail) );
+//    assert( Msat_IntVecReadSize(p->vTrailLim) <= Msat_IntVecReadSize(p->vTrail) + 1 );
+//    assert( Msat_IntVecReadSize( p->vTrailLim ) < p->nVars );
+    return Msat_SolverEnqueue( p, Lit, NULL );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reverts one variable binding on the trail.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_SolverUndoOne( Msat_Solver_t * p )
+{
+    Msat_Lit_t Lit;
+    Msat_Var_t Var;
+    Lit = Msat_IntVecPop( p->vTrail ); 
+    Var = MSAT_LIT2VAR(Lit);
+    p->pAssigns[Var] = MSAT_VAR_UNASSIGNED;
+    p->pReasons[Var] = NULL;
+    p->pLevel[Var]   = -1;
+//    Msat_OrderUndo( p->pOrder, Var );
+    Msat_OrderVarUnassigned( p->pOrder, Var );
+
+    if ( p->fVerbose )
+        printf(L_IND"unbind("L_LIT")\n", L_ind, L_lit(Lit)); 
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reverts to the state before last Msat_SolverAssume().]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_SolverCancel( Msat_Solver_t * p )
+{
+    int c;
+    assert( Msat_QueueReadSize(p->pQueue) == 0 );
+    if ( p->fVerbose )
+    {
+        if ( Msat_IntVecReadSize(p->vTrail) != Msat_IntVecReadEntryLast(p->vTrailLim) )
+        {
+            Msat_Lit_t Lit;
+            Lit = Msat_IntVecReadEntry( p->vTrail, Msat_IntVecReadEntryLast(p->vTrailLim) ); 
+            printf(L_IND"cancel("L_LIT")\n", L_ind, L_lit(Lit));
+        }
+    }
+    for ( c = Msat_IntVecReadSize(p->vTrail) - Msat_IntVecPop( p->vTrailLim ); c != 0; c-- )
+        Msat_SolverUndoOne( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reverts to the state at given level.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_SolverCancelUntil( Msat_Solver_t * p, int Level )
+{
+    while ( Msat_IntVecReadSize(p->vTrailLim) > Level )
+        Msat_SolverCancel(p);
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Record a clause and drive backtracking.]
+
+  Description [vLits[0] must contain the asserting literal.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Msat_Clause_t * Msat_SolverRecord( Msat_Solver_t * p, Msat_IntVec_t * vLits )
+{
+    Msat_Clause_t * pC;
+    int Value;
+    assert( Msat_IntVecReadSize(vLits) != 0 );
+    Value = Msat_ClauseCreate( p, vLits, 1, &pC );
+    assert( Value );
+    Value = Msat_SolverEnqueue( p, Msat_IntVecReadEntry(vLits,0), pC );
+    assert( Value );
+    if ( pC )
+        Msat_ClauseVecPush( p->vLearned, pC );
+    return pC;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Enqueues one variable assignment.]
+
+  Description [Puts a new fact on the propagation queue and immediately 
+  updates the variable value. Should a conflict arise, FALSE is returned.
+  Otherwise returns TRUE.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Msat_SolverEnqueue( Msat_Solver_t * p, Msat_Lit_t Lit, Msat_Clause_t * pC )
+{
+    Msat_Var_t Var = MSAT_LIT2VAR(Lit);
+
+    // skip literals that are not in the current cone
+    if ( !Msat_IntVecReadEntry( p->vVarsUsed, Var ) )
+        return 1;
+
+//    assert( Msat_QueueReadSize(p->pQueue) == Msat_IntVecReadSize(p->vTrail) );
+    // if the literal is assigned
+    // return 1 if the assignment is consistent
+    // return 0 if the assignment is inconsistent (conflict)
+    if ( p->pAssigns[Var] != MSAT_VAR_UNASSIGNED )
+        return p->pAssigns[Var] == Lit;
+    // new fact - store it
+    if ( p->fVerbose )
+    {
+//        printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(Lit));
+        printf(L_IND"bind("L_LIT")  ", L_ind, L_lit(Lit));
+        Msat_ClausePrintSymbols( pC );
+    }
+    p->pAssigns[Var] = Lit;
+    p->pLevel[Var]   = Msat_IntVecReadSize(p->vTrailLim);
+//    p->pReasons[Var] = p->pLevel[Var]? pC: NULL;
+    p->pReasons[Var] = pC;
+    Msat_IntVecPush( p->vTrail, Lit );
+    Msat_QueueInsert( p->pQueue, Lit );
+
+    Msat_OrderVarAssigned( p->pOrder, Var );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Propagates the assignments in the queue.]
+
+  Description [Propagates all enqueued facts. If a conflict arises, 
+  the conflicting clause is returned, otherwise NULL.]
+               
+  SideEffects [The propagation queue is empty, even if there was a conflict.]
+
+  SeeAlso     []
+
+***********************************************************************/
+Msat_Clause_t * Msat_SolverPropagate( Msat_Solver_t * p )
+{
+    Msat_ClauseVec_t ** pvWatched = p->pvWatched;
+    Msat_Clause_t ** pClauses;
+    Msat_Clause_t * pConflict;
+    Msat_Lit_t Lit, Lit_out;
+    int i, j, nClauses;
+
+    // propagate all the literals in the queue
+    while ( (Lit = Msat_QueueExtract( p->pQueue )) >= 0 )
+    {
+        p->Stats.nPropagations++;
+        // get the clauses watched by this literal
+        nClauses = Msat_ClauseVecReadSize( pvWatched[Lit] );
+        pClauses = Msat_ClauseVecReadArray( pvWatched[Lit] );
+        // go through the watched clauses and decide what to do with them
+        for ( i = j = 0; i < nClauses; i++ )
+        {
+            p->Stats.nInspects++;
+            // clear the returned literal
+            Lit_out = -1;
+            // propagate the clause
+            if ( !Msat_ClausePropagate( pClauses[i], Lit, p->pAssigns, &Lit_out ) )
+            {   // the clause is unit
+                // "Lit_out" contains the new assignment to be enqueued
+                if ( Msat_SolverEnqueue( p, Lit_out, pClauses[i] ) ) 
+                { // consistent assignment 
+                    // no changes to the implication queue; the watch is the same too
+                    pClauses[j++] = pClauses[i];
+                    continue;
+                }
+                // remember the reason of conflict (will be returned)
+                pConflict = pClauses[i];
+                // leave the remaning clauses in the same watched list
+                for ( ; i < nClauses; i++ )
+                    pClauses[j++] = pClauses[i];
+                Msat_ClauseVecShrink( pvWatched[Lit], j );
+                // clear the propagation queue
+                Msat_QueueClear( p->pQueue );
+                return pConflict;
+            }
+            // the clause is not unit
+            // in this case "Lit_out" contains the new watch if it has changed
+            if ( Lit_out >= 0 )
+                Msat_ClauseVecPush( pvWatched[Lit_out], pClauses[i] );
+            else // the watch did not change
+                pClauses[j++] = pClauses[i];
+        }
+        Msat_ClauseVecShrink( pvWatched[Lit], j );
+    }
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Simplifies the data base.]
+
+  Description [Simplify all constraints according to the current top-level 
+  assigment (redundant constraints may be removed altogether).]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Msat_SolverSimplifyDB( Msat_Solver_t * p )
+{
+    Msat_ClauseVec_t * vClauses;
+    Msat_Clause_t ** pClauses;
+    int nClauses, Type, i, j;
+    int * pAssigns;
+    int Counter;
+
+    assert( Msat_SolverReadDecisionLevel(p) == 0 );
+    if ( Msat_SolverPropagate(p) != NULL )
+        return 0;
+//Msat_SolverPrintClauses( p );
+//Msat_SolverPrintAssignment( p );
+//printf( "Simplification\n" );
+
+    // simplify and reassign clause numbers
+    Counter = 0;
+    pAssigns = Msat_SolverReadAssignsArray( p );
+    for ( Type = 0; Type < 2; Type++ )
+    {
+        vClauses = Type? p->vLearned : p->vClauses;
+        nClauses = Msat_ClauseVecReadSize( vClauses );
+        pClauses = Msat_ClauseVecReadArray( vClauses );
+        for ( i = j = 0; i < nClauses; i++ )
+            if ( Msat_ClauseSimplify( pClauses[i], pAssigns ) )
+                Msat_ClauseFree( p, pClauses[i], 1 );
+            else
+            {
+                pClauses[j++] = pClauses[i];
+                Msat_ClauseSetNum( pClauses[i], Counter++ );
+            }
+        Msat_ClauseVecShrink( vClauses, j );
+    }
+    p->nClauses = Counter;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Cleans the clause databased from the useless learnt clauses.]
+
+  Description [Removes half of the learnt clauses, minus the clauses locked 
+  by the current assignment. Locked clauses are clauses that are reason 
+  to a some assignment.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_SolverReduceDB( Msat_Solver_t * p )
+{
+    Msat_Clause_t ** pLearned;
+    int nLearned, i, j;
+    double dExtraLim = p->dClaInc / Msat_ClauseVecReadSize(p->vLearned); 
+    // Remove any clause below this activity
+
+    // sort the learned clauses in the increasing order of activity
+    Msat_SolverSortDB( p );
+
+    // discard the first half the clauses (the less active ones)
+    nLearned = Msat_ClauseVecReadSize( p->vLearned );
+    pLearned = Msat_ClauseVecReadArray( p->vLearned );
+    for ( i = j = 0; i < nLearned / 2; i++ )
+        if ( !Msat_ClauseIsLocked( p, pLearned[i]) )
+            Msat_ClauseFree( p, pLearned[i], 1 );
+        else
+            pLearned[j++] = pLearned[i];
+    // filter the more active clauses and leave those above the limit
+    for (  ; i < nLearned; i++ )
+        if ( !Msat_ClauseIsLocked( p, pLearned[i] ) && 
+            Msat_ClauseReadActivity(pLearned[i]) < dExtraLim )
+            Msat_ClauseFree( p, pLearned[i], 1 );
+        else
+            pLearned[j++] = pLearned[i];
+    Msat_ClauseVecShrink( p->vLearned, j );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes the learned clauses.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_SolverRemoveLearned( Msat_Solver_t * p )
+{
+    Msat_Clause_t ** pLearned;
+    int nLearned, i;
+
+    // discard the learned clauses
+    nLearned = Msat_ClauseVecReadSize( p->vLearned );
+    pLearned = Msat_ClauseVecReadArray( p->vLearned );
+    for ( i = 0; i < nLearned; i++ )
+    {
+        assert( !Msat_ClauseIsLocked( p, pLearned[i]) );
+        
+        Msat_ClauseFree( p, pLearned[i], 1 );
+    }
+    Msat_ClauseVecShrink( p->vLearned, 0 );
+    p->nClauses = Msat_ClauseVecReadSize(p->vClauses);
+
+    for ( i = 0; i < p->nVarsAlloc; i++ )
+        p->pReasons[i] = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes the recently added clauses.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_SolverRemoveMarked( Msat_Solver_t * p )
+{
+    Msat_Clause_t ** pLearned, ** pClauses;
+    int nLearned, nClauses, i;
+
+    // discard the learned clauses
+    nClauses = Msat_ClauseVecReadSize( p->vClauses );
+    pClauses = Msat_ClauseVecReadArray( p->vClauses );
+    for ( i = p->nClausesStart; i < nClauses; i++ )
+    {
+//        assert( !Msat_ClauseIsLocked( p, pClauses[i]) );
+        Msat_ClauseFree( p, pClauses[i], 1 );
+    }
+    Msat_ClauseVecShrink( p->vClauses, p->nClausesStart );
+
+    // discard the learned clauses
+    nLearned = Msat_ClauseVecReadSize( p->vLearned );
+    pLearned = Msat_ClauseVecReadArray( p->vLearned );
+    for ( i = 0; i < nLearned; i++ )
+    {
+//        assert( !Msat_ClauseIsLocked( p, pLearned[i]) );
+        Msat_ClauseFree( p, pLearned[i], 1 );
+    }
+    Msat_ClauseVecShrink( p->vLearned, 0 );
+    p->nClauses = Msat_ClauseVecReadSize(p->vClauses);
+/*
+    // undo the previous data
+    for ( i = 0; i < p->nVarsAlloc; i++ )
+    {
+        p->pAssigns[i]   = MSAT_VAR_UNASSIGNED;
+        p->pReasons[i]   = NULL;
+        p->pLevel[i]     = -1;
+        p->pdActivity[i] = 0.0;
+    }
+    Msat_OrderClean( p->pOrder, p->nVars, NULL );
+    Msat_QueueClear( p->pQueue );
+*/
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Analyze conflict and produce a reason clause.]
+
+  Description [Current decision level must be greater than root level.]
+               
+  SideEffects [vLits_out[0] is the asserting literal at level pLevel_out.]
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_SolverAnalyze( Msat_Solver_t * p, Msat_Clause_t * pC, Msat_IntVec_t * vLits_out, int * pLevel_out )
+{
+    Msat_Lit_t LitQ, Lit = MSAT_LIT_UNASSIGNED;
+    Msat_Var_t VarQ, Var;
+    int * pReasonArray, nReasonSize;
+    int j, pathC = 0, nLevelCur = Msat_IntVecReadSize(p->vTrailLim);
+    int iStep = Msat_IntVecReadSize(p->vTrail) - 1;
+
+    // increment the seen counter
+    p->nSeenId++;
+    // empty the vector array
+    Msat_IntVecClear( vLits_out );
+    Msat_IntVecPush( vLits_out, -1 ); // (leave room for the asserting literal)
+    *pLevel_out = 0;
+    do {
+        assert( pC != NULL );  // (otherwise should be UIP)
+        // get the reason of conflict
+        Msat_ClauseCalcReason( p, pC, Lit, p->vReason );
+        nReasonSize  = Msat_IntVecReadSize( p->vReason );
+        pReasonArray = Msat_IntVecReadArray( p->vReason );
+        for ( j = 0; j < nReasonSize; j++ ) {
+            LitQ = pReasonArray[j];
+            VarQ = MSAT_LIT2VAR(LitQ);
+            if ( p->pSeen[VarQ] != p->nSeenId ) {
+                p->pSeen[VarQ] = p->nSeenId;
+
+                // added to better fine-tune the search
+                Msat_SolverVarBumpActivity( p, LitQ );
+
+                // skip all the literals on this decision level
+                if ( p->pLevel[VarQ] == nLevelCur )
+                    pathC++;
+                else if ( p->pLevel[VarQ] > 0 ) { 
+                    // add the literals on other decision levels but
+                    // exclude variables from decision level 0
+                    Msat_IntVecPush( vLits_out, MSAT_LITNOT(LitQ) );
+                    if ( *pLevel_out < p->pLevel[VarQ] )
+                        *pLevel_out = p->pLevel[VarQ];
+                }
+            }
+        }
+        // Select next clause to look at:
+        do {
+//            Lit = Msat_IntVecReadEntryLast(p->vTrail);
+            Lit = Msat_IntVecReadEntry( p->vTrail, iStep-- );
+            Var = MSAT_LIT2VAR(Lit);
+            pC = p->pReasons[Var];
+//            Msat_SolverUndoOne( p );
+        } while ( p->pSeen[Var] != p->nSeenId );
+        pathC--;
+    } while ( pathC > 0 );
+    // we do not unbind the variables above
+    // this will be done after conflict analysis
+
+    Msat_IntVecWriteEntry( vLits_out, 0, MSAT_LITNOT(Lit) );
+    if ( p->fVerbose )
+    {
+        printf( L_IND"Learnt {", L_ind );
+        nReasonSize  = Msat_IntVecReadSize( vLits_out );
+        pReasonArray = Msat_IntVecReadArray( vLits_out );
+        for ( j = 0; j < nReasonSize; j++ ) 
+            printf(" "L_LIT, L_lit(pReasonArray[j]));
+        printf(" } at level %d\n", *pLevel_out); 
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [The search procedure called between the restarts.]
+
+  Description [Search for a satisfying solution as long as the number of 
+  conflicts does not exceed the limit (nConfLimit) while keeping the number 
+  of learnt clauses below the provided limit (nLearnedLimit). NOTE! Use 
+  negative value for nConfLimit or nLearnedLimit to indicate infinity.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Msat_Type_t Msat_SolverSearch( Msat_Solver_t * p, int nConfLimit, int nLearnedLimit, int nBackTrackLimit, Msat_SearchParams_t * pPars )
+{
+    Msat_Clause_t * pConf;
+    Msat_Var_t Var;
+    int nLevelBack, nConfs, nAssigns, Value;
+    int i;
+
+    assert( Msat_SolverReadDecisionLevel(p) == p->nLevelRoot );
+    p->Stats.nStarts++;
+    p->dVarDecay = 1 / pPars->dVarDecay;
+    p->dClaDecay = 1 / pPars->dClaDecay;
+
+    // reset the activities
+    for ( i = 0; i < p->nVars; i++ )
+       p->pdActivity[i] = (double)p->pFactors[i];
+//       p->pdActivity[i] = 0.0;
+
+    nConfs = 0;
+    while ( 1 )
+    {
+        pConf = Msat_SolverPropagate( p );
+        if ( pConf != NULL ){
+            // CONFLICT
+            if ( p->fVerbose )
+            {
+//                printf(L_IND"**CONFLICT**\n", L_ind);
+                printf(L_IND"**CONFLICT**  ", L_ind);
+                Msat_ClausePrintSymbols( pConf );
+            }
+            // count conflicts
+            p->Stats.nConflicts++;
+            nConfs++;
+
+            // if top level, return UNSAT
+            if ( Msat_SolverReadDecisionLevel(p) == p->nLevelRoot )
+                return MSAT_FALSE;
+
+            // perform conflict analysis
+            Msat_SolverAnalyze( p, pConf, p->vTemp, &nLevelBack );
+            Msat_SolverCancelUntil( p, (p->nLevelRoot > nLevelBack)? p->nLevelRoot : nLevelBack );
+            Msat_SolverRecord( p, p->vTemp );
+
+            // it is important that recording is done after cancelling
+            // because canceling cleans the queue while recording adds to it
+            Msat_SolverVarDecayActivity( p );
+            Msat_SolverClaDecayActivity( p );
+
+        }
+        else{
+            // NO CONFLICT
+            if ( Msat_IntVecReadSize(p->vTrailLim) == 0 ) {
+                // Simplify the set of problem clauses:
+//                Value = Msat_SolverSimplifyDB(p);
+//                assert( Value );
+            }
+            nAssigns = Msat_IntVecReadSize( p->vTrail );
+            if ( nLearnedLimit >= 0 && Msat_ClauseVecReadSize(p->vLearned) >= nLearnedLimit + nAssigns ) {
+                // Reduce the set of learnt clauses:
+                Msat_SolverReduceDB(p);
+            }
+
+            Var = Msat_OrderVarSelect( p->pOrder );
+            if ( Var == MSAT_ORDER_UNKNOWN ) {
+                // Model found and stored in p->pAssigns
+                memcpy( p->pModel, p->pAssigns, sizeof(int) * p->nVars );
+                Msat_QueueClear( p->pQueue );
+                Msat_SolverCancelUntil( p, p->nLevelRoot );
+                return MSAT_TRUE;
+            }
+            if ( nConfLimit > 0 && nConfs > nConfLimit ) {
+                // Reached bound on number of conflicts:
+                p->dProgress = Msat_SolverProgressEstimate( p );
+                Msat_QueueClear( p->pQueue );
+                Msat_SolverCancelUntil( p, p->nLevelRoot );
+                return MSAT_UNKNOWN; 
+            }
+            else if ( nBackTrackLimit > 0 && (int)p->Stats.nConflicts - p->nBackTracks > nBackTrackLimit ) {
+                // Reached bound on number of conflicts:
+                Msat_QueueClear( p->pQueue );
+                Msat_SolverCancelUntil( p, p->nLevelRoot );
+                return MSAT_UNKNOWN; 
+            }
+            else{
+                // New variable decision:
+                p->Stats.nDecisions++;
+                assert( Var != MSAT_ORDER_UNKNOWN && Var >= 0 && Var < p->nVars );
+                Value = Msat_SolverAssume(p, MSAT_VAR2LIT(Var,0) );
+                assert( Value );
+            }
+        }
+    }
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/msat/msatSort.c b/src/sat/msat/msatSort.c
new file mode 100644
index 00000000..3b89d102
--- /dev/null
+++ b/src/sat/msat/msatSort.c
@@ -0,0 +1,173 @@
+/**CFile****************************************************************
+
+  FileName    [msatSort.c]
+
+  PackageName [A C version of SAT solver MINISAT, originally developed 
+  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of 
+  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
+
+  Synopsis    [Sorting clauses.]
+
+  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 1, 2004.]
+
+  Revision    [$Id: msatSort.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "msatInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static int Msat_SolverSortCompare( Msat_Clause_t ** ppC1, Msat_Clause_t ** ppC2 );
+
+// Returns a random float 0 <= x < 1. Seed must never be 0.
+static 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 int irand(double seed, int size) {
+    return (int)(drand(seed) * size); }
+
+static void Msat_SolverSort( Msat_Clause_t ** array, int size, double seed );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Msat_SolverSort the learned clauses in the increasing order of activity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_SolverSortDB( Msat_Solver_t * p )
+{
+    Msat_ClauseVec_t * pVecClauses;
+    Msat_Clause_t ** pLearned;
+    int nLearned;
+    // read the parameters
+    pVecClauses = Msat_SolverReadLearned( p );
+    nLearned    = Msat_ClauseVecReadSize( pVecClauses );
+    pLearned    = Msat_ClauseVecReadArray( pVecClauses );
+    // Msat_SolverSort the array
+//    qMsat_SolverSort( (void *)pLearned, nLearned, sizeof(Msat_Clause_t *), 
+//            (int (*)(const void *, const void *)) Msat_SolverSortCompare );
+//    printf( "Msat_SolverSorting.\n" );
+    Msat_SolverSort( pLearned, nLearned, 91648253 );
+/*
+    if ( nLearned > 2 )
+    {
+    printf( "Clause 1: %0.20f\n", Msat_ClauseReadActivity(pLearned[0]) );
+    printf( "Clause 2: %0.20f\n", Msat_ClauseReadActivity(pLearned[1]) );
+    printf( "Clause 3: %0.20f\n", Msat_ClauseReadActivity(pLearned[2]) );
+    }
+*/
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Comparison procedure for two clauses.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Msat_SolverSortCompare( Msat_Clause_t ** ppC1, Msat_Clause_t ** ppC2 )
+{
+    float Value1 = Msat_ClauseReadActivity( *ppC1 );
+    float Value2 = Msat_ClauseReadActivity( *ppC2 );
+    if ( Value1 < Value2 )
+        return -1;
+    if ( Value1 > Value2 )
+        return 1;
+    return 0;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Selection sort for small array size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_SolverSortSelection( Msat_Clause_t ** array, int size )
+{
+    Msat_Clause_t * tmp;
+    int i, j, best_i;
+    for ( i = 0; i < size-1; i++ )
+    {
+        best_i = i;
+        for (j = i+1; j < size; j++)
+        {
+            if ( Msat_ClauseReadActivity(array[j]) < Msat_ClauseReadActivity(array[best_i]) )
+                best_i = j;
+        }
+        tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [The original MiniSat sorting procedure.]
+
+  Description [This procedure is used to preserve trace-equivalence
+  with the orignal C++ implemenation of the solver.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_SolverSort( Msat_Clause_t ** array, int size, double seed )
+{
+    if (size <= 15)
+        Msat_SolverSortSelection( array, size );
+    else
+    {
+        Msat_Clause_t *   pivot = array[irand(seed, size)];
+        Msat_Clause_t *   tmp;
+        int              i = -1;
+        int              j = size;
+
+        for(;;)
+        {
+            do i++; while( Msat_ClauseReadActivity(array[i]) < Msat_ClauseReadActivity(pivot) );
+            do j--; while( Msat_ClauseReadActivity(pivot) < Msat_ClauseReadActivity(array[j]) );
+
+            if ( i >= j ) break;
+
+            tmp = array[i]; array[i] = array[j]; array[j] = tmp;
+        }
+        Msat_SolverSort(array    , i     , seed);
+        Msat_SolverSort(&array[i], size-i, seed);
+    }
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/msat/msatVec.c b/src/sat/msat/msatVec.c
new file mode 100644
index 00000000..75f53047
--- /dev/null
+++ b/src/sat/msat/msatVec.c
@@ -0,0 +1,495 @@
+/**CFile****************************************************************
+
+  FileName    [msatVec.c]
+
+  PackageName [A C version of SAT solver MINISAT, originally developed 
+  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of 
+  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
+
+  Synopsis    [Integer vector borrowed from Extra.]
+
+  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 1, 2004.]
+
+  Revision    [$Id: msatVec.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "msatInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static int Msat_IntVecSortCompare1( int * pp1, int * pp2 );
+static int Msat_IntVecSortCompare2( int * pp1, int * pp2 );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates a vector with the given capacity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Msat_IntVec_t * Msat_IntVecAlloc( int nCap )
+{
+    Msat_IntVec_t * p;
+    p = ALLOC( Msat_IntVec_t, 1 );
+    if ( nCap > 0 && nCap < 16 )
+        nCap = 16;
+    p->nSize  = 0;
+    p->nCap   = nCap;
+    p->pArray = p->nCap? ALLOC( int, p->nCap ) : NULL;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the vector from an integer array of the given size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Msat_IntVec_t * Msat_IntVecAllocArray( int * pArray, int nSize )
+{
+    Msat_IntVec_t * p;
+    p = ALLOC( Msat_IntVec_t, 1 );
+    p->nSize  = nSize;
+    p->nCap   = nSize;
+    p->pArray = pArray;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the vector from an integer array of the given size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Msat_IntVec_t * Msat_IntVecAllocArrayCopy( int * pArray, int nSize )
+{
+    Msat_IntVec_t * p;
+    p = ALLOC( Msat_IntVec_t, 1 );
+    p->nSize  = nSize;
+    p->nCap   = nSize;
+    p->pArray = ALLOC( int, nSize );
+    memcpy( p->pArray, pArray, sizeof(int) * nSize );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the integer array.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Msat_IntVec_t * Msat_IntVecDup( Msat_IntVec_t * pVec )
+{
+    Msat_IntVec_t * p;
+    p = ALLOC( Msat_IntVec_t, 1 );
+    p->nSize  = pVec->nSize;
+    p->nCap   = pVec->nCap;
+    p->pArray = p->nCap? ALLOC( int, p->nCap ) : NULL;
+    memcpy( p->pArray, pVec->pArray, sizeof(int) * pVec->nSize );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transfers the array into another vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Msat_IntVec_t * Msat_IntVecDupArray( Msat_IntVec_t * pVec )
+{
+    Msat_IntVec_t * p;
+    p = ALLOC( Msat_IntVec_t, 1 );
+    p->nSize  = pVec->nSize;
+    p->nCap   = pVec->nCap;
+    p->pArray = pVec->pArray;
+    pVec->nSize  = 0;
+    pVec->nCap   = 0;
+    pVec->pArray = NULL;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_IntVecFree( Msat_IntVec_t * p )
+{
+    FREE( p->pArray );
+    FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Fills the vector with given number of entries.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_IntVecFill( Msat_IntVec_t * p, int nSize, int Entry )
+{
+    int i;
+    Msat_IntVecGrow( p, nSize );
+    p->nSize = nSize;
+    for ( i = 0; i < p->nSize; i++ )
+        p->pArray[i] = Entry;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int * Msat_IntVecReleaseArray( Msat_IntVec_t * p )
+{
+    int * pArray = p->pArray;
+    p->nCap = 0;
+    p->nSize = 0;
+    p->pArray = NULL;
+    return pArray;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int * Msat_IntVecReadArray( Msat_IntVec_t * p )
+{
+    return p->pArray;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Msat_IntVecReadSize( Msat_IntVec_t * p )
+{
+    return p->nSize;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Msat_IntVecReadEntry( Msat_IntVec_t * p, int i )
+{
+    assert( i >= 0 && i < p->nSize );
+    return p->pArray[i];
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_IntVecWriteEntry( Msat_IntVec_t * p, int i, int Entry )
+{
+    assert( i >= 0 && i < p->nSize );
+    p->pArray[i] = Entry;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Msat_IntVecReadEntryLast( Msat_IntVec_t * p )
+{
+    return p->pArray[p->nSize-1];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resizes the vector to the given capacity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_IntVecGrow( Msat_IntVec_t * p, int nCapMin )
+{
+    if ( p->nCap >= nCapMin )
+        return;
+    p->pArray = REALLOC( int, p->pArray, nCapMin ); 
+    p->nCap   = nCapMin;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_IntVecShrink( Msat_IntVec_t * p, int nSizeNew )
+{
+    assert( p->nSize >= nSizeNew );
+    p->nSize = nSizeNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_IntVecClear( Msat_IntVec_t * p )
+{
+    p->nSize = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_IntVecPush( Msat_IntVec_t * p, int Entry )
+{
+    if ( p->nSize == p->nCap )
+    {
+        if ( p->nCap < 16 )
+            Msat_IntVecGrow( p, 16 );
+        else
+            Msat_IntVecGrow( p, 2 * p->nCap );
+    }
+    p->pArray[p->nSize++] = Entry;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Add the element while ensuring uniqueness.]
+
+  Description [Returns 1 if the element was found, and 0 if it was new. ]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Msat_IntVecPushUnique( Msat_IntVec_t * p, int Entry )
+{
+    int i;
+    for ( i = 0; i < p->nSize; i++ )
+        if ( p->pArray[i] == Entry )
+            return 1;
+    Msat_IntVecPush( p, Entry );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts the element while sorting in the increasing order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_IntVecPushUniqueOrder( Msat_IntVec_t * p, int Entry, int fIncrease )
+{
+    int Entry1, Entry2;
+    int i;
+    Msat_IntVecPushUnique( p, Entry );
+    // find the p of the node
+    for ( i = p->nSize-1; i > 0; i-- )
+    {
+        Entry1 = p->pArray[i  ];
+        Entry2 = p->pArray[i-1];
+        if ( fIncrease && Entry1 >= Entry2 || 
+            !fIncrease && Entry1 <= Entry2 )
+            break;
+        p->pArray[i  ] = Entry2;
+        p->pArray[i-1] = Entry1;
+    }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the last entry and removes it from the list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Msat_IntVecPop( Msat_IntVec_t * p )
+{
+    assert( p->nSize > 0 );
+    return p->pArray[--p->nSize];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sorting the entries by their integer value.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Msat_IntVecSort( Msat_IntVec_t * p, int fReverse )
+{
+    if ( fReverse ) 
+        qsort( (void *)p->pArray, p->nSize, sizeof(int), 
+                (int (*)(const void *, const void *)) Msat_IntVecSortCompare2 );
+    else
+        qsort( (void *)p->pArray, p->nSize, sizeof(int), 
+                (int (*)(const void *, const void *)) Msat_IntVecSortCompare1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Comparison procedure for two clauses.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Msat_IntVecSortCompare1( int * pp1, int * pp2 )
+{
+    // for some reason commenting out lines (as shown) led to crashing of the release version
+    if ( *pp1 < *pp2 )
+        return -1;
+    if ( *pp1 > *pp2 ) //
+        return 1;
+    return 0; //
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Comparison procedure for two clauses.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Msat_IntVecSortCompare2( int * pp1, int * pp2 )
+{
+    // for some reason commenting out lines (as shown) led to crashing of the release version
+    if ( *pp1 > *pp2 )
+        return -1;
+    if ( *pp1 < *pp2 ) //
+        return 1;
+    return 0; //
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+