Updates to delay optimization project.

9 files changed, 446 insertions, 198 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index ac40f975..d9b1716a 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -665,21 +665,6 @@ static inline int Gia_ManAppendAnd( Gia_Man_t * p, int iLit0, int iLit1 )
     }
     return Gia_ObjId( p, pObj ) << 1;
 }
-static inline int Gia_ManAppendAnd2( Gia_Man_t * p, int iLit0, int iLit1 )  
-{ 
-    if ( !p->fGiaSimple )
-    {
-        if ( iLit0 < 2 )
-            return iLit0 ? iLit1 : 0;
-        if ( iLit1 < 2 )
-            return iLit1 ? iLit0 : 0;
-        if ( iLit0 == iLit1 )
-            return iLit1;
-        if ( iLit0 == Abc_LitNot(iLit1) )
-            return 0;
-    }
-    return Gia_ManAppendAnd( p, iLit0, iLit1 );
-}
 static inline int Gia_ManAppendXorReal( Gia_Man_t * p, int iLit0, int iLit1 )  
 { 
     Gia_Obj_t * pObj = Gia_ManAppendObj( p );
@@ -780,6 +765,44 @@ static inline int Gia_ManAppendXor( Gia_Man_t * p, int iLit0, int iLit1 )
 { 
     return Gia_ManAppendMux( p, iLit0, Abc_LitNot(iLit1), iLit1 );
 }
+
+static inline int Gia_ManAppendAnd2( Gia_Man_t * p, int iLit0, int iLit1 )  
+{ 
+    if ( !p->fGiaSimple )
+    {
+        if ( iLit0 < 2 )
+            return iLit0 ? iLit1 : 0;
+        if ( iLit1 < 2 )
+            return iLit1 ? iLit0 : 0;
+        if ( iLit0 == iLit1 )
+            return iLit1;
+        if ( iLit0 == Abc_LitNot(iLit1) )
+            return 0;
+    }
+    return Gia_ManAppendAnd( p, iLit0, iLit1 );
+}
+static inline int Gia_ManAppendOr2( Gia_Man_t * p, int iLit0, int iLit1 )
+{
+    return Abc_LitNot(Gia_ManAppendAnd2( p, Abc_LitNot(iLit0), Abc_LitNot(iLit1) ));
+}
+static inline int Gia_ManAppendMux2( Gia_Man_t * p, int iCtrl, int iData1, int iData0 )  
+{ 
+    int iTemp0 = Gia_ManAppendAnd2( p, Abc_LitNot(iCtrl), iData0 );
+    int iTemp1 = Gia_ManAppendAnd2( p, iCtrl, iData1 );
+    return Abc_LitNotCond( Gia_ManAppendAnd2( p, Abc_LitNot(iTemp0), Abc_LitNot(iTemp1) ), 1 );
+}
+static inline int Gia_ManAppendMaj2( Gia_Man_t * p, int iData0, int iData1, int iData2 )  
+{ 
+    int iTemp0 = Gia_ManAppendOr2( p, iData1, iData2 );
+    int iTemp1 = Gia_ManAppendAnd2( p, iData0, iTemp0 );
+    int iTemp2 = Gia_ManAppendAnd2( p, iData1, iData2 );
+    return Gia_ManAppendOr2( p, iTemp1, iTemp2 );
+}
+static inline int Gia_ManAppendXor2( Gia_Man_t * p, int iLit0, int iLit1 )  
+{ 
+    return Gia_ManAppendMux2( p, iLit0, Abc_LitNot(iLit1), iLit1 );
+}
+
 static inline void Gia_ManPatchCoDriver( Gia_Man_t * p, int iCoIndex, int iLit0 )  
 {
     Gia_Obj_t * pObjCo  = Gia_ManCo( p, iCoIndex );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index f9717aa8..fccd4f63 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -41010,7 +41010,7 @@ int Abc_CommandAbc9Mfsd( Abc_Frame_t * pAbc, int argc, char ** argv )
     Sbd_Par_t Pars, * pPars = &Pars;
     Sbd_ParSetDefault( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "KSWFMCacvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KSNPWFMCacvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -41036,6 +41036,28 @@ int Abc_CommandAbc9Mfsd( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nLutNum < 0 )
                 goto usage;
             break;
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nCutSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nCutSize < 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;
+            }
+            pPars->nCutNum = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nCutNum < 0 )
+                goto usage;
+            break;
         case 'W':
             if ( globalUtilOptind >= argc )
             {
@@ -41118,10 +41140,12 @@ int Abc_CommandAbc9Mfsd( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &mfsd [-KSWFMC <num>] [-acvwh]\n" );
+    Abc_Print( -2, "usage: &mfsd [-KSNPWFMC <num>] [-acvwh]\n" );
     Abc_Print( -2, "\t           performs SAT-based delay-oriented AIG optimization\n" );
     Abc_Print( -2, "\t-K <num> : the LUT size for delay minimization (2 <= num <= 6) [default = %d]\n",         pPars->nLutSize );
     Abc_Print( -2, "\t-S <num> : the LUT structure size (1 <= num <= 2) [default = %d]\n",                      pPars->nLutNum );
+    Abc_Print( -2, "\t-N <num> : the cut size considered for optimization (2 <= num <= 10) [default = %d]\n",   pPars->nCutSize );
+    Abc_Print( -2, "\t-P <num> : the number of cuts computed at a node (1 <= num <= 500) [default = %d]\n",     pPars->nCutNum );
     Abc_Print( -2, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n",             pPars->nTfoLevels );
     Abc_Print( -2, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n",                pPars->nTfoFanMax );
     Abc_Print( -2, "\t-M <num> : the max node count of windows to consider (0 = no limit) [default = %d]\n",    pPars->nWinSizeMax );
diff --git a/src/opt/dau/dauGia.c b/src/opt/dau/dauGia.c
index 68375039..8b0a76c3 100644
--- a/src/opt/dau/dauGia.c
+++ b/src/opt/dau/dauGia.c
@@ -249,7 +249,7 @@ int Dau_DsdBalance( Gia_Man_t * pGia, int * pFans, int nFans, int fAnd )
             iFan = Abc_LitNotCond( iFan, fCompl );
         }
         else 
-            iFan = Gia_ManAppendXor( pGia, iFan0, iFan1 );
+            iFan = Gia_ManAppendXor2( pGia, iFan0, iFan1 );
     }
     else
     {
diff --git a/src/opt/sbd/sbd.h b/src/opt/sbd/sbd.h
index 6cdfafe4..6e0f6b3b 100644
--- a/src/opt/sbd/sbd.h
+++ b/src/opt/sbd/sbd.h
@@ -40,6 +40,8 @@ struct Sbd_Par_t_
 {
     int             nLutSize;     // target LUT size
     int             nLutNum;      // target LUT count
+    int             nCutSize;     // target cut size
+    int             nCutNum;      // target cut count
     int             nTfoLevels;   // the number of TFO levels (windowing)
     int             nTfoFanMax;   // the max number of fanouts (windowing)
     int             nWinSizeMax;  // maximum window size (windowing)
diff --git a/src/opt/sbd/sbdCore.c b/src/opt/sbd/sbdCore.c
index 0b399b8a..a48e6489 100644
--- a/src/opt/sbd/sbdCore.c
+++ b/src/opt/sbd/sbdCore.c
@@ -43,12 +43,14 @@ struct Sbd_Man_t_
     Vec_Int_t *     vCover;      // temporary
     Vec_Int_t *     vLits;       // temporary
     Vec_Int_t *     vLits2;      // temporary
-    int             nLuts[3];    // 0=const, 1=1lut, 2=2lut
+    int             nLuts[6];    // 0=const, 1=1lut, 2=2lut, 3=3lut
+    int             nTried;  
+    int             nUsed;  
     abctime         timeWin;
+    abctime         timeCut;
+    abctime         timeCov;
     abctime         timeCnf;
     abctime         timeSat;
-    abctime         timeCov;
-    abctime         timeEnu;
     abctime         timeQbf;
     abctime         timeOther;
     abctime         timeTotal;
@@ -76,8 +78,6 @@ static inline word * Sbd_ObjSim1( Sbd_Man_t * p, int i ) { return Vec_WrdEntryP(
 static inline word * Sbd_ObjSim2( Sbd_Man_t * p, int i ) { return Vec_WrdEntryP( p->vSims[2], p->pPars->nWords * i );         }
 static inline word * Sbd_ObjSim3( Sbd_Man_t * p, int i ) { return Vec_WrdEntryP( p->vSims[3], p->pPars->nWords * i );         }
 
-extern word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDivSet, Vec_Int_t * vDivVars, Vec_Int_t * vDivValues, Vec_Int_t * vTemp );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -96,17 +96,19 @@ extern word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_
 void Sbd_ParSetDefault( Sbd_Par_t * pPars )
 {
     memset( pPars, 0, sizeof(Sbd_Par_t) );
-    pPars->nLutSize     = 4;  // target LUT size
-    pPars->nLutNum      = 2;  // target LUT count
-    pPars->nTfoLevels   = 2;  // the number of TFO levels (windowing)
-    pPars->nTfoFanMax   = 4;  // the max number of fanouts (windowing)
-    pPars->nWinSizeMax  = 0;  // maximum window size (windowing)
-    pPars->nBTLimit     = 0;  // maximum number of SAT conflicts 
-    pPars->nWords       = 1;  // simulation word count
-    pPars->fArea        = 0;  // area-oriented optimization
-    pPars->fCover       = 0;  // use complete cover procedure
-    pPars->fVerbose     = 0;  // verbose flag
-    pPars->fVeryVerbose = 0;  // verbose flag
+    pPars->nLutSize     = 4;    // target LUT size
+    pPars->nLutNum      = 3;    // target LUT count
+    pPars->nCutSize     = (pPars->nLutSize - 1) * pPars->nLutNum + 1;  // target cut size
+    pPars->nCutNum      = 128;  // target cut count
+    pPars->nTfoLevels   = 5;    // the number of TFO levels (windowing)
+    pPars->nTfoFanMax   = 4;    // the max number of fanouts (windowing)
+    pPars->nWinSizeMax  = 2000; // maximum window size (windowing)
+    pPars->nBTLimit     = 0;    // maximum number of SAT conflicts 
+    pPars->nWords       = 1;    // simulation word count
+    pPars->fArea        = 0;    // area-oriented optimization
+    pPars->fCover       = 0;    // use complete cover procedure
+    pPars->fVerbose     = 0;    // verbose flag
+    pPars->fVeryVerbose = 0;    // verbose flag
 }
 
 /**Function*************************************************************
@@ -227,7 +229,7 @@ Sbd_Man_t * Sbd_ManStart( Gia_Man_t * pGia, Sbd_Par_t * pPars )
         for ( w = 0; w < p->pPars->nWords; w++ )
             Sbd_ObjSim0(p, Id)[w] = Gia_ManRandomW( 0 );     
     // cut enumeration
-    p->pSto = Sbd_StoAlloc( pGia, p->vMirrors, pPars->nLutSize, 2*pPars->nLutSize-1, 64, 1, 1 );
+    p->pSto = Sbd_StoAlloc( pGia, p->vMirrors, pPars->nLutSize, pPars->nCutSize, pPars->nCutNum, 1, 1 );
     return p;
 }
 void Sbd_ManStop( Sbd_Man_t * p )
@@ -437,6 +439,8 @@ int Sbd_ManWindow( Sbd_Man_t * p, int Pivot )
     Gia_ManIncrementTravId( p->pGia );
     Gia_ObjSetTravIdCurrentId(p->pGia, 0);
     Sbd_ManWindowSim_rec( p, Pivot );
+    if ( p->pPars->nWinSizeMax && Vec_IntSize(p->vWinObjs) > p->pPars->nWinSizeMax )
+        return 0;
     Sbd_ManUpdateOrder( p, Pivot );
     assert( Vec_IntSize(p->vDivVars) == Vec_IntSize(p->vDivValues) );
     assert( Vec_IntSize(p->vDivVars) < Vec_IntSize(p->vWinObjs) );
@@ -461,6 +465,8 @@ int Sbd_ManWindow( Sbd_Man_t * p, int Pivot )
         Vec_IntWriteEntry( p->vObj2Var, Abc_Lit2Var(Node), Vec_IntSize(p->vWinObjs) );
         Vec_IntPush( p->vWinObjs, Abc_Lit2Var(Node) );
     }
+    if ( p->pPars->nWinSizeMax && Vec_IntSize(p->vWinObjs) > p->pPars->nWinSizeMax )
+        return 0;
     // compute controlability for node
     if ( Vec_IntSize(p->vTfo) == 0 )
         Abc_TtFill( Sbd_ObjSim2(p, Pivot), p->pPars->nWords );
@@ -473,7 +479,7 @@ int Sbd_ManWindow( Sbd_Man_t * p, int Pivot )
     // propagate controlability to fanins for the TFI nodes starting from the pivot
     Sbd_ManPropagateControl( p, Pivot );
     assert( Vec_IntSize(p->vDivValues) <= 64 );
-    return (int)(Vec_IntSize(p->vDivValues) > 64);
+    return (int)(Vec_IntSize(p->vDivValues) <= 64);
 }
 
 /**Function*************************************************************
@@ -489,10 +495,6 @@ int Sbd_ManWindow( Sbd_Man_t * p, int Pivot )
 ***********************************************************************/
 int Sbd_ManCheckConst( Sbd_Man_t * p, int Pivot )
 {
-    extern int Sbd_ManCollectConstants( sat_solver * pSat, int nCareMints[2], int PivotVar, word * pVarSims[], Vec_Int_t * vInds );
-    extern sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots, int fQbf );
-    extern void Sbd_ManPrintObj( Sbd_Man_t * p, int Pivot );
-
     int nMintCount = 1;
     Vec_Ptr_t * vSims;
     word * pSims = Sbd_ObjSim0( p, Pivot );
@@ -984,7 +986,7 @@ static inline int Sbd_ManFindCands( Sbd_Man_t * p, word Cover[64], int nDivs )
 int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth )
 {
     int fVerbose = 0;
-    abctime clk, clkSat = 0, clkEnu = 0, clkAll = Abc_Clock();
+    abctime clk;
     int nIters, nItersMax = 32;
 
     word MatrS[64] = {0}, MatrC[2][64] = {{0}}, Cubes[2][2][64] = {{{0}}}, Cover[64] = {0}, Cube, CubeNew[2];
@@ -1089,14 +1091,10 @@ int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth )
         {
             if ( p->pPars->fVerbose )
                 printf( "Cannot find a feasible cover.\n" );
-            clkEnu += Abc_Clock() - clk;
-            clkAll = Abc_Clock() - clkAll - clkSat - clkEnu;
-            p->timeSat += clkSat;
-            p->timeCov += clkAll;
-            p->timeEnu += clkEnu;
+            p->timeCov += Abc_Clock() - clk;
             return RetValue;
         }
-        clkEnu += Abc_Clock() - clk;
+        p->timeCov += Abc_Clock() - clk;
     
         if ( p->pPars->fVerbose )
             printf( "Candidate support:  " ),
@@ -1104,7 +1102,7 @@ int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth )
 
         clk = Abc_Clock();
         *pTruth = Sbd_ManSolve( p->pSat, PivotVar, FreeVar+nIters, p->vDivSet, p->vDivVars, p->vDivValues, p->vLits );
-        clkSat += Abc_Clock() - clk;
+        p->timeSat += Abc_Clock() - clk;
 
         if ( *pTruth == SBD_SAT_UNDEC )
             printf( "Node %d:  Undecided.\n", Pivot );
@@ -1143,19 +1141,12 @@ int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth )
         }
         //break;
     }
-    //printf( "Node %4d : Iter = %4d  Start table = %4d  Final table = %4d\n", Pivot, nIters, nRowsOld, nRows );
-    clkAll = Abc_Clock() - clkAll - clkSat - clkEnu;
-    p->timeSat += clkSat;
-    p->timeCov += clkAll;
-    p->timeEnu += clkEnu;
     return RetValue;
 }
 
 int Sbd_ManExplore2( Sbd_Man_t * p, int Pivot, word * pTruth )
 {
-    extern sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots, int fQbf );
-    extern int Sbd_ManCollectConstantsNew( sat_solver * pSat, Vec_Int_t * vDivVars, int nConsts, int PivotVar, word * pOnset, word * pOffset );
-    abctime clk, clkSat = 0, clkEnu = 0, clkAll;
+    abctime clk;
     word Onset[64] = {0}, Offset[64] = {0}, Cube;
     word CoverRows[64] = {0}, CoverCols[64] = {0};
     int nIters, nItersMax = 32;
