diff --git a/.gitignore b/.gitignore
index 203869de1..c745dfb57 100644
--- a/.gitignore
+++ b/.gitignore
@@ -6,6 +6,7 @@ ReleaseLib/
 ReleaseExe/
 ReleaseExt/
 
+_/
 _TEST/
 lib/abc*
 lib/m114*
diff --git a/src/aig/gia/giaDeep.c b/src/aig/gia/giaDeep.c
index 815a546e4..b58169f42 100644
--- a/src/aig/gia/giaDeep.c
+++ b/src/aig/gia/giaDeep.c
@@ -120,6 +120,7 @@ Gia_Man_t * Gia_ManDeepSynOne( int nNoImpr, int TimeOut, int nAnds, int Seed, in
         }
         if ( nTimeToStop && Abc_Clock() > nTimeToStop )
         {
+            if ( !Abc_FrameIsBatchMode() )
             printf( "Runtime limit (%d sec) is reached after %d iterations.\n", TimeOut, i );
             break;
         }
diff --git a/src/aig/gia/giaSimBase.c b/src/aig/gia/giaSimBase.c
index 47f645413..97335d378 100644
--- a/src/aig/gia/giaSimBase.c
+++ b/src/aig/gia/giaSimBase.c
@@ -3689,6 +3689,58 @@ Vec_Str_t * Gia_ManComputeRange( Gia_Man_t * p )
     return vOut;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManComparePrint( Gia_Man_t * p, Gia_Man_t * q )
+{
+    Vec_Wrd_t * vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(p) );
+    Vec_Wrd_t * vSimsP  = Gia_ManSimPatSimOut( p, vSimsPi, 0 );
+    Vec_Wrd_t * vSimsQ  = Gia_ManSimPatSimOut( q, vSimsPi, 0 );
+    int i, k, nWords = Vec_WrdSize(vSimsPi) / Gia_ManCiNum(p), Count = 0;
+    Gia_Obj_t * pObjP, * pObjQ;
+    Gia_ManSetPhase( p );
+    Gia_ManSetPhase( q );
+    Gia_ManForEachObj( p, pObjP, i ) {
+        word * pSim = Vec_WrdEntryP( vSimsP, i * nWords );
+        if ( pSim[0] & 1 ) Abc_TtNot( pSim, nWords );
+    }
+    Gia_ManForEachObj( q, pObjQ, i ) {
+        word * pSim = Vec_WrdEntryP( vSimsQ, i * nWords );
+        if ( pSim[0] & 1 ) Abc_TtNot( pSim, nWords );
+    }    
+    Gia_ManForEachAnd( q, pObjQ, i ) {
+        word * pSimQ = Vec_WrdEntryP( vSimsQ, i * nWords );
+        int fFirst = 1;
+        Gia_ManForEachObj( p, pObjP, k ) {
+            word * pSimP = Vec_WrdEntryP( vSimsP, k * nWords );
+            if ( !Abc_TtEqual(pSimQ, pSimP, nWords) )
+                continue;
+            if ( fFirst ) {
+                printf( "%5d :", i );
+                fFirst = 0;
+                Count++;
+            }
+            printf( " %5d(%d)", k, pObjQ->fPhase ^ pObjP->fPhase );
+        }
+        if ( !fFirst )
+            printf( "\n");
+    }   
+    printf( "Found %d equivalent nodes.\n", Count );
+    Vec_WrdFree( vSimsP );
+    Vec_WrdFree( vSimsQ );
+    Vec_WrdFree( vSimsPi );
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaStoch.c b/src/aig/gia/giaStoch.c
index 94f539988..57775b5cc 100644
--- a/src/aig/gia/giaStoch.c
+++ b/src/aig/gia/giaStoch.c
@@ -22,6 +22,19 @@
 #include "base/main/main.h"
 #include "base/cmd/cmd.h"
 
+
+#ifdef ABC_USE_PTHREADS
+
+#ifdef _WIN32
+#include "../lib/pthread.h"
+#else
+#include <pthread.h>
+#include <unistd.h>
+#endif
+
+#endif
+
+
 ABC_NAMESPACE_IMPL_START
 
 ////////////////////////////////////////////////////////////////////////
@@ -32,6 +45,169 @@ ABC_NAMESPACE_IMPL_START
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/**Function*************************************************************
+
+  Synopsis    [Processing on a single core.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_StochProcessOne( Gia_Man_t * p, char * pScript, int Rand, int TimeSecs )
+{
+    Gia_Man_t * pNew;
+    char FileName[100], Command[1000];
+    sprintf( FileName, "%06x.aig", Rand );
+    Gia_AigerWrite( p, FileName, 0, 0, 0 );
+    sprintf( Command, "./abc -q \"&read %s; %s; &write %s\"", FileName, pScript, FileName );
+    if ( system( (char *)Command ) )    
+    {
+        fprintf( stderr, "The following command has returned non-zero exit status:\n" );
+        fprintf( stderr, "\"%s\"\n", (char *)Command );
+        fprintf( stderr, "Sorry for the inconvenience.\n" );
+        fflush( stdout );
+        unlink( FileName );
+        return Gia_ManDup(p);
+    }    
+    pNew = Gia_AigerRead( FileName, 0, 0, 0 );
+    unlink( FileName );
+    if ( pNew && Gia_ManAndNum(pNew) < Gia_ManAndNum(p) )
+        return pNew;
+    Gia_ManStopP( &pNew );
+    return Gia_ManDup(p);
+}
+void Gia_StochProcessArray( Vec_Ptr_t * vGias, char * pScript, int TimeSecs, int fVerbose )
+{
+    Gia_Man_t * pGia, * pNew; int i;
+    Vec_Int_t * vRands = Vec_IntAlloc( Vec_PtrSize(vGias) ); 
+    Abc_Random(1);
+    for ( i = 0; i < Vec_PtrSize(vGias); i++ )
+        Vec_IntPush( vRands, Abc_Random(0) % 0x1000000 );
+    Vec_PtrForEachEntry( Gia_Man_t *, vGias, pGia, i ) 
+    {
+        pNew = Gia_StochProcessOne( pGia, pScript, Vec_IntEntry(vRands, i), TimeSecs );
+        Gia_ManStop( pGia );
+        Vec_PtrWriteEntry( vGias, i, pNew );
+    }
+    Vec_IntFree( vRands );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Processing on a many cores.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+#ifndef ABC_USE_PTHREADS
+
+void Gia_StochProcess( Vec_Ptr_t * vGias, char * pScript, int nProcs, int TimeSecs, int fVerbose )
+{
+    Gia_StochProcessArray( vGias, pScript, TimeSecs, fVerbose );
+}
+
+#else // pthreads are used
+
+
+#define PAR_THR_MAX 100
+typedef struct Gia_StochThData_t_
+{
+    Vec_Ptr_t *  vGias;
+    char *       pScript;
+    int          Index;
+    int          Rand;
+    int          nTimeOut;
+    int          fWorking;
+} Gia_StochThData_t;
+
+void * Gia_StochWorkerThread( void * pArg )
+{
+    Gia_StochThData_t * pThData = (Gia_StochThData_t *)pArg;
+    volatile int * pPlace = &pThData->fWorking;
+    Gia_Man_t * pGia, * pNew;
+    while ( 1 )
+    {
+        while ( *pPlace == 0 );
+        assert( pThData->fWorking );
+        if ( pThData->Index == -1 )
+        {
+            pthread_exit( NULL );
+            assert( 0 );
+            return NULL;
+        }
+        pGia = (Gia_Man_t *)Vec_PtrEntry( pThData->vGias, pThData->Index );
+        pNew = Gia_StochProcessOne( pGia, pThData->pScript, pThData->Rand, pThData->nTimeOut );
+        Gia_ManStop( pGia );
+        Vec_PtrWriteEntry( pThData->vGias, pThData->Index, pNew );
+        pThData->fWorking = 0;
+    }
+    assert( 0 );
+    return NULL;
+}
+
+void Gia_StochProcess( Vec_Ptr_t * vGias, char * pScript, int nProcs, int TimeSecs, int fVerbose )
+{
+    Gia_StochThData_t ThData[PAR_THR_MAX];
+    pthread_t WorkerThread[PAR_THR_MAX];
+    int i, k, status;
+    if ( fVerbose )
+        printf( "Running concurrent synthesis with %d processes.\n", nProcs );
+    fflush( stdout );
+    if ( nProcs < 2 )
+        return Gia_StochProcessArray( vGias, pScript, TimeSecs, fVerbose );
+    // subtract manager thread
+    nProcs--;
+    assert( nProcs >= 1 && nProcs <= PAR_THR_MAX );
+    // start threads
+    Abc_Random(1);
+    for ( i = 0; i < nProcs; i++ )
+    {
+        ThData[i].vGias    = vGias;
+        ThData[i].pScript  = pScript;
+        ThData[i].Index    = -1;
+        ThData[i].Rand     = Abc_Random(0) % 0x1000000;
+        ThData[i].nTimeOut = TimeSecs;
+        ThData[i].fWorking = 0;
+        status = pthread_create( WorkerThread + i, NULL, Gia_StochWorkerThread, (void *)(ThData + i) );  assert( status == 0 );
+    }
+    // look at the threads
+    for ( k = 0; k < Vec_PtrSize(vGias); k++ )
+    {
+        for ( i = 0; i < nProcs; i++ )
+        {
+            if ( ThData[i].fWorking )
+                continue;
+            ThData[i].Index = k;
+            ThData[i].fWorking = 1;   
+            break;
+        }
+        if ( i == nProcs )
+            k--;
+    }
+    // wait till threads finish
+    for ( i = 0; i < nProcs; i++ )
+        if ( ThData[i].fWorking )
+            i = -1;
+    // stop threads
+    for ( i = 0; i < nProcs; i++ )
+    {
+        assert( !ThData[i].fWorking );
+        // stop
+        ThData[i].Index = -1;
+        ThData[i].fWorking = 1;
+    }
+}
+
+#endif // pthreads are used
+
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -184,7 +360,7 @@ Gia_Man_t * Gia_ManDupDivideOne( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vA
     pNew->vMapping = vMapping;
     return pNew;
 }
-Vec_Ptr_t * Gia_ManDupDivide( Gia_Man_t * p, Vec_Wec_t * vCis, Vec_Wec_t * vAnds, Vec_Wec_t * vCos, char * pScript )
+Vec_Ptr_t * Gia_ManDupDivide( Gia_Man_t * p, Vec_Wec_t * vCis, Vec_Wec_t * vAnds, Vec_Wec_t * vCos, char * pScript, int nProcs, int TimeOut )
 {
     Vec_Ptr_t * vAigs = Vec_PtrAlloc( Vec_WecSize(vCis) );  int i;
     for ( i = 0; i < Vec_WecSize(vCis); i++ )
@@ -192,7 +368,8 @@ Vec_Ptr_t * Gia_ManDupDivide( Gia_Man_t * p, Vec_Wec_t * vCis, Vec_Wec_t * vAnds
         Gia_ManCollectNodes( p, Vec_WecEntry(vCis, i), Vec_WecEntry(vAnds, i), Vec_WecEntry(vCos, i) );
         Vec_PtrPush( vAigs, Gia_ManDupDivideOne(p, Vec_WecEntry(vCis, i), Vec_WecEntry(vAnds, i), Vec_WecEntry(vCos, i)) );
     }
-    Gia_ManStochSynthesis( vAigs, pScript );
+    //Gia_ManStochSynthesis( vAigs, pScript );
+    Gia_StochProcess( vAigs, pScript, nProcs, TimeOut, 0 );
     return vAigs;
 }
 Gia_Man_t * Gia_ManDupStitch( Gia_Man_t * p, Vec_Wec_t * vCis, Vec_Wec_t * vAnds, Vec_Wec_t * vCos, Vec_Ptr_t * vAigs, int fHash )
@@ -388,7 +565,7 @@ Vec_Wec_t * Gia_ManStochOutputs( Gia_Man_t * p, Vec_Wec_t * vAnds )
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManStochSyn( int nMaxSize, int nIters, int TimeOut, int Seed, int fVerbose, char * pScript )
+void Gia_ManStochSyn( int nMaxSize, int nIters, int TimeOut, int Seed, int fVerbose, char * pScript, int nProcs )
 {
     abctime nTimeToStop  = TimeOut ? Abc_Clock() + TimeOut * CLOCKS_PER_SEC : 0;
     abctime clkStart     = Abc_Clock();
@@ -407,7 +584,7 @@ void Gia_ManStochSyn( int nMaxSize, int nIters, int TimeOut, int Seed, int fVerb
         Vec_Wec_t * vAnds = Gia_ManStochNodes( pGia, nMaxSize, Abc_Random(0) & 0x7FFFFFFF );
         Vec_Wec_t * vIns  = Gia_ManStochInputs( pGia, vAnds );
         Vec_Wec_t * vOuts = Gia_ManStochOutputs( pGia, vAnds );
-        Vec_Ptr_t * vAigs = Gia_ManDupDivide( pGia, vIns, vAnds, vOuts, pScript );
+        Vec_Ptr_t * vAigs = Gia_ManDupDivide( pGia, vIns, vAnds, vOuts, pScript, nProcs, TimeOut );
         Gia_Man_t * pNew  = Gia_ManDupStitchMap( pGia, vIns, vAnds, vOuts, vAigs );
         int fMapped = Gia_ManHasMapping(pGia) && Gia_ManHasMapping(pNew);
         Abc_FrameUpdateGia( Abc_FrameGetGlobalFrame(), pNew );
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index 636fe30ae..94bafb53c 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -897,6 +897,16 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, i
     {
         if ( Abc_ObjIsCo(pFanout) )
         {
+            pFanin1 = Abc_ObjRegular( pNew );
+            if ( pFanin1->fMarkB )
+                Abc_AigRemoveFromLevelStructureR( pMan->vLevelsR, pFanin1 );
+            if ( fUpdateLevel && pMan->pNtkAig->vLevelsR )
+            {
+                Abc_ObjSetReverseLevel( pFanin1, Abc_ObjReverseLevel(pOld) );
+                assert( pFanin1->fMarkB == 0 );
+                pFanin1->fMarkB = 1;
+                Vec_VecPush( pMan->vLevelsR, Abc_ObjReverseLevel(pFanin1), pFanin1 );
+            }
             Abc_ObjPatchFanin( pFanout, pOld, pNew );
             continue;
         }
diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c
index 84ecf7bf3..805b91daa 100644
--- a/src/base/abc/abcFunc.c
+++ b/src/base/abc/abcFunc.c
@@ -1265,6 +1265,42 @@ int Abc_NtkToAig( Abc_Ntk_t * pNtk )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ObjFaninSort( Abc_Obj_t * pObj )
+{
+    Vec_Int_t * vFanins = Abc_ObjFaninVec( pObj );
+    char * pCube, * pSop = (char*)pObj->pData;
+    int i, j, nVars = Abc_SopGetVarNum( pSop );
+    assert( nVars == Vec_IntSize(vFanins) );
+    for ( i = 0;   i < Vec_IntSize(vFanins); i++ )
+    for ( j = i+1; j < Vec_IntSize(vFanins); j++ )
+    {
+        if ( Vec_IntEntry(vFanins, i) < Vec_IntEntry(vFanins, j) )
+            continue;
+        ABC_SWAP( int, Vec_IntArray(vFanins)[i], Vec_IntArray(vFanins)[j] );
+        for ( pCube = pSop; *pCube; pCube += nVars + 3 ) {
+            ABC_SWAP( char, pCube[i], pCube[j] );
+        }
+    }
+}
+void Abc_NtkFaninSort( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj; int i;
+    assert( Abc_NtkIsSopLogic(pNtk) );
+    Abc_NtkForEachNode( pNtk, pObj, i )
+        Abc_ObjFaninSort( pObj );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index baf0d7eec..76b56d5f4 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -540,6 +540,7 @@ static int Abc_CommandAbc9PoPart             ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9GroupProve         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9MultiProve         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9SplitProve         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9SplitSat           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Bmc                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9SBmc               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9ChainBmc           ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -1300,6 +1301,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&gprove",       Abc_CommandAbc9GroupProve,   0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&mprove",       Abc_CommandAbc9MultiProve,   0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&splitprove",   Abc_CommandAbc9SplitProve,   0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&splitsat",     Abc_CommandAbc9SplitSat,     0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&bmc",          Abc_CommandAbc9Bmc,          0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&bmcs",         Abc_CommandAbc9SBmc,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&chainbmc",     Abc_CommandAbc9ChainBmc,     0 );
@@ -11017,6 +11019,7 @@ usage:
 ***********************************************************************/
 int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
