Version abc60407

15 files changed, 759 insertions, 38 deletions

diff --git a/src/sat/aig/rwrTruth.c b/src/sat/aig/rwrTruth.c
index 63a437ce..92a39f0a 100644
--- a/src/sat/aig/rwrTruth.c
+++ b/src/sat/aig/rwrTruth.c
@@ -95,7 +95,7 @@ static inline int Aig_WordCountOnes( unsigned val )
     val = (val & 0x33333333) + ((val>>2) & 0x33333333);
     val = (val & 0x0F0F0F0F) + ((val>>4) & 0x0F0F0F0F);
     val = (val & 0x00FF00FF) + ((val>>8) & 0x00FF00FF);
-    return (val & 0x0000FFFF) + (val>>8);
+    return (val & 0x0000FFFF) + (val>>16);
 }
 
 /**Function*************************************************************
diff --git a/src/sat/asat/added.c b/src/sat/asat/added.c
index 497087fb..e1b1bb2a 100644
--- a/src/sat/asat/added.c
+++ b/src/sat/asat/added.c
@@ -41,6 +41,7 @@ static inline int  lit_sign(lit l) { return (l & 1); }
 
 static void Asat_ClauseWriteDimacs( FILE * pFile, clause * pC, bool fIncrement );
 
+extern void Io_WriteCnfOutputPiMapping( FILE * pFile, int incrementVars );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -77,6 +78,7 @@ void Asat_SolverWriteDimacs( solver * p, char * pFileName, lit* assumptionsBegin
         return;
     }
     fprintf( pFile, "c CNF generated by ABC on %s\n", Extra_TimeStamp() );
+//    Io_WriteCnfOutputPiMapping( pFile, incrementVars );
     fprintf( pFile, "p cnf %d %d\n", p->size, nClauses );
 
     // write the original clauses
@@ -161,6 +163,31 @@ int * solver_get_model( solver * p, int * pVars, int nVars )
     return pModel;    
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Writes the given clause in a file in DIMACS format.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Asat_SatPrintStats( FILE * pFile, solver * p )
+{
+    printf( "Start = %4d. Conf = %6d. Dec = %6d. Prop = %7d. Insp = %8d.\n",
+        (int)p->solver_stats.starts, 
+        (int)p->solver_stats.conflicts,
+        (int)p->solver_stats.decisions,
+        (int)p->solver_stats.propagations,
+        (int)p->solver_stats.inspects );
+    printf( "Total runtime = %7.2f sec.  Var select = %7.2f sec.  Var update = %7.2f sec.\n",
+        (float)(p->timeTotal)/(float)(CLOCKS_PER_SEC),
+        (float)(p->timeSelect)/(float)(CLOCKS_PER_SEC),
+        (float)(p->timeUpdate)/(float)(CLOCKS_PER_SEC) );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/asat/jfront.c b/src/sat/asat/jfront.c
new file mode 100644
index 00000000..1def6a37
--- /dev/null
+++ b/src/sat/asat/jfront.c
@@ -0,0 +1,514 @@
+/**CFile****************************************************************
+
+  FileName    [jfront.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [C-language MiniSat solver.]
+
+  Synopsis    [Implementation of J-frontier.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: jfront.c,v 1.4 2005/09/16 22:55:03 casem Exp $]
+
+***********************************************************************/
+
+#include <stdio.h>
+#include <assert.h>
+#include "solver.h"
+#include "extra.h"
+#include "vec.h"
+
+/*
+    At any time during the solving process, the J-frontier is the set of currently 
+    unassigned variables, each of which has at least one fanin/fanout variable that 
+    is currently assigned. In the context of a CNF-based solver, default decisions 
+    based on variable activity are modified to choose the most active variable among 
+    those currently on the J-frontier.
+*/
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// variable on the J-frontier
+typedef struct Asat_JVar_t_  Asat_JVar_t;
+struct Asat_JVar_t_
+{
+    unsigned int       Num;      // variable number
+    unsigned int       nRefs;    // the number of adjacent assigned vars
+    unsigned int       Prev;     // the previous variable
+    unsigned int       Next;     // the next variable
+    unsigned int       nFans;    // the number of fanins/fanouts
+    unsigned int       Fans[0];  // the fanin/fanout variables
+};
+
+// the J-frontier as a ring of variables
+// (ring is used instead of list because it allows to control the insertion point)
+typedef struct Asat_JRing_t_ Asat_JRing_t;
+struct Asat_JRing_t_
+{
+    Asat_JVar_t *        pRoot;    // the pointer to the root
+    int                  nItems;   // the number of variables in the ring
+};
+
+// the J-frontier manager
+struct Asat_JMan_t_
+{
+    solver *             pSat;     // the SAT solver
+    Asat_JRing_t         rVars;    // the ring of variables
+    Vec_Ptr_t *          vVars;    // the pointers to variables
+    Extra_MmFlex_t *     pMem;     // the memory manager for variables
+};
+
+// getting hold of the given variable
+static inline Asat_JVar_t * Asat_JManVar( Asat_JMan_t * p, int Num )              { return !Num? NULL : Vec_PtrEntry(p->vVars, Num); }
+static inline Asat_JVar_t * Asat_JVarPrev( Asat_JMan_t * p, Asat_JVar_t * pVar )  { return Asat_JManVar(p, pVar->Prev); }
+static inline Asat_JVar_t * Asat_JVarNext( Asat_JMan_t * p, Asat_JVar_t * pVar )  { return Asat_JManVar(p, pVar->Next); }
+
+//The solver can communicate to the variable order the following parts:
+//- the array of current assignments (pSat->pAssigns)
+//- the array of variable activities (pSat->pdActivity)
+//- the array of variables currently in the cone 
+//- the array of arrays of variables adjacent to each other
+
+static inline int Asat_JVarIsInBoundary( Asat_JMan_t * p, Asat_JVar_t * pVar )  { return pVar->Next > 0;                         }
+static inline int Asat_JVarIsAssigned( Asat_JMan_t * p, Asat_JVar_t * pVar )    { return p->pSat->assigns[pVar->Num] != l_Undef; }
+//static inline int Asat_JVarIsUsedInCone( Asat_JMan_t * p, int Var )  { return p->pSat->vVarsUsed->pArray[i];    }
+
+// manipulating the ring of variables
+static void Asat_JRingAddLast( Asat_JMan_t * p, Asat_JVar_t * pVar );
+static void Asat_JRingRemove( Asat_JMan_t * p, Asat_JVar_t * pVar );
+
+// iterator through the entries in J-boundary
+#define Asat_JRingForEachEntry( p, pVar, pNext )                \
+    for ( pVar = p->rVars.pRoot,                                \
+          pNext = pVar? Asat_JVarNext(p, pVar) : NULL;          \
+          pVar;                                                 \
+          pVar = (pNext != p->rVars.pRoot)? pNext : NULL,       \
+          pNext = pVar? Asat_JVarNext(p, pVar) : NULL )
+
+// iterator through the adjacent variables
+#define Asat_JVarForEachFanio( p, pVar, pFan, i )               \
+    for ( i = 0; (i < pVar->nFans) && (((pFan) = Asat_JManVar(p, pVar->Fans[i])), 1); i++ )
+
+extern void Asat_JManAssign( Asat_JMan_t * p, int Var );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Start the J-frontier.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Asat_JMan_t * Asat_JManStart( solver * pSat, void * pCircuit )
+{
+    Vec_Vec_t * vCircuit = pCircuit;
+    Asat_JMan_t * p;
+    Asat_JVar_t * pVar;
+    Vec_Int_t * vConnect;
+    int i, nBytes, Entry, k;
+    // make sure the number of variables is less than sizeof(unsigned int)
+    assert( Vec_VecSize(vCircuit) < (1 << 16) );
+    assert( Vec_VecSize(vCircuit) == pSat->size );
+    // allocate the manager
+    p = ALLOC( Asat_JMan_t, 1 );
+    memset( p, 0, sizeof(Asat_JMan_t) );
+    p->pSat = pSat;
+    p->pMem = Extra_MmFlexStart();
+    // fill in the variables
+    p->vVars = Vec_PtrAlloc( Vec_VecSize(vCircuit) );
+    for ( i = 0; i < Vec_VecSize(vCircuit); i++ )
+    {
+        vConnect = Vec_VecEntry( vCircuit, i );
+        nBytes = sizeof(Asat_JVar_t) + sizeof(int) * Vec_IntSize(vConnect);
+        nBytes = sizeof(void *) * (nBytes / sizeof(void *) + ((nBytes % sizeof(void *)) != 0));
+        pVar = (Asat_JVar_t *)Extra_MmFlexEntryFetch( p->pMem, nBytes );
+        memset( pVar, 0, nBytes );
+        pVar->Num = i;
+        // add fanins/fanouts
+        pVar->nFans = Vec_IntSize( vConnect );
+        Vec_IntForEachEntry( vConnect, Entry, k )
+            pVar->Fans[k] = Entry;
+        // add the variable
+        Vec_PtrPush( p->vVars, pVar );
+    }
+    // set the current assignments
+    Vec_PtrForEachEntryStart( p->vVars, pVar, i, 1 )
+    {
+//      if ( !Asat_JVarIsUsedInCone(p, pVar) )
+//          continue;
+        // skip assigned vars, vars in the boundary, and vars not used in the cone
+        if ( Asat_JVarIsAssigned(p, pVar) )
+            Asat_JManAssign( p, pVar->Num );
+    }
+
+    pSat->pJMan = p;
+    return p;
+}   
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the J-frontier.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Asat_JManStop( solver * pSat )
+{
+    Asat_JMan_t * p = pSat->pJMan;
+    if ( p == NULL )
+        return;
+    pSat->pJMan = NULL;
+    Extra_MmFlexStop( p->pMem, 0 );
+    Vec_PtrFree( p->vVars );
+    free( p );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Asat_JManCheck( Asat_JMan_t * p )
+{
+    Asat_JVar_t * pVar, * pNext, * pFan;
+//    Msat_IntVec_t * vRound;
+//    int * pRound, nRound;
+//    int * pVars, nVars, i, k;
+    int i, k;
+    int Counter = 0;
+
+    // go through all the variables in the boundary
+    Asat_JRingForEachEntry( p, pVar, pNext )
+    {
+        assert( !Asat_JVarIsAssigned(p, pVar) );
+        // go though all the variables in the neighborhood
+        // and check that it is true that there is least one assigned
+//        vRound = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( p->pSat->vAdjacents, pVar->Num );
+//        nRound = Msat_IntVecReadSize( vRound );
+//        pRound = Msat_IntVecReadArray( vRound );
+//        for ( i = 0; i < nRound; i++ )
+        Asat_JVarForEachFanio( p, pVar, pFan, i )
+        {
+//            if ( !Asat_JVarIsUsedInCone(p, pFan) )
+//                continue;
+            if ( Asat_JVarIsAssigned(p, pFan) )
+                break;
+        }
+//        assert( i != pVar->nFans );
+//        if ( i == pVar->nFans )
+//            return 0;
+        if ( i == pVar->nFans )
+            Counter++;
+    }
+    if ( Counter > 0 )
+        printf( "%d(%d) ", Counter, p->rVars.nItems );
+
+    // we may also check other unassigned variables in the cone
+    // to make sure that if they are not in J-boundary, 
+    // then they do not have an assigned neighbor
+//    nVars = Msat_IntVecReadSize( p->pSat->vConeVars );
+//    pVars = Msat_IntVecReadArray( p->pSat->vConeVars );
+//    for ( i = 0; i < nVars; i++ )
+    Vec_PtrForEachEntry( p->vVars, pVar, i )
+    {
+//        assert( Asat_JVarIsUsedInCone(p, pVar) );
+        // skip assigned vars, vars in the boundary, and vars not used in the cone
+        if ( Asat_JVarIsAssigned(p, pVar) || Asat_JVarIsInBoundary(p, pVar) )
+            continue;
+        // make sure, it does not have assigned neighbors
+//        vRound = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( p->pSat->vAdjacents, pVars[i] );
+//        nRound = Msat_IntVecReadSize( vRound );
+//        pRound = Msat_IntVecReadArray( vRound );
+//        for ( i = 0; i < nRound; i++ )
+        Asat_JVarForEachFanio( p, pVar, pFan, k )
+        {
+//            if ( !Asat_JVarIsUsedInCone(p, pFan) )
+//                continue;
+            if ( Asat_JVarIsAssigned(p, pFan) )
+                break;
+        }
+//        assert( k == pVar->nFans );
+//        if ( k != pVar->nFans )
+//            return 0;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Asat_JManAssign( Asat_JMan_t * p, int Var )
+{
+//    Msat_IntVec_t * vRound;
+    Asat_JVar_t * pVar, * pFan;
+    int i, clk = clock();
+
+    // make sure the variable is in the boundary
+    assert( Var < Vec_PtrSize(p->vVars) );
+    // if it is not in the boundary (initial decision, random decision), do not remove
+    pVar = Asat_JManVar( p, Var );
+    if ( Asat_JVarIsInBoundary( p, pVar ) )
+        Asat_JRingRemove( p, pVar );
+    // add to the boundary those neighbors that are (1) unassigned, (2) not in boundary
+    // because for them we know that there is a variable (Var) which is assigned
+//    vRound = (Msat_IntVec_t *)p->pSat->vAdjacents->pArray[Var];
+//    for ( i = 0; i < vRound->nSize; i++ )
+    Asat_JVarForEachFanio( p, pVar, pFan, i )
+    {
+//        if ( !Asat_JVarIsUsedInCone(p, pFan) )
+//            continue;
+        pFan->nRefs++;
+        if ( Asat_JVarIsAssigned(p, pFan) || Asat_JVarIsInBoundary(p, pFan) )
+            continue;
+        Asat_JRingAddLast( p, pFan );
+    }
+//timeSelect += clock() - clk;
+//    Asat_JManCheck( p );
+    p->pSat->timeUpdate += clock() - clk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Asat_JManUnassign( Asat_JMan_t * p, int Var )
+{
+//    Msat_IntVec_t * vRound, * vRound2;
+    Asat_JVar_t * pVar, * pFan;
+    int i, clk = clock();//, k
+
+    // make sure the variable is not in the boundary
+    assert( Var < Vec_PtrSize(p->vVars) );
+    pVar = Asat_JManVar( p, Var );
+    assert( !Asat_JVarIsInBoundary( p, pVar ) );
+    // go through its neigbors - if one of them is assigned add this var
+    // add to the boundary those neighbors that are not there already
+    // this will also get rid of variable outside of the current cone
+    // because they are unassigned in Msat_SolverPrepare()
+//    vRound = (Msat_IntVec_t *)p->pSat->vAdjacents->pArray[Var];
+//    for ( i = 0; i < vRound->nSize; i++ )
+//        if ( Asat_JVarIsAssigned(p, vRound->pArray[i]) ) 
+//            break;
+//    if ( i != vRound->nSize )
+//        Asat_JRingAddLast( &p->rVars, &p->pVars[Var] );
+    if ( pVar->nRefs != 0 )
+        Asat_JRingAddLast( p, pVar );
+
+/*
+    // unassigning a variable may lead to its adjacents dropping from the boundary
+    for ( i = 0; i < vRound->nSize; i++ )
+        if ( Asat_JVarIsInBoundary(p, vRound->pArray[i]) )
+        { // the neighbor is in the J-boundary (and unassigned)
+            assert( !Asat_JVarIsAssigned(p, vRound->pArray[i]) );
+            vRound2 = (Msat_IntVec_t *)p->pSat->vAdjacents->pArray[vRound->pArray[i]];
+            // go through its neighbors and determine if there is at least one assigned
+            for ( k = 0; k < vRound2->nSize; k++ )
+                if ( Asat_JVarIsAssigned(p, vRound2->pArray[k]) ) 
+                    break;
+            if ( k == vRound2->nSize ) // there is no assigned vars, delete this one
+                Asat_JRingRemove( &p->rVars, &p->pVars[vRound->pArray[i]] );
+        }
+*/
+    Asat_JVarForEachFanio( p, pVar, pFan, i )
+    {
+//        if ( !Asat_JVarIsUsedInCone(p, pFan) )
+//            continue;
+        assert( pFan->nRefs > 0 );
+        pFan->nRefs--;
+        if ( !Asat_JVarIsInBoundary(p, pFan) )
+            continue;
+        // the neighbor is in the J-boundary (and unassigned)
+        assert( !Asat_JVarIsAssigned(p, pFan) );
+        // if there is no assigned vars, delete this one
+        if ( pFan->nRefs == 0 )
+            Asat_JRingRemove( p, pFan );
+    }
+
+//timeSelect += clock() - clk;
+//    Asat_JManCheck( p );
+    p->pSat->timeUpdate += clock() - clk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Asat_JManSelect( Asat_JMan_t * p )
+{
+    Asat_JVar_t * pVar, * pNext, * pVarBest;
+    double * pdActs = p->pSat->activity;
+    double dfActBest;
+    int clk = clock();
+
+    pVarBest = NULL;
+    dfActBest = -1.0;
+    Asat_JRingForEachEntry( p, pVar, pNext )
+    {
+        if ( dfActBest <= pdActs[pVar->Num] )//+ 0.00001 )
+        {
+            dfActBest = pdActs[pVar->Num];
+            pVarBest  = pVar;
+        }
+    }
+//timeSelect += clock() - clk;
+//timeAssign += clock() - clk;
+//if ( pVarBest && pVarBest->Num % 1000 == 0 )
+//printf( "%d ", p->rVars.nItems );
+
+//    Asat_JManCheck( p );
+    p->pSat->timeSelect += clock() - clk;
+    if ( pVarBest )
+    {
+//        assert( Asat_JVarIsUsedInCone(p, pVarBest) );
+        return pVarBest->Num;
+    }
+    return var_Undef;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Adds node to the end of the ring.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Asat_JRingAddLast( Asat_JMan_t * p, Asat_JVar_t * pVar )
+{
+    Asat_JRing_t * pRing = &p->rVars;
+//printf( "adding %d\n", pVar->Num );
+    // check that the node is not in a ring
+    assert( pVar->Prev == 0 );
+    assert( pVar->Next == 0 );
+    // if the ring is empty, make the node point to itself
+    pRing->nItems++;
+    if ( pRing->pRoot == NULL )
+    {
+        pRing->pRoot = pVar;
+//        pVar->pPrev  = pVar;
+        pVar->Prev   = pVar->Num;
+//        pVar->pNext  = pVar;
+        pVar->Next   = pVar->Num;
+        return;
+    }
+    // if the ring is not empty, add it as the last entry
+//    pVar->pPrev = pRing->pRoot->pPrev;
+    pVar->Prev = pRing->pRoot->Prev;
+//    pVar->pNext = pRing->pRoot;
+    pVar->Next = pRing->pRoot->Num;
+//    pVar->pPrev->pNext = pVar;
+    Asat_JVarPrev(p, pVar)->Next = pVar->Num;
+//    pVar->pNext->pPrev = pVar;
+    Asat_JVarNext(p, pVar)->Prev = pVar->Num;
+
+    // move the root so that it points to the new entry
+//    pRing->pRoot = pRing->pRoot->pPrev;
+    pRing->pRoot = Asat_JVarPrev(p, pRing->pRoot);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes the node from the ring.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Asat_JRingRemove( Asat_JMan_t * p, Asat_JVar_t * pVar )
+{
+    Asat_JRing_t * pRing = &p->rVars;
+//printf( "removing %d\n", pVar->Num );
+    // check that the var is in a ring
+    assert( pVar->Prev );
+    assert( pVar->Next );
+    pRing->nItems--;
+    if ( pRing->nItems == 0 )
+    {
+        assert( pRing->pRoot == pVar );
+//        pVar->pPrev = NULL;
+        pVar->Prev = 0;
+//        pVar->pNext = NULL;
+        pVar->Next = 0;
+        pRing->pRoot = NULL;
+        return;
+    }
+    // move the root if needed
+    if ( pRing->pRoot == pVar )
+//        pRing->pRoot = pVar->pNext;
+        pRing->pRoot = Asat_JVarNext(p, pVar);
+    // move the root to the next entry after pVar
+    // this way all the additions to the list will be traversed first
+//    pRing->pRoot = pVar->pNext;
+    pRing->pRoot = Asat_JVarPrev(p, pVar);
+    // delete the node
+//    pVar->pPrev->pNext = pVar->pNext;
+    Asat_JVarPrev(p, pVar)->Next = Asat_JVarNext(p, pVar)->Num;
+//    pVar->pNext->pPrev = pVar->pPrev;
+    Asat_JVarNext(p, pVar)->Prev = Asat_JVarPrev(p, pVar)->Num;
+//    pVar->pPrev = NULL;
+    pVar->Prev = 0;
+//    pVar->pNext = NULL;
+    pVar->Next = 0;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/asat/module.make b/src/sat/asat/module.make
index d5cf69bf..26489191 100644
--- a/src/sat/asat/module.make
+++ b/src/sat/asat/module.make
@@ -1,3 +1,4 @@
 SRC +=  src/sat/asat/added.c \
     src/sat/asat/asatmem.c \
+    src/sat/asat/jfront.c \
     src/sat/asat/solver.c
diff --git a/src/sat/asat/solver.c b/src/sat/asat/solver.c
index 1130d437..6d76d890 100644
--- a/src/sat/asat/solver.c
+++ b/src/sat/asat/solver.c
@@ -121,6 +121,7 @@ static inline void    vec_remove(vec* v, void* e)
 
 static inline void order_update(solver* s, int v) // updateorder
 {
+//    int clk = clock();
     int*    orderpos = s->orderpos;
     double* activity = s->activity;
     int*    heap     = (int*)vec_begin(&s->order);
@@ -138,6 +139,7 @@ static inline void order_update(solver* s, int v) // updateorder
     }
     heap[i]     = x;
     orderpos[x] = i;
+//    s->timeUpdate += clock() - clk;
 }
 
 static inline void order_assigned(solver* s, int v) 
@@ -146,16 +148,19 @@ static inline void order_assigned(solver* s, int v)
 
 static inline void order_unassigned(solver* s, int v) // undoorder
 {
+//    int clk = clock();
     int* orderpos = s->orderpos;
     if (orderpos[v] == -1){
         orderpos[v] = vec_size(&s->order);
         vec_push(&s->order,(void*)v);
         order_update(s,v);
     }
+//    s->timeUpdate += clock() - clk;
 }
 
 static int  order_select(solver* s, float random_var_freq) // selectvar
 {
+//    int clk = clock();
     int*    heap;
     double* activity;
     int*    orderpos;
@@ -215,9 +220,15 @@ static int  order_select(solver* s, float random_var_freq) // selectvar
             return next;
     }
 
+//    s->timeSelect += clock() - clk;
     return var_Undef;
 }
 
+// J-frontier
+extern void Asat_JManAssign( Asat_JMan_t * p, int Var );
+extern void Asat_JManUnassign( Asat_JMan_t * p, int Var );
+extern int Asat_JManSelect( Asat_JMan_t * p );
+
 //=================================================================================================
 // Activity functions:
 
@@ -236,7 +247,7 @@ static inline void act_var_bump(solver* s, int v) {
 
     //printf("bump %d %f\n", v-1, activity[v]);
 
-    if (s->orderpos[v] != -1)
+    if ( s->pJMan == NULL && s->orderpos[v] != -1 )
         order_update(s,v);
 
 }
@@ -422,7 +433,10 @@ static inline bool enqueue(solver* s, lit l, clause* from)
         reasons[v] = from;
         s->trail[s->qtail++] = l;
 
-        order_assigned(s, v);
+        if ( s->pJMan )
+            Asat_JManAssign( s->pJMan, v );
+        else
+            order_assigned(s, v);
         return 1;
     }
 }
@@ -460,8 +474,12 @@ static inline void solver_canceluntil(solver* s, int level) {
         reasons[x] = (clause*)0;
     }
 
-    for (c = s->qhead-1; c >= bound; c--)
-        order_unassigned(s,lit_var(trail[c]));
+    if ( s->pJMan )
+        for (c = s->qtail-1; c >= bound; c--)
+            Asat_JManUnassign( s->pJMan, lit_var(trail[c]) );
+    else
+        for (c = s->qhead-1; c >= bound; c--)
+            order_unassigned( s, lit_var(trail[c]) );
 
     s->qhead = s->qtail = bound;
     vec_resize(&s->trail_lim,level);
@@ -803,7 +821,7 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts)
     int*    levels          = s->levels;
     double  var_decay       = 0.95;
     double  clause_decay    = 0.999;
-    double  random_var_freq = 0.02;
+    double  random_var_freq = 0.0;//0.02;
 
     int     conflictC       = 0;
     vec     learnt_clause;
@@ -872,7 +890,10 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts)
 
             // New variable decision:
             s->solver_stats.decisions++;
-            next = order_select(s,(float)random_var_freq);
+            if ( s->pJMan )
+                next = Asat_JManSelect( s->pJMan );
+            else
+                next = order_select(s,(float)random_var_freq);
 
             if (next == var_Undef){
                 // Model found:
@@ -953,7 +974,10 @@ solver* solver_new(void)
 #else
     s->pMem = Asat_MmStepStart( 10 );
 #endif
-
+    s->pJMan = NULL;
+    s->timeTotal = clock();
+    s->timeSelect = 0;
+    s->timeUpdate = 0;
     return s;
 }
 
@@ -998,6 +1022,7 @@ void solver_delete(solver* s)
         free(s->tags     );
     }
 
+    if ( s->pJMan ) Asat_JManStop( s );
     free(s);
 }
 