@@ -1171,12 +1162,11 @@ int Sbd_ManExplore2( Sbd_Man_t * p, int Pivot, word * pTruth )
     //sat_solver_delete_p( &p->pSat );
     p->pSat = Sbd_ManSatSolver( p->pSat, p->pGia, p->vMirrors, Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots, 0 );
     p->timeCnf += Abc_Clock() - clk;
-    clkAll = Abc_Clock();
 
     assert( nConsts <= 8 );
     clk = Abc_Clock();
     RetValue = Sbd_ManCollectConstantsNew( p->pSat, p->vDivVars, nConsts, PivotVar, Onset, Offset );
-    clkSat += Abc_Clock() - clk;
+    p->timeSat += Abc_Clock() - clk;
     if ( RetValue >= 0 )
     {
         if ( p->pPars->fVeryVerbose )
@@ -1215,21 +1205,18 @@ int Sbd_ManExplore2( Sbd_Man_t * p, int Pivot, word * pTruth )
         {
             if ( p->pPars->fVeryVerbose )
                 printf( "Cannot find a feasible cover.\n" );
-            clkEnu += Abc_Clock() - clk;
-            clkAll = Abc_Clock() - clkAll - clkSat - clkEnu;
-            p->timeSat += clkSat;
-            p->timeCov += clkAll;
-            p->timeEnu += clkEnu;
+            p->timeCov += Abc_Clock() - clk;
             return 0;
         }
-    
+        p->timeCov += Abc_Clock() - clk;
+
         if ( p->pPars->fVeryVerbose )
             printf( "Candidate support:  " ),
             Vec_IntPrint( p->vDivSet );
 
         clk = Abc_Clock();
         *pTruth = Sbd_ManSolve( p->pSat, PivotVar, FreeVar+nIters, p->vDivSet, p->vDivVars, p->vDivValues, p->vLits );
-        clkSat += Abc_Clock() - clk;
+        p->timeSat += Abc_Clock() - clk;
 
         if ( *pTruth == SBD_SAT_UNDEC )
             printf( "Node %d:  Undecided.\n", Pivot );
@@ -1271,65 +1258,42 @@ int Sbd_ManExplore2( Sbd_Man_t * p, int Pivot, word * pTruth )
             break;
         }
     }