+    extern void Abc_NtkFaninSort( Abc_Ntk_t * pNtk );
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
     int c, fCubeSort = 1, fMode = -1, nCubeLimit = 1000000;
 
@@ -11072,6 +11075,8 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Converting to SOP has failed.\n" );
         return 0;
     }
+    if ( !fCubeSort )
+        Abc_NtkFaninSort( pNtk );
     return 0;
 
 usage:
@@ -13365,6 +13370,7 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fFpga;
     int fOneHot;
     int fRandom;
+    int fGraph;
     int fVerbose;
     char * FileName;
     char Command[1000];
@@ -13376,6 +13382,7 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern void Abc_GenFpga( char * pFileName, int nLutSize, int nLuts, int nVars );
     extern void Abc_GenOneHot( char * pFileName, int nVars );
     extern void Abc_GenRandom( char * pFileName, int nPis );
+    extern void Abc_GenGraph( char * pFileName, int nPis );
     extern void Abc_GenAdderTree( char * pFileName, int nArgs, int nBits );
 
     // set defaults
@@ -13390,9 +13397,10 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
     fFpga = 0;
     fOneHot = 0;
     fRandom = 0;
+    fGraph = 0;
     fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "NAKLatsembfnrvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "NAKLatsembfnrgvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -13467,6 +13475,9 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'r':
             fRandom ^= 1;
             break;
+        case 'g':
+            fGraph ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -13506,6 +13517,8 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_GenOneHot( FileName, nVars );
     else if ( fRandom )
         Abc_GenRandom( FileName, nVars );