@@ -1155,6 +1180,7 @@ bool solver_solve(solver* s, lit* begin, lit* end, int nConfLimit, int nImpLimit
         printf("==============================================================================\n");
 
     solver_canceluntil(s,0);
+    s->timeTotal = clock() - s->timeTotal;
     return status;
 }
 
diff --git a/src/sat/asat/solver.h b/src/sat/asat/solver.h
index 62815656..3684d259 100644
--- a/src/sat/asat/solver.h
+++ b/src/sat/asat/solver.h
@@ -64,6 +64,8 @@ static inline lit toLitCond (int v, int c) { return v + v + (int)(c != 0); }
 //=================================================================================================
 // Public interface:
 
+typedef struct Asat_JMan_t_  Asat_JMan_t;
+
 struct solver_t;
 typedef struct solver_t solver;
 
@@ -82,6 +84,12 @@ extern int     solver_nclauses(solver* s);
 extern void    Asat_SolverWriteDimacs( solver * pSat, char * pFileName,
                                        lit* assumptionsBegin, lit* assumptionsEnd,
                                        int incrementVars);
+extern void    Asat_SatPrintStats( FILE * pFile, solver * p );
+
+// J-frontier support
+extern Asat_JMan_t * Asat_JManStart( solver * pSat, void * vCircuit );
+extern void          Asat_JManStop(  solver * pSat );
+
 
 struct stats_t
 {
@@ -143,7 +151,13 @@ struct solver_t
     // the memory manager
     Asat_MmStep_t *     pMem;
 
+    // J-frontier
+    Asat_JMan_t *       pJMan;
+
     stats    solver_stats;
+    int      timeTotal;
+    int      timeSelect;
+    int      timeUpdate;
 };
  
 #ifdef __cplusplus
diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c
index 2129bfb0..9184cab9 100644
--- a/src/sat/csat/csat_apis.c
+++ b/src/sat/csat/csat_apis.c
@@ -17,6 +17,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "fraig.h"
 #include "csat_apis.h"
 
 ////////////////////////////////////////////////////////////////////////
@@ -105,6 +106,8 @@ ABC_Manager ABC_InitManager()
 ***********************************************************************/
 void ABC_ReleaseManager( ABC_Manager mng )
 {
+    CSAT_Target_ResultT * p_res = ABC_Get_Target_Result( mng,0 );
+    ABC_TargetResFree(p_res);
     if ( mng->tNode2Name ) stmm_free_table( mng->tNode2Name );
     if ( mng->tName2Node ) stmm_free_table( mng->tName2Node );
     if ( mng->pMmNames )   Extra_MmFlexStop( mng->pMmNames, 0 );
@@ -536,6 +539,7 @@ void ABC_AnalyzeTargets( ABC_Manager mng )
 ***********************************************************************/
 enum CSAT_StatusT ABC_Solve( ABC_Manager mng )
 {
+    Prove_Params_t Params, * pParams = &Params;
     int RetValue, i;
 
     // check if the target network is available
@@ -544,9 +548,16 @@ enum CSAT_StatusT ABC_Solve( ABC_Manager mng )
 
     // try to prove the miter using a number of techniques
     if ( mng->mode )
-        RetValue = Abc_NtkMiterSat( mng->pTarget, mng->nConfLimit, mng->nImpLimit, 0 );
+        RetValue = Abc_NtkMiterSat( mng->pTarget, mng->nConfLimit, mng->nImpLimit, 0, 0 );
     else
-        RetValue = Abc_NtkMiterProve( &mng->pTarget, mng->nConfLimit, mng->nImpLimit, 1, 1, 0 );
+    {
+        // set default parameters for CEC
+        Prove_ParamsSetDefault( pParams );
+        // set infinite resource limit for the final mitering
+        pParams->nMiteringLimitLast = ABC_INFINITY;
+        // call the checker
+        RetValue = Abc_NtkMiterProve( &mng->pTarget, pParams );
+    }
 
     // analyze the result
     mng->pResult = ABC_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) );