-    clkAll = Abc_Clock() - clkAll - clkSat - clkEnu;
-    p->timeSat += clkSat;
-    p->timeCov += clkAll;
-    p->timeEnu += clkEnu;
     return RetValue;
 }
 
-int Sbd_ManExplore3( Sbd_Man_t * p, int Pivot, int * pnStrs, Sbd_Str_t * Strs )
+int Sbd_ManExploreCut( Sbd_Man_t * p, int Pivot, int nLeaves, int * pLeaves, int * pnStrs, Sbd_Str_t * Strs, int * pFreeVar )
 {
-    extern int Sbd_ProblemSolve( 
-                                   Gia_Man_t * p, Vec_Int_t * vMirrors, 
-                                   int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, 
-                                   Vec_Int_t * vTfo, Vec_Int_t * vRoots, 
-                                   Vec_Int_t * vDivSet, int nStrs, Sbd_Str_t * pStr0 
-                               );
-    extern sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots, int fQbf );
-    extern int Sbd_ManCollectConstantsNew( sat_solver * pSat, Vec_Int_t * vDivVars, int nConsts, int PivotVar, word * pOnset, word * pOffset );
     abctime clk = Abc_Clock();
-    word Truth;
-
     int PivotVar = Vec_IntEntry(p->vObj2Var, Pivot);
-    int FreeVar = Vec_IntSize(p->vWinObjs) + Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots);
-    //int nDivs = Vec_IntSize( p->vDivVars );
     int Delay = Vec_IntEntry( p->vLutLevs, Pivot );
-    int i, k, iObj, nIters, RetValue;
+    int pNodesTop[SBD_DIV_MAX], pNodesBot[SBD_DIV_MAX], pNodesBot1[SBD_DIV_MAX], pNodesBot2[SBD_DIV_MAX];
+    int nNodesTop = 0, nNodesBot = 0, nNodesBot1 = 0, nNodesBot2 = 0, nNodesDiff = 0, nNodesDiff1 = 0, nNodesDiff2 = 0;
+    int i, k, iObj, nIters, RetValue = 0;
 
-    int nLeaves, pLeaves[SBD_DIV_MAX];
-
-    int pNodesTop[SBD_DIV_MAX], pNodesBot[SBD_DIV_MAX];//, pNodeRefs[SBD_DIV_MAX];
-    int nNodesTop = 0, nNodesBot = 0, nNodesDiff = 0;
-
-    //sat_solver_delete_p( &p->pSat );
-    p->pSat = Sbd_ManSatSolver( p->pSat, p->pGia, p->vMirrors, Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots, 0 );
-    p->timeCnf += Abc_Clock() - clk;
-
-    // extract one cut
-    nLeaves = Sbd_StoObjBestCut( p->pSto, Pivot, pLeaves );
-    if ( nLeaves == -1 )
-        return 0;
-
-    // solve the covering problem
+    // try to remove fanins
     for ( nIters = 0; nIters < nLeaves; nIters++ )
     {
+        word Truth;
         // try to remove one variable from divisors
         Vec_IntClear( p->vDivSet );
         for ( i = 0; i < nLeaves; i++ )
-            if ( i != nIters && pLeaves[i] != -1 )
+            if ( i != nLeaves-1-nIters && pLeaves[i] != -1 )
                 Vec_IntPush( p->vDivSet, Vec_IntEntry(p->vObj2Var, pLeaves[i]) );
         assert( Vec_IntSize(p->vDivSet) < nLeaves );
         // compute truth table
         clk = Abc_Clock();
-        Truth = Sbd_ManSolve( p->pSat, PivotVar, FreeVar+nIters, p->vDivSet, p->vDivVars, p->vDivValues, p->vLits );
+        Truth = Sbd_ManSolve( p->pSat, PivotVar, (*pFreeVar)++, p->vDivSet, p->vDivVars, p->vDivValues, p->vLits );
         p->timeSat += Abc_Clock() - clk;
         if ( Truth == SBD_SAT_UNDEC )
             printf( "Node %d:  Undecided.\n", Pivot );
         else if ( Truth == SBD_SAT_SAT )
-            continue;
+        {
+            int DelayDiff = Vec_IntEntry(p->vLutLevs, pLeaves[nLeaves-1-nIters]) - Delay;
+            if ( DelayDiff > -2 )
+                return 0;
+        }
         else
-            pLeaves[nIters] = -1;
+            pLeaves[nLeaves-1-nIters] = -1;
     }
     Vec_IntClear( p->vDivSet );
     for ( i = 0; i < nLeaves; i++ )
