Version abc90220

15 files changed, 1672 insertions, 131 deletions

diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c
index b5c7272b..1852ff03 100644
--- a/src/aig/aig/aigUtil.c
+++ b/src/aig/aig/aigUtil.c
@@ -1084,6 +1084,8 @@ char * Aig_FileNameGenericAppend( char * pBase, char * pSuffix )
     if ( (pDot = strrchr( Buffer, '.' )) )
         *pDot = 0;
     strcat( Buffer, pSuffix );
+    if ( (pDot = strrchr( Buffer, '\\' )) || (pDot = strrchr( Buffer, '/' )) )
+        return pDot+1;
     return Buffer;
 }
 
diff --git a/src/aig/cec/cecSolve.c b/src/aig/cec/cecSolve.c
index 0ec7df45..e4daf719 100644
--- a/src/aig/cec/cecSolve.c
+++ b/src/aig/cec/cecSolve.c
@@ -444,7 +444,8 @@ p->timeSatUnsat += clock() - clk;
         RetValue = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
         assert( RetValue );
         p->nSatUnsat++;
-        p->nConfUnsat += p->pSat->stats.conflicts - nConflicts;
+        p->nConfUnsat += p->pSat->stats.conflicts - nConflicts;       
+//printf( "UNSAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
         return 1;
     }
     else if ( RetValue == l_True )
@@ -452,6 +453,7 @@ p->timeSatUnsat += clock() - clk;
 p->timeSatSat += clock() - clk;
         p->nSatSat++;
         p->nConfSat += p->pSat->stats.conflicts - nConflicts;
+//printf( "SAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
         return 0;
     }
     else // if ( RetValue == l_Undef )
@@ -459,6 +461,7 @@ p->timeSatSat += clock() - clk;
 p->timeSatUndec += clock() - clk;
         p->nSatUndec++;
         p->nConfUndec += p->pSat->stats.conflicts - nConflicts;
+//printf( "UNDEC after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
         return -1;
     }
 }
@@ -477,10 +480,18 @@ p->timeSatUndec += clock() - clk;
 ***********************************************************************/
 void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars )
 {
+    static int Counter;
+//    char Buffer[1000];
+
     Bar_Progress_t * pProgress = NULL;
     Cec_ManSat_t * p;
     Gia_Obj_t * pObj;
     int i, status, clk = clock();
+
+//    sprintf( Buffer, "gia%03d.aig", Counter++ );
+//Gia_WriteAiger( pAig, Buffer, 0, 0 );
+//printf( "Dumpted slice into file \"%s\".\n", Buffer );
+
     // reset the manager
     if ( pPat )
     {
@@ -501,6 +512,8 @@ void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPar
             pObj->fMark1 = 1;
             continue;
         }
+//printf( "Output %6d : ", i );
+
         Bar_ProgressUpdate( pProgress, i, "SAT..." );
         status = Cec_ManSatCheckNode( p, pObj );
         pObj->fMark0 = (status == 0);
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 73940ffa..b77dd76f 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -24,7 +24,7 @@
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
-
+ 
 #include "aig.h"
 
 ////////////////////////////////////////////////////////////////////////
@@ -303,6 +303,8 @@ static inline int Gia_XsimAndCond( int Value0, int fCompl0, int Value1, int fCom
     for ( i = 1; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ )
 #define Gia_ManForEachObjVec( vVec, p, pObj, i )                        \
     for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Gia_ManObj(p, Vec_IntEntry(vVec,i))); i++ )
+#define Gia_ManForEachObjVecLit( vVec, p, pObj, fCompl, i )             \
+    for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Gia_ManObj(p, Gia_Lit2Var(Vec_IntEntry(vVec,i)))) && (((fCompl) = Gia_LitIsCompl(Vec_IntEntry(vVec,i))),1); i++ )
 #define Gia_ManForEachAnd( p, pObj, i )                                 \
     for ( i = 0; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ )  if ( !Gia_ObjIsAnd(pObj) ) {} else
 #define Gia_ManForEachCi( p, pObj, i )                                  \
@@ -373,11 +375,12 @@ extern void                Gia_ManHashStart( Gia_Man_t * p );
 extern void                Gia_ManHashStop( Gia_Man_t * p );  
 extern int                 Gia_ManHashAnd( Gia_Man_t * p, int iLit0, int iLit1 ); 
 extern int                 Gia_ManHashXor( Gia_Man_t * p, int iLit0, int iLit1 ); 
+extern int                 Gia_ManHashMux( Gia_Man_t * p, int iCtrl, int iData1, int iData0 );
 extern int                 Gia_ManHashAndTry( Gia_Man_t * p, int iLit0, int iLit1 );
 extern Gia_Man_t *         Gia_ManRehash( Gia_Man_t * p );
 /*=== giaLogic.c ===========================================================*/
 extern void                Gia_ManTestDistance( Gia_Man_t * p );
-extern void                Gia_ManSolveProblem( Gia_Man_t * pGia, int nDims, int nSols );
+extern void                Gia_ManSolveProblem( Gia_Man_t * pGia, int nDims, int nSols, int fCluster, int fDump, int fVerbose );
  /*=== giaMan.c ===========================================================*/
 extern Gia_Man_t *         Gia_ManStart( int nObjsMax ); 
 extern void                Gia_ManStop( Gia_Man_t * p );  