@@ -658,6 +669,14 @@ void ABC_TargetResFree( CSAT_Target_ResultT * p )
 {
     if ( p == NULL )
         return;
+    if( p->names )
+    {
+        int i = 0;
+        for ( i = 0; i < p->no_sig; i++ )
+        {
+            FREE(p->names[i]);
+        }
+    }
     FREE( p->names );
     FREE( p->values );
     free( p );
diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h
index 4e2a295e..d6215465 100644
--- a/src/sat/fraig/fraig.h
+++ b/src/sat/fraig/fraig.h
@@ -41,6 +41,7 @@ typedef struct Fraig_NodeVecStruct_t_     Fraig_NodeVec_t;
 typedef struct Fraig_HashTableStruct_t_   Fraig_HashTable_t;
 typedef struct Fraig_ParamsStruct_t_      Fraig_Params_t;
 typedef struct Fraig_PatternsStruct_t_    Fraig_Patterns_t;
+typedef struct Prove_ParamsStruct_t_      Prove_Params_t;
 
 struct Fraig_ParamsStruct_t_
 {
@@ -61,6 +62,31 @@ struct Fraig_ParamsStruct_t_
     int  fInternal;     // is set to 1 for internal fraig calls
 };
 
+struct Prove_ParamsStruct_t_
+{
+    // general parameters
+    int   fUseFraiging;          // enables fraiging
+    int   fUseRewriting;         // enables rewriting
+    int   fUseBdds;              // enables BDD construction when other methods fail
+    int   fVerbose;              // prints verbose stats
+    // iterations
+    int   nItersMax;             // the number of iterations
+    // mitering 
+    int   nMiteringLimitStart;   // starting mitering limit
+    float nMiteringLimitMulti;   // multiplicative coefficient to increase the limit in each iteration
+    // rewriting 
+    int   nRewritingLimitStart;  // the number of rewriting iterations
+    float nRewritingLimitMulti;  // multiplicative coefficient to increase the limit in each iteration
+    // fraiging 
+    int   nFraigingLimitStart;   // starting backtrack(conflict) limit
+    float nFraigingLimitMulti;   // multiplicative coefficient to increase the limit in each iteration
+    // last-gasp BDD construction
+    int   nBddSizeLimit;         // the number of BDD nodes when construction is aborted
+    int   fBddReorder;           // enables dynamic BDD variable reordering
+    // last-gasp mitering
+    int   nMiteringLimitLast;    // final mitering limit
+};
+
 ////////////////////////////////////////////////////////////////////////
 ///                       GLOBAL VARIABLES                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -155,6 +181,7 @@ extern Fraig_Node_t *      Fraig_NodeMux( Fraig_Man_t * p, Fraig_Node_t * pNode,
 extern void                Fraig_NodeSetChoice( Fraig_Man_t * pMan, Fraig_Node_t * pNodeOld, Fraig_Node_t * pNodeNew );
 
 /*=== fraigMan.c =============================================================*/
+extern void                Prove_ParamsSetDefault( Prove_Params_t * pParams );
 extern void                Fraig_ParamsSetDefault( Fraig_Params_t * pParams );
 extern void                Fraig_ParamsSetDefaultFull( Fraig_Params_t * pParams );
 extern Fraig_Man_t *       Fraig_ManCreate( Fraig_Params_t * pParams );
diff --git a/src/sat/fraig/fraigApi.c b/src/sat/fraig/fraigApi.c
index 3b8da17f..b4bdbcab 100644
--- a/src/sat/fraig/fraigApi.c
+++ b/src/sat/fraig/fraigApi.c
@@ -65,7 +65,7 @@ int               Fraig_ManReadPatternNumDynamic( Fraig_Man_t * p )           {
 // returns the number of dynamic patterns proved useful to distinquish some FRAIG nodes (this number is more than 0 after the first garbage collection of patterns)
 int               Fraig_ManReadPatternNumDynamicFiltered( Fraig_Man_t * p )   { return p->iPatsPerm;        }
 // returns the number of times FRAIG package timed out
-int               Fraig_ManReadSatFails( Fraig_Man_t * p )                    { return p->nSatFails;        }      
+int               Fraig_ManReadSatFails( Fraig_Man_t * p )                    { return p->nSatFailsReal;    }      
 
 /**Function*************************************************************
 
diff --git a/src/sat/fraig/fraigInt.h b/src/sat/fraig/fraigInt.h
index 890af13c..8e016331 100644
--- a/src/sat/fraig/fraigInt.h
+++ b/src/sat/fraig/fraigInt.h
@@ -189,7 +189,8 @@ struct Fraig_ManStruct_t_
     int                   nSatCalls;     // the number of times equivalence checking was called
     int                   nSatProof;     // the number of times a proof was found
     int                   nSatCounter;   // the number of times a counter example was found
-    int                   nSatFails;     // the number of times the SAT solver failed to complete
+    int                   nSatFails;     // the number of times the SAT solver failed to complete due to resource limit or prediction
+    int                   nSatFailsReal; // the number of times the SAT solver failed to complete due to resource limit
 
     int                   nSatCallsImp;  // the number of times equivalence checking was called
     int                   nSatProofImp;  // the number of times a proof was found
@@ -243,8 +244,9 @@ struct Fraig_NodeStruct_t_
     unsigned              fMark3   :  1; // the mark used for traversals
     unsigned              fFeedUse :  1; // the presence of the variable in the feedback
     unsigned              fFeedVal :  1; // the value of the variable in the feedback
+    unsigned              fFailTfo :  1; // the node is in the TFO of the failed SAT run
     unsigned              nFanouts :  2; // the indicator of fanouts (none, one, or many)
-    unsigned              nOnes    : 21; // the number of 1's in the random sim info
+    unsigned              nOnes    : 20; // the number of 1's in the random sim info
  
     // the children of the node
     Fraig_Node_t *        p1;            // the first child
diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c
index ff6faa33..3268ac3a 100644
--- a/src/sat/fraig/fraigMan.c
+++ b/src/sat/fraig/fraigMan.c
@@ -40,6 +40,42 @@ int timeAssign;
   SeeAlso     []
 
 ***********************************************************************/
+void Prove_ParamsSetDefault( Prove_Params_t * pParams )
+{
+    // general parameters
+    pParams->fUseFraiging         = 1;       // enables fraiging
+    pParams->fUseRewriting        = 1;       // enables rewriting
+    pParams->fUseBdds             = 1;       // enables BDD construction when other methods fail
+    pParams->fVerbose             = 0;       // prints verbose stats
+    // iterations
+    pParams->nItersMax            = 6;       // the number of iterations
+    // mitering 
+    pParams->nMiteringLimitStart  = 1000;    // starting mitering limit
+    pParams->nMiteringLimitMulti  = 2.0;     // multiplicative coefficient to increase the limit in each iteration
+    // rewriting 
+    pParams->nRewritingLimitStart = 3;       // the number of rewriting iterations
+    pParams->nRewritingLimitMulti = 1.0;     // multiplicative coefficient to increase the limit in each iteration
+    // fraiging 
+    pParams->nFraigingLimitStart  = 2;       // starting backtrack(conflict) limit
+    pParams->nFraigingLimitMulti  = 8.0;     // multiplicative coefficient to increase the limit in each iteration
+    // last-gasp BDD construction
+    pParams->nBddSizeLimit        = 1000000; // the number of BDD nodes when construction is aborted
+    pParams->fBddReorder          = 1;       // enables dynamic BDD variable reordering
+    // last-gasp mitering
+    pParams->nMiteringLimitLast   = 1000000; // final mitering limit
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the default parameters of the package.]
+
+  Description [This set of parameters is tuned for equivalence checking.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Fraig_ParamsSetDefault( Fraig_Params_t * pParams )
 {
     memset( pParams, 0, sizeof(Fraig_Params_t) );
@@ -271,8 +307,8 @@ void Fraig_ManPrintStats( Fraig_Man_t * p )
         (sizeof(Fraig_Node_t) + sizeof(unsigned)*(p->nWordsRand + p->nWordsDyna) /*+ p->nSuppWords*sizeof(unsigned)*/))/(1<<20);
     printf( "Words: Random = %d. Dynamic = %d. Used = %d. Memory = %0.2f Mb.\n", 
         p->nWordsRand, p->nWordsDyna, p->iWordPerm, nMemory );
-    printf( "Proof = %d. Counter-example = %d. Fail = %d. Zero = %d.\n", 
-        p->nSatProof, p->nSatCounter, p->nSatFails, p->nSatZeros );
+    printf( "Proof = %d. Counter-example = %d. Fail = %d. FailReal = %d. Zero = %d.\n", 
+        p->nSatProof, p->nSatCounter, p->nSatFails, p->nSatFailsReal, p->nSatZeros );
     printf( "Nodes: Final = %d. Total = %d. Mux = %d. (Exor = %d.) ClaVars = %d.\n", 
         Fraig_CountNodes(p,0), p->vNodes->nSize, Fraig_ManCountMuxes(p), Fraig_ManCountExors(p), p->nVarsClauses );
     if ( p->pSat ) Msat_SolverPrintStats( p->pSat );
diff --git a/src/sat/fraig/fraigNode.c b/src/sat/fraig/fraigNode.c
index 84509e9e..6e3d3c7d 100644
--- a/src/sat/fraig/fraigNode.c
+++ b/src/sat/fraig/fraigNode.c
@@ -176,6 +176,7 @@ Fraig_Node_t * Fraig_NodeCreate( Fraig_Man_t * p, Fraig_Node_t * p1, Fraig_Node_
     // compute the level of this node
     pNode->Level = 1 + FRAIG_MAX(Fraig_Regular(p1)->Level, Fraig_Regular(p2)->Level);
     pNode->fInv  = Fraig_NodeIsSimComplement(p1) & Fraig_NodeIsSimComplement(p2);
+    pNode->fFailTfo = Fraig_Regular(p1)->fFailTfo | Fraig_Regular(p2)->fFailTfo;
 
     // derive the simulation info 
 clk = clock();
diff --git a/src/sat/fraig/fraigPrime.c b/src/sat/fraig/fraigPrime.c
index 9745b7e6..127ad478 100644
--- a/src/sat/fraig/fraigPrime.c
+++ b/src/sat/fraig/fraigPrime.c
@@ -22,7 +22,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-// The 1,000 smallest prime numbers used to compute the hash value
+// The 1,024 smallest prime numbers used to compute the hash value
 // http://www.math.utah.edu/~alfeld/math/primelist.html
 int s_FraigPrimes[FRAIG_MAX_PRIMES] = { 2, 3, 5, 
 7, 11, 13, 17, 19, 23, 29, 31, 37, 41, 43, 47, 53, 59, 61, 67, 71, 73, 79, 83, 89, 97, 
@@ -93,7 +93,9 @@ int s_FraigPrimes[FRAIG_MAX_PRIMES] = { 2, 3, 5,
 7523, 7529, 7537, 7541, 7547, 7549, 7559, 7561, 7573, 7577, 7583, 7589, 7591, 7603, 
 7607, 7621, 7639, 7643, 7649, 7669, 7673, 7681, 7687, 7691, 7699, 7703, 7717, 7723, 
 7727, 7741, 7753, 7757, 7759, 7789, 7793, 7817, 7823, 7829, 7841, 7853, 7867, 7873, 
-7877, 7879, 7883, 7901, 7907, 7919 };
+7877, 7879, 7883, 7901, 7907, 7919, 7927, 7933, 7937, 7949, 7951, 7963, 7993, 8009, 
+8011, 8017, 8039, 8053, 8059, 8069, 8081, 8087, 8089, 8093, 8101, 8111, 8117, 8123, 
+8147, 8161 };
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c
index d4358772..aa28a4f2 100644
--- a/src/sat/fraig/fraigSat.c
+++ b/src/sat/fraig/fraigSat.c
@@ -17,6 +17,7 @@
 ***********************************************************************/
 
 #include "fraigInt.h"
+#include "math.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -304,6 +305,20 @@ int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t *
     assert( !Fraig_IsComplement(pOld) );
     assert( pNew != pOld );
 
+    // if at least one of the nodes is a failed node, perform adjustments:
+    // if the backtrack limit is small, simply skip this node
+    // if the backtrack limit is > 10, take the quare root of the limit
+    if ( nBTLimit > 0 && (pOld->fFailTfo || pNew->fFailTfo) )
+    {
+        p->nSatFails++;
+//            return 0;
+//        if ( nBTLimit > 10 )
+//            nBTLimit /= 10;
+        if ( nBTLimit <= 10 )
+            return 0;
+        nBTLimit = (int)sqrt(nBTLimit);
+    }
+
     p->nSatCalls++;
 
     // make sure the solver is allocated and has enough variables
@@ -394,13 +409,27 @@ PRT( "time", clock() - clk );
 
         // record the counter example
         Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew );
+
+//        if ( pOld->fFailTfo || pNew->fFailTfo )
+//            printf( "*" );
+//        printf( "s(%d)", pNew->Level );
         p->nSatCounter++;
         return 0;
     }
     else // if ( RetValue1 == MSAT_UNKNOWN )
     {
 p->time3 += clock() - clk;
-        p->nSatFails++;
+
+//        if ( pOld->fFailTfo || pNew->fFailTfo )
+//            printf( "*" );
+//        printf( "T(%d)", pNew->Level );
+
+        // mark the node as the failed node
+        if ( pOld != p->pConst1 ) 
+            pOld->fFailTfo = 1;
+        pNew->fFailTfo = 1;
+//        p->nSatFails++;
+        p->nSatFailsReal++;
         return 0;
     }
 
@@ -454,17 +483,34 @@ PRT( "time", clock() - clk );
         // record the counter example
         Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew );
         p->nSatCounter++;
+
+//        if ( pOld->fFailTfo || pNew->fFailTfo )
+//            printf( "*" );
+//        printf( "s(%d)", pNew->Level );
         return 0;
     }
     else // if ( RetValue1 == MSAT_UNKNOWN )
     {
 p->time3 += clock() - clk;
-        p->nSatFails++;
+
+//        if ( pOld->fFailTfo || pNew->fFailTfo )
+//            printf( "*" );
+//        printf( "T(%d)", pNew->Level );
+
+        // mark the node as the failed node
+        pOld->fFailTfo = 1;
+        pNew->fFailTfo = 1;
+//        p->nSatFails++;
+        p->nSatFailsReal++;
         return 0;
     }
 
     // return SAT proof
     p->nSatProof++;