@@ -1338,13 +1302,14 @@ int Sbd_ManExplore3( Sbd_Man_t * p, int Pivot, int * pnStrs, Sbd_Str_t * Strs )
     //printf( "Reduced %d -> %d\n", nLeaves, Vec_IntSize(p->vDivSet) );
     if ( Vec_IntSize(p->vDivSet) <= p->pPars->nLutSize )
     {
+        word Truth;
         *pnStrs = 1;
         // remap divisors
         Vec_IntForEachEntry( p->vDivSet, iObj, i )
             Vec_IntWriteEntry( p->vDivSet, i, Vec_IntEntry(p->vObj2Var, iObj) );
         // compute truth table
         clk = Abc_Clock();
-        Truth = Sbd_ManSolve( p->pSat, PivotVar, FreeVar+nIters, p->vDivSet, p->vDivVars, p->vDivValues, p->vLits );
+        Truth = Sbd_ManSolve( p->pSat, PivotVar, (*pFreeVar)++, p->vDivSet, p->vDivVars, p->vDivValues, p->vLits );
         p->timeSat += Abc_Clock() - clk;
         assert( Truth != SBD_SAT_UNDEC && Truth != SBD_SAT_SAT );
         // create structure
@@ -1360,7 +1325,7 @@ int Sbd_ManExplore3( Sbd_Man_t * p, int Pivot, int * pnStrs, Sbd_Str_t * Strs )
     assert( Vec_IntSize(p->vDivSet) > p->pPars->nLutSize );
 
     // count number of nodes on each level
-    nNodesTop = 0, nNodesBot = 0;
+    nNodesTop = nNodesBot = nNodesBot1 = nNodesBot2 = 0;
     Vec_IntForEachEntry( p->vDivSet, iObj, i )
     {
         int DelayDiff = Vec_IntEntry(p->vLutLevs, iObj) - Delay;
@@ -1369,60 +1334,227 @@ int Sbd_ManExplore3( Sbd_Man_t * p, int Pivot, int * pnStrs, Sbd_Str_t * Strs )
         if ( DelayDiff == -2 )
             pNodesTop[nNodesTop++] = i;
         else // if ( DelayDiff < -2 )
+        {
             pNodesBot[nNodesBot++] = i;
+            if ( DelayDiff == -3 )
+                pNodesBot1[nNodesBot1++] = i;
+            else // if ( DelayDiff < -3 )
+                pNodesBot2[nNodesBot2++] = i;
+        }
         Vec_IntWriteEntry( p->vDivSet, i, Vec_IntEntry(p->vObj2Var, iObj) );
-        //pNodeRefs[i] = Gia_ObjRefNumId( p->pGia, iObj );
     }
+    assert( nNodesBot == nNodesBot1 + nNodesBot2 );
     if ( i < Vec_IntSize(p->vDivSet) )
         return 0;
     if ( nNodesTop > p->pPars->nLutSize-1 )
         return 0;
-    if ( nNodesBot > p->pPars->nLutSize )
+
+    // try 44
+    if ( Vec_IntSize(p->vDivSet) <= 2*p->pPars->nLutSize-1 )
     {
-        // move left-over to the top
-        while ( nNodesBot > p->pPars->nLutSize )
-            pNodesTop[nNodesTop++] = pNodesBot[--nNodesBot];
-        assert( nNodesBot == p->pPars->nLutSize );
+        int nMoved = 0;
+        if ( nNodesBot > p->pPars->nLutSize ) // need to move bottom left-over to the top
+        {
+            while ( nNodesBot > p->pPars->nLutSize )
+                pNodesTop[nNodesTop++] = pNodesBot[--nNodesBot], nMoved++;
+            assert( nNodesBot == p->pPars->nLutSize );
+        }
+        assert( nNodesBot <= p->pPars->nLutSize );
         assert( nNodesTop <= p->pPars->nLutSize-1 );
-    }
-    nNodesDiff = p->pPars->nLutSize-1 - nNodesTop;
-    
-    // number of structures
-    *pnStrs = 2 + nNodesDiff;
-
-    Strs[0].fLut = 1;
-    Strs[0].nVarIns = p->pPars->nLutSize;
-    for ( i = 0; i < nNodesTop; i++ )
-        Strs[0].VarIns[i] = pNodesTop[i];
-    for ( ; i < p->pPars->nLutSize; i++ )
-        Strs[0].VarIns[i] = Vec_IntSize(p->vDivSet)+1 + i-nNodesTop;
-    Strs[0].Res = 0;
-
-    Strs[1].fLut = 1;
-    Strs[1].nVarIns = nNodesBot;
-    for ( i = 0; i < nNodesBot; i++ )
-        Strs[1].VarIns[i] = pNodesBot[i];
-    Strs[1].Res = 0;
-
-    for ( k = 0; k < nNodesDiff; k++ )
-    {
-        Strs[2+k].fLut = 0;
-        Strs[2+k].nVarIns = nNodesBot;
+
+        Strs[0].fLut = 1;
+        Strs[0].nVarIns = p->pPars->nLutSize;
+        for ( i = 0; i < nNodesTop; i++ )
+            Strs[0].VarIns[i] = pNodesTop[i];
+        for ( ; i < p->pPars->nLutSize; i++ )
+            Strs[0].VarIns[i] = Vec_IntSize(p->vDivSet)+1 + i-nNodesTop;
+        Strs[0].Res = 0;
+
+        Strs[1].fLut = 1;
+        Strs[1].nVarIns = nNodesBot;
         for ( i = 0; i < nNodesBot; i++ )
-            Strs[2+k].VarIns[i] = pNodesBot[i];
-        Strs[2+k].Res = 0;
+            Strs[1].VarIns[i] = pNodesBot[i];
+        Strs[1].Res = 0;
+
+        nNodesDiff = p->pPars->nLutSize-1 - nNodesTop;
+        assert( nNodesDiff >= 0 && nNodesDiff <= 3 );
+        for ( k = 0; k < nNodesDiff; k++ )
+        {
+            Strs[2+k].fLut = 0;
+            Strs[2+k].nVarIns = nNodesBot;
+            for ( i = 0; i < nNodesBot; i++ )
+                Strs[2+k].VarIns[i] = pNodesBot[i];
+            Strs[2+k].Res = 0;
+        }
+
+        *pnStrs = 2 + nNodesDiff;
+        clk = Abc_Clock();
+        RetValue = Sbd_ProblemSolve( p->pGia, p->vMirrors,   Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots,   p->vDivSet, *pnStrs, Strs );
+        p->timeQbf += Abc_Clock() - clk;
+        if ( RetValue ) 
+            p->nLuts[2]++;
+
+        while ( nMoved-- )
+            pNodesBot[nNodesBot++] = pNodesTop[--nNodesTop];
     }
 
-    clk = Abc_Clock();
-    RetValue = Sbd_ProblemSolve( p->pGia, p->vMirrors, 
-                                 Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots,
-                                 p->vDivSet, *pnStrs, Strs );
-    p->timeQbf += Abc_Clock() - clk;
+    if ( RetValue )
+        return RetValue;
+    if ( p->pPars->nLutNum < 3 )
+        return 0;
+    if ( Vec_IntSize(p->vDivSet) < 2*p->pPars->nLutSize-1 )
+        return 0;
+
+    // try 444 -- LUT(LUT, LUT)
+    if ( nNodesTop <= p->pPars->nLutSize-2 )
+    {
+        int nMoved = 0;
+        if ( nNodesBot > 2*p->pPars->nLutSize ) // need to move bottom left-over to the top
+        {
+            while ( nNodesBot > 2*p->pPars->nLutSize )
+                pNodesTop[nNodesTop++] = pNodesBot[--nNodesBot], nMoved++;
+            assert( nNodesBot == 2*p->pPars->nLutSize );
+        }
+        assert( nNodesBot > p->pPars->nLutSize );
+        assert( nNodesBot <= 2*p->pPars->nLutSize );
+        assert( nNodesTop <= p->pPars->nLutSize-2 );
+
+        Strs[0].fLut = 1;
+        Strs[0].nVarIns = p->pPars->nLutSize;
+        for ( i = 0; i < nNodesTop; i++ )
+            Strs[0].VarIns[i] = pNodesTop[i];
+        for ( ; i < p->pPars->nLutSize; i++ )
+            Strs[0].VarIns[i] = Vec_IntSize(p->vDivSet)+1 + i-nNodesTop;
+        Strs[0].Res = 0;
+
+        Strs[1].fLut = 1;
+        Strs[1].nVarIns = p->pPars->nLutSize;
+        for ( i = 0; i < Strs[1].nVarIns; i++ )
+            Strs[1].VarIns[i] = pNodesBot[i];
+        Strs[1].Res = 0;
+
+        Strs[2].fLut = 1;
+        Strs[2].nVarIns = p->pPars->nLutSize;
+        for ( i = 0; i < Strs[2].nVarIns; i++ )
+            Strs[2].VarIns[i] = pNodesBot[nNodesBot-p->pPars->nLutSize+i];
+        Strs[2].Res = 0;
+
+        nNodesDiff = p->pPars->nLutSize-2 - nNodesTop;
+        assert( nNodesDiff >= 0 && nNodesDiff <= 2 );
+        for ( k = 0; k < nNodesDiff; k++ )
+        {
+            Strs[3+k].fLut = 0;
+            Strs[3+k].nVarIns = nNodesBot;
+            for ( i = 0; i < nNodesBot; i++ )
+                Strs[3+k].VarIns[i] = pNodesBot[i];
+            Strs[3+k].Res = 0;
+        }
+
+        *pnStrs = 3 + nNodesDiff;
+        clk = Abc_Clock();
+        RetValue = Sbd_ProblemSolve( p->pGia, p->vMirrors,   Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots,   p->vDivSet, *pnStrs, Strs );
+        p->timeQbf += Abc_Clock() - clk;
+        if ( RetValue ) 
+            p->nLuts[3]++;
+
+        while ( nMoved-- )
+            pNodesBot[nNodesBot++] = pNodesTop[--nNodesTop];
+    }
+    if ( RetValue )
+        return RetValue;
+
+    // try 444 -- LUT(LUT(LUT))
+    if ( nNodesBot1 + nNodesTop <= 2*p->pPars->nLutSize-2 )
+    {
+        if ( nNodesBot2 > p->pPars->nLutSize ) // need to move bottom left-over to the top
+        {
+            while ( nNodesBot2 > p->pPars->nLutSize )
+                pNodesBot1[nNodesBot1++] = pNodesBot2[--nNodesBot2];
+            assert( nNodesBot2 == p->pPars->nLutSize );
+        }
+        if ( nNodesBot1 > p->pPars->nLutSize-1 ) // need to move bottom left-over to the top
+        {
+            while ( nNodesBot1 > p->pPars->nLutSize-1 )
+                pNodesTop[nNodesTop++] = pNodesBot1[--nNodesBot1];
+            assert( nNodesBot1 == p->pPars->nLutSize-1 );
+        }
+        assert( nNodesBot2 <= p->pPars->nLutSize );
+        assert( nNodesBot1 <= p->pPars->nLutSize-1 );
+        assert( nNodesTop <= p->pPars->nLutSize-1 );
+
+        Strs[0].fLut = 1;
+        Strs[0].nVarIns = p->pPars->nLutSize;
+        for ( i = 0; i < nNodesTop; i++ )
+            Strs[0].VarIns[i] = pNodesTop[i];
+        Strs[0].VarIns[i++] = Vec_IntSize(p->vDivSet)+1;
+        for ( ; i < p->pPars->nLutSize; i++ )
+            Strs[0].VarIns[i] = Vec_IntSize(p->vDivSet)+2 + i-nNodesTop;
+        Strs[0].Res = 0;
+        nNodesDiff1 = p->pPars->nLutSize-1 - nNodesTop;
+
+        Strs[1].fLut = 1;
+        Strs[1].nVarIns = p->pPars->nLutSize;
+        for ( i = 0; i < nNodesBot1; i++ )
+            Strs[1].VarIns[i] = pNodesBot1[i];
+        Strs[1].VarIns[i++] = Vec_IntSize(p->vDivSet)+2;
+        for ( ; i < p->pPars->nLutSize; i++ )
+            Strs[1].VarIns[i] = Vec_IntSize(p->vDivSet)+2+nNodesDiff1 + i-nNodesBot1;
+        Strs[1].Res = 0;
+        nNodesDiff2 = p->pPars->nLutSize-1 - nNodesBot1;
+
+        Strs[2].fLut = 1;
+        Strs[2].nVarIns = nNodesBot2;
+        for ( i = 0; i < Strs[2].nVarIns; i++ )
+            Strs[2].VarIns[i] = pNodesBot2[i];
+        Strs[2].Res = 0;
+
+        nNodesDiff = nNodesDiff1 + nNodesDiff2;
+        assert( nNodesDiff >= 0 && nNodesDiff <= 3 );
+        for ( k = 0; k < nNodesDiff; k++ )
+        {
+            Strs[3+k].fLut = 0;
+            Strs[3+k].nVarIns = nNodesBot2;
+            for ( i = 0; i < nNodesBot2; i++ )
+                Strs[3+k].VarIns[i] = pNodesBot2[i];
+            Strs[3+k].Res = 0;
+            if ( k >= nNodesDiff1 )
+                continue;
+            Strs[3+k].nVarIns += nNodesBot1;
+            for ( i = 0; i < nNodesBot1; i++ )
+                Strs[3+k].VarIns[nNodesBot2 + i] = pNodesBot1[i];
+        }
 
-    if ( RetValue ) 
-        p->nLuts[2]++;
+        *pnStrs = 3 + nNodesDiff;
+        clk = Abc_Clock();
+        RetValue = Sbd_ProblemSolve( p->pGia, p->vMirrors,   Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots,   p->vDivSet, *pnStrs, Strs );
+        p->timeQbf += Abc_Clock() - clk;
+        if ( RetValue ) 
+            p->nLuts[4]++;
+    }
     return RetValue;
 }