+    else if ( fGraph )
+        Abc_GenGraph( FileName, nVars );
     else if ( fAdderTree )
     {
         printf( "Generating adder tree with %d arguments and %d bits.\n", nArgs, nVars );
@@ -13525,7 +13538,7 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: gen [-NAKL num] [-atsembfnrvh] <file>\n" );
+    Abc_Print( -2, "usage: gen [-NAKL num] [-atsembfnrgvh] <file>\n" );
     Abc_Print( -2, "\t         generates simple circuits\n" );
     Abc_Print( -2, "\t-N num : the number of variables [default = %d]\n", nVars );
     Abc_Print( -2, "\t-A num : the number of agruments (for adder tree) [default = %d]\n", nArgs );
@@ -13538,6 +13551,7 @@ usage:
     Abc_Print( -2, "\t-m     : generate a multiplier [default = %s]\n", fMulti? "yes": "no" );
     Abc_Print( -2, "\t-b     : generate a signed Booth multiplier [default = %s]\n", fBooth? "yes": "no" );
     Abc_Print( -2, "\t-f     : generate a LUT FPGA structure [default = %s]\n", fFpga? "yes": "no" );
+    Abc_Print( -2, "\t-g     : generate a graph structure [default = %s]\n", fGraph? "yes": "no" );
     Abc_Print( -2, "\t-n     : generate one-hotness conditions [default = %s]\n", fOneHot? "yes": "no" );
     Abc_Print( -2, "\t-r     : generate random single-output function [default = %s]\n", fRandom? "yes": "no" );
     Abc_Print( -2, "\t-v     : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );
@@ -45032,17 +45046,21 @@ usage:
 int Abc_CommandAbc9Compare( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern void Gia_Iso4TestTwo( Gia_Man_t * pGia0, Gia_Man_t * pGia1 );
+    extern void Gia_ManComparePrint( Gia_Man_t * p, Gia_Man_t * q );
     Gia_Man_t * pGia0, * pGia1;
     char ** pArgvNew; int nArgcNew;
-    int c, fVerbose = 0;
+    int c, fFunc = 0, fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "fvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'f':
+            fFunc ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
-            break;
+            break;        
         case 'h':
             goto usage;
         default:
@@ -45063,14 +45081,18 @@ int Abc_CommandAbc9Compare( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9Compare(): Reading input files did not work.\n" );
         return 1;
     }
-    Gia_Iso4TestTwo( pGia0, pGia1 );
+    if ( fFunc )
+        Gia_ManComparePrint( pGia0, pGia1 );
+    else
+        Gia_Iso4TestTwo( pGia0, pGia1 );
     Gia_ManStop( pGia0 );
     Gia_ManStop( pGia1 );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &compare <file1> <file2> [-vh]\n" );
+    Abc_Print( -2, "usage: &compare <file1> <file2> [-fvh]\n" );
     Abc_Print( -2, "\t         compared two AIGs for structural similarity\n" );
+    Abc_Print( -2, "\t-f     : toggle functional comparison [default = %s]\n", fFunc? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
@@ -46062,6 +46084,163 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9SplitSat( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern void Cnf_SplitSat( char * pFileName, int iVarBeg, int iVarEnd, int nLits, int Value, int TimeOut, int nProcs, int nIters, int Seed, int fPrepro, int fVerbose );
+    int c, iVarBeg = 0, iVarEnd = ABC_INFINITY, nLits = 10, Value = 2, TimeOut = 5, nProcs = 1, nIters = 1, Seed = 0, fPrepro = 0, fVerbose = 0; char * pFileName = NULL;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "BENVTPISpvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'B':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-B\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            iVarBeg = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( iVarBeg < 0 )
+                goto usage;
+            break;
+        case 'E':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-E\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            iVarEnd = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( iVarEnd < 0 )
+                goto usage;
+            break;
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-N\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nLits = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nLits < 0 )
+                goto usage;
+            break;                                    
+        case 'V':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-V\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            Value = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( Value < 0 || Value > 2 )
+                goto usage;
+            break;                  
+        case 'T':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-T\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            TimeOut = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( TimeOut < 0 )
+                goto usage;
+            break;
+        case 'P':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-P\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nProcs = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nProcs <= 0 )
+                goto usage;
+            break;
+        case 'I':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nIters = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nIters < 0 )
+                goto usage;
+            break;
+        case 'S':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            Seed = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( Seed < 0 )
+                goto usage;
+            break;            
+        case 'p':
+            fPrepro ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    // get the file name
+    if ( argc != globalUtilOptind + 1 )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9SplitSat(): CNF file names should be given on the command line.\n" );
+        return 1;
+    }
+    {        
+        FILE * pFile;
+        pFileName = argv[globalUtilOptind];
+        pFile = fopen( pFileName, "r" );
+        if ( pFile == NULL )
+        {
+            Abc_Print( -1, "Cannot open file \"%s\" with the input test patterns.\n", pFileName );
+            return 0;
+        }
+        fclose( pFile );
+    }
+    Cnf_SplitSat( pFileName, iVarBeg, iVarEnd, nLits, Value, TimeOut, nProcs, nIters, Seed, fPrepro, fVerbose );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &splitsat [-BENVTPIS num] [-pvh]\n" );
+    Abc_Print( -2, "\t         solves CNF-based SAT problem by randomized case-splitting\n" );
+    Abc_Print( -2, "\t-B num : the first CNF variable to use for splitting [default = %d]\n",         iVarBeg );
+    Abc_Print( -2, "\t-E num : the last CNF variable to use for splitting [default = %d]\n",          iVarEnd );
+    Abc_Print( -2, "\t-N num : the number of CNF variables to use for splitting [default = %d]\n",    nLits );
+    Abc_Print( -2, "\t-V num : the variable values to use (0, 1, or 2 for \"any\") [default = %d]\n", Value );
+    Abc_Print( -2, "\t-T num : the runtime limit in seconds per subproblem [default = %d]\n",         TimeOut );
+    Abc_Print( -2, "\t-P num : the number of concurrent processes [default = %d]\n",                  nProcs );
+    Abc_Print( -2, "\t-I num : the max number of iterations (0 = infinity) [default = %d]\n",         nIters );
+    Abc_Print( -2, "\t-S num : the random seed used to generate cofactors [default = %d]\n",          Seed );    
+    Abc_Print( -2, "\t-p     : toggle using SatELIte (http://minisat.se/SatELite.html) [default = %s]\n", fPrepro? "yes": "no" );    
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n",                 fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -49418,10 +49597,10 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9StochSyn( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern void Gia_ManStochSyn( int nMaxSize, int nIters, int TimeOut, int Seed, int fVerbose, char * pScript );
-    int c, nMaxSize = 1000, nIters = 10, TimeOut = 0, Seed = 0, fVerbose = 0; char * pScript;
+    extern void Gia_ManStochSyn( int nMaxSize, int nIters, int TimeOut, int Seed, int fVerbose, char * pScript, int nProcs );
+    int c, nMaxSize = 1000, nIters = 10, TimeOut = 0, Seed = 0, nProcs = 1, fVerbose = 0; char * pScript;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "NITSvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "NITSPvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -49469,6 +49648,17 @@ int Abc_CommandAbc9StochSyn( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( Seed < 0 )
                 goto usage;
             break;
+        case 'P':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nProcs = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nProcs < 0 )
+                goto usage;
+            break;            
         case 'v':
             fVerbose ^= 1;
             break;
@@ -49489,17 +49679,18 @@ int Abc_CommandAbc9StochSyn( Abc_Frame_t * pAbc, int argc, char ** argv )
         goto usage;
     }
     pScript = Abc_UtilStrsav( argv[globalUtilOptind] );
-    Gia_ManStochSyn( nMaxSize, nIters, TimeOut, Seed, fVerbose, pScript );
+    Gia_ManStochSyn( nMaxSize, nIters, TimeOut, Seed, fVerbose, pScript, nProcs );
     ABC_FREE( pScript );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &stochsyn [-NITS <num>] [-tvh] <script>\n" );
+    Abc_Print( -2, "usage: &stochsyn [-NITSP <num>] [-tvh] <script>\n" );
     Abc_Print( -2, "\t           performs stochastic synthesis\n" );
     Abc_Print( -2, "\t-N <num> : the max partition size (in AIG nodes or LUTs) [default = %d]\n", nMaxSize );
     Abc_Print( -2, "\t-I <num> : the number of iterations [default = %d]\n",                   nIters  );
     Abc_Print( -2, "\t-T <num> : the timeout in seconds (0 = no timeout) [default = %d]\n",    TimeOut );
     Abc_Print( -2, "\t-S <num> : user-specified random seed (0 <= num <= 100) [default = %d]\n", Seed  );
+    Abc_Print( -2, "\t-P <num> : the number of concurrent processes (1 <= num <= 100) [default = %d]\n", nProcs );
     Abc_Print( -2, "\t-v       : toggle printing optimization summary [default = %s]\n",       fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h       : print the command usage\n");
     Abc_Print( -2, "\t<script> : synthesis script to use for each partition\n");
diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c
index 5121a4fc4..27d86ae89 100644
--- a/src/base/abci/abcDsd.c
+++ b/src/base/abci/abcDsd.c
@@ -175,11 +175,11 @@ void Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t *
 
     // save the CI nodes in the DSD nodes
     Abc_AigConst1(pNtk)->pCopy = pNodeNew = Abc_NtkCreateNodeConst1(pNtkNew);
-    Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), (int)(ABC_PTRINT_T)pNodeNew );
+    Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), (word)(ABC_PTRINT_T)pNodeNew );
     Abc_NtkForEachCi( pNtk, pNode, i )
     {
         pNodeDsd = Dsd_ManagerReadInput( pManDsd, i );
-        Dsd_NodeSetMark( pNodeDsd, (int)(ABC_PTRINT_T)pNode->pCopy );
+        Dsd_NodeSetMark( pNodeDsd, (word)(ABC_PTRINT_T)pNode->pCopy );
     }
 
     // collect DSD nodes in DFS order (leaves and const1 are not collected)
@@ -298,7 +298,7 @@ printf( "\n" );
         }
     }
     pNodeNew->pData = bLocal;
-    Dsd_NodeSetMark( pNodeDsd, (int)(ABC_PTRINT_T)pNodeNew );
+    Dsd_NodeSetMark( pNodeDsd, (word)(ABC_PTRINT_T)pNodeNew );
     return pNodeNew;
 }
 
@@ -417,7 +417,7 @@ void Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager
         Abc_ObjForEachFanin( pNode, pFanin, i )
         {
             pFaninDsd = Dsd_ManagerReadInput( pManDsd, i );
-            Dsd_NodeSetMark( pFaninDsd, (int)(ABC_PTRINT_T)pFanin );
+            Dsd_NodeSetMark( pFaninDsd, (word)(ABC_PTRINT_T)pFanin );
         }
 
         // construct the intermediate nodes