+
+//    if ( pOld->fFailTfo || pNew->fFailTfo )
+//        printf( "*" );
+//    printf( "u(%d)", pNew->Level );
     return 1;
 }
 
diff --git a/src/sat/msat/msatOrderJ.c b/src/sat/msat/msatOrderJ.c
index 5cba1165..4db7ff7b 100644
--- a/src/sat/msat/msatOrderJ.c
+++ b/src/sat/msat/msatOrderJ.c
@@ -38,7 +38,7 @@ struct Msat_OrderVar_t_
 {
     Msat_OrderVar_t    * pNext;
     Msat_OrderVar_t    * pPrev;
-    int                 Num;
+    int                  Num;
 };
 
 // the ring of variables data structure (J-boundary)
@@ -170,7 +170,8 @@ int Msat_OrderCheck( Msat_Order_t * p )
     Msat_OrderVar_t * pVar, * pNext;
     Msat_IntVec_t * vRound;
     int * pRound, nRound;
-    int * pVars, nVars, i;
+    int * pVars, nVars, i, k;
+    int Counter = 0;
 
     // go through all the variables in the boundary
     Msat_OrderRingForEachEntry( p->rVars.pRoot, pVar, pNext )
@@ -188,10 +189,14 @@ int Msat_OrderCheck( Msat_Order_t * p )
             if ( Msat_OrderVarIsAssigned(p, pRound[i]) )
                 break;
         }