+int Sbd_ManExplore3( Sbd_Man_t * p, int Pivot, int * pnStrs, Sbd_Str_t * Strs )
+{
+    int FreeVar = Vec_IntSize(p->vWinObjs) + Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots);
+    int FreeVarStart = FreeVar;
+    int nSize, nLeaves, pLeaves[SBD_DIV_MAX];
+    //sat_solver_delete_p( &p->pSat );
+    abctime clk = Abc_Clock();
+    p->pSat = Sbd_ManSatSolver( p->pSat, p->pGia, p->vMirrors, Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots, 0 );
+    p->timeCnf += Abc_Clock() - clk;
+    // extract one cut
+    for ( nSize = p->pPars->nLutSize + 1; nSize <= p->pPars->nCutSize; nSize++ )
+    {
+        nLeaves = Sbd_StoObjBestCut( p->pSto, Pivot, nSize, pLeaves );
+        if ( nLeaves == -1 )
+            continue;
+        assert( nLeaves == nSize );
+        if ( Sbd_ManExploreCut( p, Pivot, nLeaves, pLeaves, pnStrs, Strs, &FreeVar ) )
+            return 1;
+    }
+    assert( FreeVar - FreeVarStart <= SBD_FVAR_MAX ); 
+    return 0;
+}
 
 
 /**Function*************************************************************
@@ -1722,7 +1854,10 @@ int Sbd_ManImplement2( Sbd_Man_t * p, int Pivot, int nStrs, Sbd_Str_t * pStrs )
     // extend data-structure to accommodate new nodes
     assert( Vec_IntSize(p->vLutLevs) == iObjLast );
     for ( i = iObjLast; i < Gia_ManObjNum(p->pGia); i++ )
+    {
+        Vec_IntPush( p->vMirrors, -1 );
         Sbd_StoRefObj( p->pSto, i, i == Gia_ManObjNum(p->pGia)-1 ? Pivot : -1 );
+    }
     Sbd_StoDerefObj( p->pSto, Pivot );
     for ( i = iObjLast; i < Gia_ManObjNum(p->pGia); i++ )
     {
@@ -1730,7 +1865,6 @@ int Sbd_ManImplement2( Sbd_Man_t * p, int Pivot, int nStrs, Sbd_Str_t * pStrs )
         assert( i == Vec_IntSize(p->vLutLevs) );
         Vec_IntPush( p->vLutLevs, Delay );
         Vec_IntPush( p->vObj2Var, 0 );
-        Vec_IntPush( p->vMirrors, -1 );
         Vec_IntFillExtra( p->vLutCuts, Vec_IntSize(p->vLutCuts) + p->pPars->nLutSize + 1, 0 );
         //Sbd_ManFindCut( p, i, p->vLits );
         for ( k = 0; k < 4; k++ )
@@ -1820,22 +1954,16 @@ Gia_Man_t * Sbd_ManDerive( Gia_Man_t * p, Vec_Int_t * vMirrors )
 ***********************************************************************/
 void Sbd_NtkPerformOne( Sbd_Man_t * p, int Pivot )
 {
-    Sbd_Str_t Strs[4];
-    int i, RetValue, nStrs = 0;
-    word Truth = 0;
-
-    if ( !p->pSto )
-    {
-        if ( Sbd_ManMergeCuts( p, Pivot ) )
-            return;
-    }
-
-//    if ( Pivot != 15 )
-//        return;
-
-    if ( Sbd_ManWindow( p, Pivot ) )
+    Sbd_Str_t Strs[SBD_DIV_MAX]; word Truth = 0;
+    int RetValue, nStrs = 0;
+    if ( !p->pSto && Sbd_ManMergeCuts( p, Pivot ) )
         return;
-
+    if ( !Sbd_ManWindow( p, Pivot ) )
+        return;
+    //if ( Vec_IntSize(p->vWinObjs) > 100 )
+    //    printf( "Obj %d : Win = %d   TFO = %d.  Roots = %d.\n", Pivot, Vec_IntSize(p->vWinObjs), Vec_IntSize(p->vTfo), Vec_IntSize(p->vRoots) );
+    p->nTried++;
+    p->nUsed++;
     RetValue = Sbd_ManCheckConst( p, Pivot );
     if ( RetValue >= 0 )
     {
@@ -1844,6 +1972,7 @@ void Sbd_NtkPerformOne( Sbd_Man_t * p, int Pivot )
     }
     else if ( p->pPars->nLutNum >= 1 && Sbd_ManExplore2( p, Pivot, &Truth ) )
     {
+        int i;
         Strs->fLut = 1;
         Strs->nVarIns = Vec_IntSize( p->vDivSet );
         for ( i = 0; i < Strs->nVarIns; i++ )
@@ -1855,8 +1984,17 @@ void Sbd_NtkPerformOne( Sbd_Man_t * p, int Pivot )
     else if ( p->pPars->nLutNum >= 2 && Sbd_ManExplore3( p, Pivot, &nStrs, Strs ) )
     {
         Sbd_ManImplement2( p, Pivot, nStrs, Strs );
-        if ( p->pPars->fVerbose ) printf( "Node %5d:  Detected %d%d\n", Pivot, p->pPars->nLutSize, p->pPars->nLutSize );
+        if ( !p->pPars->fVerbose ) 
+            return;
+        if ( Vec_IntSize(p->vDivSet) <= 4 )
+            printf( "Node %5d:  Detected %d\n", Pivot, p->pPars->nLutSize );
+        else if ( Vec_IntSize(p->vDivSet) <= 6 || (Vec_IntSize(p->vDivSet) == 7 && nStrs == 2) )
+            printf( "Node %5d:  Detected %d%d\n", Pivot, p->pPars->nLutSize, p->pPars->nLutSize );
+        else 
+            printf( "Node %5d:  Detected %d%d%d\n", Pivot, p->pPars->nLutSize, p->pPars->nLutSize, p->pPars->nLutSize );
     }
+    else
+        p->nUsed--;
 }
 Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
 {
@@ -1875,6 +2013,7 @@ Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
         Vec_Int_t * vNodes = Gia_ManOrderWithBoxes( pGia );
         Tim_Man_t * pTimOld = (Tim_Man_t *)pGia->pManTime;
         pGia->pManTime = Tim_ManDup( pTimOld, 1 );
+        //Tim_ManPrint( pGia->pManTime );
         Tim_ManIncrementTravId( (Tim_Man_t *)pGia->pManTime );
         Gia_ManForEachObjVec( vNodes, pGia, pObj, k )
         {
@@ -1883,9 +2022,11 @@ Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
                 break;
             if ( Gia_ObjIsAnd(pObj) )
             {
+                abctime clk = Abc_Clock();
                 int Delay = Sbd_StoComputeCutsNode( p->pSto, Pivot );
+                p->timeCut += Abc_Clock() - clk;
                 Vec_IntWriteEntry( p->vLutLevs, Pivot, Delay );
-                if ( Delay > 1 )
+                if ( Delay > 1 )//&& Gia_ObjRefNumId(p->pGia, Pivot) > 1 )
                     Sbd_NtkPerformOne( p, Pivot );
             }
             else if ( Gia_ObjIsCi(pObj) )
@@ -1903,7 +2044,6 @@ Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
                 Sbd_StoComputeCutsConst0( p->pSto, 0 );
             else assert( 0 );
         }
-        //Tim_ManPrint( pGia->pManTime );
         Tim_ManStop( (Tim_Man_t *)pGia->pManTime );
         pGia->pManTime = pTimOld;
         Vec_IntFree( vNodes );
@@ -1919,29 +2059,33 @@ Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
                 Sbd_StoComputeCutsCi( p->pSto, Pivot, 0, 0 );
             else if ( Gia_ObjIsAnd(pObj) )
             {
+                abctime clk = Abc_Clock();
                 int Delay = Sbd_StoComputeCutsNode( p->pSto, Pivot );
+                p->timeCut += Abc_Clock() - clk;
                 Vec_IntWriteEntry( p->vLutLevs, Pivot, Delay );
-                if ( Delay > 1 )
+                if ( Delay > 1 )//&& Gia_ObjRefNumId(p->pGia, Pivot) > 1 )
                     Sbd_NtkPerformOne( p, Pivot );
             }
             //if ( nNodesOld != Gia_ManObjNum(pGia) )
             //    break;
         }
     }