diff --git a/src/base/abci/abcGen.c b/src/base/abci/abcGen.c
index 5d1c02cef..bea20a6d7 100644
--- a/src/base/abci/abcGen.c
+++ b/src/base/abci/abcGen.c
@@ -1140,6 +1140,70 @@ void Abc_GenBooth( char * pFileName, int nVars )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_GenGraph( char * pFileName, int nPis )
+{
+    FILE * pFile;
+    int i, a, b, w, nDigitsIn, nWords = Abc_TruthWordNum( nPis*(nPis-1)/2 );
+    unsigned * pTruth = ABC_CALLOC( unsigned, nWords );
+    unsigned char M[10][10] = {{0}}, C[100][2] = {{0}}, nVars = 0;
+    assert( nPis <= 8 );
+    for ( a = 0;   a < nPis; a++ )
+    for ( b = a+1; b < nPis; b++ )
+        C[nVars][0] = a, C[nVars][1] = b, nVars++;
+    for ( i = 0; i < (1<<nVars); i++ )
+    {
+        int fChanges = 1;
+        for ( w = 0; w < nVars; w++ )
+            M[C[w][0]][C[w][1]] = M[C[w][1]][C[w][0]] = (i >> w) & 1;
+        while ( fChanges && !M[0][1] ) {
+            fChanges = 0;
+            for ( a = 0; a < nPis; a++ )
+            for ( b = 0; b < nPis; b++ )
+                if ( M[a][b] )
+                    for ( w = 0; w < nPis; w++ )
+                        if ( M[b][w] && !M[a][w] )
+                            M[a][w] = 1, fChanges = 1;
+        }
+        if ( M[0][1] )
+            Abc_InfoSetBit(pTruth, i);    
+    }
+    pFile = fopen( pFileName, "w" );
+    fprintf( pFile, "# Function with %d inputs generated by ABC on %s\n", nVars, Extra_TimeStamp() );
+    fprintf( pFile, ".model fun%d\n", nVars );
+    fprintf( pFile, ".inputs" );
+    nDigitsIn = Abc_Base10Log( nVars );
+    for ( i = 0; i < nVars; i++ )
+        fprintf( pFile, " i%0*d", nDigitsIn, i );
+    fprintf( pFile, "\n" );
+    fprintf( pFile, ".outputs f\n" );
+    fprintf( pFile, ".names" );
+    nDigitsIn = Abc_Base10Log( nVars );
+    for ( b = nVars-1; b >= 0; b-- )
+        fprintf( pFile, " i%0*d", nDigitsIn, b );
+    fprintf( pFile, " f\n" );
+    for ( i = 0; i < (1<<nVars); i++ )
+        if ( Abc_InfoHasBit(pTruth, i) )
+        {
+            for ( b = nVars-1; b >= 0; b-- )
+                fprintf( pFile, "%d", (i>>b)&1 );
+            fprintf( pFile, " 1\n" );
+        }
+    fprintf( pFile, ".end\n" ); 
+    fprintf( pFile, "\n" ); 
+    fclose( pFile );
+    ABC_FREE( pTruth );
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/bdd/dsd/dsd.h b/src/bdd/dsd/dsd.h
index 837579510..4c5cd8915 100644
--- a/src/bdd/dsd/dsd.h
+++ b/src/bdd/dsd/dsd.h
@@ -92,8 +92,8 @@ extern DdNode *        Dsd_NodeReadSupp( Dsd_Node_t * p );
 extern Dsd_Node_t **   Dsd_NodeReadDecs( Dsd_Node_t * p );
 extern Dsd_Node_t *    Dsd_NodeReadDec ( Dsd_Node_t * p, int i );
 extern int             Dsd_NodeReadDecsNum( Dsd_Node_t * p );
-extern int             Dsd_NodeReadMark( Dsd_Node_t * p );
-extern void            Dsd_NodeSetMark( Dsd_Node_t * p, int Mark ); 
+extern word            Dsd_NodeReadMark( Dsd_Node_t * p );
+extern void            Dsd_NodeSetMark( Dsd_Node_t * p, word Mark ); 
 extern DdManager *     Dsd_ManagerReadDd( Dsd_Manager_t * pMan );
 extern Dsd_Node_t *    Dsd_ManagerReadRoot( Dsd_Manager_t * pMan, int i );
 extern Dsd_Node_t *    Dsd_ManagerReadInput( Dsd_Manager_t * pMan, int i );
diff --git a/src/bdd/dsd/dsdApi.c b/src/bdd/dsd/dsdApi.c
index 181dfb281..a94d0d26c 100644
--- a/src/bdd/dsd/dsdApi.c
+++ b/src/bdd/dsd/dsdApi.c
@@ -56,7 +56,7 @@ DdNode *      Dsd_NodeReadSupp( Dsd_Node_t * p )         { return p->S;        }
 Dsd_Node_t ** Dsd_NodeReadDecs( Dsd_Node_t * p )         { return p->pDecs;    } 
 Dsd_Node_t *  Dsd_NodeReadDec ( Dsd_Node_t * p, int i )  { return p->pDecs[i]; } 
 int           Dsd_NodeReadDecsNum( Dsd_Node_t * p )      { return p->nDecs;    } 
-int           Dsd_NodeReadMark( Dsd_Node_t * p )         { return p->Mark;     } 
+word          Dsd_NodeReadMark( Dsd_Node_t * p )         { return p->Mark;     } 
 
 /**Function*************************************************************
 
@@ -74,7 +74,7 @@ int           Dsd_NodeReadMark( Dsd_Node_t * p )         { return p->Mark;     }
   SeeAlso     []
 
 ***********************************************************************/
-void          Dsd_NodeSetMark( Dsd_Node_t * p, int Mark ){ p->Mark = Mark;     } 
+void          Dsd_NodeSetMark( Dsd_Node_t * p, word Mark ){ p->Mark = Mark;     } 
 
 /**Function*************************************************************
 
diff --git a/src/bdd/dsd/dsdInt.h b/src/bdd/dsd/dsdInt.h
index 37e9746f5..89bfd22ee 100644
--- a/src/bdd/dsd/dsdInt.h
+++ b/src/bdd/dsd/dsdInt.h
@@ -57,7 +57,7 @@ struct Dsd_Node_t_
     DdNode *       G;          // function of the node   
     DdNode *       S;          // support of this function
     Dsd_Node_t **  pDecs;      // pointer to structures for formal inputs
-    int            Mark;       // the mark used by CASE 4 of disjoint decomposition
+    word           Mark;       // the mark used by CASE 4 of disjoint decomposition
     short          nDecs;      // the number of formal inputs
     short          nVisits;    // the counter of visits
 };
diff --git a/src/misc/util/abc_global.h b/src/misc/util/abc_global.h
index 2217bb87e..c7b6f160b 100644
--- a/src/misc/util/abc_global.h
+++ b/src/misc/util/abc_global.h
@@ -325,8 +325,8 @@ static inline int      Abc_Var2Lit4( int Var, int Att )       { assert(!(Att >>
 static inline int      Abc_Lit2Var4( int Lit )                { assert(Lit >= 0);    return Lit >> 4;         }
 static inline int      Abc_Lit2Att4( int Lit )                { assert(Lit >= 0);    return Lit & 15;         }
 
-// time counting
 typedef ABC_INT64_T abctime;
+// counting wall time
 static inline abctime Abc_Clock()
 {
 #if defined(__APPLE__) && defined(__MACH__)
@@ -334,6 +334,25 @@ static inline abctime Abc_Clock()
 #else
   #define APPLE_MACH 0
 #endif
+#if (defined(LIN) || defined(LIN64)) && !APPLE_MACH && !defined(__MINGW32__)
+    struct timespec ts;
+    if ( clock_gettime(CLOCK_MONOTONIC, &ts) < 0 ) 
+        return (abctime)-1;
+    abctime res = ((abctime) ts.tv_sec) * CLOCKS_PER_SEC;
+    res += (((abctime) ts.tv_nsec) * CLOCKS_PER_SEC) / 1000000000;
+    return res;
+#else
+    return (abctime) clock();
+#endif
+}
+// counting thread time
+static inline abctime Abc_ThreadClock()
+{
+#if defined(__APPLE__) && defined(__MACH__)
+  #define APPLE_MACH (__APPLE__ & __MACH__)
+#else
+  #define APPLE_MACH 0
+#endif
 #if (defined(LIN) || defined(LIN64)) && !APPLE_MACH && !defined(__MINGW32__)
     struct timespec ts;
     if ( clock_gettime(CLOCK_THREAD_CPUTIME_ID, &ts) < 0 ) 
@@ -346,7 +365,6 @@ static inline abctime Abc_Clock()
 #endif
 }
 
-
 // misc printing procedures
 enum Abc_VerbLevel
 {
diff --git a/src/proof/cec/cecSplit.c b/src/proof/cec/cecSplit.c
index e2fa8ff1d..34a635b88 100644
--- a/src/proof/cec/cecSplit.c
+++ b/src/proof/cec/cecSplit.c
@@ -705,7 +705,7 @@ finish:
     // wait till threads finish
     for ( i = 0; i < nProcs; i++ )
         if ( ThData[i].fWorking )
-            i = 0;
+            i = -1;
     // stop threads
     for ( i = 0; i < nProcs; i++ )
     {
diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c
index 1e2a253f2..d3a3ac18d 100644
--- a/src/sat/bmc/bmcMaj.c
+++ b/src/sat/bmc/bmcMaj.c
@@ -1637,22 +1637,6 @@ Vec_Int_t * Exa4_ManSolve( char * pFileNameIn, char * pFileNameOut, int TimeOut,
     char * pKissat = "kissat";
 #endif
     char Command[1000], * pCommand = (char *)&Command;
-    {
-        FILE * pFile = fopen( pKissat, "rb" );
-        if ( pFile == NULL )
-        {
-            printf( "Cannot find the Kissat binary \"%s\".\n", pKissat );
-            pKissat = "./kissat";
-            pFile = fopen( pKissat, "rb" );
-            if ( pFile == NULL )
-            {
-                printf( "Cannot find the Kissat binary \"%s\".\n", pKissat );
-                return NULL;
-            }
-            fclose( pFile );        
-        }
-        fclose( pFile );        
-    }
     if ( TimeOut )
         sprintf( pCommand, "%s --time=%d %s %s > %s", pKissat, TimeOut, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut );
     else
diff --git a/src/sat/cnf/cnf.h b/src/sat/cnf/cnf.h
index 35c0fa2f7..1fbf58049 100644
--- a/src/sat/cnf/cnf.h
+++ b/src/sat/cnf/cnf.h
@@ -154,6 +154,8 @@ extern void            Cnf_ManStop( Cnf_Man_t * p );
 extern Vec_Int_t *     Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p );
 extern Cnf_Dat_t *     Cnf_DataAlloc( Aig_Man_t * pAig, int nVars, int nClauses, int nLiterals );
 extern Cnf_Dat_t *     Cnf_DataDup( Cnf_Dat_t * p );
+extern Cnf_Dat_t *     Cnf_DataDupCof( Cnf_Dat_t * p, int Lit );
+extern Cnf_Dat_t *     Cnf_DataDupCofArray( Cnf_Dat_t * p, Vec_Int_t * vLits );
 extern void            Cnf_DataFree( Cnf_Dat_t * p );
 extern void            Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus );
 extern void            Cnf_DataCollectFlipLits( Cnf_Dat_t * p, int iFlipVar, Vec_Int_t * vFlips );
diff --git a/src/sat/cnf/cnfMan.c b/src/sat/cnf/cnfMan.c
index f63cc6335..16a4cf219 100644
--- a/src/sat/cnf/cnfMan.c
+++ b/src/sat/cnf/cnfMan.c
@@ -103,10 +103,8 @@ void Cnf_ManStop( Cnf_Man_t * p )
 ***********************************************************************/
 Vec_Int_t * Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p )
 {
-    Vec_Int_t * vCiIds;
-    Aig_Obj_t * pObj;
-    int i;
-    vCiIds = Vec_IntAlloc( Aig_ManCiNum(p) );
+    Aig_Obj_t * pObj; int i;
+    Vec_Int_t * vCiIds = Vec_IntAlloc( Aig_ManCiNum(p) );
     Aig_ManForEachCi( p, pObj, i )
         Vec_IntPush( vCiIds, pCnf->pVarNums[pObj->Id] );
     return vCiIds;
@@ -126,9 +124,7 @@ Vec_Int_t * Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p )
 Cnf_Dat_t * Cnf_DataAlloc( Aig_Man_t * pAig, int nVars, int nClauses, int nLiterals )
 {
     Cnf_Dat_t * pCnf;
-    int i;
-    pCnf = ABC_ALLOC( Cnf_Dat_t, 1 );
-    memset( pCnf, 0, sizeof(Cnf_Dat_t) );
+    pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
     pCnf->pMan = pAig;
     pCnf->nVars = nVars;
     pCnf->nClauses = nClauses;
@@ -136,10 +132,8 @@ Cnf_Dat_t * Cnf_DataAlloc( Aig_Man_t * pAig, int nVars, int nClauses, int nLiter
     pCnf->pClauses = ABC_ALLOC( int *, nClauses + 1 );
     pCnf->pClauses[0] = ABC_ALLOC( int, nLiterals );
     pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
-    pCnf->pVarNums = ABC_ALLOC( int, Aig_ManObjNumMax(pAig) );
-//    memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(pAig) );
-    for ( i = 0; i < Aig_ManObjNumMax(pAig); i++ )
-        pCnf->pVarNums[i] = -1;
+    if ( pCnf->pVarNums )
+    pCnf->pVarNums = ABC_FALLOC( int, Aig_ManObjNumMax(pAig) );
     return pCnf;
 }
 
@@ -160,11 +154,44 @@ Cnf_Dat_t * Cnf_DataDup( Cnf_Dat_t * p )
     int i;
     pCnf = Cnf_DataAlloc( p->pMan, p->nVars, p->nClauses, p->nLiterals );
     memcpy( pCnf->pClauses[0], p->pClauses[0], sizeof(int) * p->nLiterals );
+    if ( p->pVarNums )
     memcpy( pCnf->pVarNums, p->pVarNums, sizeof(int) * Aig_ManObjNumMax(p->pMan) );
     for ( i = 1; i < p->nClauses; i++ )
         pCnf->pClauses[i] = pCnf->pClauses[0] + (p->pClauses[i] - p->pClauses[0]);
     return pCnf;
 }