-        assert( i != nRound );
-        if ( i != nRound )
-            return 0;
+//        assert( i != nRound );
+//        if ( i == nRound )
+//            return 0;
+        if ( i == nRound )
+            Counter++;
     }
+    if ( Counter > 0 )
+        printf( "%d(%d) ", Counter, p->rVars.nItems );
 
     // we may also check other unassigned variables in the cone
     // to make sure that if they are not in J-boundary, 
@@ -209,16 +214,16 @@ int Msat_OrderCheck( Msat_Order_t * p )
         vRound = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( p->pSat->vAdjacents, pVars[i] );
         nRound = Msat_IntVecReadSize( vRound );
         pRound = Msat_IntVecReadArray( vRound );
-        for ( i = 0; i < nRound; i++ )
+        for ( k = 0; k < nRound; k++ )
         {
-            if ( !Msat_OrderVarIsUsedInCone(p, pRound[i]) )
+            if ( !Msat_OrderVarIsUsedInCone(p, pRound[k]) )
                 continue;
-            if ( Msat_OrderVarIsAssigned(p, pRound[i]) )
+            if ( Msat_OrderVarIsAssigned(p, pRound[k]) )
                 break;
         }
-        assert( i == nRound );
-        if ( i == nRound )
-            return 0;
+//        assert( k == nRound );
+//        if ( k != nRound )
+//            return 0;
     }
     return 1;
 }