-    printf( "Found %d constants, %d one-LUT and %d two-LUT replacements with delay %d.  ", 
-        p->nLuts[0], p->nLuts[1], p->nLuts[2], Sbd_ManDelay(p) );
+    printf( "K = %d. S = %d. N = %d. P = %d.  ", 
+        p->pPars->nLutSize, p->pPars->nLutNum, p->pPars->nCutSize, p->pPars->nCutNum );
+    printf( "Try = %d. Use = %d.  C = %d. 1 = %d. 2 = %d. 3a = %d. 3b = %d.  Lev = %d.  ", 
+        p->nTried, p->nUsed, p->nLuts[0], p->nLuts[1], p->nLuts[2], p->nLuts[3], p->nLuts[4], Sbd_ManDelay(p) );
     p->timeTotal = Abc_Clock() - p->timeTotal;
     Abc_PrintTime( 1, "Time", p->timeTotal );
     pNew = Sbd_ManDerive( pGia, p->vMirrors );
     // print runtime statistics
-    p->timeOther = p->timeTotal - p->timeWin - p->timeCnf - p->timeSat - p->timeCov - p->timeEnu - p->timeQbf;
-    if ( p->pPars->fVerbose )
+    p->timeOther = p->timeTotal - p->timeWin - p->timeCut - p->timeCov - p->timeCnf - p->timeSat - p->timeQbf;
+    //if ( p->pPars->fVerbose )
     {
         ABC_PRTP( "Win", p->timeWin  ,  p->timeTotal );
+        ABC_PRTP( "Cut", p->timeCut  ,  p->timeTotal );
+        ABC_PRTP( "Cov", p->timeCov  ,  p->timeTotal );
         ABC_PRTP( "Cnf", p->timeCnf  ,  p->timeTotal );
         ABC_PRTP( "Sat", p->timeSat  ,  p->timeTotal );
-        ABC_PRTP( "Cov", p->timeCov  ,  p->timeTotal );
-        ABC_PRTP( "Enu", p->timeEnu  ,  p->timeTotal );
         ABC_PRTP( "Qbf", p->timeQbf  ,  p->timeTotal );
         ABC_PRTP( "Oth", p->timeOther,  p->timeTotal );
         ABC_PRTP( "ALL", p->timeTotal,  p->timeTotal );
diff --git a/src/opt/sbd/sbdCut.c b/src/opt/sbd/sbdCut.c
index 9c54c74a..7bcf2189 100644
--- a/src/opt/sbd/sbdCut.c
+++ b/src/opt/sbd/sbdCut.c
@@ -27,9 +27,9 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-#define SBD_MAX_CUTSIZE   8
-#define SBD_MAX_CUTNUM    1001
-#define SBD_MAX_TT_WORDS  ((SBD_MAX_CUTSIZE > 6) ? 1 << (SBD_MAX_CUTSIZE-6) : 1)
+#define SBD_MAX_CUTSIZE    10
+#define SBD_MAX_CUTNUM     501
+#define SBD_MAX_TT_WORDS   ((SBD_MAX_CUTSIZE > 6) ? 1 << (SBD_MAX_CUTSIZE-6) : 1)
 
 #define SBD_CUT_NO_LEAF   0xF
 
@@ -568,6 +568,7 @@ static inline void Sbd_CutPrint( Sbd_Sto_t * p, int iObj, Sbd_Cut_t * pCut )
 {
     int i, nDigits = Abc_Base10Log(Gia_ManObjNum(p->pGia)); 
     int Delay = Vec_IntEntry(p->vDelays, iObj);
+    if ( pCut == NULL ) { printf( "No cut.\n" ); return; }
     printf( "%d  {", pCut->nLeaves );
     for ( i = 0; i < (int)pCut->nLeaves; i++ )
         printf( " %*d", nDigits, pCut->pLeaves[i] );
@@ -724,45 +725,88 @@ int Sbd_StoComputeCutsNode( Sbd_Sto_t * p, int iObj )
     Sbd_StoMergeCuts( p, iObj );
     return Vec_IntEntry( p->vDelays, iObj );
 }
+int Sbd_StoObjRefs( Sbd_Sto_t * p, int iObj )
+{
+    return Vec_IntEntry(p->vRefs, iObj);
+}
 void Sbd_StoRefObj( Sbd_Sto_t * p, int iObj, int iMirror )
 {
     Gia_Obj_t * pObj = Gia_ManObj(p->pGia, iObj);
     assert( iObj == Vec_IntSize(p->vRefs) );
     assert( iMirror < iObj );
-    Vec_IntPush( p->vRefs, iMirror > 0 ? Vec_IntEntry(p->vRefs, iMirror) : 0 );
+    Vec_IntPush( p->vRefs, 0 );
+//printf( "Ref %d\n", iObj );
+    if ( iMirror > 0 )
+    {
+        Vec_IntWriteEntry( p->vRefs, iObj, Vec_IntEntry(p->vRefs, iMirror) );
+        Vec_IntWriteEntry( p->vRefs, iMirror, 1 );
+    }
     if ( Gia_ObjIsAnd(pObj) )
     {
-        Vec_IntAddToEntry( p->vRefs, Gia_ObjFaninId0(pObj, iObj), 1 );
-        Vec_IntAddToEntry( p->vRefs, Gia_ObjFaninId1(pObj, iObj), 1 );
+        int Lit0m = Vec_IntEntry( p->vMirrors, Gia_ObjFaninId0(pObj, iObj) );
+        int Lit1m = Vec_IntEntry( p->vMirrors, Gia_ObjFaninId1(pObj, iObj) );
+        int Fan0 = Lit0m >= 0 ? Abc_Lit2Var(Lit0m) : Gia_ObjFaninId0(pObj, iObj);
+        int Fan1 = Lit1m >= 0 ? Abc_Lit2Var(Lit1m) : Gia_ObjFaninId1(pObj, iObj);
+        Vec_IntAddToEntry( p->vRefs, Fan0, 1 );
+        Vec_IntAddToEntry( p->vRefs, Fan1, 1 );
     }
     else if ( Gia_ObjIsCo(pObj) )
+    {
+        int Lit0m = Vec_IntEntry( p->vMirrors, Gia_ObjFaninId0(pObj, iObj) );
+        assert( Lit0m == -1 );
         Vec_IntAddToEntry( p->vRefs, Gia_ObjFaninId0(pObj, iObj), 1 );
+    }
 }
 void Sbd_StoDerefObj( Sbd_Sto_t * p, int iObj )
 {
-    Gia_Obj_t * pObj = Gia_ManObj(p->pGia, iObj);
+    Gia_Obj_t * pObj;
+    int Lit0m, Lit1m, Fan0, Fan1;
+    return;
+
+    pObj = Gia_ManObj(p->pGia, iObj);
+    if ( Vec_IntEntry(p->vRefs, iObj) == 0 )
+        printf( "Ref count mismatch at node %d\n", iObj );
+    assert( Vec_IntEntry(p->vRefs, iObj) > 0 );
     Vec_IntAddToEntry( p->vRefs, iObj, -1 );
     if ( Vec_IntEntry( p->vRefs, iObj ) > 0 )
         return;
     if ( Gia_ObjIsCi(pObj) )
         return;
+//printf( "Deref %d\n", iObj );
     assert( Gia_ObjIsAnd(pObj) );
-    Sbd_StoDerefObj( p, Gia_ObjFaninId0(pObj, iObj) );
-    Sbd_StoDerefObj( p, Gia_ObjFaninId1(pObj, iObj) );
+    Lit0m = Vec_IntEntry( p->vMirrors, Gia_ObjFaninId0(pObj, iObj) );
+    Lit1m = Vec_IntEntry( p->vMirrors, Gia_ObjFaninId1(pObj, iObj) );
+    Fan0 = Lit0m >= 0 ? Abc_Lit2Var(Lit0m) : Gia_ObjFaninId0(pObj, iObj);
+    Fan1 = Lit1m >= 0 ? Abc_Lit2Var(Lit1m) : Gia_ObjFaninId1(pObj, iObj);
+    if ( Fan0 ) Sbd_StoDerefObj( p, Fan0 );
+    if ( Fan1 ) Sbd_StoDerefObj( p, Fan1 );
 }
-int Sbd_StoObjBestCut( Sbd_Sto_t * p, int iObj, int * pLeaves )
+int Sbd_StoObjBestCut( Sbd_Sto_t * p, int iObj, int nSize, int * pLeaves )
 {
+    int fVerbose = 0;
     Sbd_Cut_t * pCutBest = NULL;   int i;
     assert( p->Pivot == iObj );
+    if ( fVerbose && iObj % 1000 == 0 )
+        printf( "Node %6d : \n", iObj );
     for ( i = 0; i < p->nCutsR; i++ )
+    {
+        if ( fVerbose && iObj % 1000 == 0 )
+            Sbd_CutPrint( p, iObj, p->ppCuts[i] );
+        if ( nSize && (int)p->ppCuts[i]->nLeaves != nSize )
+            continue;
         if ( (int)p->ppCuts[i]->nLeaves > p->nLutSize && 
-             (int)p->ppCuts[i]->nSlowLeaves == 0 &&
+             (int)p->ppCuts[i]->nSlowLeaves <= 1 &&
              (int)p->ppCuts[i]->nTopLeaves <= p->nLutSize-1 &&
              (pCutBest == NULL || Sbd_CutCompare2(pCutBest, p->ppCuts[i]) == 1) )
             pCutBest = p->ppCuts[i];
+    }
+    if ( fVerbose && iObj % 1000 == 0 )
+    {
+        printf( "Best cut of size %d:\n", nSize );
+        Sbd_CutPrint( p, iObj, pCutBest );
+    }
     if ( pCutBest == NULL )
         return -1;
-//Sbd_CutPrint( p, iObj, pCutBest );
     assert( pCutBest->nLeaves <= SBD_DIV_MAX );
     for ( i = 0; i < (int)pCutBest->nLeaves; i++ )
         pLeaves[i] = pCutBest->pLeaves[i];
diff --git a/src/opt/sbd/sbdInt.h b/src/opt/sbd/sbdInt.h
index d54285f8..668c1231 100644
--- a/src/opt/sbd/sbdInt.h
+++ b/src/opt/sbd/sbdInt.h
@@ -52,9 +52,10 @@ ABC_NAMESPACE_HEADER_START
 #define SBD_SAT_UNDEC 0x1234567812345678
 #define SBD_SAT_SAT   0x8765432187654321
 
-#define SBD_LUTS_MAX  2
-#define SBD_SIZE_MAX  4
-#define SBD_DIV_MAX   8
+#define SBD_LUTS_MAX    2
+#define SBD_SIZE_MAX    4
+#define SBD_DIV_MAX    10
+#define SBD_FVAR_MAX  100
 
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
@@ -81,16 +82,28 @@ struct Sbd_Str_t_
 ////////////////////////////////////////////////////////////////////////
 
 /*=== sbdCut.c ==========================================================*/
-extern Sbd_Sto_t * Sbd_StoAlloc( Gia_Man_t * pGia, Vec_Int_t * vMirrors, int nLutSize, int nCutSize, int nCutNum, int fCutMin, int fVerbose );
-extern void        Sbd_StoFree( Sbd_Sto_t * p );
-extern void        Sbd_StoRefObj( Sbd_Sto_t * p, int iObj, int iMirror );
-extern void        Sbd_StoDerefObj( Sbd_Sto_t * p, int iObj );
-extern void        Sbd_StoComputeCutsConst0( Sbd_Sto_t * p, int iObj );
-extern void        Sbd_StoComputeCutsObj( Sbd_Sto_t * p, int iObj, int Delay, int Level );
-extern void        Sbd_StoComputeCutsCi( Sbd_Sto_t * p, int iObj, int Delay, int Level );
-extern int         Sbd_StoComputeCutsNode( Sbd_Sto_t * p, int iObj );
-extern int         Sbd_StoObjBestCut( Sbd_Sto_t * p, int iObj, int * pLeaves );
-
+extern Sbd_Sto_t *  Sbd_StoAlloc( Gia_Man_t * pGia, Vec_Int_t * vMirrors, int nLutSize, int nCutSize, int nCutNum, int fCutMin, int fVerbose );
+extern void         Sbd_StoFree( Sbd_Sto_t * p );
+extern int          Sbd_StoObjRefs( Sbd_Sto_t * p, int iObj );
+extern void         Sbd_StoRefObj( Sbd_Sto_t * p, int iObj, int iMirror );
+extern void         Sbd_StoDerefObj( Sbd_Sto_t * p, int iObj );
+extern void         Sbd_StoComputeCutsConst0( Sbd_Sto_t * p, int iObj );
+extern void         Sbd_StoComputeCutsObj( Sbd_Sto_t * p, int iObj, int Delay, int Level );
+extern void         Sbd_StoComputeCutsCi( Sbd_Sto_t * p, int iObj, int Delay, int Level );
+extern int          Sbd_StoComputeCutsNode( Sbd_Sto_t * p, int iObj );
+extern int          Sbd_StoObjBestCut( Sbd_Sto_t * p, int iObj, int nSize, int * pLeaves );
+/*=== sbdWin.c ==========================================================*/
+extern word         Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDivSet, Vec_Int_t * vDivVars, Vec_Int_t * vDivValues, Vec_Int_t * vTemp );
+extern sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots, int fQbf );
+extern int          Sbd_ManCollectConstants( sat_solver * pSat, int nCareMints[2], int PivotVar, word * pVarSims[], Vec_Int_t * vInds );
+extern int          Sbd_ManCollectConstantsNew( sat_solver * pSat, Vec_Int_t * vDivVars, int nConsts, int PivotVar, word * pOnset, word * pOffset );
+/*=== sbdQbf.c ==========================================================*/
+extern int          Sbd_ProblemSolve( 
+                                       Gia_Man_t * p, Vec_Int_t * vMirrors, 
+                                       int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, 
+                                       Vec_Int_t * vTfo, Vec_Int_t * vRoots, 
+                                       Vec_Int_t * vDivSet, int nStrs, Sbd_Str_t * pStr0 
+                                    );
 
 ABC_NAMESPACE_HEADER_END
 