+Cnf_Dat_t * Cnf_DataDupCof( Cnf_Dat_t * p, int Lit )
+{
+    Cnf_Dat_t * pCnf;
+    int i;
+    pCnf = Cnf_DataAlloc( p->pMan, p->nVars, p->nClauses+1, p->nLiterals+1 );
+    memcpy( pCnf->pClauses[0], p->pClauses[0], sizeof(int) * p->nLiterals );
+    if ( pCnf->pVarNums )
+    memcpy( pCnf->pVarNums, p->pVarNums, sizeof(int) * Aig_ManObjNumMax(p->pMan) );
+    for ( i = 1; i < p->nClauses; i++ )
+        pCnf->pClauses[i] = pCnf->pClauses[0] + (p->pClauses[i] - p->pClauses[0]);
+    pCnf->pClauses[p->nClauses] = pCnf->pClauses[0] + p->nLiterals;
+    pCnf->pClauses[p->nClauses][0] = Lit;
+    assert( pCnf->pClauses[p->nClauses+1] == pCnf->pClauses[0] + p->nLiterals+1 );
+    return pCnf;
+}
+Cnf_Dat_t * Cnf_DataDupCofArray( Cnf_Dat_t * p, Vec_Int_t * vLits )
+{
+    Cnf_Dat_t * pCnf;
+    int i, iLit;
+    pCnf = Cnf_DataAlloc( p->pMan, p->nVars, p->nClauses+Vec_IntSize(vLits), p->nLiterals+Vec_IntSize(vLits) );
+    memcpy( pCnf->pClauses[0], p->pClauses[0], sizeof(int) * p->nLiterals );
+    if ( pCnf->pVarNums )
+    memcpy( pCnf->pVarNums, p->pVarNums, sizeof(int) * Aig_ManObjNumMax(p->pMan) );
+    for ( i = 1; i < p->nClauses; i++ )
+        pCnf->pClauses[i] = pCnf->pClauses[0] + (p->pClauses[i] - p->pClauses[0]);
+    Vec_IntForEachEntry( vLits, iLit, i ) {
+        pCnf->pClauses[p->nClauses+i] = pCnf->pClauses[0] + p->nLiterals+i;
+        pCnf->pClauses[p->nClauses+i][0] = iLit;
+    }
+    assert( pCnf->pClauses[p->nClauses+Vec_IntSize(vLits)] == pCnf->pClauses[0] + p->nLiterals+Vec_IntSize(vLits) );
+    return pCnf;
+}
 
 /**Function*************************************************************
 
diff --git a/src/sat/cnf/cnfUtil.c b/src/sat/cnf/cnfUtil.c
index 5ccbeb0dd..ac6d0ebf1 100644
--- a/src/sat/cnf/cnfUtil.c
+++ b/src/sat/cnf/cnfUtil.c
@@ -9,7 +9,7 @@
   Synopsis    []
 
   Author      [Alan Mishchenko]
-  
+
   Affiliation [UC Berkeley]
 
   Date        [Ver. 1.0. Started - April 28, 2007.]
@@ -23,55 +23,253 @@
 
 ABC_NAMESPACE_IMPL_START
 
+#ifdef ABC_USE_PTHREADS
+
+#ifdef _WIN32
+#include "../lib/pthread.h"
+#else
+#include <pthread.h>
+#include <unistd.h>
+#endif
+
+#endif
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+extern Vec_Int_t *Exa4_ManParse(char *pFileName);
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Computes area, references, and nodes used in the mapping.]
+  Synopsis    [Solving problems using one core.]
 
   Description []
-               
+
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int Aig_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped )
+Vec_Int_t *Cnf_RunSolverOnce(int Id, int Rand, int TimeOut, int fVerbose)
 {
-    Aig_Obj_t * pLeaf;
-    Dar_Cut_t * pCutBest;
-    int aArea, i;
-    if ( pObj->nRefs++ || Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj) )
-        return 0;
-    assert( Aig_ObjIsAnd(pObj) );
-    // collect the node first to derive pre-order
-    if ( vMapped )
-        Vec_PtrPush( vMapped, pObj );
-    // visit the transitive fanin of the selected cut
-    if ( pObj->fMarkB )
+    int fVerboseSolver = 0;
+    Vec_Int_t *vRes = NULL;
+    abctime clkTotal = Abc_Clock();
+    char FileNameIn[100], FileNameOut[100];
+    sprintf(FileNameIn,  "%02d.cnf", Id);
+    sprintf(FileNameOut, "%02d.txt", Id);
+#ifdef _WIN32
+    char *pKissat = "kissat.exe";
+#else
+    char *pKissat = "kissat";
+#endif
+    char Command[1000], *pCommand = (char *)&Command;
+    if (TimeOut)
+        sprintf(pCommand, "%s --seed=%d --time=%d %s %s > %s", pKissat, Rand, TimeOut, fVerboseSolver ? "" : "-q", FileNameIn, FileNameOut);
+    else
+        sprintf(pCommand, "%s --seed=%d %s %s > %s", pKissat, Rand, fVerboseSolver ? "" : "-q", FileNameIn, FileNameOut);
+    //printf( "Thread command: %s\n", pCommand);
+    FILE * pFile = fopen(FileNameIn, "rb");
+    if ( pFile != NULL ) {
+        fclose( pFile );
+        if (system(pCommand) == -1) {
+            fprintf(stdout, "Command \"%s\" did not succeed.\n", pCommand);
+            return 0;
+        }
+        vRes = Exa4_ManParse(FileNameOut); // FileNameOut is removed here
+    }
+    if (fVerbose) {
+        double SolvingTime = ((double)(Abc_Clock() - clkTotal))/((double)CLOCKS_PER_SEC);
+        if (vRes)
+            printf("Problem %2d has a solution. ", Id);
+        else if (vRes == NULL && (TimeOut == 0 || SolvingTime < (double)TimeOut))
+            printf("Problem %2d has no solution. ", Id);
+        else if (vRes == NULL)
+            printf("Problem %2d has no solution or timed out after %d sec. ", Id, TimeOut);
+        Abc_PrintTime(1, "Solving time", Abc_Clock() - clkTotal );
+    }
+    else if (vRes) {   
+        printf("Problem %2d has a solution. ", Id);
+        Abc_PrintTime(1, "Solving time", Abc_Clock() - clkTotal );
+        printf("(Currently waiting for %d sec for other threads to finish.)\n", TimeOut);
+    }
+    return vRes;
+}
+Vec_Int_t * Cnf_RunSolverArray(int nProcs, int TimeOut, int fVerbose)
+{
+    Vec_Int_t *vRes = NULL; int i;
+    for ( i = 0; i < nProcs; i++ )
+        if ((vRes = Cnf_RunSolverOnce(i, 0, TimeOut, fVerbose))) 
+            break;
+    return vRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Solving problems using many cores.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+#ifndef ABC_USE_PTHREADS
+
+Vec_Int_t *Cnf_RunSolver(int nProcs, int TimeOut, int fVerbose)
+{
+    return Cnf_RunSolverArray(nProcs, TimeOut, fVerbose);
+}
+
+#else // pthreads are used
+
+#define PAR_THR_MAX 100
+typedef struct Cnf_ThData_t_
+{
+    Vec_Int_t *vRes;
+    int Index;
+    int Rand;
+    int nTimeOut;
+    int fWorking;
+    int fVerbose;
+} Cnf_ThData_t;
+
+void *Cnf_WorkerThread(void *pArg)
+{
+    Cnf_ThData_t *pThData = (Cnf_ThData_t *)pArg;
+    volatile int *pPlace = &pThData->fWorking;
+    while (1)
     {
-        Vec_Ptr_t * vSuper = Vec_PtrAlloc( 100 );
-        Aig_ObjCollectSuper( pObj, vSuper );
+        while (*pPlace == 0)
+            ;
+        assert(pThData->fWorking);
+        if (pThData->Index == -1)
+        {
+            pthread_exit(NULL);
+            assert(0);
+            return NULL;
+        }
+        pThData->vRes = Cnf_RunSolverOnce(pThData->Index, pThData->Rand, pThData->nTimeOut, pThData->fVerbose);
+        pThData->fWorking = 0;
+    }
+    assert(0);
+    return NULL;
+}
+
+Vec_Int_t *Cnf_RunSolver(int nProcs, int TimeOut, int fVerbose)
+{
+    Vec_Int_t *vRes = NULL;
+    Cnf_ThData_t ThData[PAR_THR_MAX];
+    pthread_t WorkerThread[PAR_THR_MAX];
+    int i, k, status;
+    if (fVerbose)
+        printf("Running concurrent solving with %d processes.\n", nProcs);
+    fflush(stdout);
+    if (nProcs < 2)
+        return Cnf_RunSolverArray(nProcs, TimeOut, fVerbose);
+    // subtract manager thread
+    // nProcs--;
+    assert(nProcs >= 1 && nProcs <= PAR_THR_MAX);
+    // start threads
+    for (i = 0; i < nProcs; i++)
+    {
+        ThData[i].vRes     = NULL;
+        ThData[i].Index    = -1;
+        ThData[i].Rand     = Abc_Random(0) % 0x1000000;
+        ThData[i].nTimeOut = TimeOut;
+        ThData[i].fWorking = 0;
+        ThData[i].fVerbose = fVerbose;
+        status = pthread_create(WorkerThread + i, NULL, Cnf_WorkerThread, (void *)(ThData + i));
+        assert(status == 0);
+    }
+    // look at the threads
+    for (k = 0; k < nProcs;)
+    {
+        for (i = 0; i < nProcs; i++)
+        {
+            if (ThData[i].fWorking)
+                continue;
+            if (ThData[i].vRes)
+            {
+                k = nProcs;
+                break;
+            }
+            ThData[i].Index = k++;
+            ThData[i].fWorking = 1;
+            break;
+        }
+    }
+    // wait till threads finish
+    for (i = 0; i < nProcs; i++)
+        if (ThData[i].fWorking)
+            i = -1;
+    // stop threads
+    for (i = 0; i < nProcs; i++)
+    {
+        assert(!ThData[i].fWorking);
+        if (ThData[i].vRes && vRes == NULL)
+        {
+            vRes = ThData[i].vRes;
+            ThData[i].vRes = NULL;
+        }
+        Vec_IntFreeP(&ThData[i].vRes);
+        // stop
+        ThData[i].Index = -1;
+        ThData[i].fWorking = 1;
+    }
+    return vRes;
+}
+
+#endif // pthreads are used
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes area, references, and nodes used in the mapping.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManScanMapping_rec(Cnf_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vMapped)
+{
+    Aig_Obj_t *pLeaf;
+    Dar_Cut_t *pCutBest;
+    int aArea, i;
+    if (pObj->nRefs++ || Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj))
+        return 0;
+    assert(Aig_ObjIsAnd(pObj));
+    // collect the node first to derive pre-order
+    if (vMapped)
+        Vec_PtrPush(vMapped, pObj);
+    // visit the transitive fanin of the selected cut
+    if (pObj->fMarkB)
+    {
+        Vec_Ptr_t *vSuper = Vec_PtrAlloc(100);
+        Aig_ObjCollectSuper(pObj, vSuper);
         aArea = Vec_PtrSize(vSuper) + 1;
-        Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pLeaf, i )
-            aArea += Aig_ManScanMapping_rec( p, Aig_Regular(pLeaf), vMapped );
-        Vec_PtrFree( vSuper );
+        Vec_PtrForEachEntry(Aig_Obj_t *, vSuper, pLeaf, i)
+            aArea += Aig_ManScanMapping_rec(p, Aig_Regular(pLeaf), vMapped);
+        Vec_PtrFree(vSuper);
         ////////////////////////////
         pObj->fMarkB = 1;
     }
     else
     {
-        pCutBest = Dar_ObjBestCut( pObj );
-        aArea = Cnf_CutSopCost( p, pCutBest );
-        Dar_CutForEachLeaf( p->pManAig, pCutBest, pLeaf, i )
-            aArea += Aig_ManScanMapping_rec( p, pLeaf, vMapped );
+        pCutBest = Dar_ObjBestCut(pObj);
+        aArea = Cnf_CutSopCost(p, pCutBest);
+        Dar_CutForEachLeaf(p->pManAig, pCutBest, pLeaf, i)
+            aArea += Aig_ManScanMapping_rec(p, pLeaf, vMapped);
     }
     return aArea;
 }
@@ -81,28 +279,28 @@ int Aig_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped
   Synopsis    [Computes area, references, and nodes used in the mapping.]
 
   Description [Collects the nodes in reverse topological order.]
-               
+
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Aig_ManScanMapping( Cnf_Man_t * p, int fCollect )
+Vec_Ptr_t *Aig_ManScanMapping(Cnf_Man_t *p, int fCollect)
 {
-    Vec_Ptr_t * vMapped = NULL;
-    Aig_Obj_t * pObj;
+    Vec_Ptr_t *vMapped = NULL;
+    Aig_Obj_t *pObj;
     int i;
     // clean all references
-    Aig_ManForEachObj( p->pManAig, pObj, i )
+    Aig_ManForEachObj(p->pManAig, pObj, i)
         pObj->nRefs = 0;
     // allocate the array
-    if ( fCollect )
-        vMapped = Vec_PtrAlloc( 1000 );
+    if (fCollect)
+        vMapped = Vec_PtrAlloc(1000);
     // collect nodes reachable from POs in the DFS order through the best cuts
     p->aArea = 0;
-    Aig_ManForEachCo( p->pManAig, pObj, i )
-        p->aArea += Aig_ManScanMapping_rec( p, Aig_ObjFanin0(pObj), vMapped );
-//    printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManCiNum(p->pManAig) + 1 : 0, p->aArea + 2 );
+    Aig_ManForEachCo(p->pManAig, pObj, i)
+        p->aArea += Aig_ManScanMapping_rec(p, Aig_ObjFanin0(pObj), vMapped);
+    //    printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManCiNum(p->pManAig) + 1 : 0, p->aArea + 2 );
     return vMapped;
 }
 
@@ -111,48 +309,48 @@ Vec_Ptr_t * Aig_ManScanMapping( Cnf_Man_t * p, int fCollect )
   Synopsis    [Computes area, references, and nodes used in the mapping.]
 
   Description []
-               
+
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int Cnf_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped, int fPreorder )
+int Cnf_ManScanMapping_rec(Cnf_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vMapped, int fPreorder)
 {
-    Aig_Obj_t * pLeaf;
-    Cnf_Cut_t * pCutBest;
+    Aig_Obj_t *pLeaf;
+    Cnf_Cut_t *pCutBest;
     int aArea, i;
-    if ( pObj->nRefs++ || Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj) )
+    if (pObj->nRefs++ || Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj))
         return 0;
-    assert( Aig_ObjIsAnd(pObj) );
-    assert( pObj->pData != NULL );
+    assert(Aig_ObjIsAnd(pObj));
+    assert(pObj->pData != NULL);
     // add the node to the mapping
-    if ( vMapped && fPreorder )
-         Vec_PtrPush( vMapped, pObj );
+    if (vMapped && fPreorder)
+        Vec_PtrPush(vMapped, pObj);
     // visit the transitive fanin of the selected cut
-    if ( pObj->fMarkB )
+    if (pObj->fMarkB)
     {
-        Vec_Ptr_t * vSuper = Vec_PtrAlloc( 100 );
-        Aig_ObjCollectSuper( pObj, vSuper );
+        Vec_Ptr_t *vSuper = Vec_PtrAlloc(100);
+        Aig_ObjCollectSuper(pObj, vSuper);
         aArea = Vec_PtrSize(vSuper) + 1;
-        Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pLeaf, i )
-            aArea += Cnf_ManScanMapping_rec( p, Aig_Regular(pLeaf), vMapped, fPreorder );
-        Vec_PtrFree( vSuper );
+        Vec_PtrForEachEntry(Aig_Obj_t *, vSuper, pLeaf, i)
+            aArea += Cnf_ManScanMapping_rec(p, Aig_Regular(pLeaf), vMapped, fPreorder);
+        Vec_PtrFree(vSuper);
         ////////////////////////////
         pObj->fMarkB = 1;
     }
     else
     {
         pCutBest = (Cnf_Cut_t *)pObj->pData;
-//        assert( pCutBest->nFanins > 0 );
-        assert( pCutBest->Cost < 127 );
+        //        assert( pCutBest->nFanins > 0 );
+        assert(pCutBest->Cost < 127);
         aArea = pCutBest->Cost;
-        Cnf_CutForEachLeaf( p->pManAig, pCutBest, pLeaf, i )
-            aArea += Cnf_ManScanMapping_rec( p, pLeaf, vMapped, fPreorder );
+        Cnf_CutForEachLeaf(p->pManAig, pCutBest, pLeaf, i)
+            aArea += Cnf_ManScanMapping_rec(p, pLeaf, vMapped, fPreorder);
     }
     // add the node to the mapping
-    if ( vMapped && !fPreorder )
-         Vec_PtrPush( vMapped, pObj );
+    if (vMapped && !fPreorder)
+        Vec_PtrPush(vMapped, pObj);
     return aArea;
 }
 
@@ -161,28 +359,28 @@ int Cnf_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped
   Synopsis    [Computes area, references, and nodes used in the mapping.]
 
   Description [Collects the nodes in reverse topological order.]
-               
+
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPreorder )
+Vec_Ptr_t *Cnf_ManScanMapping(Cnf_Man_t *p, int fCollect, int fPreorder)
 {
-    Vec_Ptr_t * vMapped = NULL;
-    Aig_Obj_t * pObj;
+    Vec_Ptr_t *vMapped = NULL;
+    Aig_Obj_t *pObj;
     int i;
     // clean all references
-    Aig_ManForEachObj( p->pManAig, pObj, i )
+    Aig_ManForEachObj(p->pManAig, pObj, i)
         pObj->nRefs = 0;
     // allocate the array
-    if ( fCollect )
-        vMapped = Vec_PtrAlloc( 1000 );
+    if (fCollect)
+        vMapped = Vec_PtrAlloc(1000);
     // collect nodes reachable from POs in the DFS order through the best cuts
     p->aArea = 0;
-    Aig_ManForEachCo( p->pManAig, pObj, i )
-        p->aArea += Cnf_ManScanMapping_rec( p, Aig_ObjFanin0(pObj), vMapped, fPreorder );
-//    printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManCiNum(p->pManAig) + 1 : 0, p->aArea + 2 );
+    Aig_ManForEachCo(p->pManAig, pObj, i)
+        p->aArea += Cnf_ManScanMapping_rec(p, Aig_ObjFanin0(pObj), vMapped, fPreorder);
+    //    printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManCiNum(p->pManAig) + 1 : 0, p->aArea + 2 );
     return vMapped;
 }
 
@@ -191,20 +389,20 @@ Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPreorder )
   Synopsis    [Returns the array of CI IDs.]
 
   Description []
-               
+
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Cnf_DataCollectCiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p )
+Vec_Int_t *Cnf_DataCollectCiSatNums(Cnf_Dat_t *pCnf, Aig_Man_t *p)
 {
-    Vec_Int_t * vCiIds;
-    Aig_Obj_t * pObj;
+    Vec_Int_t *vCiIds;
+    Aig_Obj_t *pObj;
     int i;
-    vCiIds = Vec_IntAlloc( Aig_ManCiNum(p) );
-    Aig_ManForEachCi( p, pObj, i )
-        Vec_IntPush( vCiIds, pCnf->pVarNums[pObj->Id] );
+    vCiIds = Vec_IntAlloc(Aig_ManCiNum(p));
+    Aig_ManForEachCi(p, pObj, i)
+        Vec_IntPush(vCiIds, pCnf->pVarNums[pObj->Id]);
     return vCiIds;
 }
 
@@ -213,20 +411,20 @@ Vec_Int_t * Cnf_DataCollectCiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p )
   Synopsis    [Returns the array of CI IDs.]
 
   Description []
-               
+
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Cnf_DataCollectCoSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p )
+Vec_Int_t *Cnf_DataCollectCoSatNums(Cnf_Dat_t *pCnf, Aig_Man_t *p)
 {
-    Vec_Int_t * vCoIds;
-    Aig_Obj_t * pObj;
+    Vec_Int_t *vCoIds;
+    Aig_Obj_t *pObj;
     int i;
-    vCoIds = Vec_IntAlloc( Aig_ManCoNum(p) );
-    Aig_ManForEachCo( p, pObj, i )
-        Vec_IntPush( vCoIds, pCnf->pVarNums[pObj->Id] );
+    vCoIds = Vec_IntAlloc(Aig_ManCoNum(p));
+    Aig_ManForEachCo(p, pObj, i)
+        Vec_IntPush(vCoIds, pCnf->pVarNums[pObj->Id]);
     return vCoIds;
 }
 
@@ -235,58 +433,58 @@ Vec_Int_t * Cnf_DataCollectCoSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p )
   Synopsis    []
 
   Description []
-               
+
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-unsigned char * Cnf_DataDeriveLitPolarities( Cnf_Dat_t * p )
+unsigned char *Cnf_DataDeriveLitPolarities(Cnf_Dat_t *p)
 {
-    int i, c, iClaBeg, iClaEnd, * pLit;
-    unsigned * pPols0 = ABC_CALLOC( unsigned, Aig_ManObjNumMax(p->pMan) );
-    unsigned * pPols1 = ABC_CALLOC( unsigned, Aig_ManObjNumMax(p->pMan) );
-    unsigned char * pPres = ABC_CALLOC( unsigned char, p->nClauses );
-    for ( i = 0; i < Aig_ManObjNumMax(p->pMan); i++ )
+    int i, c, iClaBeg, iClaEnd, *pLit;
+    unsigned *pPols0 = ABC_CALLOC(unsigned, Aig_ManObjNumMax(p->pMan));
+    unsigned *pPols1 = ABC_CALLOC(unsigned, Aig_ManObjNumMax(p->pMan));
+    unsigned char *pPres = ABC_CALLOC(unsigned char, p->nClauses);
+    for (i = 0; i < Aig_ManObjNumMax(p->pMan); i++)
     {
-        if ( p->pObj2Count[i] == 0 )
+        if (p->pObj2Count[i] == 0)
             continue;
         iClaBeg = p->pObj2Clause[i];
         iClaEnd = p->pObj2Clause[i] + p->pObj2Count[i];
         // go through the negative polarity clauses
-        for ( c = iClaBeg; c < iClaEnd; c++ )
-            for ( pLit = p->pClauses[c]+1; pLit < p->pClauses[c+1]; pLit++ )
-                if ( Abc_LitIsCompl(p->pClauses[c][0]) )
-                    pPols0[Abc_Lit2Var(*pLit)] |= (unsigned)(2 - Abc_LitIsCompl(*pLit));  // taking the opposite (!) -- not the case
+        for (c = iClaBeg; c < iClaEnd; c++)
+            for (pLit = p->pClauses[c] + 1; pLit < p->pClauses[c + 1]; pLit++)
+                if (Abc_LitIsCompl(p->pClauses[c][0]))
+                    pPols0[Abc_Lit2Var(*pLit)] |= (unsigned)(2 - Abc_LitIsCompl(*pLit)); // taking the opposite (!) -- not the case
                 else
-                    pPols1[Abc_Lit2Var(*pLit)] |= (unsigned)(2 - Abc_LitIsCompl(*pLit));  // taking the opposite (!) -- not the case
+                    pPols1[Abc_Lit2Var(*pLit)] |= (unsigned)(2 - Abc_LitIsCompl(*pLit)); // taking the opposite (!) -- not the case
         // record these clauses
-        for ( c = iClaBeg; c < iClaEnd; c++ )
-            for ( pLit = p->pClauses[c]+1; pLit < p->pClauses[c+1]; pLit++ )
-                if ( Abc_LitIsCompl(p->pClauses[c][0]) )
-                    pPres[c] = (unsigned char)( (unsigned)pPres[c] | (pPols0[Abc_Lit2Var(*pLit)] << (2*(pLit-p->pClauses[c]-1))) );
+        for (c = iClaBeg; c < iClaEnd; c++)
+            for (pLit = p->pClauses[c] + 1; pLit < p->pClauses[c + 1]; pLit++)
+                if (Abc_LitIsCompl(p->pClauses[c][0]))
+                    pPres[c] = (unsigned char)((unsigned)pPres[c] | (pPols0[Abc_Lit2Var(*pLit)] << (2 * (pLit - p->pClauses[c] - 1))));
                 else
-                    pPres[c] = (unsigned char)( (unsigned)pPres[c] | (pPols1[Abc_Lit2Var(*pLit)] << (2*(pLit-p->pClauses[c]-1))) );
+                    pPres[c] = (unsigned char)((unsigned)pPres[c] | (pPols1[Abc_Lit2Var(*pLit)] << (2 * (pLit - p->pClauses[c] - 1))));
         // clean negative polarity
-        for ( c = iClaBeg; c < iClaEnd; c++ )
-            for ( pLit = p->pClauses[c]+1; pLit < p->pClauses[c+1]; pLit++ )
+        for (c = iClaBeg; c < iClaEnd; c++)
+            for (pLit = p->pClauses[c] + 1; pLit < p->pClauses[c + 1]; pLit++)
                 pPols0[Abc_Lit2Var(*pLit)] = pPols1[Abc_Lit2Var(*pLit)] = 0;
     }
-    ABC_FREE( pPols0 );
-    ABC_FREE( pPols1 );
-/*
-//    for ( c = 0; c < p->nClauses; c++ )
-    for ( c = 0; c < 100; c++ )
-    {
-        printf( "Clause %6d : ", c );
-        for ( i = 0; i < 4; i++ )
-            printf( "%d ", ((unsigned)pPres[c] >> (2*i)) & 3 );
-        printf( "  " );
-        for ( pLit = p->pClauses[c]; pLit < p->pClauses[c+1]; pLit++ )
-            printf( "%6d ", *pLit );
-        printf( "\n" );
-    }
-*/
+    ABC_FREE(pPols0);
+    ABC_FREE(pPols1);
+    /*
+    //    for ( c = 0; c < p->nClauses; c++ )
+        for ( c = 0; c < 100; c++ )
+        {
+            printf( "Clause %6d : ", c );
+            for ( i = 0; i < 4; i++ )
+                printf( "%d ", ((unsigned)pPres[c] >> (2*i)) & 3 );
+            printf( "  " );
+            for ( pLit = p->pClauses[c]; pLit < p->pClauses[c+1]; pLit++ )
+                printf( "%6d ", *pLit );
+            printf( "\n" );
+        }
+    */
     return pPres;
 }
 