@@ -256,7 +261,7 @@ int Msat_OrderVarSelect( Msat_Order_t * p )
     Msat_OrderVar_t * pVar, * pNext, * pVarBest;
     double * pdActs = p->pSat->pdActivity;
     double dfActBest;
-    int clk = clock();
+//    int clk = clock();
 
     pVarBest = NULL;
     dfActBest = -1.0;
@@ -268,12 +273,13 @@ int Msat_OrderVarSelect( Msat_Order_t * p )
             pVarBest  = pVar;
         }
     }
-timeSelect += clock() - clk;
-timeAssign += clock() - clk;
+//timeSelect += clock() - clk;
+//timeAssign += clock() - clk;
 
 //if ( pVarBest && pVarBest->Num % 1000 == 0 )
 //printf( "%d ", p->rVars.nItems );
 
+//    Msat_OrderCheck( p );
     if ( pVarBest )
     {
         assert( Msat_OrderVarIsUsedInCone(p, pVarBest->Num) );
@@ -296,7 +302,7 @@ timeAssign += clock() - clk;
 void Msat_OrderVarAssigned( Msat_Order_t * p, int Var )
 {
     Msat_IntVec_t * vRound;
-    int i, clk = clock();
+    int i;//, clk = clock();
 
     // make sure the variable is in the boundary
     assert( Var < p->nVarsAlloc );
@@ -316,7 +322,7 @@ void Msat_OrderVarAssigned( Msat_Order_t * p, int Var )
             continue;
         Msat_OrderRingAddLast( &p->rVars, &p->pVars[vRound->pArray[i]] );
     }
-timeSelect += clock() - clk;
+//timeSelect += clock() - clk;
 //    Msat_OrderCheck( p );
 }
 