diff --git a/src/opt/sbd/sbdLut.c b/src/opt/sbd/sbdLut.c
index e8aee790..ffcb71f8 100644
--- a/src/opt/sbd/sbdLut.c
+++ b/src/opt/sbd/sbdLut.c
@@ -96,7 +96,6 @@ int Sbd_ProblemAddClauses( sat_solver * pSat, int nVars, int nStrs, int * pVars,
             }
         }
     }
-//printf( "Stop par = %d.\n", VarPar );
     return 1;
 }
 void Sbd_ProblemAddClausesInit( sat_solver * pSat, int nVars, int nStrs, int * pVars, Sbd_Str_t * pStr0 )
diff --git a/src/opt/sbd/sbdWin.c b/src/opt/sbd/sbdWin.c
index d5b7dd9d..b62332d1 100644
--- a/src/opt/sbd/sbdWin.c
+++ b/src/opt/sbd/sbdWin.c
@@ -54,7 +54,6 @@ sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMi
                                Vec_Int_t * vTfo, Vec_Int_t * vRoots, int fQbf )
 {
     Gia_Obj_t * pObj;
-    int nAddVars = 64;
     int i, iLit = 1, iObj, Fan0, Fan1, Lit0m, Lit1m, Node, fCompl0, fCompl1, RetValue;
     int TfoStart = Vec_IntSize(vWinObjs) - Vec_IntSize(vTfo);
     int PivotVar = Vec_IntEntry(vObj2Var, Pivot);
@@ -67,7 +66,7 @@ sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMi
         pSat = sat_solver_new();
     else
         sat_solver_restart( pSat );
-    sat_solver_setnvars( pSat, Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots) + nAddVars );
+    sat_solver_setnvars( pSat, Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots) + SBD_FVAR_MAX );
     // create constant 0 clause
     sat_solver_addclause( pSat, &iLit, &iLit + 1 );
     // add clauses for all nodes
@@ -139,7 +138,7 @@ sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMi
             sat_solver_delete( pSat );
             return NULL;
         }
-        assert( sat_solver_nvars(pSat) == nVars + nAddVars );
+        assert( sat_solver_nvars(pSat) == nVars + SBD_FVAR_MAX );
     }
     else if ( fQbf )
     {