@@ -295,96 +493,96 @@ unsigned char * Cnf_DataDeriveLitPolarities( Cnf_Dat_t * p )
   Synopsis    []
 
   Description []
-               
+
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Cnf_Dat_t * Cnf_DataReadFromFile( char * pFileName )
+Cnf_Dat_t *Cnf_DataReadFromFile(char *pFileName)
 {
     int MaxLine = 1000000;
     int Var, Lit, nVars = -1, nClas = -1, i, Entry, iLine = 0;
-    Cnf_Dat_t * pCnf = NULL;
-    Vec_Int_t * vClas = NULL;
-    Vec_Int_t * vLits = NULL;
-    char * pBuffer, * pToken;
-    FILE * pFile = fopen( pFileName, "rb" );
-    if ( pFile == NULL )
+    Cnf_Dat_t *pCnf = NULL;
+    Vec_Int_t *vClas = NULL;
+    Vec_Int_t *vLits = NULL;
+    char *pBuffer, *pToken;
+    FILE *pFile = fopen(pFileName, "rb");
+    if (pFile == NULL)
     {
-        printf( "Cannot open file \"%s\" for writing.\n", pFileName );
+        printf("Cannot open file \"%s\" for writing.\n", pFileName);
         return NULL;
     }
-    pBuffer = ABC_ALLOC( char, MaxLine );
-    while ( fgets(pBuffer, MaxLine, pFile) != NULL )
+    pBuffer = ABC_ALLOC(char, MaxLine);
+    while (fgets(pBuffer, MaxLine, pFile) != NULL)
     {
         iLine++;
-        if ( pBuffer[0] == 'c' )
+        if (pBuffer[0] == 'c')
             continue;
-        if ( pBuffer[0] == 'p' )
+        if (pBuffer[0] == 'p')
         {
-            pToken = strtok( pBuffer+1, " \t" );
-            if ( strcmp(pToken, "cnf") )
+            pToken = strtok(pBuffer + 1, " \t");
+            if (strcmp(pToken, "cnf"))
             {
-                printf( "Incorrect input file.\n" );
+                printf("Incorrect input file.\n");
                 goto finish;
             }
-            pToken = strtok( NULL, " \t" );
-            nVars = atoi( pToken );
-            pToken = strtok( NULL, " \t" );
-            nClas = atoi( pToken );
-            if ( nVars <= 0 || nClas <= 0 )
+            pToken = strtok(NULL, " \t");
+            nVars = atoi(pToken);
+            pToken = strtok(NULL, " \t");
+            nClas = atoi(pToken);
+            if (nVars <= 0 || nClas <= 0)
             {
-                printf( "Incorrect parameters.\n" );
+                printf("Incorrect parameters.\n");
                 goto finish;
             }
             // temp storage
-            vClas = Vec_IntAlloc( nClas+1 );
-            vLits = Vec_IntAlloc( nClas*8 );
+            vClas = Vec_IntAlloc(nClas + 1);
+            vLits = Vec_IntAlloc(nClas * 8);
             continue;
         }
-        pToken = strtok( pBuffer, " \t\r\n" );
-        if ( pToken == NULL )
+        pToken = strtok(pBuffer, " \t\r\n");
+        if (pToken == NULL)
             continue;
-        Vec_IntPush( vClas, Vec_IntSize(vLits) );
-        while ( pToken )
+        Vec_IntPush(vClas, Vec_IntSize(vLits));
+        while (pToken)
         {
-            Var = atoi( pToken );
-            if ( Var == 0 )
+            Var = atoi(pToken);
+            if (Var == 0)
                 break;
-            Lit = (Var > 0) ? Abc_Var2Lit(Var-1, 0) : Abc_Var2Lit(-Var-1, 1);
-            if ( Lit >= 2*nVars )
+            Lit = (Var > 0) ? Abc_Var2Lit(Var - 1, 0) : Abc_Var2Lit(-Var - 1, 1);
+            if (Lit >= 2 * nVars)
             {
-                printf( "Literal %d is out-of-bound for %d variables.\n", Lit, nVars );
+                printf("Literal %d is out-of-bound for %d variables.\n", Lit, nVars);
                 goto finish;
             }
-            Vec_IntPush( vLits, Lit );
-            pToken = strtok( NULL, " \t\r\n" );
+            Vec_IntPush(vLits, Lit);
+            pToken = strtok(NULL, " \t\r\n");
         }
-        if ( Var != 0 )
+        if (Var != 0)
         {
-            printf( "There is no zero-terminator in line %d.\n", iLine );
+            printf("There is no zero-terminator in line %d.\n", iLine);
             goto finish;
         }
     }
     // finalize
-    if ( Vec_IntSize(vClas) != nClas )
-        printf( "Warning! The number of clauses (%d) is different from declaration (%d).\n", Vec_IntSize(vClas), nClas );
-    Vec_IntPush( vClas, Vec_IntSize(vLits) );
+    if (Vec_IntSize(vClas) != nClas)
+        printf("Warning! The number of clauses (%d) is different from declaration (%d).\n", Vec_IntSize(vClas), nClas);
+    Vec_IntPush(vClas, Vec_IntSize(vLits));
     // create
-    pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
-    pCnf->nVars     = nVars;
-    pCnf->nClauses  = Vec_IntSize(vClas)-1;
+    pCnf = ABC_CALLOC(Cnf_Dat_t, 1);
+    pCnf->nVars = nVars;
+    pCnf->nClauses = Vec_IntSize(vClas) - 1;
     pCnf->nLiterals = Vec_IntSize(vLits);
-    pCnf->pClauses  = ABC_ALLOC( int *, Vec_IntSize(vClas) );
+    pCnf->pClauses = ABC_ALLOC(int *, Vec_IntSize(vClas));
     pCnf->pClauses[0] = Vec_IntReleaseArray(vLits);
-    Vec_IntForEachEntry( vClas, Entry, i )
+    Vec_IntForEachEntry(vClas, Entry, i)
         pCnf->pClauses[i] = pCnf->pClauses[0] + Entry;
 finish:
-    fclose( pFile );
-    Vec_IntFreeP( &vClas );
-    Vec_IntFreeP( &vLits );
-    ABC_FREE( pBuffer );
+    fclose(pFile);
+    Vec_IntFreeP(&vClas);
+    Vec_IntFreeP(&vLits);
+    ABC_FREE(pBuffer);
     return pCnf;
 }
 