@@ -334,7 +340,7 @@ timeSelect += clock() - clk;
 void Msat_OrderVarUnassigned( Msat_Order_t * p, int Var )
 {
     Msat_IntVec_t * vRound, * vRound2;
-    int i, k, clk = clock();
+    int i, k;//, clk = clock();
 
     // make sure the variable is not in the boundary
     assert( Var < p->nVarsAlloc );
@@ -363,7 +369,7 @@ void Msat_OrderVarUnassigned( Msat_Order_t * p, int Var )
             if ( k == vRound2->nSize ) // there is no assigned vars, delete this one
                 Msat_OrderRingRemove( &p->rVars, &p->pVars[vRound->pArray[i]] );
         }
-timeSelect += clock() - clk;
+//timeSelect += clock() - clk;
 //    Msat_OrderCheck( p );
 }
 
@@ -450,7 +456,7 @@ void Msat_OrderRingRemove( Msat_OrderRing_t * pRing, Msat_OrderVar_t * pVar )
         pRing->pRoot = pVar->pNext;
     // move the root to the next entry after pVar
     // this way all the additions to the list will be traversed first
-//    pRing->pRoot = pVar->pNext;
+//    pRing->pRoot = pVar->pPrev;
     // delete the node
     pVar->pPrev->pNext = pVar->pNext;
     pVar->pNext->pPrev = pVar->pPrev;