Version abc71001

11 files changed, 4153 insertions, 0 deletions

diff --git a/src/sat/bsat/module.make b/src/sat/bsat/module.make
new file mode 100644
index 00000000..563c8dfc
--- /dev/null
+++ b/src/sat/bsat/module.make
@@ -0,0 +1,6 @@
+SRC +=  src/sat/bsat/satMem.c \
+    src/sat/bsat/satInter.c \
+    src/sat/bsat/satSolver.c \
+    src/sat/bsat/satStore.c \
+    src/sat/bsat/satTrace.c \
+    src/sat/bsat/satUtil.c
diff --git a/src/sat/bsat/satInter.c b/src/sat/bsat/satInter.c
new file mode 100644
index 00000000..8759aa09
--- /dev/null
+++ b/src/sat/bsat/satInter.c
@@ -0,0 +1,991 @@
+/**CFile****************************************************************
+
+  FileName    [satInter.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT sat_solver.]
+
+  Synopsis    [Interpolation package.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: satInter.c,v 1.4 2005/09/16 22:55:03 casem Exp $]
+
+***********************************************************************/
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+#include <time.h>
+#include "satStore.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// variable assignments 
+static const lit    LIT_UNDEF = 0xffffffff;
+
+// interpolation manager
+struct Int_Man_t_
+{
+    // clauses of the problems
+    Sto_Man_t *     pCnf;         // the set of CNF clauses for A and B
+    // various parameters
+    int             fVerbose;     // verbosiness flag
+    int             fProofVerif;  // verifies the proof
+    int             fProofWrite;  // writes the proof file
+    int             nVarsAlloc;   // the allocated size of var arrays
+    int             nClosAlloc;   // the allocated size of clause arrays
+    // internal BCP
+    int             nRootSize;    // the number of root level assignments
+    int             nTrailSize;   // the number of assignments made 
+    lit *           pTrail;       // chronological order of assignments (size nVars)
+    lit *           pAssigns;     // assignments by variable (size nVars) 
+    char *          pSeens;       // temporary mark (size nVars)
+    Sto_Cls_t **    pReasons;     // reasons for each assignment (size nVars)          
+    Sto_Cls_t **    pWatches;     // watched clauses for each literal (size 2*nVars)          
+    // interpolation data
+    int             nVarsAB;      // the number of global variables
+    char *          pVarTypes;    // variable type (size nVars) [1=A, 0=B, <0=AB]
+    unsigned *      pInters;      // storage for interpolants as truth tables (size nClauses)
+    int             nIntersAlloc; // the allocated size of truth table array
+    int             nWords;       // the number of words in the truth table
+    // proof recording
+    int             Counter;      // counter of resolved clauses
+    int *           pProofNums;   // the proof numbers for each clause (size nClauses)
+    FILE *          pFile;        // the file for proof recording
+    // internal verification
+    lit *           pResLits;     // the literals of the resolvent   
+    int             nResLits;     // the number of literals of the resolvent
+    int             nResLitsAlloc;// the number of literals of the resolvent
+    // runtime stats
+    int             timeBcp;      // the runtime for BCP
+    int             timeTrace;    // the runtime of trace construction
+    int             timeTotal;    // the total runtime of interpolation
+};
+
+// procedure to get hold of the clauses' truth table 
+static inline unsigned * Int_ManTruthRead( Int_Man_t * p, Sto_Cls_t * pCls )          { return p->pInters + pCls->Id * p->nWords;                 }
+static inline void       Int_ManTruthClear( unsigned * p, int nWords )                { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i]  =  0;    }
+static inline void       Int_ManTruthFill( unsigned * p, int nWords )                 { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i]  = ~0;    }
+static inline void       Int_ManTruthCopy( unsigned * p, unsigned * q, int nWords )   { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i]  =  q[i]; }
+static inline void       Int_ManTruthAnd( unsigned * p, unsigned * q, int nWords )    { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] &=  q[i]; }
+static inline void       Int_ManTruthOr( unsigned * p, unsigned * q, int nWords )     { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] |=  q[i]; }
+static inline void       Int_ManTruthOrNot( unsigned * p, unsigned * q, int nWords )  { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] |= ~q[i]; }
+
+// reading/writing the proof for a clause
+static inline int        Int_ManProofGet( Int_Man_t * p, Sto_Cls_t * pCls )           { return p->pProofNums[pCls->Id];  }
+static inline void       Int_ManProofSet( Int_Man_t * p, Sto_Cls_t * pCls, int n )    { p->pProofNums[pCls->Id] = n;     }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocate proof manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Int_Man_t * Int_ManAlloc( int nVarsAlloc )
+{
+    Int_Man_t * p;
+    // allocate the manager
+    p = (Int_Man_t *)malloc( sizeof(Int_Man_t) );
+    memset( p, 0, sizeof(Int_Man_t) );
+    // verification
+    p->nResLitsAlloc = (1<<16);
+    p->pResLits = malloc( sizeof(lit) * p->nResLitsAlloc );
+    // parameters
+    p->fProofWrite = 0;
+    p->fProofVerif = 1;
+    return p;    
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Count common variables in the clauses of A and B.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Int_ManGlobalVars( Int_Man_t * p )
+{
+    Sto_Cls_t * pClause;
+    int Var, nVarsAB, v;
+
+    // mark the variable encountered in the clauses of A
+    Sto_ManForEachClauseRoot( p->pCnf, pClause )
+    {
+        if ( !pClause->fA )
+            break;
+        for ( v = 0; v < (int)pClause->nLits; v++ )
+            p->pVarTypes[lit_var(pClause->pLits[v])] = 1;
+    }
+
+    // check variables that appear in clauses of B
+    nVarsAB = 0;
+    Sto_ManForEachClauseRoot( p->pCnf, pClause )
+    {
+        if ( pClause->fA )
+            continue;
+        for ( v = 0; v < (int)pClause->nLits; v++ )
+        {
+            Var = lit_var(pClause->pLits[v]);
+            if ( p->pVarTypes[Var] == 1 ) // var of A
+            {
+                // change it into a global variable
+                nVarsAB++;
+                p->pVarTypes[Var] = -1;
+            }
+        }
+    }
+
+    // order global variables
+    nVarsAB = 0;
+    for ( v = 0; v < p->pCnf->nVars; v++ )
+        if ( p->pVarTypes[v] == -1 )
+            p->pVarTypes[v] -= nVarsAB++;
+//printf( "There are %d global variables.\n", nVarsAB );
+    return nVarsAB;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resize proof manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Int_ManResize( Int_Man_t * p )
+{
+    // check if resizing is needed
+    if ( p->nVarsAlloc < p->pCnf->nVars )
+    {
+        // find the new size
+        if ( p->nVarsAlloc == 0 )
+            p->nVarsAlloc = 1;
+        while ( p->nVarsAlloc < p->pCnf->nVars ) 
+            p->nVarsAlloc *= 2;
+        // resize the arrays
+        p->pTrail    = (lit *)       realloc( p->pTrail,    sizeof(lit) * p->nVarsAlloc );
+        p->pAssigns  = (lit *)       realloc( p->pAssigns,  sizeof(lit) * p->nVarsAlloc );
+        p->pSeens    = (char *)      realloc( p->pSeens,    sizeof(char) * p->nVarsAlloc );
+        p->pVarTypes = (char *)      realloc( p->pVarTypes, sizeof(char) * p->nVarsAlloc );
+        p->pReasons  = (Sto_Cls_t **)realloc( p->pReasons,  sizeof(Sto_Cls_t *) * p->nVarsAlloc );
+        p->pWatches  = (Sto_Cls_t **)realloc( p->pWatches,  sizeof(Sto_Cls_t *) * p->nVarsAlloc*2 );
+    }
+
+    // clean the free space
+    memset( p->pAssigns , 0xff, sizeof(lit) * p->pCnf->nVars );
+    memset( p->pSeens   , 0,    sizeof(char) * p->pCnf->nVars );
+    memset( p->pVarTypes, 0,    sizeof(char) * p->pCnf->nVars );
+    memset( p->pReasons , 0,    sizeof(Sto_Cls_t *) * p->pCnf->nVars );
+    memset( p->pWatches , 0,    sizeof(Sto_Cls_t *) * p->pCnf->nVars*2 );
+
+    // compute the number of common variables
+    p->nVarsAB = Int_ManGlobalVars( p );
+    // compute the number of words in the truth table
+    p->nWords = (p->nVarsAB <= 5 ? 1 : (1 << (p->nVarsAB - 5)));
+
+    // check if resizing of clauses is needed
+    if ( p->nClosAlloc < p->pCnf->nClauses )
+    {
+        // find the new size
+        if ( p->nClosAlloc == 0 )
+            p->nClosAlloc = 1;
+        while ( p->nClosAlloc < p->pCnf->nClauses ) 
+            p->nClosAlloc *= 2;
+        // resize the arrays
+        p->pProofNums = (int *) realloc( p->pProofNums,  sizeof(int) * p->nClosAlloc );
+    }
+    memset( p->pProofNums, 0, sizeof(int) * p->pCnf->nClauses );
+
+    // check if resizing of truth tables is needed
+    if ( p->nIntersAlloc < p->nWords * p->pCnf->nClauses )
+    {
+        p->nIntersAlloc = p->nWords * p->pCnf->nClauses;
+        p->pInters = (unsigned *) realloc( p->pInters, sizeof(unsigned) * p->nIntersAlloc );
+    }
+//    memset( p->pInters, 0, sizeof(unsigned) * p->nWords * p->pCnf->nClauses );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocate proof manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Int_ManFree( Int_Man_t * p )
+{
+/*
+    printf( "Runtime stats:\n" );
+PRT( "BCP     ", p->timeBcp   );
+PRT( "Trace   ", p->timeTrace );
+PRT( "TOTAL   ", p->timeTotal );
+*/
+    free( p->pInters );
+    free( p->pProofNums );
+    free( p->pTrail );
+    free( p->pAssigns );
+    free( p->pSeens );
+    free( p->pVarTypes );
+    free( p->pReasons );
+    free( p->pWatches );
+    free( p->pResLits );
+    free( p );
+}
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Int_ManPrintClause( Int_Man_t * p, Sto_Cls_t * pClause )
+{
+    int i;
+    printf( "Clause ID = %d. Proof = %d. {", pClause->Id, Int_ManProofGet(p, pClause) );
+    for ( i = 0; i < (int)pClause->nLits; i++ )
+        printf( " %d", pClause->pLits[i] );
+    printf( " }\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the resolvent.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Int_ManPrintResolvent( lit * pResLits, int nResLits )
+{
+    int i;
+    printf( "Resolvent: {" );
+    for ( i = 0; i < nResLits; i++ )
+        printf( " %d", pResLits[i] );
+    printf( " }\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Records the proof.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_PrintBinary__( FILE * pFile, unsigned Sign[], int nBits )
+{
+    int Remainder, nWords;
+    int w, i;
+
+    Remainder = (nBits%(sizeof(unsigned)*8));
+    nWords    = (nBits/(sizeof(unsigned)*8)) + (Remainder>0);
+
+    for ( w = nWords-1; w >= 0; w-- )
+        for ( i = ((w == nWords-1 && Remainder)? Remainder-1: 31); i >= 0; i-- )
+            fprintf( pFile, "%c", '0' + (int)((Sign[w] & (1<<i)) > 0) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the interpolant for one clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Int_ManPrintInterOne( Int_Man_t * p, Sto_Cls_t * pClause )
+{
+    printf( "Clause %2d :  ", pClause->Id );
+    Extra_PrintBinary__( stdout, Int_ManTruthRead(p, pClause), (1 << p->nVarsAB) );
+    printf( "\n" );
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Adds one clause to the watcher list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Int_ManWatchClause( Int_Man_t * p, Sto_Cls_t * pClause, lit Lit )
+{
+    assert( lit_check(Lit, p->pCnf->nVars) );
+    if ( pClause->pLits[0] == Lit )
+        pClause->pNext0 = p->pWatches[lit_neg(Lit)];  
+    else
+    {
+        assert( pClause->pLits[1] == Lit );
+        pClause->pNext1 = p->pWatches[lit_neg(Lit)];  
+    }
+    p->pWatches[lit_neg(Lit)] = pClause;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Records implication.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Int_ManEnqueue( Int_Man_t * p, lit Lit, Sto_Cls_t * pReason )
+{
+    int Var = lit_var(Lit);
+    if ( p->pAssigns[Var] != LIT_UNDEF )
+        return p->pAssigns[Var] == Lit;
+    p->pAssigns[Var] = Lit;
+    p->pReasons[Var] = pReason;
+    p->pTrail[p->nTrailSize++] = Lit;
+//printf( "assigning var %d value %d\n", Var, !lit_sign(Lit) );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Records implication.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Int_ManCancelUntil( Int_Man_t * p, int Level )
+{
+    lit Lit;
+    int i, Var;
+    for ( i = p->nTrailSize - 1; i >= Level; i-- )
+    {
+        Lit = p->pTrail[i];
+        Var = lit_var( Lit );
+        p->pReasons[Var] = NULL;
+        p->pAssigns[Var] = LIT_UNDEF;
+//printf( "cancelling var %d\n", Var );
+    }
+    p->nTrailSize = Level;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Propagate one assignment.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Sto_Cls_t * Int_ManPropagateOne( Int_Man_t * p, lit Lit )
+{
+    Sto_Cls_t ** ppPrev, * pCur, * pTemp;
+    lit LitF = lit_neg(Lit);
+    int i;
+    // iterate through the literals
+    ppPrev = p->pWatches + Lit;
+    for ( pCur = p->pWatches[Lit]; pCur; pCur = *ppPrev )
+    {
+        // make sure the false literal is in the second literal of the clause
+        if ( pCur->pLits[0] == LitF )
+        {
+            pCur->pLits[0] = pCur->pLits[1];
+            pCur->pLits[1] = LitF;
+            pTemp = pCur->pNext0;
+            pCur->pNext0 = pCur->pNext1;
+            pCur->pNext1 = pTemp;
+        }
+        assert( pCur->pLits[1] == LitF );
+
+        // if the first literal is true, the clause is satisfied
+        if ( pCur->pLits[0] == p->pAssigns[lit_var(pCur->pLits[0])] )
+        {
+            ppPrev = &pCur->pNext1;
+            continue;
+        }
+
+        // look for a new literal to watch
+        for ( i = 2; i < (int)pCur->nLits; i++ )
+        {
+            // skip the case when the literal is false
+            if ( lit_neg(pCur->pLits[i]) == p->pAssigns[lit_var(pCur->pLits[i])] )
+                continue;
+            // the literal is either true or unassigned - watch it
+            pCur->pLits[1] = pCur->pLits[i];
+            pCur->pLits[i] = LitF;
+            // remove this clause from the watch list of Lit
+            *ppPrev = pCur->pNext1;
+            // add this clause to the watch list of pCur->pLits[i] (now it is pCur->pLits[1])
+            Int_ManWatchClause( p, pCur, pCur->pLits[1] );
+            break;
+        }
+        if ( i < (int)pCur->nLits ) // found new watch
+            continue;
+
+        // clause is unit - enqueue new implication
+        if ( Int_ManEnqueue(p, pCur->pLits[0], pCur) )
+        {
+            ppPrev = &pCur->pNext1;
+            continue;
+        }
+
+        // conflict detected - return the conflict clause
+        return pCur;
+    }
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Propagate the current assignments.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Sto_Cls_t * Int_ManPropagate( Int_Man_t * p, int Start )
+{
+    Sto_Cls_t * pClause;
+    int i;
+    int clk = clock();
+    for ( i = Start; i < p->nTrailSize; i++ )
+    {
+        pClause = Int_ManPropagateOne( p, p->pTrail[i] );
+        if ( pClause )
+        {
+p->timeBcp += clock() - clk;
+            return pClause;
+        }
+    }
+p->timeBcp += clock() - clk;
+    return NULL;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Writes one root clause into a file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Int_ManProofWriteOne( Int_Man_t * p, Sto_Cls_t * pClause )
+{
+    Int_ManProofSet( p, pClause, ++p->Counter );
+
+    if ( p->fProofWrite )
+    {
+        int v;
+        fprintf( p->pFile, "%d", Int_ManProofGet(p, pClause) );
+        for ( v = 0; v < (int)pClause->nLits; v++ )
+            fprintf( p->pFile, " %d", lit_print(pClause->pLits[v]) );
+        fprintf( p->pFile, " 0 0\n" );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Traces the proof for one clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Int_ManProofTraceOne( Int_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pFinal )
+{
+    Sto_Cls_t * pReason;
+    int i, v, Var, PrevId;
+    int fPrint = 0;
+    int clk = clock();
+
+    // collect resolvent literals
+    if ( p->fProofVerif )
+    {
+        assert( (int)pConflict->nLits <= p->nResLitsAlloc );
+        memcpy( p->pResLits, pConflict->pLits, sizeof(lit) * pConflict->nLits );
+        p->nResLits = pConflict->nLits;
+    }
+
+    // mark all the variables in the conflict as seen
+    for ( v = 0; v < (int)pConflict->nLits; v++ )
+        p->pSeens[lit_var(pConflict->pLits[v])] = 1;
+
+    // start the anticedents
+//    pFinal->pAntis = Vec_PtrAlloc( 32 );
+//    Vec_PtrPush( pFinal->pAntis, pConflict );
+
+    if ( p->pCnf->nClausesA )
+        Int_ManTruthCopy( Int_ManTruthRead(p, pFinal), Int_ManTruthRead(p, pConflict), p->nWords );
+
+    // follow the trail backwards
+    PrevId = Int_ManProofGet(p, pConflict);
+    for ( i = p->nTrailSize - 1; i >= 0; i-- )
+    {
+        // skip literals that are not involved
+        Var = lit_var(p->pTrail[i]);
+        if ( !p->pSeens[Var] )
+            continue;
+        p->pSeens[Var] = 0;
+
+        // skip literals of the resulting clause
+        pReason = p->pReasons[Var];
+        if ( pReason == NULL )
+            continue;
+        assert( p->pTrail[i] == pReason->pLits[0] );
+
+        // add the variables to seen
+        for ( v = 1; v < (int)pReason->nLits; v++ )
+            p->pSeens[lit_var(pReason->pLits[v])] = 1;
+
+
+        // record the reason clause
+        assert( Int_ManProofGet(p, pReason) > 0 );
+        p->Counter++;
+        if ( p->fProofWrite )
+            fprintf( p->pFile, "%d * %d %d 0\n", p->Counter, PrevId, Int_ManProofGet(p, pReason) );
+        PrevId = p->Counter;
+
+        if ( p->pCnf->nClausesA )
+        {
+            if ( p->pVarTypes[Var] == 1 ) // var of A
+                Int_ManTruthOr( Int_ManTruthRead(p, pFinal), Int_ManTruthRead(p, pReason), p->nWords );
+            else
+                Int_ManTruthAnd( Int_ManTruthRead(p, pFinal), Int_ManTruthRead(p, pReason), p->nWords );
+        }
+ 
+        // resolve the temporary resolvent with the reason clause
+        if ( p->fProofVerif )
+        {
+            int v1, v2; 
+            if ( fPrint )
+                Int_ManPrintResolvent( p->pResLits, p->nResLits );
+            // check that the var is present in the resolvent
+            for ( v1 = 0; v1 < p->nResLits; v1++ )
+                if ( lit_var(p->pResLits[v1]) == Var )
+                    break;
+            if ( v1 == p->nResLits )
+                printf( "Recording clause %d: Cannot find variable %d in the temporary resolvent.\n", pFinal->Id, Var );
+            if ( p->pResLits[v1] != lit_neg(pReason->pLits[0]) )
+                printf( "Recording clause %d: The resolved variable %d is in the wrong polarity.\n", pFinal->Id, Var );
+            // remove this variable from the resolvent
+            assert( lit_var(p->pResLits[v1]) == Var );
+            p->nResLits--;
+            for ( ; v1 < p->nResLits; v1++ )
+                p->pResLits[v1] = p->pResLits[v1+1];
+            // add variables of the reason clause
+            for ( v2 = 1; v2 < (int)pReason->nLits; v2++ )
+            {
+                for ( v1 = 0; v1 < p->nResLits; v1++ )
+                    if ( lit_var(p->pResLits[v1]) == lit_var(pReason->pLits[v2]) )
+                        break;
+                // if it is a new variable, add it to the resolvent
+                if ( v1 == p->nResLits ) 
+                {
+                    if ( p->nResLits == p->nResLitsAlloc )
+                        printf( "Recording clause %d: Ran out of space for intermediate resolvent.\n", pFinal->Id );
+                    p->pResLits[ p->nResLits++ ] = pReason->pLits[v2];
+                    continue;
+                }
+                // if the variable is the same, the literal should be the same too
+                if ( p->pResLits[v1] == pReason->pLits[v2] )
+                    continue;
+                // the literal is different
+                printf( "Recording clause %d: Trying to resolve the clause with more than one opposite literal.\n", pFinal->Id );
+            }
+        }
+
+//        Vec_PtrPush( pFinal->pAntis, pReason );
+    }
+
+    // unmark all seen variables
+//    for ( i = p->nTrailSize - 1; i >= 0; i-- )
+//        p->pSeens[lit_var(p->pTrail[i])] = 0;
+    // check that the literals are unmarked
+//    for ( i = p->nTrailSize - 1; i >= 0; i-- )
+//        assert( p->pSeens[lit_var(p->pTrail[i])] == 0 );
+
+    // use the resulting clause to check the correctness of resolution
+    if ( p->fProofVerif )
+    {
+        int v1, v2; 
+        if ( fPrint )
+            Int_ManPrintResolvent( p->pResLits, p->nResLits );
+        for ( v1 = 0; v1 < p->nResLits; v1++ )
+        {
+            for ( v2 = 0; v2 < (int)pFinal->nLits; v2++ )
+                if ( pFinal->pLits[v2] == p->pResLits[v1] )
+                    break;
+            if ( v2 < (int)pFinal->nLits )
+                continue;
+            break;
+        }
+        if ( v1 < p->nResLits )
+        {
+            printf( "Recording clause %d: The final resolvent is wrong.\n", pFinal->Id );
+            Int_ManPrintClause( p, pConflict );
+            Int_ManPrintResolvent( p->pResLits, p->nResLits );
+            Int_ManPrintClause( p, pFinal );
+        }
+    }
+p->timeTrace += clock() - clk;
+
+    // return the proof pointer 
+    if ( p->pCnf->nClausesA )
+    {
+//        Int_ManPrintInterOne( p, pFinal );
+    }
+    Int_ManProofSet( p, pFinal, p->Counter );
+    return p->Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Records the proof for one clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Int_ManProofRecordOne( Int_Man_t * p, Sto_Cls_t * pClause )
+{
+    Sto_Cls_t * pConflict;
+    int i;
+
+    // empty clause never ends up there
+    assert( pClause->nLits > 0 );
+    if ( pClause->nLits == 0 )
+        printf( "Error: Empty clause is attempted.\n" );
+
+    // add assumptions to the trail
+    assert( !pClause->fRoot );
+    assert( p->nTrailSize == p->nRootSize );
+    for ( i = 0; i < (int)pClause->nLits; i++ )
+        if ( !Int_ManEnqueue( p, lit_neg(pClause->pLits[i]), NULL ) )
+        {
+            assert( 0 ); // impossible
+            return 0;
+        }
+
+    // propagate the assumptions
+    pConflict = Int_ManPropagate( p, p->nRootSize );
+    if ( pConflict == NULL )
+    {
+        assert( 0 ); // cannot prove
+        return 0;
+    }
+
+    // construct the proof
+    Int_ManProofTraceOne( p, pConflict, pClause );
+
+    // undo to the root level
+    Int_ManCancelUntil( p, p->nRootSize );
+
+    // add large clauses to the watched lists
+    if ( pClause->nLits > 1 )
+    {
+        Int_ManWatchClause( p, pClause, pClause->pLits[0] );
+        Int_ManWatchClause( p, pClause, pClause->pLits[1] );
+        return 1;
+    }
+    assert( pClause->nLits == 1 );
+
+    // if the clause proved is unit, add it and propagate
+    if ( !Int_ManEnqueue( p, pClause->pLits[0], pClause ) )
+    {
+        assert( 0 ); // impossible
+        return 0;
+    }
+
+    // propagate the assumption
+    pConflict = Int_ManPropagate( p, p->nRootSize );
+    if ( pConflict )
+    {
+        // construct the proof
+        Int_ManProofTraceOne( p, pConflict, p->pCnf->pEmpty );
+        if ( p->fVerbose )
+            printf( "Found last conflict after adding unit clause number %d!\n", pClause->Id );
+        return 0;
+    }
+
+    // update the root level
+    p->nRootSize = p->nTrailSize;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Propagate the root clauses.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Int_ManProcessRoots( Int_Man_t * p )
+{
+    Sto_Cls_t * pClause;
+    int Counter;
+
+    // make sure the root clauses are preceeding the learnt clauses
+    Counter = 0;
+    Sto_ManForEachClause( p->pCnf, pClause )
+    {
+        assert( (int)pClause->fA    == (Counter < (int)p->pCnf->nClausesA) );
+        assert( (int)pClause->fRoot == (Counter < (int)p->pCnf->nRoots)    );
+        Counter++;
+    }
+    assert( p->pCnf->nClauses == Counter );
+
+    // make sure the last clause if empty
+    assert( p->pCnf->pTail->nLits == 0 );
+
+    // go through the root unit clauses
+    p->nTrailSize = 0;
+    Sto_ManForEachClauseRoot( p->pCnf, pClause )
+    {
+        // create watcher lists for the root clauses
+        if ( pClause->nLits > 1 )
+        {
+            Int_ManWatchClause( p, pClause, pClause->pLits[0] );
+            Int_ManWatchClause( p, pClause, pClause->pLits[1] );
+        }
+        // empty clause and large clauses
+        if ( pClause->nLits != 1 )
+            continue;
+        // unit clause
+        assert( lit_check(pClause->pLits[0], p->pCnf->nVars) );
+        if ( !Int_ManEnqueue( p, pClause->pLits[0], pClause ) )
+        {
+            // detected root level conflict
+            printf( "Error in Int_ManProcessRoots(): Detected a root-level conflict too early!\n" );
+            assert( 0 );
+            return 0;
+        }
+    }
+
+    // propagate the root unit clauses
+    pClause = Int_ManPropagate( p, 0 );
+    if ( pClause )
+    {
+        // detected root level conflict
+        Int_ManProofTraceOne( p, pClause, p->pCnf->pEmpty );
+        if ( p->fVerbose )
+            printf( "Found root level conflict!\n" );
+        return 0;
+    }
+
+    // set the root level
+    p->nRootSize = p->nTrailSize;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Records the proof.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Int_ManPrepareInter( Int_Man_t * p )
+{
+    // elementary truth tables
+    unsigned uTruths[8][8] = {
+        { 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA },
+        { 0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC },
+        { 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 },
+        { 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 },
+        { 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 }, 
+        { 0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF }, 
+        { 0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF }, 
+        { 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF } 
+    };
+    Sto_Cls_t * pClause;
+    int Var, VarAB, v;
+    assert( p->nVarsAB <= 8 );
+
+    // set interpolants for root clauses
+    Sto_ManForEachClauseRoot( p->pCnf, pClause )
+    {
+        if ( !pClause->fA ) // clause of B
+        {
+            Int_ManTruthFill( Int_ManTruthRead(p, pClause), p->nWords );
+//            Int_ManPrintInterOne( p, pClause );
+            continue;
+        }
+        // clause of A
+        Int_ManTruthClear( Int_ManTruthRead(p, pClause), p->nWords );
+        for ( v = 0; v < (int)pClause->nLits; v++ )
+        {
+            Var = lit_var(pClause->pLits[v]);
+            if ( p->pVarTypes[Var] < 0 ) // global var
+            {
+                VarAB = -p->pVarTypes[Var]-1;
+                assert( VarAB >= 0 && VarAB < p->nVarsAB );
+                if ( lit_sign(pClause->pLits[v]) ) // negative var
+                    Int_ManTruthOrNot( Int_ManTruthRead(p, pClause), uTruths[VarAB], p->nWords );
+                else
+                    Int_ManTruthOr( Int_ManTruthRead(p, pClause), uTruths[VarAB], p->nWords );
+            }
+        }
+//        Int_ManPrintInterOne( p, pClause );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes interpolant for the given CNF.]
+
+  Description [Returns the number of common variable found and interpolant.
+  Returns 0, if something did not work.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned ** ppResult )
+{
+    Sto_Cls_t * pClause;
+    int RetValue = 1;
+    int clkTotal = clock();
+
+    // check that the CNF makes sense
+    assert( pCnf->nVars > 0 && pCnf->nClauses > 0 );
+    p->pCnf = pCnf;
+    p->fVerbose = fVerbose;
+    *ppResult = NULL;
+
+    // adjust the manager
+    Int_ManResize( p );
+
+    // prepare the interpolant computation
+    Int_ManPrepareInter( p );
+
+    // construct proof for each clause
+    // start the proof
+    if ( p->fProofWrite )
+    {
+        p->pFile = fopen( "proof.cnf_", "w" );
+        p->Counter = 0;
+    }
+
+    // write the root clauses
+    Sto_ManForEachClauseRoot( p->pCnf, pClause )
+        Int_ManProofWriteOne( p, pClause );
+
+    // propagate root level assignments
+    if ( Int_ManProcessRoots( p ) )
+    {
+        // if there is no conflict, consider learned clauses
+        Sto_ManForEachClause( p->pCnf, pClause )
+        {
+            if ( pClause->fRoot )
+                continue;
+            if ( !Int_ManProofRecordOne( p, pClause ) )
+            {
+                RetValue = 0;
+                break;
+            }
+        }
+    }
+
+    // stop the proof
+    if ( p->fProofWrite )
+    {
+        fclose( p->pFile );
+        p->pFile = NULL;    
+    }
+
+    if ( fVerbose )
+    {
+    printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d.  Ave = %.2f.  Mem = %.2f Mb\n", 
+        p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter,  
+        1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots), 
+        1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) );
+p->timeTotal += clock() - clkTotal;
+    }
+
+    *ppResult = Int_ManTruthRead( p, p->pCnf->pTail );
+    return p->nVarsAB;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/bsat/satMem.c b/src/sat/bsat/satMem.c
new file mode 100644
index 00000000..7fa1a824
--- /dev/null
+++ b/src/sat/bsat/satMem.c
@@ -0,0 +1,527 @@
+/**CFile****************************************************************
+
+  FileName    [satMem.c]
+
+  PackageName [SAT solver.]
+
+  Synopsis    [Memory management.]
+
+  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 1, 2004.]
+
+  Revision    [$Id: satMem.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "satMem.h"
+#include "vec.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+struct Sat_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 Sat_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 Sat_MmStep_t_
+{
+    int                nMems;    // the number of fixed memory managers employed
+    Sat_MmFixed_t **  pMems;    // memory managers: 2^1 words, 2^2 words, etc
+    int                nMapSize; // the size of the memory array
+    Sat_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     []
+
+***********************************************************************/
+Sat_MmFixed_t * Sat_MmFixedStart( int nEntrySize )
+{
+    Sat_MmFixed_t * p;
+
+    p = ALLOC( Sat_MmFixed_t, 1 );
+    memset( p, 0, sizeof(Sat_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 Sat_MmFixedStop( Sat_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 * Sat_MmFixedEntryFetch( Sat_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 Sat_MmFixedEntryRecycle( Sat_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 Sat_MmFixedRestart( Sat_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 Sat_MmFixedReadMemUsage( Sat_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     []
+
+***********************************************************************/
+Sat_MmFlex_t * Sat_MmFlexStart()
+{
+    Sat_MmFlex_t * p;
+
+    p = ALLOC( Sat_MmFlex_t, 1 );
+    memset( p, 0, sizeof(Sat_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 Sat_MmFlexStop( Sat_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 * Sat_MmFlexEntryFetch( Sat_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 Sat_MmFlexReadMemUsage( Sat_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     []
+
+***********************************************************************/
+Sat_MmStep_t * Sat_MmStepStart( int nSteps )
+{
+    Sat_MmStep_t * p;
+    int i, k;
+    p = ALLOC( Sat_MmStep_t, 1 );
+    p->nMems = nSteps;
+    // start the fixed memory managers
+    p->pMems = ALLOC( Sat_MmFixed_t *, p->nMems );
+    for ( i = 0; i < p->nMems; i++ )
+        p->pMems[i] = Sat_MmFixedStart( (8<<i) );
+    // set up the mapping of the required memory size into the corresponding manager
+    p->nMapSize = (4<<p->nMems);
+    p->pMap = ALLOC( Sat_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 Sat_MmStepStop( Sat_MmStep_t * p, int fVerbose )
+{
+    int i;
+    for ( i = 0; i < p->nMems; i++ )
+        Sat_MmFixedStop( p->pMems[i], fVerbose );
+    free( p->pMems );
+    free( p->pMap );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the entry.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Sat_MmStepEntryFetch( Sat_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 Sat_MmFixedEntryFetch( p->pMap[nBytes] );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Recycles the entry.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sat_MmStepEntryRecycle( Sat_MmStep_t * p, char * pEntry, int nBytes )
+{
+    if ( nBytes == 0 )
+        return;
+    if ( nBytes > p->nMapSize )
+    {
+        free( pEntry );
+        return;
+    }
+    Sat_MmFixedEntryRecycle( p->pMap[nBytes], pEntry );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sat_MmStepReadMemUsage( Sat_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/bsat/satMem.h b/src/sat/bsat/satMem.h
new file mode 100644
index 00000000..22b7a87c
--- /dev/null
+++ b/src/sat/bsat/satMem.h
@@ -0,0 +1,80 @@
+/**CFile****************************************************************
+
+  FileName    [satMem.h]
+
+  PackageName [SAT solver.]
+
+  Synopsis    [Memory management.]
+
+  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 1, 2004.]
+
+  Revision    [$Id: satMem.h,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __SAT_MEM_H__
+#define __SAT_MEM_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+//#include "leaks.h"       
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    STRUCTURE DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Sat_MmFixed_t_ Sat_MmFixed_t;
+typedef struct Sat_MmFlex_t_  Sat_MmFlex_t;
+typedef struct Sat_MmStep_t_  Sat_MmStep_t;
+
+////////////////////////////////////////////////////////////////////////
+///                       GLOBAL VARIABLES                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                       MACRO DEFINITIONS                          ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DECLARATIONS                        ///
+////////////////////////////////////////////////////////////////////////
+
+// fixed-size-block memory manager
+extern Sat_MmFixed_t *     Sat_MmFixedStart( int nEntrySize );
+extern void                Sat_MmFixedStop( Sat_MmFixed_t * p, int fVerbose );
+extern char *              Sat_MmFixedEntryFetch( Sat_MmFixed_t * p );
+extern void                Sat_MmFixedEntryRecycle( Sat_MmFixed_t * p, char * pEntry );
+extern void                Sat_MmFixedRestart( Sat_MmFixed_t * p );
+extern int                 Sat_MmFixedReadMemUsage( Sat_MmFixed_t * p );
+// flexible-size-block memory manager
+extern Sat_MmFlex_t *      Sat_MmFlexStart();
+extern void                Sat_MmFlexStop( Sat_MmFlex_t * p, int fVerbose );
+extern char *              Sat_MmFlexEntryFetch( Sat_MmFlex_t * p, int nBytes );
+extern int                 Sat_MmFlexReadMemUsage( Sat_MmFlex_t * p );
+// hierarchical memory manager
+extern Sat_MmStep_t *      Sat_MmStepStart( int nSteps );
+extern void                Sat_MmStepStop( Sat_MmStep_t * p, int fVerbose );
+extern char *              Sat_MmStepEntryFetch( Sat_MmStep_t * p, int nBytes );
+extern void                Sat_MmStepEntryRecycle( Sat_MmStep_t * p, char * pEntry, int nBytes );
+extern int                 Sat_MmStepReadMemUsage( Sat_MmStep_t * p );
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
new file mode 100644
index 00000000..fbc9874d
--- /dev/null
+++ b/src/sat/bsat/satSolver.c
@@ -0,0 +1,1358 @@
+/**************************************************************************************************
+MiniSat -- Copyright (c) 2005, Niklas Sorensson
+http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko
+
+#include <stdio.h>
+#include <assert.h>
+#include <string.h>
+#include <math.h>
+
+#include "satSolver.h"
+
+//#define SAT_USE_SYSTEM_MEMORY_MANAGEMENT
+
+//=================================================================================================
+// Debug:
+
+//#define VERBOSEDEBUG
+
+// For derivation output (verbosity level 2)
+#define L_IND    "%-*d"
+#define L_ind    sat_solver_dlevel(s)*3+3,sat_solver_dlevel(s)
+#define L_LIT    "%sx%d"
+#define L_lit(p) lit_sign(p)?"~":"", (lit_var(p))
+
+// Just like 'assert()' but expression will be evaluated in the release version as well.
+static inline void check(int expr) { assert(expr); }
+
+static void printlits(lit* begin, lit* end)
+{
+    int i;
+    for (i = 0; i < end - begin; i++)
+        printf(L_LIT" ",L_lit(begin[i]));
+}
+
+//=================================================================================================
+// Random numbers:
+
+
+// Returns a random float 0 <= x < 1. Seed must never be 0.
+static inline double drand(double* seed) {
+    int q;
+    *seed *= 1389796;
+    q = (int)(*seed / 2147483647);
+    *seed -= (double)q * 2147483647;
+    return *seed / 2147483647; }
+
+
+// Returns a random integer 0 <= x < size. Seed must never be 0.
+static inline int irand(double* seed, int size) {
+    return (int)(drand(seed) * size); }
+
+
+//=================================================================================================
+// Predeclarations:
+
+static void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *));
+
+//=================================================================================================
+// Clause datatype + minor functions:
+
+struct clause_t
+{
+    int size_learnt;
+    lit lits[0];
+};
+
+static inline int   clause_size       (clause* c)          { return c->size_learnt >> 1; }
+static inline lit*  clause_begin      (clause* c)          { return c->lits; }
+static inline int   clause_learnt     (clause* c)          { return c->size_learnt & 1; }
+static inline float clause_activity   (clause* c)          { return *((float*)&c->lits[c->size_learnt>>1]); }
+static inline void  clause_setactivity(clause* c, float a) { *((float*)&c->lits[c->size_learnt>>1]) = a; }
+
+//=================================================================================================
+// Encode literals in clause pointers:
+
+static inline clause* clause_from_lit (lit l)     { return (clause*)((unsigned long)l + (unsigned long)l + 1);  }
+static inline bool    clause_is_lit   (clause* c) { return ((unsigned long)c & 1);                              }
+static inline lit     clause_read_lit (clause* c) { return (lit)((unsigned long)c >> 1);                        }
+
+//=================================================================================================
+// Simple helpers:
+
+static inline int     sat_solver_dlevel(sat_solver* s)            { return veci_size(&s->trail_lim); }
+static inline vecp*   sat_solver_read_wlist(sat_solver* s, lit l) { return &s->wlists[l]; }
+static inline void    vecp_remove(vecp* v, void* e)
+{
+    void** ws = vecp_begin(v);
+    int    j  = 0;
+    for (; ws[j] != e  ; j++);
+    assert(j < vecp_size(v));
+    for (; j < vecp_size(v)-1; j++) ws[j] = ws[j+1];
+    vecp_resize(v,vecp_size(v)-1);
+}
+
+//=================================================================================================
+// Variable order functions:
+
+static inline void order_update(sat_solver* s, int v) // updateorder
+{
+    int*    orderpos = s->orderpos;
+    double* activity = s->activity;
+    int*    heap     = veci_begin(&s->order);
+    int     i        = orderpos[v];
+    int     x        = heap[i];
+    int     parent   = (i - 1) / 2;
+
+    assert(s->orderpos[v] != -1);
+
+    while (i != 0 && activity[x] > activity[heap[parent]]){
+        heap[i]           = heap[parent];
+        orderpos[heap[i]] = i;
+        i                 = parent;
+        parent            = (i - 1) / 2;
+    }
+    heap[i]     = x;
+    orderpos[x] = i;
+}
+
+static inline void order_assigned(sat_solver* s, int v) 
+{
+}
+
+static inline void order_unassigned(sat_solver* s, int v) // undoorder
+{
+    int* orderpos = s->orderpos;
+    if (orderpos[v] == -1){
+        orderpos[v] = veci_size(&s->order);
+        veci_push(&s->order,v);
+        order_update(s,v);
+//printf( "+%d ", v );
+    }
+}
+
+static inline int  order_select(sat_solver* s, float random_var_freq) // selectvar
+{
+    int*    heap;
+    double* activity;
+    int*    orderpos;
+
+    lbool* values = s->assigns;
+
+    // Random decision:
+    if (drand(&s->random_seed) < random_var_freq){
+        int next = irand(&s->random_seed,s->size);
+        assert(next >= 0 && next < s->size);
+        if (values[next] == l_Undef)
+            return next;
+    }
+
+    // Activity based decision:
+
+    heap     = veci_begin(&s->order);
+    activity = s->activity;
+    orderpos = s->orderpos;
+
+
+    while (veci_size(&s->order) > 0){
+        int    next  = heap[0];
+        int    size  = veci_size(&s->order)-1;
+        int    x     = heap[size];
+
+        veci_resize(&s->order,size);
+
+        orderpos[next] = -1;
+
+        if (size > 0){
+            double act   = activity[x];
+
+            int    i     = 0;
+            int    child = 1;
+
+
+            while (child < size){
+                if (child+1 < size && activity[heap[child]] < activity[heap[child+1]])
+                    child++;
+
+                assert(child < size);
+
+                if (act >= activity[heap[child]])
+                    break;
+
+                heap[i]           = heap[child];
+                orderpos[heap[i]] = i;
+                i                 = child;
+                child             = 2 * child + 1;
+            }
+            heap[i]           = x;
+            orderpos[heap[i]] = i;
+        }
+
+//printf( "-%d ", next );
+        if (values[next] == l_Undef)
+            return next;
+    }
+
+    return var_Undef;
+}
+
+//=================================================================================================
+// Activity functions:
+
+static inline void act_var_rescale(sat_solver* s) {
+    double* activity = s->activity;
+    int i;
+    for (i = 0; i < s->size; i++)
+        activity[i] *= 1e-100;
+    s->var_inc *= 1e-100;
+}
+
+static inline void act_var_bump(sat_solver* s, int v) {
+    s->activity[v] += s->var_inc;
+    if (s->activity[v] > 1e100)
+        act_var_rescale(s);
+    //printf("bump %d %f\n", v-1, activity[v]);
+    if (s->orderpos[v] != -1)
+        order_update(s,v);
+}
+
+static inline void act_var_bump_factor(sat_solver* s, int v) {
+    s->activity[v] += (s->var_inc * s->factors[v]);
+    if (s->activity[v] > 1e100)
+        act_var_rescale(s);
+    //printf("bump %d %f\n", v-1, activity[v]);
+    if (s->orderpos[v] != -1)
+        order_update(s,v);
+}
+
+static inline void act_var_decay(sat_solver* s) { s->var_inc *= s->var_decay; }
+
+static inline void act_clause_rescale(sat_solver* s) {
+    clause** cs = (clause**)vecp_begin(&s->learnts);
+    int i;
+    for (i = 0; i < vecp_size(&s->learnts); i++){
+        float a = clause_activity(cs[i]);
+        clause_setactivity(cs[i], a * (float)1e-20);
+    }
+    s->cla_inc *= (float)1e-20;
+}
+
+
+static inline void act_clause_bump(sat_solver* s, clause *c) {
+    float a = clause_activity(c) + s->cla_inc;
+    clause_setactivity(c,a);
+    if (a > 1e20) act_clause_rescale(s);
+}
+
+static inline void act_clause_decay(sat_solver* s) { s->cla_inc *= s->cla_decay; }
+
+//=================================================================================================
+// Clause functions:
+
+/* pre: size > 1 && no variable occurs twice
+ */
+static clause* clause_new(sat_solver* s, lit* begin, lit* end, int learnt)
+{
+    int size;
+    clause* c;
+    int i;
+
+    assert(end - begin > 1);
+    assert(learnt >= 0 && learnt < 2);
+    size           = end - begin;
+//    c              = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
+#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
+    c = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
+#else
+    c = (clause*)Sat_MmStepEntryFetch( s->pMem, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float) );
+#endif
+
+    c->size_learnt = (size << 1) | learnt;
+    assert(((unsigned long)c & 1) == 0);
+
+    for (i = 0; i < size; i++)
+        c->lits[i] = begin[i];
+
+    if (learnt)
+        *((float*)&c->lits[size]) = 0.0;
+
+    assert(begin[0] >= 0);
+    assert(begin[0] < s->size*2);
+    assert(begin[1] >= 0);
+    assert(begin[1] < s->size*2);
+
+    assert(lit_neg(begin[0]) < s->size*2);
+    assert(lit_neg(begin[1]) < s->size*2);
+
+    //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)c);
+    //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)c);
+
+    vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)(size > 2 ? c : clause_from_lit(begin[1])));
+    vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)(size > 2 ? c : clause_from_lit(begin[0])));
+
+    return c;
+}
+
+
+static void clause_remove(sat_solver* s, clause* c)
+{
+    lit* lits = clause_begin(c);
+    assert(lit_neg(lits[0]) < s->size*2);
+    assert(lit_neg(lits[1]) < s->size*2);
+
+    //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)c);
+    //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)c);
+
+    assert(lits[0] < s->size*2);
+    vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1])));
+    vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0])));
+
+    if (clause_learnt(c)){
+        s->stats.learnts--;
+        s->stats.learnts_literals -= clause_size(c);
+    }else{
+        s->stats.clauses--;
+        s->stats.clauses_literals -= clause_size(c);
+    }
+
+#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
+    free(c);
+#else
+    Sat_MmStepEntryRecycle( s->pMem, (char *)c, sizeof(clause) + sizeof(lit) * clause_size(c) + clause_learnt(c) * sizeof(float) );
+#endif
+}
+
+
+static lbool clause_simplify(sat_solver* s, clause* c)
+{
+    lit*   lits   = clause_begin(c);
+    lbool* values = s->assigns;
+    int i;
+
+    assert(sat_solver_dlevel(s) == 0);
+
+    for (i = 0; i < clause_size(c); i++){
+        lbool sig = !lit_sign(lits[i]); sig += sig - 1;
+        if (values[lit_var(lits[i])] == sig)
+            return l_True;
+    }
+    return l_False;
+}
+
+//=================================================================================================
+// Minor (solver) functions:
+
+void sat_solver_setnvars(sat_solver* s,int n)
+{
+    int var;
+
+    if (s->cap < n){
+
+        while (s->cap < n) s->cap = s->cap*2+1;
+
+        s->wlists    = (vecp*)   realloc(s->wlists,   sizeof(vecp)*s->cap*2);
+        s->activity  = (double*) realloc(s->activity, sizeof(double)*s->cap);
+        s->factors   = (double*) realloc(s->factors,  sizeof(double)*s->cap);
+        s->assigns   = (lbool*)  realloc(s->assigns,  sizeof(lbool)*s->cap);
+        s->orderpos  = (int*)    realloc(s->orderpos, sizeof(int)*s->cap);
+        s->reasons   = (clause**)realloc(s->reasons,  sizeof(clause*)*s->cap);
+        s->levels    = (int*)    realloc(s->levels,   sizeof(int)*s->cap);
+        s->tags      = (lbool*)  realloc(s->tags,     sizeof(lbool)*s->cap);
+        s->trail     = (lit*)    realloc(s->trail,    sizeof(lit)*s->cap);
+    }
+
+    for (var = s->size; var < n; var++){
+        vecp_new(&s->wlists[2*var]);
+        vecp_new(&s->wlists[2*var+1]);
+        s->activity [var] = 0;
+        s->factors  [var] = 0;
+        s->assigns  [var] = l_Undef;
+        s->orderpos [var] = veci_size(&s->order);
+        s->reasons  [var] = (clause*)0;
+        s->levels   [var] = 0;
+        s->tags     [var] = l_Undef;
+        
+        /* does not hold because variables enqueued at top level will not be reinserted in the heap
+           assert(veci_size(&s->order) == var); 
+         */
+        veci_push(&s->order,var);
+        order_update(s, var);
+    }
+
+    s->size = n > s->size ? n : s->size;
+}
+
+
+static inline bool enqueue(sat_solver* s, lit l, clause* from)
+{
+    lbool* values = s->assigns;
+    int    v      = lit_var(l);
+    lbool  val    = values[v];
+#ifdef VERBOSEDEBUG
+    printf(L_IND"enqueue("L_LIT")\n", L_ind, L_lit(l));
+#endif
+
+    lbool sig = !lit_sign(l); sig += sig - 1;
+    if (val != l_Undef){
+        return val == sig;
+    }else{
+        // New fact -- store it.
+#ifdef VERBOSEDEBUG
+        printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(l));
+#endif
+        int*     levels  = s->levels;
+        clause** reasons = s->reasons;
+
+        values [v] = sig;
+        levels [v] = sat_solver_dlevel(s);
+        reasons[v] = from;
+        s->trail[s->qtail++] = l;
+
+        order_assigned(s, v);
+        return true;
+    }
+}
+
+
+static inline void assume(sat_solver* s, lit l){
+    assert(s->qtail == s->qhead);
+    assert(s->assigns[lit_var(l)] == l_Undef);
+#ifdef VERBOSEDEBUG
+    printf(L_IND"assume("L_LIT")\n", L_ind, L_lit(l));
+#endif
+    veci_push(&s->trail_lim,s->qtail);
+    enqueue(s,l,(clause*)0);
+}
+
+
+static void sat_solver_canceluntil(sat_solver* s, int level) {
+    lit*     trail;   
+    lbool*   values;  
+    clause** reasons; 
+    int      bound;
+    int      c;
+    
+    if (sat_solver_dlevel(s) <= level)
+        return;
+
+    trail   = s->trail;
+    values  = s->assigns;
+    reasons = s->reasons;
+    bound   = (veci_begin(&s->trail_lim))[level];
+
+    ////////////////////////////////////////
+    // added to cancel all assignments
+//    if ( level == -1 )
+//        bound = 0;
+    ////////////////////////////////////////
+
+    for (c = s->qtail-1; c >= bound; c--) {
+        int     x  = lit_var(trail[c]);
+        values [x] = l_Undef;
+        reasons[x] = (clause*)0;
+    }
+
+    for (c = s->qhead-1; c >= bound; c--)
+        order_unassigned(s,lit_var(trail[c]));
+
+    s->qhead = s->qtail = bound;
+    veci_resize(&s->trail_lim,level);
+}
+
+static void sat_solver_record(sat_solver* s, veci* cls)
+{
+    lit*    begin = veci_begin(cls);
+    lit*    end   = begin + veci_size(cls);
+    clause* c     = (veci_size(cls) > 1) ? clause_new(s,begin,end,1) : (clause*)0;
+    enqueue(s,*begin,c);
+
+    ///////////////////////////////////
+    // add clause to internal storage
+    if ( s->pStore )
+    {
+        extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd );
+        int RetValue = Sto_ManAddClause( s->pStore, begin, end );
+        assert( RetValue );
+    }
+    ///////////////////////////////////
+
+    assert(veci_size(cls) > 0);
+
+    if (c != 0) {
+        vecp_push(&s->learnts,c);
+        act_clause_bump(s,c);
+        s->stats.learnts++;
+        s->stats.learnts_literals += veci_size(cls);
+    }
+}
+
+
+static double sat_solver_progress(sat_solver* s)
+{
+    lbool*  values = s->assigns;
+    int*    levels = s->levels;
+    int     i;
+
+    double  progress = 0;
+    double  F        = 1.0 / s->size;
+    for (i = 0; i < s->size; i++)
+        if (values[i] != l_Undef)
+            progress += pow(F, levels[i]);
+    return progress / s->size;
+}
+
+//=================================================================================================
+// Major methods:
+
+static bool sat_solver_lit_removable(sat_solver* s, lit l, int minl)
+{
+    lbool*   tags    = s->tags;
+    clause** reasons = s->reasons;
+    int*     levels  = s->levels;
+    int      top     = veci_size(&s->tagged);
+
+    assert(lit_var(l) >= 0 && lit_var(l) < s->size);
+    assert(reasons[lit_var(l)] != 0);
+    veci_resize(&s->stack,0);
+    veci_push(&s->stack,lit_var(l));
+
+    while (veci_size(&s->stack) > 0){
+        clause* c;
+        int v = veci_begin(&s->stack)[veci_size(&s->stack)-1];
+        assert(v >= 0 && v < s->size);
+        veci_resize(&s->stack,veci_size(&s->stack)-1);
+        assert(reasons[v] != 0);
+        c    = reasons[v];
+
+        if (clause_is_lit(c)){
+            int v = lit_var(clause_read_lit(c));
+            if (tags[v] == l_Undef && levels[v] != 0){
+                if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){
+                    veci_push(&s->stack,v);
+                    tags[v] = l_True;
+                    veci_push(&s->tagged,v);
+                }else{
+                    int* tagged = veci_begin(&s->tagged);
+                    int j;
+                    for (j = top; j < veci_size(&s->tagged); j++)
+                        tags[tagged[j]] = l_Undef;
+                    veci_resize(&s->tagged,top);
+                    return false;
+                }
+            }
+        }else{
+            lit*    lits = clause_begin(c);
+            int     i, j;
+
+            for (i = 1; i < clause_size(c); i++){
+                int v = lit_var(lits[i]);
+                if (tags[v] == l_Undef && levels[v] != 0){
+                    if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){
+
+                        veci_push(&s->stack,lit_var(lits[i]));
+                        tags[v] = l_True;
+                        veci_push(&s->tagged,v);
+                    }else{
+                        int* tagged = veci_begin(&s->tagged);
+                        for (j = top; j < veci_size(&s->tagged); j++)
+                            tags[tagged[j]] = l_Undef;
+                        veci_resize(&s->tagged,top);
+                        return false;
+                    }
+                }
+            }
+        }
+    }
+
+    return true;
+}
+
+static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt)
+{
+    lit*     trail   = s->trail;
+    lbool*   tags    = s->tags;
+    clause** reasons = s->reasons;
+    int*     levels  = s->levels;
+    int      cnt     = 0;
+    lit      p       = lit_Undef;
+    int      ind     = s->qtail-1;
+    lit*     lits;
+    int      i, j, minl;
+    int*     tagged;
+
+    veci_push(learnt,lit_Undef);
+
+    do{
+        assert(c != 0);
+
+        if (clause_is_lit(c)){
+            lit q = clause_read_lit(c);
+            assert(lit_var(q) >= 0 && lit_var(q) < s->size);
+            if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){
+                tags[lit_var(q)] = l_True;
+                veci_push(&s->tagged,lit_var(q));
+                act_var_bump(s,lit_var(q));
+                if (levels[lit_var(q)] == sat_solver_dlevel(s))
+                    cnt++;
+                else
+                    veci_push(learnt,q);
+            }
+        }else{
+
+            if (clause_learnt(c))
+                act_clause_bump(s,c);
+
+            lits = clause_begin(c);
+            //printlits(lits,lits+clause_size(c)); printf("\n");
+            for (j = (p == lit_Undef ? 0 : 1); j < clause_size(c); j++){
+                lit q = lits[j];
+                assert(lit_var(q) >= 0 && lit_var(q) < s->size);
+                if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){
+                    tags[lit_var(q)] = l_True;
+                    veci_push(&s->tagged,lit_var(q));
+                    act_var_bump(s,lit_var(q));
+                    if (levels[lit_var(q)] == sat_solver_dlevel(s))
+                        cnt++;
+                    else
+                        veci_push(learnt,q);
+                }
+            }
+        }
+
+        while (tags[lit_var(trail[ind--])] == l_Undef);
+
+        p = trail[ind+1];
+        c = reasons[lit_var(p)];
+        cnt--;
+
+    }while (cnt > 0);
+
+    *veci_begin(learnt) = lit_neg(p);
+
+    lits = veci_begin(learnt);
+    minl = 0;
+    for (i = 1; i < veci_size(learnt); i++){
+        int lev = levels[lit_var(lits[i])];
+        minl    |= 1 << (lev & 31);
+    }
+
+    // simplify (full)
+    for (i = j = 1; i < veci_size(learnt); i++){
+        if (reasons[lit_var(lits[i])] == 0 || !sat_solver_lit_removable(s,lits[i],minl))
+            lits[j++] = lits[i];
+    }
+
+    // update size of learnt + statistics
+    s->stats.max_literals += veci_size(learnt);
+    veci_resize(learnt,j);
+    s->stats.tot_literals += j;
+
+    // clear tags
+    tagged = veci_begin(&s->tagged);
+    for (i = 0; i < veci_size(&s->tagged); i++)
+        tags[tagged[i]] = l_Undef;
+    veci_resize(&s->tagged,0);
+
+#ifdef DEBUG
+    for (i = 0; i < s->size; i++)
+        assert(tags[i] == l_Undef);
+#endif
+
+#ifdef VERBOSEDEBUG
+    printf(L_IND"Learnt {", L_ind);
+    for (i = 0; i < veci_size(learnt); i++) printf(" "L_LIT, L_lit(lits[i]));
+#endif
+    if (veci_size(learnt) > 1){
+        int max_i = 1;
+        int max   = levels[lit_var(lits[1])];
+        lit tmp;
+
+        for (i = 2; i < veci_size(learnt); i++)
+            if (levels[lit_var(lits[i])] > max){
+                max   = levels[lit_var(lits[i])];
+                max_i = i;
+            }
+
+        tmp         = lits[1];
+        lits[1]     = lits[max_i];
+        lits[max_i] = tmp;
+    }
+#ifdef VERBOSEDEBUG
+    {
+        int lev = veci_size(learnt) > 1 ? levels[lit_var(lits[1])] : 0;
+        printf(" } at level %d\n", lev);
+    }
+#endif
+}
+
+
+clause* sat_solver_propagate(sat_solver* s)
+{
+    lbool*  values = s->assigns;
+    clause* confl  = (clause*)0;
+    lit*    lits;
+
+    //printf("sat_solver_propagate\n");
+    while (confl == 0 && s->qtail - s->qhead > 0){
+        lit  p  = s->trail[s->qhead++];
+        vecp* ws = sat_solver_read_wlist(s,p);
+        clause **begin = (clause**)vecp_begin(ws);
+        clause **end   = begin + vecp_size(ws);
+        clause **i, **j;
+
+        s->stats.propagations++;
+        s->simpdb_props--;
+
+        //printf("checking lit %d: "L_LIT"\n", veci_size(ws), L_lit(p));
+        for (i = j = begin; i < end; ){
+            if (clause_is_lit(*i)){
+//                s->stats.inspects2++;
+                *j++ = *i;
+                if (!enqueue(s,clause_read_lit(*i),clause_from_lit(p))){
+                    confl = s->binary;
+                    (clause_begin(confl))[1] = lit_neg(p);
+                    (clause_begin(confl))[0] = clause_read_lit(*i++);
+                    // Copy the remaining watches:
+//                    s->stats.inspects2 += end - i;
+                    while (i < end)
+                        *j++ = *i++;
+                }
+            }else{
+                lit false_lit;
+                lbool sig;
+
+                lits = clause_begin(*i);
+
+                // Make sure the false literal is data[1]:
+                false_lit = lit_neg(p);
+                if (lits[0] == false_lit){
+                    lits[0] = lits[1];
+                    lits[1] = false_lit;
+                }
+                assert(lits[1] == false_lit);
+                //printf("checking clause: "); printlits(lits, lits+clause_size(*i)); printf("\n");
+
+                // If 0th watch is true, then clause is already satisfied.
+                sig = !lit_sign(lits[0]); sig += sig - 1;
+                if (values[lit_var(lits[0])] == sig){
+                    *j++ = *i;
+                }else{
+                    // Look for new watch:
+                    lit* stop = lits + clause_size(*i);
+                    lit* k;
+                    for (k = lits + 2; k < stop; k++){
+                        lbool sig = lit_sign(*k); sig += sig - 1;
+                        if (values[lit_var(*k)] != sig){
+                            lits[1] = *k;
+                            *k = false_lit;
+                            vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i);
+                            goto next; }
+                    }
+
+                    *j++ = *i;
+                    // Clause is unit under assignment:
+                    if (!enqueue(s,lits[0], *i)){
+                        confl = *i++;
+                        // Copy the remaining watches:
+//                        s->stats.inspects2 += end - i;
+                        while (i < end)
+                            *j++ = *i++;
+                    }
+                }
+            }
+        next:
+            i++;
+        }
+
+        s->stats.inspects += j - (clause**)vecp_begin(ws);
+        vecp_resize(ws,j - (clause**)vecp_begin(ws));
+    }
+
+    return confl;
+}
+
+static inline int clause_cmp (const void* x, const void* y) {
+    return clause_size((clause*)x) > 2 && (clause_size((clause*)y) == 2 || clause_activity((clause*)x) < clause_activity((clause*)y)) ? -1 : 1; }
+
+void sat_solver_reducedb(sat_solver* s)
+{
+    int      i, j;
+    double   extra_lim = s->cla_inc / vecp_size(&s->learnts); // Remove any clause below this activity
+    clause** learnts = (clause**)vecp_begin(&s->learnts);
+    clause** reasons = s->reasons;
+
+    sat_solver_sort(vecp_begin(&s->learnts), vecp_size(&s->learnts), &clause_cmp);
+
+    for (i = j = 0; i < vecp_size(&s->learnts) / 2; i++){
+        if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i])
+            clause_remove(s,learnts[i]);
+        else
+            learnts[j++] = learnts[i];
+    }
+    for (; i < vecp_size(&s->learnts); i++){
+        if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i] && clause_activity(learnts[i]) < extra_lim)
+            clause_remove(s,learnts[i]);
+        else
+            learnts[j++] = learnts[i];
+    }
+
+    //printf("reducedb deleted %d\n", vecp_size(&s->learnts) - j);
+
+
+    vecp_resize(&s->learnts,j);
+}
+
+static lbool sat_solver_search(sat_solver* s, sint64 nof_conflicts, sint64 nof_learnts)
+{
+    int*    levels          = s->levels;
+    double  var_decay       = 0.95;
+    double  clause_decay    = 0.999;
+    double  random_var_freq = 0.02;
+
+    sint64  conflictC       = 0;
+    veci    learnt_clause;
+    int     i;
+
+    assert(s->root_level == sat_solver_dlevel(s));
+
+    s->nRestarts++;
+    s->stats.starts++;
+    s->var_decay = (float)(1 / var_decay   );
+    s->cla_decay = (float)(1 / clause_decay);
+    veci_resize(&s->model,0);
+    veci_new(&learnt_clause);
+
+    // use activity factors in every even restart
+    if ( (s->nRestarts & 1) && veci_size(&s->act_vars) > 0 )
+        for ( i = 0; i < s->act_vars.size; i++ )
+            act_var_bump_factor(s, s->act_vars.ptr[i]);
+
+    for (;;){
+        clause* confl = sat_solver_propagate(s);
+        if (confl != 0){
+            // CONFLICT
+            int blevel;
+
+#ifdef VERBOSEDEBUG
+            printf(L_IND"**CONFLICT**\n", L_ind);
+#endif
+            s->stats.conflicts++; conflictC++;
+            if (sat_solver_dlevel(s) == s->root_level){
+                veci_delete(&learnt_clause);
+                return l_False;
+            }
+
+            veci_resize(&learnt_clause,0);
+            sat_solver_analyze(s, confl, &learnt_clause);
+            blevel = veci_size(&learnt_clause) > 1 ? levels[lit_var(veci_begin(&learnt_clause)[1])] : s->root_level;
+            blevel = s->root_level > blevel ? s->root_level : blevel;
+            sat_solver_canceluntil(s,blevel);
+            sat_solver_record(s,&learnt_clause);
+            act_var_decay(s);
+            act_clause_decay(s);
+
+        }else{
+            // NO CONFLICT
+            int next;
+
+            if (nof_conflicts >= 0 && conflictC >= nof_conflicts){
+                // Reached bound on number of conflicts:
+                s->progress_estimate = sat_solver_progress(s);
+                sat_solver_canceluntil(s,s->root_level);
+                veci_delete(&learnt_clause);
+                return l_Undef; }
+
+            if ( (s->nConfLimit && s->stats.conflicts > s->nConfLimit) ||
+                 (s->nInsLimit  && s->stats.inspects  > s->nInsLimit) )
+            {
+                // Reached bound on number of conflicts:
+                s->progress_estimate = sat_solver_progress(s);
+                sat_solver_canceluntil(s,s->root_level);
+                veci_delete(&learnt_clause);
+                return l_Undef; 
+            }
+
+            if (sat_solver_dlevel(s) == 0 && !s->fSkipSimplify)
+                // Simplify the set of problem clauses:
+                sat_solver_simplify(s);
+
+            if (nof_learnts >= 0 && vecp_size(&s->learnts) - s->qtail >= nof_learnts)
+                // Reduce the set of learnt clauses:
+                sat_solver_reducedb(s);
+
+            // New variable decision:
+            s->stats.decisions++;
+            next = order_select(s,(float)random_var_freq);
+
+            if (next == var_Undef){
+                // Model found:
+                lbool* values = s->assigns;
+                int i;
+                veci_resize(&s->model, 0);
+                for (i = 0; i < s->size; i++) 
+                    veci_push(&s->model,(int)values[i]);
+                sat_solver_canceluntil(s,s->root_level);
+                veci_delete(&learnt_clause);
+
+                /*
+                veci apa; veci_new(&apa);
+                for (i = 0; i < s->size; i++) 
+                    veci_push(&apa,(int)(s->model.ptr[i] == l_True ? toLit(i) : lit_neg(toLit(i))));
+                printf("model: "); printlits((lit*)apa.ptr, (lit*)apa.ptr + veci_size(&apa)); printf("\n");
+                veci_delete(&apa);
+                */
+
+                return l_True;
+            }
+
+            assume(s,lit_neg(toLit(next)));
+        }
+    }
+
+    return l_Undef; // cannot happen
+}
+
+//=================================================================================================
+// External solver functions:
+
+sat_solver* sat_solver_new(void)
+{
+    sat_solver* s = (sat_solver*)malloc(sizeof(sat_solver));
+    memset( s, 0, sizeof(sat_solver) );
+
+    // initialize vectors
+    vecp_new(&s->clauses);
+    vecp_new(&s->learnts);
+    veci_new(&s->order);
+    veci_new(&s->trail_lim);
+    veci_new(&s->tagged);
+    veci_new(&s->stack);
+    veci_new(&s->model);
+    veci_new(&s->act_vars);
+
+    // initialize arrays
+    s->wlists    = 0;
+    s->activity  = 0;
+    s->factors   = 0;
+    s->assigns   = 0;
+    s->orderpos  = 0;
+    s->reasons   = 0;
+    s->levels    = 0;
+    s->tags      = 0;
+    s->trail     = 0;
+
+
+    // initialize other vars
+    s->size                   = 0;
+    s->cap                    = 0;
+    s->qhead                  = 0;
+    s->qtail                  = 0;
+    s->cla_inc                = 1;
+    s->cla_decay              = 1;
+    s->var_inc                = 1;
+    s->var_decay              = 1;
+    s->root_level             = 0;
+    s->simpdb_assigns         = 0;
+    s->simpdb_props           = 0;
+    s->random_seed            = 91648253;
+    s->progress_estimate      = 0;
+    s->binary                 = (clause*)malloc(sizeof(clause) + sizeof(lit)*2);
+    s->binary->size_learnt    = (2 << 1);
+    s->verbosity              = 0;
+
+    s->stats.starts           = 0;
+    s->stats.decisions        = 0;
+    s->stats.propagations     = 0;
+    s->stats.inspects         = 0;
+    s->stats.conflicts        = 0;
+    s->stats.clauses          = 0;
+    s->stats.clauses_literals = 0;
+    s->stats.learnts          = 0;
+    s->stats.learnts_literals = 0;
+    s->stats.max_literals     = 0;
+    s->stats.tot_literals     = 0;
+
+#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
+    s->pMem = NULL;
+#else
+    s->pMem = Sat_MmStepStart( 10 );
+#endif
+    return s;
+}
+
+
+void sat_solver_delete(sat_solver* s)
+{
+
+#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
+    int i;
+    for (i = 0; i < vecp_size(&s->clauses); i++)
+        free(vecp_begin(&s->clauses)[i]);
+    for (i = 0; i < vecp_size(&s->learnts); i++)
+        free(vecp_begin(&s->learnts)[i]);
+#else
+    Sat_MmStepStop( s->pMem, 0 );
+#endif
+
+    // delete vectors
+    vecp_delete(&s->clauses);
+    vecp_delete(&s->learnts);
+    veci_delete(&s->order);
+    veci_delete(&s->trail_lim);
+    veci_delete(&s->tagged);
+    veci_delete(&s->stack);
+    veci_delete(&s->model);
+    veci_delete(&s->act_vars);
+    free(s->binary);
+
+    // delete arrays
+    if (s->wlists != 0){
+        int i;
+        for (i = 0; i < s->size*2; i++)
+            vecp_delete(&s->wlists[i]);
+
+        // if one is different from null, all are
+        free(s->wlists   );
+        free(s->activity );
+        free(s->factors  );
+        free(s->assigns  );
+        free(s->orderpos );
+        free(s->reasons  );
+        free(s->levels   );
+        free(s->trail    );
+        free(s->tags     );
+    }
+
+    sat_solver_store_free(s);
+    free(s);
+}
+
+
+bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
+{
+    lit *i,*j;
+    int maxvar;
+    lbool* values;
+    lit last;
+
+    if (begin == end) return false;
+
+    //printlits(begin,end); printf("\n");
+    // insertion sort
+    maxvar = lit_var(*begin);
+    for (i = begin + 1; i < end; i++){
+        lit l = *i;
+        maxvar = lit_var(l) > maxvar ? lit_var(l) : maxvar;
+        for (j = i; j > begin && *(j-1) > l; j--)
+            *j = *(j-1);
+        *j = l;
+    }
+    sat_solver_setnvars(s,maxvar+1);
+//    sat_solver_setnvars(s, lit_var(*(end-1))+1 );
+
+    //printlits(begin,end); printf("\n");
+    values = s->assigns;
+
+    // delete duplicates
+    last = lit_Undef;
+    for (i = j = begin; i < end; i++){
+        //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]));
+        lbool sig = !lit_sign(*i); sig += sig - 1;
+        if (*i == lit_neg(last) || sig == values[lit_var(*i)])
+            return true;   // tautology
+        else if (*i != last && values[lit_var(*i)] == l_Undef)
+            last = *j++ = *i;
+    }
+
+    //printf("final: "); printlits(begin,j); printf("\n");
+
+    if (j == begin)          // empty clause
+        return false;
+
+    ///////////////////////////////////
+    // add clause to internal storage
+    if ( s->pStore )
+    {
+        extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd );
+        int RetValue = Sto_ManAddClause( s->pStore, begin, j );
+        assert( RetValue );
+    }
+    ///////////////////////////////////
+
+    if (j - begin == 1) // unit clause
+        return enqueue(s,*begin,(clause*)0);
+
+    // create new clause
+    vecp_push(&s->clauses,clause_new(s,begin,j,0));
+
+
+    s->stats.clauses++;
+    s->stats.clauses_literals += j - begin;
+
+    return true;
+}
+
+
+bool sat_solver_simplify(sat_solver* s)
+{
+    clause** reasons;
+    int type;
+
+    assert(sat_solver_dlevel(s) == 0);
+
+    if (sat_solver_propagate(s) != 0)
+        return false;
+
+    if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0)
+        return true;
+
+    reasons = s->reasons;
+    for (type = 0; type < 2; type++){
+        vecp*    cs  = type ? &s->learnts : &s->clauses;
+        clause** cls = (clause**)vecp_begin(cs);
+
+        int i, j;
+        for (j = i = 0; i < vecp_size(cs); i++){
+            if (reasons[lit_var(*clause_begin(cls[i]))] != cls[i] &&
+                clause_simplify(s,cls[i]) == l_True)
+                clause_remove(s,cls[i]);
+            else
+                cls[j++] = cls[i];
+        }
+        vecp_resize(cs,j);
+    }
+
+    s->simpdb_assigns = s->qhead;
+    // (shouldn't depend on 'stats' really, but it will do for now)
+    s->simpdb_props   = (int)(s->stats.clauses_literals + s->stats.learnts_literals);
+
+    return true;
+}
+
+
+int sat_solver_solve(sat_solver* s, lit* begin, lit* end, sint64 nConfLimit, sint64 nInsLimit, sint64 nConfLimitGlobal, sint64 nInsLimitGlobal)
+{
+    sint64  nof_conflicts = 100;
+    sint64  nof_learnts   = sat_solver_nclauses(s) / 3;
+    lbool   status        = l_Undef;
+    lbool*  values        = s->assigns;
+    lit*    i;
+
+    // set the external limits
+    s->nCalls++;
+    s->nRestarts  = 0;
+    s->nConfLimit = 0;
+    s->nInsLimit  = 0;
+    if ( nConfLimit )
+        s->nConfLimit = s->stats.conflicts + nConfLimit;
+    if ( nInsLimit )
+        s->nInsLimit = s->stats.inspects + nInsLimit;
+    if ( nConfLimitGlobal && (s->nConfLimit == 0 || s->nConfLimit > nConfLimitGlobal) )
+        s->nConfLimit = nConfLimitGlobal;
+    if ( nInsLimitGlobal && (s->nInsLimit == 0 || s->nInsLimit > nInsLimitGlobal) )
+        s->nInsLimit = nInsLimitGlobal;
+
+    //printf("solve: "); printlits(begin, end); printf("\n");
+    for (i = begin; i < end; i++){
+        switch (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]){
+        case 1: /* l_True: */
+            break;
+        case 0: /* l_Undef */
+            assume(s, *i);
+            if (sat_solver_propagate(s) == NULL)
+                break;
+            // fallthrough
+        case -1: /* l_False */
+            sat_solver_canceluntil(s, 0);
+            return l_False;
+        }
+    }
+    s->nCalls2++;
+
+    s->root_level = sat_solver_dlevel(s);
+
+    if (s->verbosity >= 1){
+        printf("==================================[MINISAT]===================================\n");
+        printf("| Conflicts |     ORIGINAL     |              LEARNT              | Progress |\n");
+        printf("|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |\n");
+        printf("==============================================================================\n");
+    }
+
+    while (status == l_Undef){
+        double Ratio = (s->stats.learnts == 0)? 0.0 :
+            s->stats.learnts_literals / (double)s->stats.learnts;
+
+        if (s->verbosity >= 1)
+        {
+            printf("| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %6.3f %% |\n", 
+                (double)s->stats.conflicts,
+                (double)s->stats.clauses, 
+                (double)s->stats.clauses_literals,
+                (double)nof_learnts, 
+                (double)s->stats.learnts, 
+                (double)s->stats.learnts_literals,
+                Ratio,
+                s->progress_estimate*100);
+            fflush(stdout);
+        }
+        status = sat_solver_search(s, nof_conflicts, nof_learnts);
+        nof_conflicts = nof_conflicts * 3 / 2; //*= 1.5;
+        nof_learnts   = nof_learnts * 11 / 10; //*= 1.1;
+
+        // quit the loop if reached an external limit
+        if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit )
+        {
+//            printf( "Reached the limit on the number of conflicts (%d).\n", s->nConfLimit );
+            break;
+        }
+        if ( s->nInsLimit  && s->stats.inspects > s->nInsLimit )
+        {
+//            printf( "Reached the limit on the number of implications (%d).\n", s->nInsLimit );
+            break;
+        }
+    }
+    if (s->verbosity >= 1)
+        printf("==============================================================================\n");
+
+    sat_solver_canceluntil(s,0);
+
+    ////////////////////////////////////////////////
+    if ( status == l_False && s->pStore )
+    {
+        extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd );
+        int RetValue = Sto_ManAddClause( s->pStore, NULL, NULL );
+        assert( RetValue );
+    }
+    ////////////////////////////////////////////////
+    return status;
+}
+
+
+int sat_solver_nvars(sat_solver* s)
+{
+    return s->size;
+}
+
+
+int sat_solver_nclauses(sat_solver* s)
+{
+    return vecp_size(&s->clauses);
+}
+
+
+int sat_solver_nconflicts(sat_solver* s)
+{
+    return (int)s->stats.conflicts;
+}
+
+//=================================================================================================
+// Clause storage functions:
+
+void sat_solver_store_alloc( sat_solver * s )
+{
+    extern void * Sto_ManAlloc();
+    assert( s->pStore == NULL );
+    s->pStore = Sto_ManAlloc();
+}
+
+void sat_solver_store_write( sat_solver * s, char * pFileName )
+{
+    extern void Sto_ManDumpClauses( void * p, char * pFileName );
+    if ( s->pStore ) Sto_ManDumpClauses( s->pStore, pFileName );
+}
+
+void sat_solver_store_free( sat_solver * s )
+{
+    extern void Sto_ManFree( void * p );
+    if ( s->pStore ) Sto_ManFree( s->pStore );
+    s->pStore = NULL;
+}
+ 
+void sat_solver_store_mark_roots( sat_solver * s )
+{
+    extern void Sto_ManMarkRoots( void * p );
+    if ( s->pStore ) Sto_ManMarkRoots( s->pStore );
+}
+
+void sat_solver_store_mark_clauses_a( sat_solver * s )
+{
+    extern void Sto_ManMarkClausesA( void * p );
+    if ( s->pStore ) Sto_ManMarkClausesA( s->pStore );
+}
+
+void * sat_solver_store_release( sat_solver * s )
+{
+    void * pTemp;
+    if ( s->pStore == NULL )
+        return NULL;
+    pTemp = s->pStore;
+    s->pStore = NULL;
+    return pTemp;
+}
+
+//=================================================================================================
+// Sorting functions (sigh):
+
+static inline void selectionsort(void** array, int size, int(*comp)(const void *, const void *))
+{
+    int     i, j, best_i;
+    void*   tmp;
+
+    for (i = 0; i < size-1; i++){
+        best_i = i;
+        for (j = i+1; j < size; j++){
+            if (comp(array[j], array[best_i]) < 0)
+                best_i = j;
+        }
+        tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp;
+    }
+}
+
+
+static void sortrnd(void** array, int size, int(*comp)(const void *, const void *), double* seed)
+{
+    if (size <= 15)
+        selectionsort(array, size, comp);
+
+    else{
+        void*       pivot = array[irand(seed, size)];
+        void*       tmp;
+        int         i = -1;
+        int         j = size;
+
+        for(;;){
+            do i++; while(comp(array[i], pivot)<0);
+            do j--; while(comp(pivot, array[j])<0);
+
+            if (i >= j) break;
+
+            tmp = array[i]; array[i] = array[j]; array[j] = tmp;
+        }
+
+        sortrnd(array    , i     , comp, seed);
+        sortrnd(&array[i], size-i, comp, seed);
+    }
+}
+
+void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *))
+{
+    double seed = 91648253;
+    sortrnd(array,size,comp,&seed);
+}
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
new file mode 100644
index 00000000..542b9895
--- /dev/null
+++ b/src/sat/bsat/satSolver.h
@@ -0,0 +1,191 @@
+/**************************************************************************************************
+MiniSat -- Copyright (c) 2005, Niklas Sorensson
+http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko
+
+#ifndef satSolver_h
+#define satSolver_h
+
+#ifdef _WIN32
+#define inline __inline // compatible with MS VS 6.0
+#endif
+
+#include "satVec.h"
+#include "satMem.h"
+
+//=================================================================================================
+// Simple types:
+
+// does not work for c++
+//typedef int                   bool;
+#ifndef __cplusplus
+#ifndef bool
+#define bool int
+#endif
+#endif
+
+static const bool  true      = 1;
+static const bool  false     = 0;
+
+typedef int                lit;
+typedef char               lbool;
+
+#ifndef SINT64
+#define SINT64
+
+#ifdef _WIN32
+typedef signed __int64     sint64;   // compatible with MS VS 6.0
+#else
+typedef long long          sint64;
+#endif
+
+#endif
+
+static const int   var_Undef = -1;
+static const lit   lit_Undef = -2;
+
+static const lbool l_Undef   =  0;
+static const lbool l_True    =  1;
+static const lbool l_False   = -1;
+
+static inline lit  toLit    (int v)        { return v + v; }
+static inline lit  toLitCond(int v, int c) { return v + v + (c != 0); }
+static inline lit  lit_neg  (lit l)        { return l ^ 1; }
+static inline int  lit_var  (lit l)        { return l >> 1; }
+static inline int  lit_sign (lit l)        { return l & 1; }
+static inline int  lit_print(lit l)        { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; }
+static inline lit  lit_read (int s)        { return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); }
+
+
+//=================================================================================================
+// Public interface:
+
+struct sat_solver_t;
+typedef struct sat_solver_t sat_solver;
+
+extern sat_solver* sat_solver_new(void);
+extern void        sat_solver_delete(sat_solver* s);
+
+extern bool        sat_solver_addclause(sat_solver* s, lit* begin, lit* end);
+extern bool        sat_solver_simplify(sat_solver* s);
+extern int         sat_solver_solve(sat_solver* s, lit* begin, lit* end, sint64 nConfLimit, sint64 nInsLimit, sint64 nConfLimitGlobal, sint64 nInsLimitGlobal);
+
+extern int         sat_solver_nvars(sat_solver* s);
+extern int         sat_solver_nclauses(sat_solver* s);
+extern int         sat_solver_nconflicts(sat_solver* s);
+
+extern void        sat_solver_setnvars(sat_solver* s,int n);
+
+struct stats_t
+{
+    sint64   starts, decisions, propagations, inspects, conflicts;
+    sint64   clauses, clauses_literals, learnts, learnts_literals, max_literals, tot_literals;
+};
+typedef struct stats_t stats;
+
+extern void        Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars );
+extern void        Sat_SolverPrintStats( FILE * pFile, sat_solver * p );
+extern int *       Sat_SolverGetModel( sat_solver * p, int * pVars, int nVars );
+extern void        Sat_SolverDoubleClauses( sat_solver * p, int iVar );
+
+// trace recording
+extern void        Sat_SolverTraceStart( sat_solver * pSat, char * pName );
+extern void        Sat_SolverTraceStop( sat_solver * pSat );
+extern void        Sat_SolverTraceWrite( sat_solver * pSat, int * pBeg, int * pEnd, int fRoot );
+
+// clause storage
+extern void        sat_solver_store_alloc( sat_solver * s );
+extern void        sat_solver_store_write( sat_solver * s, char * pFileName );
+extern void        sat_solver_store_free( sat_solver * s );
+extern void        sat_solver_store_mark_roots( sat_solver * s );
+extern void        sat_solver_store_mark_clauses_a( sat_solver * s );
+extern void *      sat_solver_store_release( sat_solver * s ); 
+
+//=================================================================================================
+// Solver representation:
+
+struct clause_t;
+typedef struct clause_t clause;
+
+struct sat_solver_t
+{
+    int      size;          // nof variables
+    int      cap;           // size of varmaps
+    int      qhead;         // Head index of queue.
+    int      qtail;         // Tail index of queue.
+
+    // clauses
+    vecp     clauses;       // List of problem constraints. (contains: clause*)
+    vecp     learnts;       // List of learnt clauses. (contains: clause*)
+
+    // activities
+    double   var_inc;       // Amount to bump next variable with.
+    double   var_decay;     // INVERSE decay factor for variable activity: stores 1/decay. 
+    float    cla_inc;       // Amount to bump next clause with.
+    float    cla_decay;     // INVERSE decay factor for clause activity: stores 1/decay.
+
+    vecp*    wlists;        // 
+    double*  activity;      // A heuristic measurement of the activity of a variable.
+    lbool*   assigns;       // Current values of variables.
+    int*     orderpos;      // Index in variable order.
+    clause** reasons;       //
+    int*     levels;        //
+    lit*     trail;
+
+    clause*  binary;        // A temporary binary clause
+    lbool*   tags;          //
+    veci     tagged;        // (contains: var)
+    veci     stack;         // (contains: var)
+
+    veci     order;         // Variable order. (heap) (contains: var)
+    veci     trail_lim;     // Separator indices for different decision levels in 'trail'. (contains: int)
+    veci     model;         // If problem is solved, this vector contains the model (contains: lbool).
+
+    int      root_level;    // Level of first proper decision.
+    int      simpdb_assigns;// Number of top-level assignments at last 'simplifyDB()'.
+    int      simpdb_props;  // Number of propagations before next 'simplifyDB()'.
+    double   random_seed;
+    double   progress_estimate;
+    int      verbosity;     // Verbosity level. 0=silent, 1=some progress report, 2=everything
+
+    stats    stats;
+
+    sint64   nConfLimit;    // external limit on the number of conflicts
+    sint64   nInsLimit;     // external limit on the number of implications
+
+    veci     act_vars;      // variables whose activity has changed
+    double*  factors;       // the activity factors
+    int      nRestarts;     // the number of local restarts
+    int      nCalls;        // the number of local restarts
+    int      nCalls2;        // the number of local restarts
+ 
+    Sat_MmStep_t * pMem;
+
+    int      fSkipSimplify; // set to one to skip simplification of the clause database
+
+    // clause store
+    void *   pStore;
+
+    // trace recording
+    FILE *   pFile;
+    int      nClauses;
+    int      nRoots;
+};
+
+#endif
diff --git a/src/sat/bsat/satStore.c b/src/sat/bsat/satStore.c
new file mode 100644
index 00000000..f968162e
--- /dev/null
+++ b/src/sat/bsat/satStore.c
@@ -0,0 +1,437 @@
+/**CFile****************************************************************
+
+  FileName    [satStore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT solver.]
+
+  Synopsis    [Records the trace of SAT solving in the CNF form.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: satStore.c,v 1.4 2005/09/16 22:55:03 casem Exp $]
+
+***********************************************************************/
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+#include <time.h>
+#include "satStore.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Fetches memory.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Sto_ManMemoryFetch( Sto_Man_t * p, int nBytes )
+{
+    char * pMem;
+    if ( p->pChunkLast == NULL || nBytes > p->nChunkSize - p->nChunkUsed )
+    {
+        pMem = (char *)malloc( p->nChunkSize );
+        *(char **)pMem = p->pChunkLast;
+        p->pChunkLast = pMem;
+        p->nChunkUsed = sizeof(char *);
+    }
+    pMem = p->pChunkLast + p->nChunkUsed;
+    p->nChunkUsed += nBytes;
+    return pMem;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees memory manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sto_ManMemoryStop( Sto_Man_t * p )
+{
+    char * pMem, * pNext;
+    if ( p->pChunkLast == NULL )
+        return;
+    for ( pMem = p->pChunkLast; (pNext = *(char **)pMem); pMem = pNext )
+        free( pMem );
+    free( pMem );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reports memory usage in bytes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sto_ManMemoryReport( Sto_Man_t * p )
+{
+    int Total;
+    char * pMem, * pNext;
+    if ( p->pChunkLast == NULL )
+        return 0;
+    Total = p->nChunkUsed; 
+    for ( pMem = p->pChunkLast; (pNext = *(char **)pMem); pMem = pNext )
+        Total += p->nChunkSize;
+    return Total;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Allocate proof manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Sto_Man_t * Sto_ManAlloc()
+{
+    Sto_Man_t * p;
+    // allocate the manager
+    p = (Sto_Man_t *)malloc( sizeof(Sto_Man_t) );
+    memset( p, 0, sizeof(Sto_Man_t) );
+    // memory management
+    p->nChunkSize = (1<<16); // use 64K chunks
+    return p;    
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocate proof manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sto_ManFree( Sto_Man_t * p )
+{
+    Sto_ManMemoryStop( p );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds one clause to the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sto_ManAddClause( Sto_Man_t * p, lit * pBeg, lit * pEnd )
+{
+    Sto_Cls_t * pClause;
+    lit Lit, * i, * j;
+    int nSize;
+
+    // process the literals
+    if ( pBeg < pEnd )
+    {
+        // insertion sort
+        for ( i = pBeg + 1; i < pEnd; i++ )
+        {
+            Lit = *i;
+            for ( j = i; j > pBeg && *(j-1) > Lit; j-- )
+                *j = *(j-1);
+            *j = Lit;
+        }
+        // make sure there is no duplicated variables
+        for ( i = pBeg + 1; i < pEnd; i++ )
+            if ( lit_var(*(i-1)) == lit_var(*i) )
+            {
+                printf( "The clause contains two literals of the same variable: %d and %d.\n", *(i-1), *i );
+                return 0;
+            }
+        // check the largest var size
+        p->nVars = STO_MAX( p->nVars, lit_var(*(pEnd-1)) + 1 );
+    }
+
+    // get memory for the clause
+    nSize = sizeof(Sto_Cls_t) + sizeof(lit) * (pEnd - pBeg);
+    pClause = (Sto_Cls_t *)Sto_ManMemoryFetch( p, nSize );
+    memset( pClause, 0, sizeof(Sto_Cls_t) );
+
+    // assign the clause
+    pClause->Id = p->nClauses++;
+    pClause->nLits = pEnd - pBeg;
+    memcpy( pClause->pLits, pBeg, sizeof(lit) * (pEnd - pBeg) );
+
+    // add the clause to the list
+    if ( p->pHead == NULL )
+        p->pHead = pClause;
+    if ( p->pTail == NULL )
+        p->pTail = pClause;
+    else
+    {
+        p->pTail->pNext = pClause;
+        p->pTail = pClause;
+    }
+
+    // add the empty clause
+    if ( pClause->nLits == 0 )
+    {
+        if ( p->pEmpty )
+        {
+            printf( "More than one empty clause!\n" );
+            return 0;
+        }
+        p->pEmpty = pClause;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Mark all clauses added so far as root clauses.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sto_ManMarkRoots( Sto_Man_t * p )
+{
+    Sto_Cls_t * pClause;
+    p->nRoots = 0;
+    Sto_ManForEachClause( p, pClause )
+    {
+        pClause->fRoot = 1;
+        p->nRoots++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Mark all clauses added so far as clause of A.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sto_ManMarkClausesA( Sto_Man_t * p )
+{
+    Sto_Cls_t * pClause;
+    p->nClausesA = 0;
+    Sto_ManForEachClause( p, pClause )
+    {
+        pClause->fA = 1;
+        p->nClausesA++;
+    }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the stored clauses into a file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sto_ManDumpClauses( Sto_Man_t * p, char * pFileName )
+{
+    FILE * pFile;
+    Sto_Cls_t * pClause;
+    int i;
+    // start the file
+    pFile = fopen( pFileName, "w" );
+    if ( pFile == NULL )
+    {
+        printf( "Error: Cannot open output file (%s).\n", pFileName );
+        return;
+    }
+    // write the data
+    fprintf( pFile, "p %d %d %d %d\n", p->nVars, p->nClauses, p->nRoots, p->nClausesA );
+    Sto_ManForEachClause( p, pClause )
+    {
+        for ( i = 0; i < (int)pClause->nLits; i++ )
+            fprintf( pFile, " %d", lit_print(pClause->pLits[i]) );
+        fprintf( pFile, "\n" );
+    }
+    fprintf( pFile, " 0\n" );
+    fclose( pFile );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reads one literal from file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sto_ManLoadNumber( FILE * pFile, int * pNumber )
+{
+    int Char, Number = 0, Sign = 0;
+    // skip space-like chars
+    do {
+        Char = fgetc( pFile );
+        if ( Char == EOF )
+            return 0;
+    } while ( Char == ' ' || Char == '\t' || Char == '\r' || Char == '\n' );
+    // read the literal
+    while ( 1 )
+    {
+        // get the next character
+        Char = fgetc( pFile );
+        if ( Char == ' ' || Char == '\t' || Char == '\r' || Char == '\n' )
+            break;
+        // check that the char is a digit
+        if ( (Char < '0' || Char > '9') && Char != '-' )
+        {
+            printf( "Error: Wrong char (%c) in the input file.\n", Char );
+            return 0;
+        }
+        // check if this is a minus
+        if ( Char == '-' )
+            Sign = 1;
+        else
+            Number = 10 * Number + Char;
+    }
+    // return the number
+    *pNumber = Sign? -Number : Number;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reads CNF from file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Sto_Man_t * Sto_ManLoadClauses( char * pFileName )
+{
+    FILE * pFile;
+    Sto_Man_t * p;
+    Sto_Cls_t * pClause;
+    char pBuffer[1024];
+    int nLits, nLitsAlloc, Counter, Number;
+    lit * pLits;
+
+    // start the file
+    pFile = fopen( pFileName, "r" );
+    if ( pFile == NULL )
+    {
+        printf( "Error: Cannot open input file (%s).\n", pFileName );
+        return NULL;
+    }
+
+    // create the manager
+    p = Sto_ManAlloc();
+
+    // alloc the array of literals
+    nLitsAlloc = 1024;
+    pLits = (lit *)malloc( sizeof(lit) * nLitsAlloc );
+
+    // read file header
+    p->nVars = p->nClauses = p->nRoots = p->nClausesA = 0;
+    while ( fgets( pBuffer, 1024, pFile ) )
+    {
+        if ( pBuffer[0] == 'c' )
+            continue;
+        if ( pBuffer[0] == 'p' )
+        {
+            sscanf( pBuffer + 1, "%d %d %d %d", &p->nVars, &p->nClauses, &p->nRoots, &p->nClausesA );
+            break;
+        }
+        printf( "Warning: Skipping line: \"%s\"\n", pBuffer );
+    }
+
+    // read the clauses
+    nLits = 0;
+    while ( Sto_ManLoadNumber(pFile, &Number) )
+    {
+        if ( Number == 0 )
+        {
+            int RetValue;
+            RetValue = Sto_ManAddClause( p, pLits, pLits + nLits );
+            assert( RetValue );
+            nLits = 0;
+            continue;
+        }
+        if ( nLits == nLitsAlloc )
+        {
+            nLitsAlloc *= 2;
+            pLits = (lit *)realloc( pLits, sizeof(lit) * nLitsAlloc );
+        }
+        pLits[ nLits++ ] = lit_read(Number);
+    }
+    if ( nLits > 0 )
+        printf( "Error: The last clause was not saved.\n" );
+
+    // count clauses
+    Counter = 0;
+    Sto_ManForEachClause( p, pClause )
+        Counter++;
+
+    // check the number of clauses
+    if ( p->nClauses != Counter )
+    {
+        printf( "Error: The actual number of clauses (%d) is different than declared (%d).\n", Counter, p->nClauses );
+        Sto_ManFree( p );
+        return NULL;
+    }
+
+    free( pLits );
+    fclose( pFile );
+    return p;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/bsat/satStore.h b/src/sat/bsat/satStore.h
new file mode 100644
index 00000000..346b59df
--- /dev/null
+++ b/src/sat/bsat/satStore.h
@@ -0,0 +1,137 @@
+/**CFile****************************************************************
+
+  FileName    [pr.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Proof recording.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: pr.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __PR_H__
+#define __PR_H__
+
+/*
+    The trace of SAT solving contains the original clause of the problem
+    along with the learned clauses derived during SAT solving.
+    The first line of the resulting file contains 3 numbers instead of 2:
+    c <num_vars> <num_all_clauses> <num_root_clauses>
+*/
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+#ifdef _WIN32
+#define inline __inline // compatible with MS VS 6.0
+#endif
+
+#ifndef PRT
+#define PRT(a,t)  printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
+#endif
+
+#define STO_MAX(a,b)  ((a) > (b) ? (a) : (b))
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef unsigned lit;
+
+typedef struct Sto_Cls_t_ Sto_Cls_t;
+struct Sto_Cls_t_
+{
+    Sto_Cls_t *     pNext;        // the next clause
+    Sto_Cls_t *     pNext0;       // the next 0-watch
+    Sto_Cls_t *     pNext1;       // the next 0-watch
+    int             Id;           // the clause ID
+    unsigned        fA     :  1;  // belongs to A
+    unsigned        fRoot  :  1;  // original clause
+    unsigned        fVisit :  1;  // visited clause
+    unsigned        nLits  : 24;  // the number of literals
+    lit             pLits[0];     // literals of this clause
+};
+
+typedef struct Sto_Man_t_ Sto_Man_t;
+struct Sto_Man_t_
+{
+    // general data
+    int             nVars;        // the number of variables
+    int             nRoots;       // the number of root clauses
+    int             nClauses;     // the number of all clauses
+    int             nClausesA;    // the number of clauses of A 
+    Sto_Cls_t *     pHead;        // the head clause
+    Sto_Cls_t *     pTail;        // the tail clause
+    Sto_Cls_t *     pEmpty;       // the empty clause
+    // memory management
+    int             nChunkSize;   // the number of bytes in a chunk
+    int             nChunkUsed;   // the number of bytes used in the last chunk
+    char *          pChunkLast;   // the last memory chunk
+};
+
+// variable/literal conversions (taken from MiniSat)
+static inline lit   toLit    (int v)        { return v + v;  }
+static inline lit   toLitCond(int v, int c) { return v + v + (c != 0); }
+static inline lit   lit_neg  (lit l)        { return l ^ 1;  }
+static inline int   lit_var  (lit l)        { return l >> 1; }
+static inline int   lit_sign (lit l)        { return l & 1;  }
+static inline int   lit_print(lit l)        { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; }
+static inline lit   lit_read (int s)        { return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); }
+static inline int   lit_check(lit l, int n) { return l >= 0 && lit_var(l) < n;                  }
+
+// iterators through the clauses
+#define Sto_ManForEachClause( p, pCls )      for( pCls = p->pHead; pCls; pCls = pCls->pNext )
+#define Sto_ManForEachClauseRoot( p, pCls )  for( pCls = p->pHead; pCls && pCls->fRoot; pCls = pCls->pNext )
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== satStore.c ==========================================================*/
+extern Sto_Man_t *  Sto_ManAlloc();
+extern void         Sto_ManFree( Sto_Man_t * p );
+extern int          Sto_ManAddClause( Sto_Man_t * p, lit * pBeg, lit * pEnd );
+extern int          Sto_ManMemoryReport( Sto_Man_t * p );
+extern void         Sto_ManMarkRoots( Sto_Man_t * p );
+extern void         Sto_ManMarkClausesA( Sto_Man_t * p );
+extern void         Sto_ManDumpClauses( Sto_Man_t * p, char * pFileName );
+extern Sto_Man_t *  Sto_ManLoadClauses( char * pFileName );
+
+/*=== satInter.c ==========================================================*/
+typedef struct Int_Man_t_ Int_Man_t;
+extern Int_Man_t *  Int_ManAlloc( int nVarsAlloc );
+extern void         Int_ManFree( Int_Man_t * p );
+extern int          Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned ** ppResult );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/sat/bsat/satTrace.c b/src/sat/bsat/satTrace.c
new file mode 100644
index 00000000..111e8dfb
--- /dev/null
+++ b/src/sat/bsat/satTrace.c
@@ -0,0 +1,109 @@
+/**CFile****************************************************************
+
+  FileName    [satTrace.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT sat_solver.]
+
+  Synopsis    [Records the trace of SAT solving in the CNF form.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: satTrace.c,v 1.4 2005/09/16 22:55:03 casem Exp $]
+
+***********************************************************************/
+
+#include <stdio.h>
+#include <assert.h>
+#include "satSolver.h"
+
+/*
+    The trace of SAT solving contains the original clause of the problem
+    along with the learned clauses derived during SAT solving.
+    The first line of the resulting file contains 3 numbers instead of 2:
+    c <num_vars> <num_all_clauses> <num_root_clauses>
+*/
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Start the trace recording.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sat_SolverTraceStart( sat_solver * pSat, char * pName )
+{
+    assert( pSat->pFile == NULL );
+    pSat->pFile = fopen( pName, "w" );
+    fprintf( pSat->pFile, "                                        \n" );
+    pSat->nClauses = 0;
+    pSat->nRoots = 0;
+}   
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the trace recording.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sat_SolverTraceStop( sat_solver * pSat )
+{
+    if ( pSat->pFile == NULL )
+        return;
+    rewind( pSat->pFile );
+    fprintf( pSat->pFile, "p %d %d %d", sat_solver_nvars(pSat), pSat->nClauses, pSat->nRoots );
+    fclose( pSat->pFile );
+    pSat->pFile = NULL;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Writes one clause into the trace file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sat_SolverTraceWrite( sat_solver * pSat, int * pBeg, int * pEnd, int fRoot )
+{
+    if ( pSat->pFile == NULL )
+        return;
+    pSat->nClauses++;
+    pSat->nRoots += fRoot;
+    for ( ; pBeg < pEnd ; pBeg++ )
+        fprintf( pSat->pFile, " %d", lit_print(*pBeg) );
+    fprintf( pSat->pFile, " 0\n" );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c
new file mode 100644
index 00000000..3961cf7e
--- /dev/null
+++ b/src/sat/bsat/satUtil.c
@@ -0,0 +1,234 @@
+/**CFile****************************************************************
+
+  FileName    [satUtil.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [C-language MiniSat solver.]
+
+  Synopsis    [Additional SAT solver procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: satUtil.c,v 1.4 2005/09/16 22:55:03 casem Exp $]
+
+***********************************************************************/
+
+#include <stdio.h>
+#include <assert.h>
+#include "satSolver.h"
+#include "vec.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+struct clause_t
+{
+    int size_learnt;
+    lit lits[0];
+};
+
+static inline int  clause_size( clause* c )  { return c->size_learnt >> 1; }
+static inline lit* clause_begin( clause* c ) { return c->lits;             }
+
+static void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, bool fIncrement );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Write the clauses in the solver into a file in DIMACS format.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars )
+{
+    FILE * pFile;
+    void ** pClauses;
+    int nClauses, i;
+
+    // count the number of clauses
+    nClauses = p->clauses.size + p->learnts.size;
+    for ( i = 0; i < p->size; i++ )
+        if ( p->levels[i] == 0 && p->assigns[i] != l_Undef )
+            nClauses++;
+
+    // start the file
+    pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL )
+    {
+        printf( "Sat_SolverWriteDimacs(): Cannot open the ouput file.\n" );
+        return;
+    }
+//    fprintf( pFile, "c CNF generated by ABC on %s\n", Extra_TimeStamp() );
+    fprintf( pFile, "p cnf %d %d\n", p->size, nClauses );
+
+    // write the original clauses
+    nClauses = p->clauses.size;
+    pClauses = p->clauses.ptr;
+    for ( i = 0; i < nClauses; i++ )
+        Sat_SolverClauseWriteDimacs( pFile, pClauses[i], incrementVars );
+
+    // write the learned clauses
+    nClauses = p->learnts.size;
+    pClauses = p->learnts.ptr;
+    for ( i = 0; i < nClauses; i++ )
+        Sat_SolverClauseWriteDimacs( pFile, pClauses[i], incrementVars );
+
+    // write zero-level assertions
+    for ( i = 0; i < p->size; i++ )
+        if ( p->levels[i] == 0 && p->assigns[i] != l_Undef )
+            fprintf( pFile, "%s%d%s\n",
+                     (p->assigns[i] == l_False)? "-": "",
+                     i + (int)(incrementVars>0),
+                     (incrementVars) ? " 0" : "");
+
+    // write the assumptions
+    if (assumptionsBegin) {
+        for (; assumptionsBegin != assumptionsEnd; assumptionsBegin++) {
+            fprintf( pFile, "%s%d%s\n",
+                     lit_sign(*assumptionsBegin)? "-": "",
+                     lit_var(*assumptionsBegin) + (int)(incrementVars>0),
+                     (incrementVars) ? " 0" : "");
+        }
+    }
+
+    fprintf( pFile, "\n" );
+    fclose( pFile );
+}   
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the given clause in a file in DIMACS format.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, bool fIncrement )
+{
+    lit * pLits = clause_begin(pC);
+    int nLits = clause_size(pC);
+    int i;
+
+    for ( i = 0; i < nLits; i++ )
+        fprintf( pFile, "%s%d ", (lit_sign(pLits[i])? "-": ""),  lit_var(pLits[i]) + (int)(fIncrement>0) );
+    if ( fIncrement )
+        fprintf( pFile, "0" );
+    fprintf( pFile, "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the given clause in a file in DIMACS format.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sat_SolverPrintStats( FILE * pFile, sat_solver * p )
+{
+//    printf( "calls         : %8d (%d)\n", (int)p->nCalls, (int)p->nCalls2 );
+    printf( "starts        : %8d\n", (int)p->stats.starts );
+    printf( "conflicts     : %8d\n", (int)p->stats.conflicts );
+    printf( "decisions     : %8d\n", (int)p->stats.decisions );
+    printf( "propagations  : %8d\n", (int)p->stats.propagations );
+    printf( "inspects      : %8d\n", (int)p->stats.inspects );
+//    printf( "inspects2     : %8d\n", (int)p->stats.inspects2 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns a counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int * Sat_SolverGetModel( sat_solver * p, int * pVars, int nVars )
+{
+    int * pModel;
+    int i;
+    pModel = ALLOC( int, nVars );
+    for ( i = 0; i < nVars; i++ )
+    {
+        assert( pVars[i] >= 0 && pVars[i] < p->size );
+        pModel[i] = (int)(p->model.ptr[pVars[i]] == l_True);
+    }
+    return pModel;    
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates all clauses, complements unit clause of the given var.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sat_SolverDoubleClauses( sat_solver * p, int iVar )
+{
+    clause * pClause;
+    lit Lit, * pLits;
+    int RetValue, nClauses, nVarsOld, nLitsOld, nLits, c, v;
+    // get the number of variables
+    nVarsOld = p->size;
+    nLitsOld = 2 * p->size;
+    // extend the solver to depend on two sets of variables
+    sat_solver_setnvars( p, 2 * p->size );
+    // duplicate implications
+    for ( v = 0; v < nVarsOld; v++ )
+        if ( p->assigns[v] != l_Undef )
+        {
+            Lit = nLitsOld + toLitCond( v, p->assigns[v]==l_False );
+            if ( v == iVar )
+                Lit = lit_neg(Lit);
+            RetValue = sat_solver_addclause( p, &Lit, &Lit + 1 );
+            assert( RetValue );
+        }
+    // duplicate clauses
+    nClauses = vecp_size(&p->clauses);
+    for ( c = 0; c < nClauses; c++ )
+    {
+        pClause = p->clauses.ptr[c];
+        nLits = clause_size(pClause);
+        pLits = clause_begin(pClause);
+        for ( v = 0; v < nLits; v++ )
+            pLits[v] += nLitsOld;
+        RetValue = sat_solver_addclause( p, pLits, pLits + nLits );
+        assert( RetValue );
+        for ( v = 0; v < nLits; v++ )
+            pLits[v] -= nLitsOld;
+    }
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/bsat/satVec.h b/src/sat/bsat/satVec.h
new file mode 100644
index 00000000..d7fce5c0
--- /dev/null
+++ b/src/sat/bsat/satVec.h
@@ -0,0 +1,83 @@
+/**************************************************************************************************
+MiniSat -- Copyright (c) 2005, Niklas Sorensson
+http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko
+
+#ifndef satVec_h
+#define satVec_h
+
+#include <stdlib.h>
+
+// vector of 32-bit intergers (added for 64-bit portability)
+struct veci_t {
+    int    size;
+    int    cap;
+    int*   ptr;
+};
+typedef struct veci_t veci;
+
+static inline void veci_new (veci* v) {
+    v->size = 0;
+    v->cap  = 4;
+    v->ptr  = (int*)malloc(sizeof(int)*v->cap);
+}
+
+static inline void   veci_delete (veci* v)          { free(v->ptr);   }
+static inline int*   veci_begin  (veci* v)          { return v->ptr;  }
+static inline int    veci_size   (veci* v)          { return v->size; }
+static inline void   veci_resize (veci* v, int k)   { v->size = k;    } // only safe to shrink !!
+static inline void   veci_push   (veci* v, int e)
+{
+    if (v->size == v->cap) {
+        int newsize = v->cap * 2;//+1;
+        v->ptr = (int*)realloc(v->ptr,sizeof(int)*newsize);
+        v->cap = newsize; }
+    v->ptr[v->size++] = e;
+}
+
+
+// vector of 32- or 64-bit pointers
+struct vecp_t {
+    int    size;
+    int    cap;
+    void** ptr;
+};
+typedef struct vecp_t vecp;
+
+static inline void vecp_new (vecp* v) {
+    v->size = 0;
+    v->cap  = 4;
+    v->ptr  = (void**)malloc(sizeof(void*)*v->cap);
+}
+
+static inline void   vecp_delete (vecp* v)          { free(v->ptr);   }
+static inline void** vecp_begin  (vecp* v)          { return v->ptr;  }
+static inline int    vecp_size   (vecp* v)          { return v->size; }
+static inline void   vecp_resize (vecp* v, int   k) { v->size = k;    } // only safe to shrink !!
+static inline void   vecp_push   (vecp* v, void* e)
+{
+    if (v->size == v->cap) {
+        int newsize = v->cap * 2;//+1;
+        v->ptr = (void**)realloc(v->ptr,sizeof(void*)*newsize);
+        v->cap = newsize; }
+    v->ptr[v->size++] = e;
+}
+
+
+#endif