@@ -393,87 +591,224 @@ finish:
   Synopsis    []
 
   Description []
-               
+
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fVerbose, int fShowPattern, int ** ppModel, int nPis )
+int Cnf_DataSolveFromFile(char *pFileName, int nConfLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fVerbose, int fShowPattern, int **ppModel, int nPis)
 {
     abctime clk = Abc_Clock();
-    Cnf_Dat_t * pCnf = Cnf_DataReadFromFile( pFileName );
-    sat_solver * pSat;
+    Cnf_Dat_t *pCnf = Cnf_DataReadFromFile(pFileName);
+    sat_solver *pSat;
     int i, status, RetValue = -1;
-    if ( pCnf == NULL )
+    if (pCnf == NULL)
         return -1;
-    if ( fVerbose )
+    if (fVerbose)
     {
-        printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
-        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+        printf("CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals);
+        Abc_PrintTime(1, "Time", Abc_Clock() - clk);
     }
     // convert into SAT solver
-    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
-    if ( pSat == NULL )
+    pSat = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0);
+    if (pSat == NULL)
     {
-        printf( "The problem is trivially UNSAT.\n" );
-        Cnf_DataFree( pCnf );
+        printf("The problem is trivially UNSAT.\n");
+        Cnf_DataFree(pCnf);
         return 1;
     }
-    if ( nLearnedStart )
+    if (nLearnedStart)
         pSat->nLearntStart = pSat->nLearntMax = nLearnedStart;
-    if ( nLearnedDelta )
+    if (nLearnedDelta)
         pSat->nLearntDelta = nLearnedDelta;
-    if ( nLearnedPerce )
+    if (nLearnedPerce)
         pSat->nLearntRatio = nLearnedPerce;
-    if ( fVerbose )
+    if (fVerbose)
         pSat->fVerbose = fVerbose;
 
-//sat_solver_start_cardinality( pSat, 100 );
+    // sat_solver_start_cardinality( pSat, 100 );
 
     // solve the miter
-    status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, 0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-    if ( status == l_Undef )
+    status = sat_solver_solve(pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, 0, (ABC_INT64_T)0, (ABC_INT64_T)0);
+    if (status == l_Undef)
         RetValue = -1;
-    else if ( status == l_True )
+    else if (status == l_True)
         RetValue = 0;
-    else if ( status == l_False )
+    else if (status == l_False)
         RetValue = 1;
     else
-        assert( 0 );
-    if ( fVerbose )
-        Sat_SolverPrintStats( stdout, pSat );
-    if ( RetValue == -1 )
-        Abc_Print( 1, "UNDECIDED      " );
-    else if ( RetValue == 0 )
-        Abc_Print( 1, "SATISFIABLE    " );
+        assert(0);
+    if (fVerbose)
+        Sat_SolverPrintStats(stdout, pSat);
+    if (RetValue == -1)
+        Abc_Print(1, "UNDECIDED      ");
+    else if (RetValue == 0)
+        Abc_Print(1, "SATISFIABLE    ");
     else
-        Abc_Print( 1, "UNSATISFIABLE  " );
-    //Abc_Print( -1, "\n" );
-    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+        Abc_Print(1, "UNSATISFIABLE  ");
+    // Abc_Print( -1, "\n" );
+    Abc_PrintTime(1, "Time", Abc_Clock() - clk);
     // derive SAT assignment
-    if ( RetValue == 0 && nPis > 0 )
+    if (RetValue == 0 && nPis > 0)
     {
-        *ppModel = ABC_ALLOC( int, nPis );
-        for ( i = 0; i < nPis; i++ )
-            (*ppModel)[i] = sat_solver_var_value( pSat, pCnf->nVars - nPis + i );
+        *ppModel = ABC_ALLOC(int, nPis);
+        for (i = 0; i < nPis; i++)
+            (*ppModel)[i] = sat_solver_var_value(pSat, pCnf->nVars - nPis + i);
     }
-    if ( RetValue == 0 && fShowPattern )
+    if (RetValue == 0 && fShowPattern)
     {
-        for ( i = 0; i < pCnf->nVars; i++ )
-            printf( "%d", sat_solver_var_value(pSat,i) );
-        printf( "\n" );
+        for (i = 0; i < pCnf->nVars; i++)
+            printf("%d", sat_solver_var_value(pSat, i));
+        printf("\n");
     }
-    Cnf_DataFree( pCnf );
-    sat_solver_delete( pSat );
+    Cnf_DataFree(pCnf);
+    sat_solver_delete(pSat);
     return RetValue;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cnf_DataBestVar(Cnf_Dat_t *p, int *pSkip)
+{
+    int *pNums = ABC_CALLOC(int, p->nVars);
+    int i, *pLit, NumMax = -1, iVarMax = -1;
+    for (i = 0; i < p->nClauses; i++)
+        for (pLit = p->pClauses[i]; pLit < p->pClauses[i + 1]; pLit++)
+            pNums[Abc_Lit2Var(*pLit)]++;
+    for (i = 0; i < p->nVars; i++)
+        if ((!pSkip || !pSkip[i]) && NumMax < pNums[i])
+            NumMax = pNums[i], iVarMax = i;
+    ABC_FREE(pNums);
+    return iVarMax;
+}
+void Cnf_Experiment1()
+{
+    Cnf_Dat_t *pTemp, *p = Cnf_DataReadFromFile("../166b.cnf");
+    int i, *pSkip = ABC_CALLOC(int, p->nVars);
+    for (i = 0; i < 100; i++)
+    {
+        int iVar = Cnf_DataBestVar(p, pSkip);
+        char FileName[100];
+        sprintf(FileName, "cnf/%03d.cnf", i);
+        Cnf_DataWriteIntoFile(p, FileName, 0, NULL, NULL);
+        printf("Dumped file \"%s\".\n", FileName);
+        p = Cnf_DataDupCof(pTemp = p, Abc_Var2Lit(iVar, 0));
+        Cnf_DataFree(pTemp);
+        pSkip[iVar] = 1;
+    }
+    Cnf_DataFree(p);
+    ABC_FREE(pSkip);
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t *Cnf_GenRandLits(int iVarBeg, int iVarEnd, int nLits, int Value, int Rand, int fVerbose)
+{
+    Vec_Int_t *vLits = Vec_IntAlloc(nLits);
+    assert(iVarBeg < iVarEnd && nLits < iVarEnd - iVarBeg);
+    while (Vec_IntSize(vLits) < nLits)
+    {
+        int iVar = iVarBeg + (Abc_Random(0) ^ Rand) % (iVarEnd - iVarBeg);
+        assert(iVar >= iVarBeg && iVar < iVarEnd);
+        if (Vec_IntFind(vLits, Abc_Var2Lit(iVar, 0)) == -1 && Vec_IntFind(vLits, Abc_Var2Lit(iVar, 1)) == -1)
+        {
+            if (Value == 0)
+                Vec_IntPush(vLits, Abc_Var2Lit(iVar, 1));
+            else if (Value == 1)
+                Vec_IntPush(vLits, Abc_Var2Lit(iVar, 0));
+            else
+                Vec_IntPush(vLits, Abc_Var2Lit(iVar, Abc_Random(0) & 1));
+        }
+    }
+    Vec_IntSort(vLits, 0);
+    if ( fVerbose )
+    Vec_IntPrint(vLits);
+    fflush(stdout);
+    return vLits;
+}
+void Cnf_SplitCnfFile(char * pFileName, int nParts, int iVarBeg, int iVarEnd, int nLits, int Value, int Rand, int fPrepro, int fVerbose)
+{
+    Cnf_Dat_t *p = Cnf_DataReadFromFile(pFileName); int k;
+    if (iVarEnd == ABC_INFINITY)
+        iVarEnd = p->nVars;
+    for (k = 0; k < nParts; k++)
+    {
+        Vec_Int_t *vLits = Cnf_GenRandLits(iVarBeg, iVarEnd, nLits, Value, Rand, fVerbose);
+        Cnf_Dat_t *pCnf = Cnf_DataDupCofArray(p, vLits);
+        char FileName[100];  sprintf(FileName, "%02d.cnf", k);
+        if ( fPrepro ) {
+            char Command[1000];   
+            sprintf(Command, "satelite --verbosity=0 -pre temp.cnf %s", FileName);
+            Cnf_DataWriteIntoFile(pCnf, "temp.cnf", 0, NULL, NULL);
+            if (system(Command) == -1) {
+                fprintf(stdout, "Command \"%s\" did not succeed. Preprocessing skipped.\n", Command);
+                Cnf_DataWriteIntoFile(pCnf, FileName, 0, NULL, NULL);
+            }
+            unlink("temp.cnf");
+        }
+        else 
+            Cnf_DataWriteIntoFile(pCnf, FileName, 0, NULL, NULL);
+        Cnf_DataFree(pCnf);
+        Vec_IntFree(vLits);
+    }    
+    Cnf_DataFree(p);
+}
+void Cnf_SplitCnfCleanup(int nParts)
+{
+    char FileName[100];  int k;
+    for (k = 0; k < nParts; k++) {
+        sprintf(FileName, "%02d.cnf", k);
+        unlink(FileName);
+    }   
+}
+void Cnf_SplitSat(char *pFileName, int iVarBeg, int iVarEnd, int nLits, int Value, int TimeOut, int nProcs, int nIters, int Seed, int fPrepro, int fVerbose)
+{
+    abctime clk = Abc_Clock();
+    Vec_Int_t *vSol = NULL;
+    int i, Rand = 0;
+    if ( nIters == 0 )
+        nIters = ABC_INFINITY;
+    Abc_Random(1);
+    for ( i = 0; i < Seed; i++ )
+        Abc_Random(0);
+    Rand = Abc_Random(0);
+    for (i = 0; i < nIters && !vSol; i++)
+    {
+        abctime clk2 = Abc_Clock();
+        Cnf_SplitCnfFile(pFileName, nProcs, iVarBeg, iVarEnd, nLits, Value, Rand, fPrepro, fVerbose);
+        vSol = Cnf_RunSolver(nProcs, TimeOut, fVerbose);
+        Cnf_SplitCnfCleanup(nProcs);
+        if (fVerbose) {
+            printf( "Finished iteration %d.  ", i);    
+            Abc_PrintTime(0, "Time", Abc_Clock() - clk2);
+        }
+    }
+    printf("%solution is found.  ", vSol ? "S" : "No s");
+    Abc_PrintTime(0, "Total time", Abc_Clock() - clk);
+    Vec_IntFreeP(&vSol);
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-
 ABC_NAMESPACE_IMPL_END
-