diff --git a/src/aig/gia/giaCSat0.c b/src/aig/gia/giaCSat0.c
new file mode 100644
index 00000000..599ad43c
--- /dev/null
+++ b/src/aig/gia/giaCSat0.c
@@ -0,0 +1,326 @@
+/**CFile****************************************************************
+
+  FileName    [giaCsat0.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Scalable AIG package.]
+
+  Synopsis    [Circuit-based SAT solver.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: giaCsat0.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int          Sat_ObjXValue( Gia_Obj_t * pObj )          { return (pObj->fMark1 << 1) | pObj->fMark0; }
+static inline void         Sat_ObjSetXValue( Gia_Obj_t * pObj, int v) { pObj->fMark0 = (v & 1); pObj->fMark1 = ((v >> 1) & 1); }
+
+static inline int          Sat_VarIsAssigned( Gia_Obj_t * pVar )      { return pVar->Value > 0;                    }
+static inline void         Sat_VarAssign( Gia_Obj_t * pVar, int i )   { assert(!pVar->Value); pVar->Value = i;     }
+static inline void         Sat_VarUnassign( Gia_Obj_t * pVar )        { assert(pVar->Value);  pVar->Value = 0;     }
+static inline int          Sat_VarValue( Gia_Obj_t * pVar )           { assert(pVar->Value);  return pVar->fMark0; }
+static inline void         Sat_VarSetValue( Gia_Obj_t * pVar, int v ) { assert(pVar->Value);  pVar->fMark0 = v;    }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Collects nodes in the cone and initialized them to x.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_SatCollectCone_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vVisit )
+{
+    if ( Sat_ObjXValue(pObj) == GIA_UND )
+        return;
+    assert( pObj->Value == 0 );
+    if ( Gia_ObjIsAnd(pObj) )
+    {
+        Gia_SatCollectCone_rec( p, Gia_ObjFanin0(pObj), vVisit );
+        Gia_SatCollectCone_rec( p, Gia_ObjFanin1(pObj), vVisit );
+    }
+    assert( Sat_ObjXValue(pObj) == 0 );
+    Sat_ObjSetXValue( pObj, GIA_UND );
+    Vec_IntPush( vVisit, Gia_ObjId(p, pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects nodes in the cone and initialized them to x.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_SatCollectCone( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vVisit )
+{
+    assert( !Gia_IsComplement(pObj) );
+    assert( !Gia_ObjIsConst0(pObj) );
+    assert( Sat_ObjXValue(pObj) == 0 );
+    Vec_IntClear( vVisit );
+    Gia_SatCollectCone_rec( p, pObj, vVisit );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects nodes in the cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_SatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vCex, Vec_Int_t * vVisit )
+{
+    Gia_Obj_t * pObj;
+    int i, Entry, Value, Value0, Value1;
+    assert( Gia_ObjIsCo(pRoot) );
+    assert( !Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) );
+    // collect nodes and initialized them to x
+    Gia_SatCollectCone( p, Gia_ObjFanin0(pRoot), vVisit );
+    // set binary values to nodes in the counter-example
+    Vec_IntForEachEntry( vCex, Entry, i )
+    {
+        pObj = Gia_NotCond( Gia_ManObj( p, Gia_Lit2Var(Entry) ), Gia_LitIsCompl(Entry) );
+        Sat_ObjSetXValue( Gia_Regular(pObj), Gia_IsComplement(pObj)? GIA_ZER : GIA_ONE );
+        assert( Sat_ObjXValue(Gia_Regular(pObj)) == (Gia_IsComplement(pObj)? GIA_ZER : GIA_ONE) );
+    }
+    // simulate
+    Gia_ManForEachObjVec( vVisit, p, pObj, i )
+    {
+        if ( Gia_ObjIsCi(pObj) )
+            continue;
+        assert( Gia_ObjIsAnd(pObj) );
+        Value0 = Sat_ObjXValue( Gia_ObjFanin0(pObj) );
+        Value1 = Sat_ObjXValue( Gia_ObjFanin1(pObj) );
+        Value = Gia_XsimAndCond( Value0, Gia_ObjFaninC0(pObj), Value1, Gia_ObjFaninC1(pObj) );
+        Sat_ObjSetXValue( pObj, Value );
+    }
+    Value = Gia_XsimNotCond( Value, Gia_ObjFaninC0(pRoot) );
+    if ( Value != GIA_ONE )
+        printf( "Gia_SatVerifyPattern(): Verification failed.\n" );
+    assert( Value == GIA_ONE );
+    // clean the nodes
+    Gia_ManForEachObjVec( vVisit, p, pObj, i )
+        Sat_ObjSetXValue( pObj, 0 );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Undoes the assignment since the given value.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_SatUndo_rec( Gia_Obj_t * pObj, unsigned Value, Vec_Int_t * vCex )
+{
+    if ( pObj->Value < Value )
+        return;
+    pObj->Value = 0;
+    if ( Gia_ObjIsCi(pObj) )
+    {
+        if ( vCex ) Vec_IntPush( vCex, Gia_Var2Lit(Gia_ObjCioId(pObj), !pObj->fPhase) );
+        return;
+    }
+    Gia_SatUndo_rec( Gia_ObjFanin0(pObj), Value, vCex );
+    Gia_SatUndo_rec( Gia_ObjFanin1(pObj), Value, vCex );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Propagates assignments.]
+
+  Description [Returns 1 if UNSAT, 0 if SAT.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_SatProp_rec( Gia_Obj_t * pObj, unsigned Phase, unsigned * pValue, int * pnConfs )
+{
+    int Value = *pValue;
+    if ( pObj->Value )
+        return pObj->fPhase != Phase;
+    if ( Gia_ObjIsCi(pObj) )
+    {
+        pObj->Value = Value;
+        pObj->fPhase = Phase;
+        return 0;
+    }
+    if ( Phase ) // output of AND should be 1
+    {
+        if ( Gia_SatProp_rec( Gia_ObjFanin0(pObj), !Gia_ObjFaninC0(pObj), pValue, pnConfs ) )
+            return 1;
+        if ( Gia_SatProp_rec( Gia_ObjFanin1(pObj), !Gia_ObjFaninC1(pObj), pValue, pnConfs ) )
+        {
+            Gia_SatUndo_rec( Gia_ObjFanin0(pObj), Value, NULL );
+            return 1;
+        }
+/*
+        if ( Gia_SatProp_rec( Gia_ObjFanin1(pObj), !Gia_ObjFaninC1(pObj), pValue, pnConfs ) )
+            return 1;
+        if ( Gia_SatProp_rec( Gia_ObjFanin0(pObj), !Gia_ObjFaninC0(pObj), pValue, pnConfs ) )
+        {
+            Gia_SatUndo_rec( Gia_ObjFanin1(pObj), Value, NULL );
+            return 1;
+        }
+*/
+        pObj->Value = Value;
+        pObj->fPhase = 1;
+        return 0; 
+    }
+    // output of AND should be 0
+
+    (*pValue)++;
+    if ( !Gia_SatProp_rec( Gia_ObjFanin1(pObj), Gia_ObjFaninC1(pObj), pValue, pnConfs ) )
+    {
+        pObj->Value = Value;
+        pObj->fPhase = 0;
+        return 0;
+    }
+    if ( !*pnConfs )
+        return 1;
+
+    (*pValue)++;
+    if ( !Gia_SatProp_rec( Gia_ObjFanin0(pObj), Gia_ObjFaninC0(pObj), pValue, pnConfs ) )
+    {
+        pObj->Value = Value;
+        pObj->fPhase = 0;
+        return 0;
+    }
+    if ( !*pnConfs )
+        return 1;
+    // cannot be satisfied
+    (*pnConfs)--;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Procedure to solve SAT for the node.]
+
+  Description [Returns 1 if UNSAT, 0 if SAT, and -1 if undecided.]
+               
+  SideEffects [Precondition: pObj->Value should be 0.]
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_SatSolve( Gia_Obj_t * pObj, unsigned Phase, int nConfsMax, Vec_Int_t * vCex )
+{
+    int Value = 1;
+    int nConfs = nConfsMax? nConfsMax : (1<<30);
+    assert( !Gia_IsComplement(pObj) );
+    assert( !Gia_ObjIsConst0(pObj) );
+    assert( pObj->Value == 0 );
+    if ( Gia_SatProp_rec( pObj, Phase, &Value, &nConfs ) )
+    {
+//        if ( nConfs )
+//            printf( "UNSAT after %d conflicts\n", nConfsMax - nConfs );
+//        else
+//            printf( "UNDEC after %d conflicts\n", nConfsMax );
+        return nConfs? 1 : -1;
+    }
+    Vec_IntClear( vCex );
+    Gia_SatUndo_rec( pObj, 1, vCex );
+//    printf( "SAT after %d conflicts\n", nConfsMax - nConfs );
+    return 0;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Procedure to test the new SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_SatSolveTest( Gia_Man_t * p )
+{
+    int nConfsMax = 1000;
+    int CountUnsat, CountSat, CountUndec;
+    Vec_Int_t * vCex;
+    Vec_Int_t * vVisit;
+    Gia_Obj_t * pRoot; 
+    int i, RetValue, clk = clock();
+    // prepare AIG
+    Gia_ManCleanValue( p );
+    Gia_ManCleanMark0( p );
+    Gia_ManCleanMark1( p );
+    vCex   = Vec_IntAlloc( 100 );
+    vVisit = Vec_IntAlloc( 100 );
+    // solve for each output
+    CountUnsat = CountSat = CountUndec = 0;
+    Gia_ManForEachCo( p, pRoot, i )
+    {
+        if ( Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) )
+            continue;
+//printf( "Output %6d : ", i );
+        RetValue = Gia_SatSolve( Gia_ObjFanin0(pRoot), !Gia_ObjFaninC0(pRoot), nConfsMax, vCex );
+        if ( RetValue == 1 )
+            CountUnsat++;
+        else if ( RetValue == -1 )
+            CountUndec++;
+        else 
+        {
+//            Gia_Obj_t * pTemp;
+//            int k;
+            assert( RetValue == 0 );
+            CountSat++;
+/*
+            Vec_IntForEachEntry( vCex, pTemp, k )
+//                printf( "%s%d ", Gia_IsComplement(pTemp)? "!": "", Gia_ObjCioId(Gia_Regular(pTemp)) );
+                printf( "%s%d ", Gia_IsComplement(pTemp)? "!": "", Gia_ObjId(p,Gia_Regular(pTemp)) );
+            printf( "\n" );
+*/
+//            Gia_SatVerifyPattern( p, pRoot, vCex, vVisit );
+        }
+//        Gia_ManCheckMark0( p );
+//        Gia_ManCheckMark1( p );
+    }
+    Vec_IntFree( vCex );
+    Vec_IntFree( vVisit );
+    printf( "Unsat = %d. Sat = %d. Undec = %d.  ", CountUnsat, CountSat, CountUndec );
+    ABC_PRT( "Time", clock() - clk );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/gia/giaCSat1.c b/src/aig/gia/giaCSat1.c
new file mode 100644
index 00000000..12b7071f
--- /dev/null
+++ b/src/aig/gia/giaCSat1.c
@@ -0,0 +1,602 @@
+/**CFile****************************************************************
+
+  FileName    [giaCsat1.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Scalable AIG package.]
+
+  Synopsis    [Circuit-based SAT solver.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: giaCsat1.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+
+typedef struct Css_Fan_t_ Css_Fan_t;
+struct Css_Fan_t_
+{
+    unsigned       iFan     : 31;    // ID of the fanin/fanout
+    unsigned       fCompl   :  1;    // complemented attribute
+};
+
+typedef struct Css_Obj_t_ Css_Obj_t;
+struct Css_Obj_t_
+{
+    unsigned       fCi      :  1;    // terminal node CI
+    unsigned       fCo      :  1;    // terminal node CO
+    unsigned       fAssign  :  1;    // assigned variable
+    unsigned       fValue   :  1;    // variable value
+    unsigned       fPhase   :  1;    // value under 000 pattern
+    unsigned       nFanins  :  5;    // the number of fanins
+    unsigned       nFanouts : 22;    // total number of fanouts
+    unsigned       hHandle;          // application specific data
+    union {
+    unsigned       iFanouts;         // application specific data
+    int            TravId;           // ID of the node
+    };
+    Css_Fan_t      Fanios[0];        // the array of fanins/fanouts
+};
+
+typedef struct Css_Man_t_ Css_Man_t;
+struct Css_Man_t_
+{
+    Gia_Man_t *    pGia;             // the original AIG manager
+    Vec_Int_t *    vCis;             // the vector of CIs (PIs + LOs)
+    Vec_Int_t *    vCos;             // the vector of COs (POs + LIs)
+    int            nObjs;            // the number of objects
+    int            nNodes;           // the number of nodes
+    int *          pObjData;         // the logic network defined for the AIG
+    int            nObjData;         // the size of array to store the logic network
+    int *          pLevels;          // the linked lists of levels
+    int            nLevels;          // the max number of logic levels
+    int            nTravIds;         // traversal ID to mark the cones
+    Vec_Int_t *    vTrail;           // sequence of assignments
+    int            nConfsMax;         // max number of conflicts
+};
+
+static inline unsigned    Gia_ObjHandle( Gia_Obj_t * pObj )                           { return pObj->Value;                                 } 
+
+static inline int         Css_ObjIsCi( Css_Obj_t * pObj )                             { return pObj->fCi;                                   } 
+static inline int         Css_ObjIsCo( Css_Obj_t * pObj )                             { return pObj->fCo;                                   } 
+static inline int         Css_ObjIsNode( Css_Obj_t * pObj )                           { return!pObj->fCi &&!pObj->fCo && pObj->nFanins > 0; } 
+static inline int         Css_ObjIsConst0( Css_Obj_t * pObj )                         { return!pObj->fCi &&!pObj->fCo && pObj->nFanins == 0;} 
+
+static inline int         Css_ObjFaninNum( Css_Obj_t * pObj )                         { return pObj->nFanins;                               } 
+static inline int         Css_ObjFanoutNum( Css_Obj_t * pObj )                        { return pObj->nFanouts;                              } 
+static inline int         Css_ObjSize( Css_Obj_t * pObj )                             { return sizeof(Css_Obj_t) / 4 + pObj->nFanins + pObj->nFanouts;  } 
+static inline int         Css_ObjId( Css_Obj_t * pObj )                               { assert( 0 ); return -1;                             } 
+
+static inline Css_Obj_t * Css_ManObj( Css_Man_t * p, unsigned iHandle )               { return (Css_Obj_t *)(p->pObjData + iHandle);        } 
+static inline Css_Obj_t * Css_ObjFanin( Css_Obj_t * pObj, int i )                     { return (Css_Obj_t *)(((int *)pObj) - pObj->Fanios[i].iFan);               } 
+static inline Css_Obj_t * Css_ObjFanout( Css_Obj_t * pObj, int i )                    { return (Css_Obj_t *)(((int *)pObj) + pObj->Fanios[pObj->nFanins+i].iFan); } 
+static inline int         Css_ObjFaninC( Css_Obj_t * pObj, int i )                    { return pObj->Fanios[i].fCompl;                      } 
+static inline int         Css_ObjFanoutC( Css_Obj_t * pObj, int i )                   { return pObj->Fanios[pObj->nFanins+i].fCompl;        } 
+
+static inline int         Css_ManObjNum( Css_Man_t * p )                              { return p->nObjs;                                    } 
+static inline int         Css_ManNodeNum( Css_Man_t * p )                             { return p->nNodes;                                   } 
+ 
+static inline void        Css_ManIncrementTravId( Css_Man_t * p )                     { p->nTravIds++;                                      }
+static inline void        Css_ObjSetTravId( Css_Obj_t * pObj, int TravId )            { pObj->TravId = TravId;                              }
+static inline void        Css_ObjSetTravIdCurrent( Css_Man_t * p, Css_Obj_t * pObj )  { pObj->TravId = p->nTravIds;                         }
+static inline void        Css_ObjSetTravIdPrevious( Css_Man_t * p, Css_Obj_t * pObj ) { pObj->TravId = p->nTravIds - 1;                     }
+static inline int         Css_ObjIsTravIdCurrent( Css_Man_t * p, Css_Obj_t * pObj )   { return ((int)pObj->TravId == p->nTravIds);          }
+static inline int         Css_ObjIsTravIdPrevious( Css_Man_t * p, Css_Obj_t * pObj )  { return ((int)pObj->TravId == p->nTravIds - 1);      }
+
+static inline int   Css_VarIsAssigned( Css_Obj_t * pVar )      { return pVar->fAssign;                        }
+static inline void  Css_VarAssign( Css_Obj_t * pVar )          { assert(!pVar->fAssign); pVar->fAssign = 1;   }
+static inline void  Css_VarUnassign( Css_Obj_t * pVar )        { assert(pVar->fAssign);  pVar->fAssign = 0;   }
+static inline int   Css_VarValue( Css_Obj_t * pVar )           { assert(pVar->fAssign);  return pVar->fValue; }
+static inline void  Css_VarSetValue( Css_Obj_t * pVar, int v ) { assert(pVar->fAssign);  pVar->fValue = v;    }
+
+#define Css_ManForEachObj( p, pObj, i )               \
+    for ( i = 0; (i < p->nObjData) && (pObj = Css_ManObj(p,i)); i += Css_ObjSize(pObj) )
+#define Css_ManForEachObjVecStart( vVec, p, pObj, i, iStart )            \
+    for ( i = iStart; (i < Vec_IntSize(vVec)) && (pObj = Css_ManObj(p,Vec_IntEntry(vVec,i))); i++ )
+#define Css_ManForEachNode( p, pObj, i )              \
+    for ( i = 0; (i < p->nObjData) && (pObj = Css_ManObj(p,i)); i += Css_ObjSize(pObj) ) if ( Css_ObjIsTerm(pObj) ) {} else
+#define Css_ObjForEachFanin( pObj, pNext, i )         \
+    for ( i = 0; (i < (int)pObj->nFanins) && (pNext = Css_ObjFanin(pObj,i)); i++ )
+#define Css_ObjForEachFanout( pObj, pNext, i )        \
+    for ( i = 0; (i < (int)pObj->nFanouts) && (pNext = Css_ObjFanout(pObj,i)); i++ )
+#define Css_ObjForEachFaninLit( pObj, pNext, fCompl, i )         \
+    for ( i = 0; (i < (int)pObj->nFanins) && (pNext = Css_ObjFanin(pObj,i)) && ((fCompl = Css_ObjFaninC(pObj,i)),1); i++ )
+#define Css_ObjForEachFanoutLit( pObj, pNext, fCompl, i )        \
+    for ( i = 0; (i < (int)pObj->nFanouts) && (pNext = Css_ObjFanout(pObj,i)) && ((fCompl = Css_ObjFanoutC(pObj,i)),1); i++ )
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Creates logic network isomorphic to the given AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Css_Man_t * Css_ManCreateLogicSimple( Gia_Man_t * pGia )
+{
+    Css_Man_t * p;
+    Css_Obj_t * pObjLog, * pFanLog;
+    Gia_Obj_t * pObj;
+    int i, iHandle = 0;
+    p = ABC_CALLOC( Css_Man_t, 1 );
+    p->pGia = pGia;
+    p->vCis = Vec_IntAlloc( Gia_ManCiNum(pGia) );
+    p->vCos = Vec_IntAlloc( Gia_ManCoNum(pGia) );
+    p->nObjData = (sizeof(Css_Obj_t) / 4) * Gia_ManObjNum(pGia) + 4 * Gia_ManAndNum(pGia) + 2 * Gia_ManCoNum(pGia);
+    p->pObjData = ABC_CALLOC( int, p->nObjData );
+    ABC_FREE( pGia->pRefs );
+    Gia_ManCreateRefs( pGia );
+    Gia_ManForEachObj( pGia, pObj, i )
+    {
+        pObj->Value = iHandle;
+        pObjLog = Css_ManObj( p, iHandle );
+        pObjLog->nFanins  = 0;
+        pObjLog->nFanouts = Gia_ObjRefs( pGia, pObj );
+        pObjLog->hHandle  = iHandle;
+        pObjLog->iFanouts = 0;
+        if ( Gia_ObjIsAnd(pObj) )
+        {
+            pFanLog = Css_ManObj( p, Gia_ObjHandle(Gia_ObjFanin0(pObj)) ); 
+            pFanLog->Fanios[pFanLog->nFanins + pFanLog->iFanouts].iFan = 
+                pObjLog->Fanios[pObjLog->nFanins].iFan = pObjLog->hHandle - pFanLog->hHandle;
+            pFanLog->Fanios[pFanLog->nFanins + pFanLog->iFanouts++].fCompl =
+                pObjLog->Fanios[pObjLog->nFanins++].fCompl = Gia_ObjFaninC0(pObj);
+
+            pFanLog = Css_ManObj( p, Gia_ObjHandle(Gia_ObjFanin1(pObj)) ); 
+            pFanLog->Fanios[pFanLog->nFanins + pFanLog->iFanouts].iFan = 
+                pObjLog->Fanios[pObjLog->nFanins].iFan = pObjLog->hHandle - pFanLog->hHandle;
+            pFanLog->Fanios[pFanLog->nFanins + pFanLog->iFanouts++].fCompl =
+                pObjLog->Fanios[pObjLog->nFanins++].fCompl = Gia_ObjFaninC1(pObj);
+
+            p->nNodes++;
+        }
+        else if ( Gia_ObjIsCo(pObj) )
+        {
+            pFanLog = Css_ManObj( p, Gia_ObjHandle(Gia_ObjFanin0(pObj)) ); 
+            pFanLog->Fanios[pFanLog->nFanins + pFanLog->iFanouts].iFan = 
+                pObjLog->Fanios[pObjLog->nFanins].iFan = pObjLog->hHandle - pFanLog->hHandle;
+            pFanLog->Fanios[pFanLog->nFanins + pFanLog->iFanouts++].fCompl =
+                pObjLog->Fanios[pObjLog->nFanins++].fCompl = Gia_ObjFaninC0(pObj);
+
+            pObjLog->fCo = 1;
+            Vec_IntPush( p->vCos, iHandle );
+        }
+        else if ( Gia_ObjIsCi(pObj) )
+        {
+            pObjLog->fCi = 1;
+            Vec_IntPush( p->vCis, iHandle );
+        }
+        iHandle += Css_ObjSize( pObjLog );
+        p->nObjs++;
+    }
+    assert( iHandle == p->nObjData );
+    Gia_ManForEachObj( pGia, pObj, i )
+    {
+        pObjLog = Css_ManObj( p, Gia_ObjHandle(pObj) );
+        assert( pObjLog->nFanouts == pObjLog->iFanouts );
+        pObjLog->TravId = 0;
+    }
+    p->nTravIds = 1;
+    p->vTrail = Vec_IntAlloc( 100 );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates logic network isomorphic to the given AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Css_ManStop( Css_Man_t * p )
+{
+    Vec_IntFree( p->vTrail );
+    Vec_IntFree( p->vCis );
+    Vec_IntFree( p->vCos );
+    ABC_FREE( p->pObjData );
+    ABC_FREE( p->pLevels );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Propagates implications for the net.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Css_ManImplyNet_rec( Css_Man_t * p, Css_Obj_t * pVar, unsigned Value )
+{
+    static inline Css_ManImplyNode_rec( Css_Man_t * p, Css_Obj_t * pVar );
+    Css_Obj_t * pNext;
+    int i;
+    if ( !Css_ObjIsTravIdCurrent(p, pVar) )
+        return 0;
+    // assign the variable
+    assert( !Css_VarIsAssigned(pVar) );
+    Css_VarAssign( pVar );
+    Css_VarSetValue( pVar, Value );
+    Vec_IntPush( p->vTrail, pVar->hHandle );
+    // propagate fanouts, then fanins
+    Css_ObjForEachFanout( pVar, pNext, i )
+        if ( Css_ManImplyNode_rec( p, pNext ) )
+            return 1;
+    Css_ObjForEachFanin( pVar, pNext, i )
+        if ( Css_ManImplyNode_rec( p, pNext ) )
+            return 1;
+    return 0;
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    [Propagates implications for the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Css_ManImplyNode_rec( Css_Man_t * p, Css_Obj_t * pVar )
+{
+    Css_Obj_t * pFan0, * pFan1;
+    if ( Css_ObjIsCi(pVar) )
+        return 0;
+    pFan0 = Css_ObjFanin(pVar, 0);
+    pFan1 = Css_ObjFanin(pVar, 1);
+    if ( !Css_VarIsAssigned(pVar) )
+    {
+        if ( Css_VarIsAssigned(pFan0) )
+        {
+            if ( Css_VarValue(pFan0) == Css_ObjFaninC(pVar,0) ) // negative -> propagate
+                return Css_ManImplyNet_rec(p, pVar, 0);
+            // assigned positive
+            if ( Css_VarIsAssigned(pFan1) )
+            {
+                if ( Css_VarValue(pFan1) == Css_ObjFaninC(pVar,1) ) // negative -> propagate
+                    return Css_ManImplyNet_rec(p, pVar, 0);
+                // asigned positive -> propagate
+                return Css_ManImplyNet_rec(p, pVar, 1);
+            }
+            return 0;
+        }
+        if ( Css_VarIsAssigned(pFan1) )
+        {
+            if ( Css_VarValue(pFan1) == Css_ObjFaninC(pVar,1) ) // negative -> propagate
+                return Css_ManImplyNet_rec(p, pVar, 0);
+            return 0;
+        }
+        assert( 0 );
+        return 0;
+    }
+    if ( Css_VarValue(pVar) ) // positive
+    {
+        if ( Css_VarIsAssigned(pFan0) )
+        {
+            if ( Css_VarValue(pFan0) == Css_ObjFaninC(pVar,0) ) // negative -> conflict
+                return 1;
+            // check second var
+            if ( Css_VarIsAssigned(pFan1) )
+            {
+                if ( Css_VarValue(pFan1) == Css_ObjFaninC(pVar,1) ) // negative -> conflict
+                    return 1;
+                // positive + positive -> nothing to do
+                return 0;
+            }
+        }
+        else
+        {
+            // pFan0 unassigned -> enqueue first var
+//            Css_ManEnqueue( p, pFan0, !Css_ObjFaninC(pVar,0) );
+            if ( Css_ManImplyNet_rec( p, pFan0, !Css_ObjFaninC(pVar,0) ) )
+                return 1;
+            // check second var
+            if ( Css_VarIsAssigned(pFan1) )
+            {
+                if ( Css_VarValue(pFan1) == Css_ObjFaninC(pVar,1) ) // negative -> conflict
+                    return 1;
+                // positive + positive -> nothing to do
+                return 0;
+            }
+        }
+        // unassigned -> enqueue second var
+//        Css_ManEnqueue( p, pFan1, !Css_ObjFaninC(pVar,1) );
+        return Css_ManImplyNet_rec( p, pFan1, !Css_ObjFaninC(pVar,1) );
+    }
+    else // negative
+    {
+        if ( Css_VarIsAssigned(pFan0) )
+        {
+            if ( Css_VarValue(pFan0) == Css_ObjFaninC(pVar,0) ) // negative -> nothing to do
+                return 0;
+            if ( Css_VarIsAssigned(pFan1) )
+            {
+                if ( Css_VarValue(pFan1) == Css_ObjFaninC(pVar,1) ) // negative -> nothing to do
+                    return 0;
+                // positive + positive -> conflict
+                return 1;
+            }
+            // positive + unassigned -> enqueue second var
+//            Css_ManEnqueue( p, pFan1, Css_ObjFaninC(pVar,1) );
+            return Css_ManImplyNet_rec( p, pFan1, Css_ObjFaninC(pVar,1) );
+        }
+        else
+        {
+            if ( Css_VarIsAssigned(pFan1) )
+            {
+                if ( Css_VarValue(pFan1) == Css_ObjFaninC(pVar,1) ) // negative -> nothing to do
+                    return 0;
+                // unassigned + positive -> enqueue first var
+//                Css_ManEnqueue( p, pFan0, Css_ObjFaninC(pVar,0) );
+                return Css_ManImplyNet_rec( p, pFan0, Css_ObjFaninC(pVar,0) );
+            }
+        }
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Css_ManCancelUntil( Css_Man_t * p, int iBound, Vec_Int_t * vCex )
+{
+    Css_Obj_t * pVar;
+    int i;
+    Css_ManForEachObjVecStart( p->vTrail, p, pVar, i, iBound )
+    {
+        if ( vCex )  
+            Vec_IntPush( vCex, Gia_Var2Lit(Css_ObjId(pVar), !pVar->fValue) );
+        Css_VarUnassign( pVar );
+    }
+    Vec_IntShrink( p->vTrail, iBound );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Justifies assignments.]
+
+  Description [Returns 1 for UNSAT, 0 for SAT, -1 for UNDECIDED.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Css_ManJustify( Css_Man_t * p, int iBegin )
+{
+    Css_Obj_t * pVar, * pFan0, * pFan1;
+    int iState, iThis;
+    if ( p->nConfsMax == 0 )
+        return 1;
+    // get the next variable to justify
+    Css_ManForEachObjVecStart( p->vTrail, p, pVar, iThis, iBegin )
+    {
+        assert( Css_VarIsAssigned(pVar) );
+        if ( Css_VarValue(pVar) || Css_ObjIsCi(pVar) )
+            continue;
+        pFan0 = Css_ObjFanin(pVar,0);
+        pFan1 = Css_ObjFanin(pVar,0);
+        if ( !Css_VarIsAssigned(pFan0) && !Css_VarIsAssigned(pFan1) )
+            break;
+    }
+    if ( iThis == Vec_IntSize(p->vTrail) ) // could not find
+        return 0;
+    // found variable to justify
+    assert( !Css_VarValue(pVar) && !Css_VarIsAssigned(pFan0) && !Css_VarIsAssigned(pFan1) );
+    // remember the state of the stack
+    iState = Vec_IntSize( p->vTrail );
+    // try to justify by setting first fanin to 0
+    if ( !Css_ManImplyNet_rec(p, pFan0, 0) && !Css_ManJustify(p, iThis) )
+        return 0;
+    Css_ManCancelUntil( p, iState, NULL );
+    if ( p->nConfsMax == 0 )
+        return 1;
+    // try to justify by setting second fanin to 0
+    if ( !Css_ManImplyNet_rec(p, pFan1, 0) && !Css_ManJustify(p, iThis) )
+        return 0;
+    Css_ManCancelUntil( p, iState, NULL );
+    if ( p->nConfsMax == 0 )
+        return 1;
+    p->nConfsMax--;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marsk logic cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Css_ManMarkCone_rec( Css_Man_t * p, Css_Obj_t * pVar )
+{
+    if ( Css_ObjIsTravIdCurrent(p, pVar) )
+        return;
+    Css_ObjSetTravIdCurrent(p, pVar);
+    assert( !Css_VarIsAssigned(pVar) );
+    if ( Css_ObjIsCi(pVar) )
+        return;
+    else
+    {
+        Css_Obj_t * pNext;
+        int i;
+        Css_ObjForEachFanin( pVar, pNext, i )
+            Css_ManMarkCone_rec( p, pNext );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Runs one call to the SAT solver.]
+
+  Description [Returns 1 for UNSAT, 0 for SAT, -1 for UNDECIDED.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Css_ManPrepare( Css_Man_t * p, int * pLits, int nLits )
+{
+    Css_Obj_t * pVar;
+    int i;
+    // mark the cone
+    Css_ManIncrementTravId( p );
+    for ( i = 0; i < nLits; i++ )
+    {
+        pVar = Css_ManObj( p, Gia_Lit2Var(pLits[i]) );
+        Css_ManMarkCone_rec( p, pVar );
+    }
+    // assign literals
+    Vec_IntClear( p->vTrail );
+    for ( i = 0; i < nLits; i++ )
+    {
+        pVar = Css_ManObj( p, Gia_Lit2Var(pLits[i]) );
+        if ( Css_ManImplyNet_rec( p, pVar, !Gia_LitIsCompl(pLits[i]) ) )
+        {
+            Css_ManCancelUntil( p, 0, NULL );
+            return 1;
+        }
+    }
+    return 0;
+}
+ 
+
+/**Function*************************************************************
+
+  Synopsis    [Runs one call to the SAT solver.]
+
+  Description [Returns 1 for UNSAT, 0 for SAT, -1 for UNDECIDED.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Css_ManSolve( Css_Man_t * p, int * pLits, int nLits, int nConfsMax, Vec_Int_t * vCex )
+{
+    // propagate the assignments
+    if ( Css_ManPrepare( p, pLits, nLits ) )
+        return 1;
+    // justify the assignments
+    p->nConfsMax = nConfsMax;
+    if ( Css_ManJustify( p, 0 ) )
+        return p->nConfsMax? 1 : -1;
+    // derive model and return the solver to the initial state
+    Vec_IntClear( vCex );
+    Css_ManCancelUntil( p, 0, vCex );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Procedure to test the new SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_SatSolveTest2( Gia_Man_t * pGia )
+{
+    extern void Gia_SatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vCex, Vec_Int_t * vVisit );
+    int nConfsMax = 1000;
+    int CountUnsat, CountSat, CountUndec;
+    Css_Man_t * p; 
+    Vec_Int_t * vCex;
+    Vec_Int_t * vVisit;
+    Gia_Obj_t * pRoot; 
+    int i, RetValue, iLit, clk = clock();
+    // create logic network
+    p = Css_ManCreateLogicSimple( pGia );
+    // prepare AIG
+    Gia_ManCleanValue( pGia );
+    Gia_ManCleanMark0( pGia );
+    Gia_ManCleanMark1( pGia );
+    vCex   = Vec_IntAlloc( 100 );
+    vVisit = Vec_IntAlloc( 100 );
+    // solve for each output
+    CountUnsat = CountSat = CountUndec = 0;
+    Gia_ManForEachCo( pGia, pRoot, i )
+    {
+        if ( Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) )
+            continue;
+//printf( "Output %6d : ", i );
+        iLit = Gia_Var2Lit( Gia_ObjHandle(Gia_ObjFanin0(pRoot)), Gia_ObjFaninC0(pRoot) );
+        RetValue = Css_ManSolve( p, &iLit, 1, nConfsMax, vCex );
+        if ( RetValue == 1 )
+            CountUnsat++;
+        else if ( RetValue == -1 )
+            CountUndec++;
+        else 
+        {
+//            Gia_Obj_t * pTemp;
+//            int k;
+            assert( RetValue == 0 );
+            CountSat++;
+/*
+            Vec_PtrForEachEntry( vCex, pTemp, k )
+//                printf( "%s%d ", Gia_IsComplement(pTemp)? "!": "", Gia_ObjCioId(Gia_Regular(pTemp)) );
+                printf( "%s%d ", Gia_IsComplement(pTemp)? "!": "", Gia_ObjId(p,Gia_Regular(pTemp)) );
+            printf( "\n" );
+*/
+            Gia_SatVerifyPattern( pGia, pRoot, vCex, vVisit );
+        }
+//        Gia_ManCheckMark0( p );
+//        Gia_ManCheckMark1( p );
+    }
+    Css_ManStop( p );
+    Vec_IntFree( vCex );
+    Vec_IntFree( vVisit );
+    printf( "Unsat = %d. Sat = %d. Undec = %d.  ", CountUnsat, CountSat, CountUndec );
+    ABC_PRT( "Time", clock() - clk );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/gia/giaSolver_cnf.c b/src/aig/gia/giaCSatA.c
index 12f6895a..12f6895a 100644
--- a/src/aig/gia/giaSolver_cnf.c
+++ b/src/aig/gia/giaCSatA.c
diff --git a/src/aig/gia/giaSolver.c b/src/aig/gia/giaCSatB.c
index e1f68c6f..e1f68c6f 100644
--- a/src/aig/gia/giaSolver.c
+++ b/src/aig/gia/giaCSatB.c
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index f8d759be..d5c0862f 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -417,39 +417,67 @@ Gia_Man_t * Gia_ManDupCofactored( Gia_Man_t * p, int iVar )
 {
     Gia_Man_t * pNew, * pTemp;
     Gia_Obj_t * pObj, * pPivot;
-    int i;
-    assert( Gia_ManRegNum(p) == 0 );
-    assert( iVar < Gia_ManObjNum(p) );
+    int i, iCofVar = -1;
+    if ( !(iVar > 0 && iVar < Gia_ManObjNum(p)) )
+    {
+        printf( "Gia_ManDupCofactored(): Variable %d is out of range (%d; %d).\n", iVar, 0, Gia_ManObjNum(p) );
+        return NULL;
+    }
+    // find the cofactoring variable
+    pPivot = Gia_ManObj( p, iVar );
+    if ( !(Gia_ObjIsCi(pPivot) || Gia_ObjIsAnd(pPivot)) )
+    {
+        printf( "Gia_ManDupCofactored(): Variable %d should be a CI or an AND node.\n", iVar );
+        return NULL;
+    }
+//    assert( Gia_ManRegNum(p) == 0 );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Aig_UtilStrsav( p->pName );
     Gia_ManHashAlloc( pNew );
     Gia_ManConst0(p)->Value = 0;
+    // compute negative cofactor
     Gia_ManForEachCi( p, pObj, i )
+    {
         pObj->Value = Gia_ManAppendCi(pNew);
-    // find the cofactoring variable
-    pPivot = Gia_ManObj(p, iVar);
-    // compute the negative cofactor
-    if ( Gia_ObjIsCi(pPivot) )
-        pPivot->Value = Gia_Var2Lit( 0, 0 );
+        if ( pObj == pPivot )
+        {
+            iCofVar = pObj->Value;
+            pObj->Value = Gia_Var2Lit( 0, 0 );
+        }
+    }
     Gia_ManForEachAnd( p, pObj, i )
     {
         pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
         if ( pObj == pPivot )
-            pPivot->Value = Gia_Var2Lit( 0, 0 );
+        {
+            iCofVar = pObj->Value;
+            pObj->Value = Gia_Var2Lit( 0, 0 );
+        }
     }
     Gia_ManForEachCo( p, pObj, i )
-        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+        pObj->Value = Gia_ObjFanin0Copy(pObj);
     // compute the positive cofactor
-    if ( Gia_ObjIsCi(pPivot) )
-        pPivot->Value = Gia_Var2Lit( 0, 1 );
+    Gia_ManForEachCi( p, pObj, i )
+    {
+        pObj->Value = Gia_Var2Lit( Gia_ObjId(pNew, Gia_ManCi(pNew, i)), 0 );
+        if ( pObj == pPivot )
+            pObj->Value = Gia_Var2Lit( 0, 1 );
+    }
     Gia_ManForEachAnd( p, pObj, i )
     {
         pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
         if ( pObj == pPivot )
-            pPivot->Value = Gia_Var2Lit( 0, 1 );
+            pObj->Value = Gia_Var2Lit( 0, 1 );
     }
+    // create MUXes
+    assert( iCofVar > 0 );
     Gia_ManForEachCo( p, pObj, i )
-        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    {
+        if ( pObj->Value == (unsigned)Gia_ObjFanin0Copy(pObj) )
+            pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+        else
+            pObj->Value = Gia_ManAppendCo( pNew, Gia_ManHashMux(pNew, iCofVar, Gia_ObjFanin0Copy(pObj), pObj->Value) );
+    }
     Gia_ManHashStop( pNew );
     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
     // rehash the result
diff --git a/src/aig/gia/giaEmbed.c b/src/aig/gia/giaEmbed.c
index 0abaa55e..0469d1a4 100644
--- a/src/aig/gia/giaEmbed.c
+++ b/src/aig/gia/giaEmbed.c
@@ -1,6 +1,6 @@
 /**CFile****************************************************************
 
-  FileName    [giaLogic.c]
+  FileName    [giaEmbed.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: giaLogic.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: giaEmbed.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
@@ -24,13 +24,15 @@
 /* 
     The code is based on the paper by D. Harel and Y. Koren, 
     "Graph drawing by high-dimensional embedding", 
-    J. Graph Algs & Apps, Vol 8(2), pp. 195-217 (2004)
+    J. Graph Algs & Apps, Vol 8(2), pp. 195-217 (2004).
 */
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+typedef float  Emb_Dat_t;
+
 typedef struct Emb_Obj_t_ Emb_Obj_t;
 struct Emb_Obj_t_
 {
@@ -63,12 +65,14 @@ struct Emb_Man_t_
     int            nTravIds;         // traversal ID of the network
     int *          pObjData;         // the array containing data for objects
     int            nObjData;         // the size of array to store the logic network
-    unsigned char* pVecs;            // array of vectors of size nObjs * nDims
+    int            fVerbose;         // verbose output flag
+    Emb_Dat_t *    pVecs;            // array of vectors of size nObjs * nDims
     int            nReached;         // the number of nodes reachable from the pivot
     int            nDistMax;         // the maximum distance from the node
     float **       pMatr;            // covariance matrix nDims * nDims
     float **       pEigen;           // the first several eigen values of the matrix
     float *        pSols;            // solutions to the problem nObjs * nSols;
+    unsigned short*pPlacement;       // (x,y) coordinates for each cell
 };
 
 static inline int         Emb_ManRegNum( Emb_Man_t * p )                              { return p->nRegs;                                    }
@@ -105,8 +109,8 @@ static inline void        Emb_ObjSetTravIdPrevious( Emb_Man_t * p, Emb_Obj_t * p
 static inline int         Emb_ObjIsTravIdCurrent( Emb_Man_t * p, Emb_Obj_t * pObj )   { return ((int)pObj->TravId == p->nTravIds);          }
 static inline int         Emb_ObjIsTravIdPrevious( Emb_Man_t * p, Emb_Obj_t * pObj )  { return ((int)pObj->TravId == p->nTravIds - 1);      }
 
-static inline unsigned char * Emb_ManVec( Emb_Man_t * p, int v )                      { return p->pVecs + v * p->nObjs;                     }
-static inline float *         Emb_ManSol( Emb_Man_t * p, int v )                      { return p->pSols + v * p->nObjs;                     }
+static inline Emb_Dat_t * Emb_ManVec( Emb_Man_t * p, int v )                      { return p->pVecs + v * p->nObjs;                     }
+static inline float *     Emb_ManSol( Emb_Man_t * p, int v )                      { return p->pSols + v * p->nObjs;                     }
 
 #define Emb_ManForEachObj( p, pObj, i )               \
     for ( i = 0; (i < p->nObjData) && (pObj = Emb_ManObj(p,i)); i += Emb_ObjSize(pObj) )
@@ -125,6 +129,136 @@ static inline float *         Emb_ManSol( Emb_Man_t * p, int v )
 
 /**Function*************************************************************
 
+  Synopsis    [Creates fanin/fanout pair.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Emb_ObjAddFanin( Emb_Obj_t * pObj, Emb_Obj_t * pFanin )
+{ 
+    assert( pObj->iFanin < pObj->nFanins );
+    assert( pFanin->iFanout < pFanin->nFanouts );
+    pFanin->Fanios[pFanin->nFanins + pFanin->iFanout++] = 
+    pObj->Fanios[pObj->iFanin++] = pObj->hHandle - pFanin->hHandle;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates logic network isomorphic to the given AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Emb_Man_t * Emb_ManStartSimple( Gia_Man_t * pGia )
+{
+    Emb_Man_t * p;
+    Emb_Obj_t * pObjLog, * pFanLog;
+    Gia_Obj_t * pObj, * pObjRi, * pObjRo;
+    int i, nNodes, hHandle = 0;
+    // prepare the AIG
+    Gia_ManCreateRefs( pGia );
+    // create logic network
+    p = ABC_CALLOC( Emb_Man_t, 1 );
+    p->pGia  = pGia;
+    p->nRegs = Gia_ManRegNum(pGia);
+    p->vCis  = Vec_IntAlloc( Gia_ManCiNum(pGia) );
+    p->vCos  = Vec_IntAlloc( Gia_ManCoNum(pGia) );
+    p->nObjData = (sizeof(Emb_Obj_t) / 4) * Gia_ManObjNum(pGia) + 2 * (2 * Gia_ManAndNum(pGia) + Gia_ManCoNum(pGia) + Gia_ManRegNum(pGia));
+    p->pObjData = ABC_CALLOC( int, p->nObjData );
+    // create constant node
+    Gia_ManConst0(pGia)->Value = hHandle;
+    pObjLog = Emb_ManObj( p, hHandle );
+    pObjLog->hHandle  = hHandle;
+    pObjLog->nFanins  = 0;
+    pObjLog->nFanouts = Gia_ObjRefs( pGia, Gia_ManConst0(pGia) );
+    // count objects
+    hHandle += Emb_ObjSize( pObjLog );
+    nNodes = 1;
+    p->nObjs++;
+    // create the PIs
+    Gia_ManForEachCi( pGia, pObj, i )
+    {
+        // create PI object
+        pObj->Value = hHandle;
+        Vec_IntPush( p->vCis, hHandle );
+        pObjLog = Emb_ManObj( p, hHandle );
+        pObjLog->hHandle  = hHandle;
+        pObjLog->nFanins  = Gia_ObjIsRo( pGia, pObj );
+        pObjLog->nFanouts = Gia_ObjRefs( pGia, pObj );
+        pObjLog->fCi = 1;
+        // count objects
+        hHandle += Emb_ObjSize( pObjLog );
+        p->nObjs++;
+    }
+    // create internal nodes
+    Gia_ManForEachAnd( pGia, pObj, i )
+    {
+        assert( Gia_ObjRefs( pGia, pObj ) > 0 );
+        // create node object
+        pObj->Value = hHandle;
+        pObjLog = Emb_ManObj( p, hHandle );
+        pObjLog->hHandle  = hHandle;
+        pObjLog->nFanins  = 2;
+        pObjLog->nFanouts = Gia_ObjRefs( pGia, pObj );
+        // add fanins
+        pFanLog = Emb_ManObj( p, Gia_ObjValue(Gia_ObjFanin0(pObj)) ); 
+        Emb_ObjAddFanin( pObjLog, pFanLog );
+        pFanLog = Emb_ManObj( p, Gia_ObjValue(Gia_ObjFanin1(pObj)) ); 
+        Emb_ObjAddFanin( pObjLog, pFanLog );
+        // count objects
+        hHandle += Emb_ObjSize( pObjLog );
+        nNodes++;
+        p->nObjs++;
+    }
+    // create the POs
+    Gia_ManForEachCo( pGia, pObj, i )
+    {
+        // create PO object
+        pObj->Value = hHandle;
+        Vec_IntPush( p->vCos, hHandle );
+        pObjLog = Emb_ManObj( p, hHandle );
+        pObjLog->hHandle  = hHandle;
+        pObjLog->nFanins  = 1;
+        pObjLog->nFanouts = Gia_ObjIsRi( pGia, pObj );
+        pObjLog->fCo = 1;
+        // add fanins
+        pFanLog = Emb_ManObj( p, Gia_ObjValue(Gia_ObjFanin0(pObj)) );
+        Emb_ObjAddFanin( pObjLog, pFanLog );
+        // count objects
+        hHandle += Emb_ObjSize( pObjLog );
+        p->nObjs++;
+    }
+    // connect registers
+    Gia_ManForEachRiRo( pGia, pObjRi, pObjRo, i )
+        Emb_ObjAddFanin( Emb_ManObj(p,Gia_ObjValue(pObjRo)), Emb_ManObj(p,Gia_ObjValue(pObjRi)) );
+    assert( nNodes  == Emb_ManNodeNum(p) );
+    assert( hHandle == p->nObjData );
+    if ( hHandle != p->nObjData )
+        printf( "Emb_ManStartSimple(): Fatal error in internal representation.\n" );
+    // make sure the fanin/fanout counters are correct
+    Gia_ManForEachObj( pGia, pObj, i )
+    {
+        if ( !~Gia_ObjValue(pObj) )
+            continue;
+        pObjLog = Emb_ManObj( p, Gia_ObjValue(pObj) );
+        assert( pObjLog->nFanins  == pObjLog->iFanin );
+        assert( pObjLog->nFanouts == pObjLog->iFanout );
+        pObjLog->iFanin = pObjLog->iFanout = 0;
+    }
+    ABC_FREE( pGia->pRefs );
+    return p;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Collect the fanin IDs.]
 
   Description []
@@ -334,25 +468,6 @@ void Emb_ManSetValue( Emb_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Creates fanin/fanout pair.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Emb_ObjAddFanin( Emb_Obj_t * pObj, Emb_Obj_t * pFanin )
-{ 
-    assert( pObj->iFanin < pObj->nFanins );
-    assert( pFanin->iFanout < pFanin->nFanouts );
-    pFanin->Fanios[pFanin->nFanins + pFanin->iFanout++] = 
-    pObj->Fanios[pObj->iFanin++] = pObj->hHandle - pFanin->hHandle;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Creates logic network isomorphic to the given AIG.]
 
   Description []
@@ -524,6 +639,7 @@ void Emb_ManStop( Emb_Man_t * p )
 {
     Vec_IntFree( p->vCis );
     Vec_IntFree( p->vCos );
+    ABC_FREE( p->pPlacement );
     ABC_FREE( p->pVecs );
     ABC_FREE( p->pSols );
     ABC_FREE( p->pMatr );
@@ -797,7 +913,7 @@ ABC_PRT( "Time", clock() - clk );
   SeeAlso     []
 
 ***********************************************************************/
-Emb_Obj_t * Emb_ManFindDistances( Emb_Man_t * p, Vec_Int_t * vStart, unsigned char * pDist )
+Emb_Obj_t * Emb_ManFindDistances( Emb_Man_t * p, Vec_Int_t * vStart, Emb_Dat_t * pDist )
 {
     Vec_Int_t * vThis, * vNext, * vTemp;
     Emb_Obj_t * pThis, * pNext, * pResult;
@@ -818,9 +934,6 @@ Emb_Obj_t * Emb_ManFindDistances( Emb_Man_t * p, Vec_Int_t * vStart, unsigned ch
         Vec_IntClear( vNext );
         Emb_ManForEachObjVec( vThis, p, pThis, i )
         {
-            assert( p->nDistMax < 255 ); // current data-structure used unsigned char
-            if ( p->nDistMax > 254 )
-                p->nDistMax = 254;
             if ( pDist ) pDist[pThis->Value] = p->nDistMax;
             Emb_ObjForEachFanin( pThis, pNext, k )
             {
@@ -862,7 +975,7 @@ Emb_Obj_t * Emb_ManRandomVertex( Emb_Man_t * p )
 {
     Emb_Obj_t * pPivot;
     do {
-        int iNode = Aig_ManRandom( 0 ) % Gia_ManObjNum(p->pGia);
+        int iNode = (911 * Aig_ManRandom(0)) % Gia_ManObjNum(p->pGia);
         if ( ~Gia_ManObj(p->pGia, iNode)->Value )
             pPivot = Emb_ManObj( p, Gia_ManObj(p->pGia, iNode)->Value );
         else
@@ -874,6 +987,36 @@ Emb_Obj_t * Emb_ManRandomVertex( Emb_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Computes the distances from the given set of objects.]
+
+  Description [Returns one of the most distant objects.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Emb_DumpGraphIntoFile( Emb_Man_t * p )
+{
+    FILE * pFile;
+    Emb_Obj_t * pThis, * pNext;
+    int i, k;
+    pFile = fopen( "1.g", "w" );
+    Emb_ManForEachObj( p, pThis, i )
+    {
+        if ( !Emb_ObjIsTravIdCurrent(p, pThis) )
+            continue;
+        Emb_ObjForEachFanout( pThis, pNext, k )
+        {
+            assert( Emb_ObjIsTravIdCurrent(p, pNext) );
+            fprintf( pFile, "%d %d\n", pThis->Value, pNext->Value );
+        }
+    }
+    fclose( pFile );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Computes dimentions of the graph.]
 
   Description []
@@ -890,16 +1033,21 @@ void Emb_ManComputeDimensions( Emb_Man_t * p, int nDims )
     int d, nReached;
     int i, Counter;
     assert( p->pVecs == NULL );
-    p->pVecs = ABC_FALLOC( unsigned char, p->nObjs * nDims );
+    p->pVecs = ABC_ALLOC( Emb_Dat_t, p->nObjs * nDims );
+    for ( i = 0; i < p->nObjs * nDims; i++ )
+        p->pVecs[i] = ABC_INFINITY;
     vStart = Vec_IntAlloc( nDims );
     // get the pivot vertex
     pRandom = Emb_ManRandomVertex( p );
     Vec_IntPush( vStart, pRandom->hHandle );
     // get the most distant vertex from the pivot
     pPivot = Emb_ManFindDistances( p, vStart, NULL );
+//    Emb_DumpGraphIntoFile( p );
     nReached = p->nReached;
     if ( nReached < Emb_ManObjNum(p) )
-        printf( "Visited less objects (%d) than present (%d).\n", p->nReached, Emb_ManObjNum(p) );
+    {
+        printf( "Considering a connected component with %d objects (out of %d).\n", p->nReached, Emb_ManObjNum(p) );
+    }
     // start dimensions with this vertex
     Vec_IntClear( vStart );
     for ( d = 0; d < nDims; d++ )
@@ -915,7 +1063,7 @@ void Emb_ManComputeDimensions( Emb_Man_t * p, int nDims )
     // make sure the number of reached objects is correct
     Counter = 0;
     for ( i = 0; i < p->nObjs; i++ )
-        if ( p->pVecs[i] < 255 )
+        if ( p->pVecs[i] < ABC_INFINITY )
             Counter++;
     assert( Counter == nReached );
 }
@@ -954,19 +1102,26 @@ float ** Emb_ManMatrAlloc( int nDims )
 ***********************************************************************/
 void Emb_ManComputeCovariance( Emb_Man_t * p, int nDims )
 {
-    unsigned char * pOne, * pTwo;
-    float * pAves, * pCol;
+    Emb_Dat_t * pOne, * pTwo;
+    double Ave;
+    float * pRow;
     int d, i, k, v;
-    // compute averages of vectors
-    pAves = ABC_ALLOC( float, nDims );
+    // average vectors
     for ( d = 0; d < nDims; d++ )
     {
-        pAves[d] = 0.0;
+        // compute average
+        Ave = 0.0;
         pOne = Emb_ManVec( p, d );
         for ( v = 0; v < p->nObjs; v++ )
-            if ( pOne[v] < 255 )
-                pAves[d] += pOne[v];
-        pAves[d] /= p->nReached;
+            if ( pOne[v] < ABC_INFINITY )
+                Ave += pOne[v];
+        Ave /= p->nReached;
+        // update the vector
+        for ( v = 0; v < p->nObjs; v++ )
+            if ( pOne[v] < ABC_INFINITY )
+                pOne[v] -= Ave;
+            else
+                pOne[v] = 0.0;        
     }
     // compute the matrix
     assert( p->pMatr == NULL );
@@ -976,17 +1131,15 @@ void Emb_ManComputeCovariance( Emb_Man_t * p, int nDims )
     for ( i = 0; i < nDims; i++ )
     {
         pOne = Emb_ManVec( p, i );
-        pCol = p->pMatr[i];
+        pRow = p->pMatr[i];
         for ( k = 0; k < nDims; k++ )
         {
             pTwo = Emb_ManVec( p, k );
-            pCol[k] = 0.0;
+            pRow[k] = 0.0;
             for ( v = 0; v < p->nObjs; v++ )
-                if ( pOne[i] < 255 && pOne[k] < 255 )
-                    pCol[k] += (pOne[i] - pAves[i])*(pOne[k] - pAves[k]);
+                pRow[k] += pOne[v]*pTwo[v];
         }
     }
-    ABC_FREE( pAves );
 }
 
 /**Function*************************************************************
@@ -1080,9 +1233,9 @@ void Emb_ManVecCopyOne( float * pVecDest, float * pVecSour, int nDims )
 ***********************************************************************/
 void Emb_ManVecMultiply( float ** pMatr, float * pVec, int nDims, float * pRes )
 {
-    int i;
-    for ( i = 0; i < nDims; i++ )
-        pRes[i] = Emb_ManVecMultiplyOne( pMatr[i], pVec, nDims );
+    int k;
+    for ( k = 0; k < nDims; k++ )
+        pRes[k] = Emb_ManVecMultiplyOne( pMatr[k], pVec, nDims );
 }
 
 /**Function*************************************************************
@@ -1096,17 +1249,16 @@ void Emb_ManVecMultiply( float ** pMatr, float * pVec, int nDims, float * pRes )
   SeeAlso     []
 
 ***********************************************************************/
-void Emb_ManVecOrthogonolize( float ** pEigen, int nVecs, float * pVec, int nDims )
+void Emb_ManVecOrthogonolizeOne( float * pEigen, float * pVecI, int nDims, float * pVecRes )
 {
-    int i, k;
-    for ( k = 0; k < nVecs; k++ )
-        for ( i = 0; i < nDims; i++ )
-            pVec[i] -= pEigen[k][i] * Emb_ManVecMultiplyOne( pEigen[k], pVec, nDims );
+    int k;
+    for ( k = 0; k < nDims; k++ )
+        pVecRes[k] = pVecI[k] - pEigen[k] * Emb_ManVecMultiplyOne( pVecI, pEigen, nDims );
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Computes the first eigen-vectors.]
+  Synopsis    [Computes the first nSols eigen-vectors.]
 
   Description []
                
@@ -1115,32 +1267,226 @@ void Emb_ManVecOrthogonolize( float ** pEigen, int nVecs, float * pVec, int nDim
   SeeAlso     []
 
 ***********************************************************************/
-void Emb_ManComputeSolutions( Emb_Man_t * p, int nDims, int nSols )
+void Emb_ManComputeEigenvectors( Emb_Man_t * p, int nDims, int nSols )
 {
-    float * pVecTemp, * pVecCur;
-    int i, k, j;
+    float * pVecUiHat, * pVecUi;
+    int i, j, k;
     assert( nSols < nDims );
-    pVecTemp = p->pEigen[nSols];
+    pVecUiHat = p->pEigen[nSols];
     for ( i = 0; i < nSols; i++ )
     {
-        pVecCur = p->pEigen[i];
-        Emb_ManVecRandom( pVecTemp, nDims );
-        Emb_ManVecNormal( pVecTemp, nDims );
+        pVecUi = p->pEigen[i];
+        Emb_ManVecRandom( pVecUiHat, nDims );
+        Emb_ManVecNormal( pVecUiHat, nDims );
+        k = 0;
         do {
-            Emb_ManVecCopyOne( pVecCur, pVecTemp, nDims );
+            k++;
+            Emb_ManVecCopyOne( pVecUi, pVecUiHat, nDims );
             for ( j = 0; j < i; j++ )
-                Emb_ManVecOrthogonolize( p->pEigen, i, pVecCur, nDims );
-            Emb_ManVecMultiply( p->pMatr, pVecCur, nDims, pVecTemp );
-            Emb_ManVecNormal( pVecTemp, nDims );
-        } while ( Emb_ManVecMultiplyOne(pVecTemp, pVecCur, nDims) < 0.999 );
-        Emb_ManVecCopyOne( pVecCur, pVecTemp, nDims );
+            {
+                Emb_ManVecOrthogonolizeOne( p->pEigen[j], pVecUi, nDims, pVecUiHat );
+                Emb_ManVecCopyOne( pVecUi, pVecUiHat, nDims );
+            }
+            Emb_ManVecMultiply( p->pMatr, pVecUi, nDims, pVecUiHat );
+            Emb_ManVecNormal( pVecUiHat, nDims );
+        } while ( Emb_ManVecMultiplyOne( pVecUiHat, pVecUi, nDims ) < 0.999 && k < 100 );
+        Emb_ManVecCopyOne( pVecUi, pVecUiHat, nDims );
+//        printf( "Converged after %d iterations.\n", k );
     }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives solutions from original vectors and eigenvectors.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Emb_ManComputeSolutions( Emb_Man_t * p, int nDims, int nSols )
+{
+    Emb_Dat_t * pX;
+    float * pY;
+    int i, j, k;
     assert( p->pSols == NULL );
     p->pSols = ABC_CALLOC( float, p->nObjs * nSols );
+    for ( i = 0; i < nDims; i++ )
+    {
+        pX = Emb_ManVec( p, i );
+        for ( j = 0; j < nSols; j++ )
+        {
+            pY = Emb_ManSol( p, j );
+            for ( k = 0; k < p->nObjs; k++ )
+                pY[k] += pX[k] * p->pEigen[j][i];
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Projects into square of size [0;0xffff] x [0;0xffff].]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Emb_ManDerivePlacement( Emb_Man_t * p, int nSols )
+{
+    extern int * Gia_SortFloats( float * pArray, int nSize );
+    float * pY0, * pY1, Max0, Max1, Min0, Min1, Str0, Str1;
+    int * pPerm0, * pPerm1;
+    int k;
+    if ( nSols != 2 )
+        return;
+    // compute intervals
+    Min0 =  ABC_INFINITY;
+    Max0 = -ABC_INFINITY;
+    pY0 = Emb_ManSol( p, 0 );
+    for ( k = 0; k < p->nObjs; k++ )
+    {
+        Min0 = ABC_MIN( Min0, pY0[k] );
+        Max0 = ABC_MAX( Max0, pY0[k] );
+    }
+    Str0 = 1.0*0xffff/(Max0 - Min0);
+    // update the coordinates
+    for ( k = 0; k < p->nObjs; k++ )
+        pY0[k] = (pY0[k] != 0.0) ? ((pY0[k] - Min0) * Str0) : 0.0;
+
+    // compute intervals
+    Min1 =  ABC_INFINITY;
+    Max1 = -ABC_INFINITY;
+    pY1 = Emb_ManSol( p, 1 );
+    for ( k = 0; k < p->nObjs; k++ )
+    {
+        Min1 = ABC_MIN( Min1, pY1[k] );
+        Max1 = ABC_MAX( Max1, pY1[k] );
+    }
+    Str1 = 1.0*0xffff/(Max1 - Min1);
+    // update the coordinates
+    for ( k = 0; k < p->nObjs; k++ )
+        pY1[k] = (pY1[k] != 0.0) ? ((pY1[k] - Min1) * Str1) : 0.0;
+
+    // derive the order of these numbers
+    pPerm0 = Gia_SortFloats( pY0, p->nObjs );
+    pPerm1 = Gia_SortFloats( pY1, p->nObjs );
+
+    // average solutions and project them into 32K by 32K square
+    p->pPlacement = ABC_ALLOC( unsigned short, 2 * p->nObjs );
+    for ( k = 0; k < p->nObjs; k++ )
+    {
+        p->pPlacement[2*pPerm0[k]+0] = (unsigned short)(int)(1.0 * k * 0xffff / p->nObjs);
+        p->pPlacement[2*pPerm1[k]+1] = (unsigned short)(int)(1.0 * k * 0xffff / p->nObjs);
+    }
+    ABC_FREE( pPerm0 );
+    ABC_FREE( pPerm1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives solutions from original vectors and eigenvectors.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Emb_ManPrintSolutions( Emb_Man_t * p, int nSols )
+{
+    float * pSol;
+    int i, k;
     for ( i = 0; i < nSols; i++ )
-        for ( k = 0; k < nDims; k++ )
-            for ( j = 0; j < p->nObjs; j++ )
-                Emb_ManSol(p, i)[j] += Emb_ManVec(p, k)[j] * p->pEigen[i][k];
+    {
+        pSol = Emb_ManSol( p, i );
+        for ( k = 0; k < p->nObjs; k++ )
+            printf( "%4d ", (int)(100 * pSol[k]) );
+        printf( "\n" );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives solutions from original vectors and eigenvectors.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Emb_ManDumpGnuplot( Emb_Man_t * p, int nSols, char * pName )
+{
+    int fDumpImage = 1;
+//    char * pDirectory = "place\\";
+    char * pDirectory = "";
+    extern char * Ioa_TimeStamp();
+    FILE * pFile;
+    char Buffer[1000];
+    Emb_Obj_t * pThis, * pNext;
+    float * pSol0, * pSol1;
+    int i, k;
+    if ( nSols < 2 )
+        return;
+    if ( p->pPlacement == NULL )
+    {
+        printf( "Emb_ManDumpGnuplot(): Placement is not available.\n" );
+        return;
+    }
+    pSol0 = Emb_ManSol( p, 0 );
+    pSol1 = Emb_ManSol( p, 1 );
+    sprintf( Buffer, "%s%s", pDirectory, Aig_FileNameGenericAppend(pName, ".plt") ); 
+    pFile = fopen( Buffer, "w" );
+    fprintf( pFile, "# This Gnuplot file was produced by ABC on %s\n", Ioa_TimeStamp() );
+    fprintf( pFile, "\n" );
+    if ( fDumpImage )
+    {
+    fprintf( pFile, "set nokey\n" );
+//    fprintf( pFile, "set terminal postscript\n" );
+//    fprintf( pFile, "set output \'%s\'\n", Aig_FileNameGenericAppend(pName, ".ps") );
+    fprintf( pFile, "set terminal gif font \'arial\' 10 size 800,600 xffffff x000000 x000000 x000000\n" );
+    fprintf( pFile, "set output \'%s\'\n", Aig_FileNameGenericAppend(pName, ".gif") );
+    fprintf( pFile, "\n" );
+    }
+    fprintf( pFile, "set title \"%s :  PI = %d   PO = %d   FF = %d   Node = %d   Obj = %d\\n", 
+        pName, Emb_ManPiNum(p), Emb_ManPoNum(p), Emb_ManRegNum(p), Emb_ManNodeNum(p), Emb_ManObjNum(p) );
+    fprintf( pFile, "(image generated by ABC and Gnuplot on %s)\"", Ioa_TimeStamp() );
+    fprintf( pFile, "font \"Times, 12\"\n" );
+    fprintf( pFile, "\n" );
+    fprintf( pFile, "plot [:] '-' w l\n" );
+    fprintf( pFile, "\n" );
+    Emb_ManForEachObj( p, pThis, i )
+    {
+        if ( !Emb_ObjIsTravIdCurrent(p, pThis) )
+            continue;
+        Emb_ObjForEachFanout( pThis, pNext, k )
+        {
+            assert( Emb_ObjIsTravIdCurrent(p, pNext) );
+//            fprintf( pFile, "%d %d\n", (int)pSol0[pThis->Value], (int)pSol1[pThis->Value] );
+//            fprintf( pFile, "%d %d\n", (int)pSol0[pNext->Value], (int)pSol1[pNext->Value] );
+//            fprintf( pFile, "%5.2f %5.2f\n", pSol0[pThis->Value], pSol1[pThis->Value] );
+//            fprintf( pFile, "%5.2f %5.2f\n", pSol0[pNext->Value], pSol1[pNext->Value] );
+            fprintf( pFile, "%5d %5d\n", p->pPlacement[2*pThis->Value+0], p->pPlacement[2*pThis->Value+1] );
+            fprintf( pFile, "%5d %5d\n", p->pPlacement[2*pNext->Value+0], p->pPlacement[2*pNext->Value+1] );
+            fprintf( pFile, "\n" );
+        }
+    }
+    fprintf( pFile, "EOF\n" );
+    fprintf( pFile, "\n" );
+    if ( !fDumpImage )
+    {
+    fprintf( pFile, "pause -1 \"Hit return to continue\"\n" );
+    fprintf( pFile, "reset\n" );
+    fprintf( pFile, "\n" );
+    }
+    fclose( pFile );
 }
 
 /**Function*************************************************************
@@ -1154,34 +1500,55 @@ void Emb_ManComputeSolutions( Emb_Man_t * p, int nDims, int nSols )
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManSolveProblem( Gia_Man_t * pGia, int nDims, int nSols )
+void Gia_ManSolveProblem( Gia_Man_t * pGia, int nDims, int nSols, int fCluster, int fDump, int fVerbose )
 {
     Emb_Man_t * p;
-    int clk;
+    int clk, clkSetup;
 //   Gia_ManTestDistance( pGia );
 
+    // transform AIG into internal data-structure
 clk = clock();
-    p = Emb_ManStart( pGia );
+    if ( fCluster )
+    {
+        p = Emb_ManStart( pGia );
+        if ( fVerbose )
+        {
+            printf( "After clustering: " );
+            Emb_ManPrintStats( p );
+        }
+    }
+    else
+        p = Emb_ManStartSimple( pGia );
+    p->fVerbose = fVerbose;
 //    Emb_ManPrintFanio( p );
-    Emb_ManPrintStats( p );
-    Aig_ManRandom( 1 );
+
+    // prepare data-structure
+    Aig_ManRandom( 1 );  // reset random numbers for deterministic behavior
     Emb_ManResetTravId( p );
-    // set all nodes to have their IDs
     Emb_ManSetValue( p );
-ABC_PRT( "Setup     ", clock() - clk );
+clkSetup = clock() - clk;
 
 clk = clock();
     Emb_ManComputeDimensions( p, nDims );
+if ( fVerbose )
+ABC_PRT( "Setup     ", clkSetup );
+if ( fVerbose )
 ABC_PRT( "Dimensions", clock() - clk );
 
 clk = clock();
     Emb_ManComputeCovariance( p, nDims );
+if ( fVerbose )
 ABC_PRT( "Matrix    ", clock() - clk );
 
 clk = clock();
-//    Emb_ManComputeSolutions( p, nDims, nSols );
+    Emb_ManComputeEigenvectors( p, nDims, nSols );
+    Emb_ManComputeSolutions( p, nDims, nSols );
+    Emb_ManDerivePlacement( p, nSols );
+if ( fVerbose )
 ABC_PRT( "Eigenvecs ", clock() - clk );
 
+    if ( fDump )
+        Emb_ManDumpGnuplot( p, nSols, pGia->pName );
     Emb_ManStop( p );
 }
 
diff --git a/src/aig/gia/giaForce.c b/src/aig/gia/giaForce.c
index e5080e81..c2d2d33f 100644
--- a/src/aig/gia/giaForce.c
+++ b/src/aig/gia/giaForce.c
@@ -42,7 +42,7 @@ struct For_Man_t_
     Gia_Man_t *    pGia;             // the original AIG manager
     int            nObjs;            // the number of objects
     int            iObj;             // the last added object
-    int *          pPlace;           // Placeing of objects
+    int *          pPlace;           // coordinates of objects
     int *          piNext;           // array of next pointers
     int *          piRoot;           // array of root pointers
     float *        plEdge;           // edge coordinates
@@ -413,7 +413,7 @@ void For_ManSortObjects( For_Man_t * p )
         p->piNext[i] = p->piRoot[iPlace];
         p->piRoot[iPlace] = i;        
     }
-    // recostruct the order
+    // reconstruct the order
     p->iObj = 0;
     pPrev = NULL;
     vArray = Vec_PtrAlloc( 100 );
diff --git a/src/aig/gia/giaGlitch.c b/src/aig/gia/giaGlitch.c
index 6da24083..443a1ae8 100644
--- a/src/aig/gia/giaGlitch.c
+++ b/src/aig/gia/giaGlitch.c
@@ -630,23 +630,38 @@ static inline unsigned Gli_ManUpdateRandomInput( unsigned uInfo, float PiTransPr
   SeeAlso     []
 
 ***********************************************************************/
-static inline void Gli_ManSimulateSeqOne( Gli_Man_t * p, float PiTransProb )
+void Gli_ManSimulateSeqPref( Gli_Man_t * p, int nPref )
 {
     Gli_Obj_t * pObj, * pObjRi, * pObjRo;
-    int i;
+    int i, f;
+    // initialize simulation data
     Gli_ManForEachPi( p, pObj, i )
-        pObj->uSimInfo = Gli_ManUpdateRandomInput( pObj->uSimInfo, PiTransProb );
-    Gli_ManForEachNode( p, pObj, i )
-        pObj->uSimInfo = Gli_ManSimulateSeqNode( p, pObj );
-    Gli_ManForEachRi( p, pObj, i )
-        pObj->uSimInfo = Gli_ObjFanin(pObj, 0)->uSimInfo;
-    Gli_ManForEachRiRo( p, pObjRi, pObjRo, i )
-        pObjRo->uSimInfo = pObjRi->uSimInfo;
+        pObj->uSimInfo = Gli_ManUpdateRandomInput( pObj->uSimInfo, 0.5 );
+    Gli_ManForEachRo( p, pObj, i )
+        pObj->uSimInfo = 0;
+    for ( f = 0; f < nPref; f++ )
+    {
+        // simulate one frame
+        Gli_ManForEachNode( p, pObj, i )
+            pObj->uSimInfo = Gli_ManSimulateSeqNode( p, pObj );
+        Gli_ManForEachRi( p, pObj, i )
+            pObj->uSimInfo = Gli_ObjFanin(pObj, 0)->uSimInfo;
+        // initialize the next frame
+        Gli_ManForEachPi( p, pObj, i )
+            pObj->uSimInfo = Gli_ManUpdateRandomInput( pObj->uSimInfo, 0.5 );
+        Gli_ManForEachRiRo( p, pObjRi, pObjRo, i )
+            pObjRo->uSimInfo = pObjRi->uSimInfo;
+    }
+    // save simulation data after nPref timeframes
+    if ( p->pSimInfoPrev == NULL )
+        p->pSimInfoPrev = ABC_ALLOC( unsigned, Gli_ManCiNum(p) );
+    Gli_ManForEachCi( p, pObj, i )
+        p->pSimInfoPrev[i] = pObj->uSimInfo;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Simulates sequential network randomly for the given number of frames.]
+  Synopsis    [Initialized object values to be one pattern in the saved data.]
 
   Description []
                
@@ -655,19 +670,19 @@ static inline void Gli_ManSimulateSeqOne( Gli_Man_t * p, float PiTransProb )
   SeeAlso     []
 
 ***********************************************************************/
-static inline void Gli_ManSaveCiInfo( Gli_Man_t * p )
+void Gli_ManSetDataSaved( Gli_Man_t * p, int iBit )
 {
     Gli_Obj_t * pObj;
     int i;
-    if ( p->pSimInfoPrev == NULL )
-        p->pSimInfoPrev = ABC_ALLOC( unsigned, Gli_ManCiNum(p) );
     Gli_ManForEachCi( p, pObj, i )
-        p->pSimInfoPrev[i] = pObj->uSimInfo;
+        pObj->fPhase = pObj->fPhase2 = ((p->pSimInfoPrev[i] >> iBit) & 1);
+    Gli_ManForEachNode( p, pObj, i )
+        pObj->fPhase = pObj->fPhase2 = Gli_NodeComputeValue( pObj );
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Simulates sequential network randomly for the given number of frames.]
+  Synopsis    [Sets random info at the PIs and collects changed PIs.]
 
   Description []
                
@@ -676,14 +691,37 @@ static inline void Gli_ManSaveCiInfo( Gli_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Gli_ManSimulateSeqPref( Gli_Man_t * p, int nPref )
+void Gli_ManSetPiRandomSeq( Gli_Man_t * p, float PiTransProb )
 {
-    Gli_Obj_t * pObj;
-    int i, f;
-    Gli_ManForEachRo( p, pObj, i )
-        pObj->uSimInfo = 0;
-    for ( f = 0; f < nPref; f++ )
-        Gli_ManSimulateSeqOne( p, 0.5 );
+    Gli_Obj_t * pObj, * pObjRi;
+    float Multi = 1.0 / (1 << 16);
+    int i;
+    assert( 0.0 < PiTransProb && PiTransProb < 1.0 );
+    // transfer data to the COs
+    Gli_ManForEachCo( p, pObj, i )
+        pObj->fPhase = pObj->fPhase2 = Gli_ObjFanin(pObj, 0)->fPhase;
+    // set changed PIs
+    Vec_IntClear( p->vCisChanged );
+    Gli_ManForEachPi( p, pObj, i )
+        if ( Multi * (Aig_ManRandom(0) & 0xffff) < PiTransProb )
+        {
+            Vec_IntPush( p->vCisChanged, pObj->Handle );
+            pObj->fPhase  ^= 1;
+            pObj->fPhase2 ^= 1;
+            pObj->nSwitches++;
+            pObj->nGlitches++;
+        }
+    // set changed ROs
+    Gli_ManForEachRiRo( p, pObjRi, pObj, i )
+        if ( pObjRi->fPhase != pObj->fPhase )
+        {
+            Vec_IntPush( p->vCisChanged, pObj->Handle );
+            pObj->fPhase  ^= 1;
+            pObj->fPhase2 ^= 1;
+            pObj->nSwitches++;
+            pObj->nGlitches++;
+        }
+
 }
 
 /**Function*************************************************************
@@ -714,14 +752,14 @@ void Gli_ManSwitchesAndGlitches( Gli_Man_t * p, int nPatterns, float PiTransProb
     }
     else 
     {
+        int nIters = Aig_BitWordNum(nPatterns);
         Gli_ManSimulateSeqPref( p, 16 );
-        for ( k = Aig_BitWordNum(nPatterns) - 1; k >= 0; k-- )
+        for ( i = 0; i < 32; i++ )
         {
-            Gli_ManSaveCiInfo( p );
-            Gli_ManSimulateSeqOne( p, PiTransProb );
-            for ( i = 0; i < 32; i++ )
+            Gli_ManSetDataSaved( p, i );
+            for ( k = 0; k < nIters; k++ )
             {
-                Gli_ManSetPiFromSaved( p, i );
+                Gli_ManSetPiRandomSeq( p, PiTransProb );
                 Gli_ManSwitching( p );
                 Gli_ManGlitching( p );
 //                Gli_ManVerify( p );
diff --git a/src/aig/gia/giaHash.c b/src/aig/gia/giaHash.c
index c2bde6ba..8bc38ed9 100644
--- a/src/aig/gia/giaHash.c
+++ b/src/aig/gia/giaHash.c
@@ -509,6 +509,24 @@ int Gia_ManHashXor( Gia_Man_t * p, int iLit0, int iLit1 )
   SeeAlso     []
 
 ***********************************************************************/
+int Gia_ManHashMux( Gia_Man_t * p, int iCtrl, int iData1, int iData0 )  
+{ 
+    int iTemp0 = Gia_ManHashAnd( p, Gia_LitNot(iCtrl), iData0 );
+    int iTemp1 = Gia_ManHashAnd( p, iCtrl, iData1 );
+    return Gia_LitNotCond( Gia_ManHashAnd( p, Gia_LitNot(iTemp0), Gia_LitNot(iTemp1) ), 1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Rehashes AIG with mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Gia_Man_t * Gia_ManRehash( Gia_Man_t * p )  
 {
     Gia_Man_t * pNew;
diff --git a/src/aig/gia/giaSort.c b/src/aig/gia/giaSort.c
index 6986bc47..aec98fd8 100644
--- a/src/aig/gia/giaSort.c
+++ b/src/aig/gia/giaSort.c
@@ -59,13 +59,13 @@ static void sort_rec(int* array, int size, int(*comp)(const void *, const void *
     if (size <= 15)
         selectionsort(array, size, comp);
     else{
-        int *  pivot = array + size/2;
+        int    pivot = array[size/2];
         int    tmp;
         int    i = -1;
         int    j = size;
         for(;;){
-            do i++; while(comp(array + i, pivot));
-            do j--; while(comp(pivot, array + j));
+            do i++; while(comp(array + i, &pivot));
+            do j--; while(comp(&pivot, array + j));
             if (i >= j) break;
             tmp = array[i]; array[i] = array[j]; array[j] = tmp;
         }
@@ -79,6 +79,65 @@ void minisat_sort(int* array, int size, int(*comp)(const void *, const void *))
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [This is implementation of qsort in MiniSat.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void selectionsort2(int* array, int size)
+{
+    int     i, j, best_i;
+    int     tmp;
+    for (i = 0; i < size-1; i++){
+        best_i = i;
+        for (j = i+1; j < size; j++){
+            if (array[j] < array[best_i])
+                best_i = j;
+        }
+        tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp;
+    }
+}
+static void sort_rec2(int* array, int size)
+{
+    if (size <= 15)
+        selectionsort2(array, size);
+    else{
+        int    pivot = array[size/2];
+        int    tmp;
+        int    i = -1;
+        int    j = size;
+        for(;;){
+            do i++; while(array[i] < pivot);
+            do j--; while(pivot < array[j]);
+            if (i >= j) break;
+            tmp = array[i]; array[i] = array[j]; array[j] = tmp;
+        }
+        sort_rec2(array    , i     );
+        sort_rec2(&array[i], size-i);
+    }
+}
+void minisat_sort2(int* array, int size)
+{
+    sort_rec2(array,size);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [This is implementation of qsort in MiniSat.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int * Gia_SortGetTest( int nSize )
 {
     int i, * pArray;
@@ -96,10 +155,11 @@ void Gia_SortVerifySorted( int * pArray, int nSize )
 }
 void Gia_SortTest()
 {
-    int nSize = 1000000;
+    int nSize = 100000000;
     int * pArray;
     int clk = clock();
 
+    printf( "Sorting %d integers\n", nSize );
     pArray = Gia_SortGetTest( nSize );
 clk = clock();
     qsort( pArray, nSize, 4, (int (*)(const void *, const void *)) num_cmp1 );
@@ -113,8 +173,91 @@ clk = clock();
 ABC_PRT( "minisat", clock() - clk );
     Gia_SortVerifySorted( pArray, nSize );
     ABC_FREE( pArray );
+
+    pArray = Gia_SortGetTest( nSize );
+clk = clock();
+    minisat_sort2( pArray, nSize );
+ABC_PRT( "minisat with inlined comparison", clock() - clk );
+    Gia_SortVerifySorted( pArray, nSize );
+    ABC_FREE( pArray );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [This is implementation of qsort in MiniSat.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void selectionsort3(float* array, int* perm, int size)
+{
+    float   tmpf;
+    int     tmpi;
+    int     i, j, best_i;
+    for (i = 0; i < size-1; i++){
+        best_i = i;
+        for (j = i+1; j < size; j++){
+            if (array[j] < array[best_i])
+                best_i = j;
+        }
+        tmpf = array[i]; array[i] = array[best_i]; array[best_i] = tmpf;
+        tmpi = perm[i];  perm[i]  = perm[best_i];  perm[best_i]  = tmpi;
+    }
+}
+static void sort_rec3(float* array, int* perm, int size)
+{
+    if (size <= 15)
+        selectionsort3(array, perm, size);
+    else{
+        float  pivot = array[size/2];
+        float  tmpf;
+        int    tmpi;
+        int    i = -1;
+        int    j = size;
+        for(;;){
+            do i++; while(array[i] < pivot);
+            do j--; while(pivot < array[j]);
+            if (i >= j) break;
+            tmpf = array[i]; array[i] = array[j]; array[j] = tmpf;
+            tmpi = perm[i];  perm[i]  = perm[j];  perm[j]  = tmpi;
+        }
+        sort_rec3(array    , perm,     i     );
+        sort_rec3(&array[i], &perm[i], size-i);
+    }
+}
+void minisat_sort3(float* array, int* perm, int size)
+{
+    sort_rec3(array, perm, size);
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Sorts the array of floating point numbers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int * Gia_SortFloats( float * pArray, int nSize )
+{
+    int i, * pPerm;
+    pPerm = ABC_ALLOC( int, nSize );
+    for ( i = 0; i < nSize; i++ )
+        pPerm[i] = i;
+    minisat_sort3( pArray, pPerm, nSize );
+//    for ( i = 1; i < nSize; i++ )
+//        assert( pArray[i-1] <= pArray[i] );
+    return pPerm;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index d86d897f..7a68b554 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -14,6 +14,7 @@ SRC +=    src/aig/gia/gia.c \
     src/aig/gia/giaMan.c \
     src/aig/gia/giaScl.c \
     src/aig/gia/giaSim.c \
+    src/aig/gia/giaSort.c \
     src/aig/gia/giaSwitch.c \
     src/aig/gia/giaTsim.c \
     src/aig/gia/giaUtil.c
diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c
index 485a5146..16430ace 100644
--- a/src/aig/ssw/sswCore.c
+++ b/src/aig/ssw/sswCore.c
@@ -50,7 +50,7 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
     p->nBTLimit       =    1000;  // conflict limit at a node
     p->nBTLimitGlobal = 5000000;  // conflict limit for all runs
     p->nMinDomSize    =     100;  // min clock domain considered for optimization
-    p->nItersStop     =       0;  // stop after the given number of iterations
+    p->nItersStop     =      -1;  // stop after the given number of iterations
     p->nResimDelta    =    1000;  // the internal of nodes to resimulate
     p->fPolarFlip     =       0;  // uses polarity adjustment
     p->fLatchCorr     =       0;  // performs register correspondence
@@ -199,7 +199,7 @@ clk = clock();
         if ( !RetValue ) 
             break;
 
-        if ( p->pPars->nItersStop && p->pPars->nItersStop == nIter )
+        if ( p->pPars->nItersStop >= 0 && p->pPars->nItersStop == nIter )
         {
             Aig_Man_t * pSRed = Ssw_SpeculativeReduction( p );
             Aig_ManDumpBlif( pSRed, "srm.blif", NULL, NULL );