Updates to delay optimization project.

5 files changed, 181 insertions, 150 deletions

diff --git a/src/opt/sbd/sbd.h b/src/opt/sbd/sbd.h
index 89d29958..6cdfafe4 100644
--- a/src/opt/sbd/sbd.h
+++ b/src/opt/sbd/sbd.h
@@ -39,6 +39,7 @@ typedef struct Sbd_Par_t_ Sbd_Par_t;
 struct Sbd_Par_t_
 {
     int             nLutSize;     // target LUT size
+    int             nLutNum;      // target LUT 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 daefb9af..0b399b8a 100644
--- a/src/opt/sbd/sbdCore.c
+++ b/src/opt/sbd/sbdCore.c
@@ -1,12 +1,12 @@
 /**CFile****************************************************************
 
-  FileName    [sbd.c]
+  FileName    [sbdCore.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
   PackageName [SAT-based optimization using internal don't-cares.]
 
-  Synopsis    []
+  Synopsis    [Core procedures.]
 
   Author      [Alan Mishchenko]
   
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: sbd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: sbdCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
@@ -30,7 +30,6 @@ ABC_NAMESPACE_IMPL_START
 
 #define SBD_MAX_LUTSIZE 6
 
-
 typedef struct Sbd_Man_t_ Sbd_Man_t;
 struct Sbd_Man_t_
 {
@@ -44,13 +43,13 @@ struct Sbd_Man_t_
     Vec_Int_t *     vCover;      // temporary
     Vec_Int_t *     vLits;       // temporary
     Vec_Int_t *     vLits2;      // temporary
-    int             nConsts;     // constants
-    int             nChanges;    // changes
+    int             nLuts[3];    // 0=const, 1=1lut, 2=2lut
     abctime         timeWin;
     abctime         timeCnf;
     abctime         timeSat;
     abctime         timeCov;
     abctime         timeEnu;
+    abctime         timeQbf;
     abctime         timeOther;
     abctime         timeTotal;
     Sbd_Sto_t *     pSto;
@@ -98,6 +97,7 @@ 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)
@@ -489,24 +489,26 @@ 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 );
     word * pCtrl = Sbd_ObjSim2( p, Pivot );
     int PivotVar = Vec_IntEntry(p->vObj2Var, Pivot);
     int RetValue, i, iObj, Ind, fFindOnset, nCares[2] = {0};
+
     abctime clk = Abc_Clock();
-    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 );
     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;
     if ( p->pSat == NULL )
     {
-        if ( p->pPars->fVerbose )
-            printf( "Found stuck-at-%d node %d.\n", 0, Pivot );
+        //if ( p->pPars->fVerbose )
+        //    printf( "Found stuck-at-%d node %d.\n", 0, Pivot );
         Vec_IntWriteEntry( p->vLutLevs, Pivot, 0 );
-        p->nConsts++;
+        p->nLuts[0]++;
         return 0;
     }
     //return -1;
@@ -526,7 +528,7 @@ int Sbd_ManCheckConst( Sbd_Man_t * p, int Pivot )
     nCares[0] = nCares[0] < nMintCount ? nMintCount - nCares[0] : 0;
     nCares[1] = nCares[1] < nMintCount ? nMintCount - nCares[1] : 0;
 
-    if ( p->pPars->fVerbose )
+    if ( p->pPars->fVeryVerbose )
         printf( "Computing %d offset and %d onset minterms for node %d.\n", nCares[0], nCares[1], Pivot );
 
     if ( Vec_IntSize(p->vLits) >= nCares[0] + nCares[1] )
@@ -565,10 +567,10 @@ int Sbd_ManCheckConst( Sbd_Man_t * p, int Pivot )
     Vec_PtrFree( vSims );
     if ( RetValue >= 0 )
     {
-        if ( p->pPars->fVerbose )
+        if ( p->pPars->fVeryVerbose )
             printf( "Found stuck-at-%d node %d.\n", RetValue, Pivot );
         Vec_IntWriteEntry( p->vLutLevs, Pivot, 0 );
-        p->nConsts++;
+        p->nLuts[0]++;
         return RetValue;
     }
     // set controlability of these minterms
@@ -1153,7 +1155,7 @@ 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 = Abc_Clock();
+    abctime clk, clkSat = 0, clkEnu = 0, clkAll;
     word Onset[64] = {0}, Offset[64] = {0}, Cube;
     word CoverRows[64] = {0}, CoverCols[64] = {0};
     int nIters, nItersMax = 32;
@@ -1165,20 +1167,25 @@ int Sbd_ManExplore2( Sbd_Man_t * p, int Pivot, word * pTruth )
     int nConsts = 4;
     int RetValue;
 
-    sat_solver_delete_p( &p->pSat );
+    clk = Abc_Clock();
+    //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;
     if ( RetValue >= 0 )
     {
-        if ( p->pPars->fVerbose )
+        if ( p->pPars->fVeryVerbose )
             printf( "Found stuck-at-%d node %d.\n", RetValue, Pivot );
         Vec_IntWriteEntry( p->vLutLevs, Pivot, 0 );
-        p->nConsts++;
+        p->nLuts[0]++;
         return RetValue;
     }
+    RetValue = 0;
 
     // create rows of the table
     nRows = 0;
@@ -1200,36 +1207,35 @@ int Sbd_ManExplore2( Sbd_Man_t * p, int Pivot, word * pTruth )
     // solve the covering problem
     for ( nIters = 0; nIters < nItersMax && nRows < 64; nIters++ )
     {
-        if ( p->pPars->fVerbose )
+        if ( p->pPars->fVeryVerbose )
             Sbd_ManMatrPrint( p, CoverCols, nDivs, nRows );
 
         clk = Abc_Clock();
         if ( !Sbd_ManFindCands( p, CoverCols, nDivs ) )
         {
-            if ( p->pPars->fVerbose )
+            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;
+            clkEnu += Abc_Clock() - clk;
+            clkAll = Abc_Clock() - clkAll - clkSat - clkEnu;
+            p->timeSat += clkSat;
+            p->timeCov += clkAll;
+            p->timeEnu += clkEnu;
             return 0;
         }
-        //clkEnu += Abc_Clock() - clk;
     
-        if ( p->pPars->fVerbose )
+        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;
+        clkSat += Abc_Clock() - clk;
 
         if ( *pTruth == SBD_SAT_UNDEC )
             printf( "Node %d:  Undecided.\n", Pivot );
         else if ( *pTruth == SBD_SAT_SAT )
         {
-            if ( p->pPars->fVerbose )
+            if ( p->pPars->fVeryVerbose )
             {
                 int i;
                 printf( "Node %d:  SAT.\n", Pivot );
@@ -1255,15 +1261,21 @@ int Sbd_ManExplore2( Sbd_Man_t * p, int Pivot, word * pTruth )
         }
         else
         {
-            if ( p->pPars->fVerbose )
+            if ( p->pPars->fVeryVerbose )
             {
                 printf( "Node %d:  UNSAT.   ", Pivot );
                 Extra_PrintBinary( stdout, (unsigned *)pTruth, 1 << Vec_IntSize(p->vDivSet) ), printf( "\n" );
             }
-            return 1;
+            p->nLuts[1]++;
+            RetValue = 1;
+            break;
         }
     }
-    return 0;
+    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 )
@@ -1277,37 +1289,41 @@ int Sbd_ManExplore3( Sbd_Man_t * p, int Pivot, int * pnStrs, Sbd_Str_t * Strs )
     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 nDivs = Vec_IntSize( p->vDivVars );
     int Delay = Vec_IntEntry( p->vLutLevs, Pivot );
-    int i, k, iObj, nIters;
+    int i, k, iObj, nIters, RetValue;
 
     int nLeaves, pLeaves[SBD_DIV_MAX];
 
-    int pNodesTop[SBD_DIV_MAX], pNodesBot[SBD_DIV_MAX], pNodeRefs[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 );
+    //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
     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 )
                 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 );
+        p->timeSat += Abc_Clock() - clk;
         if ( Truth == SBD_SAT_UNDEC )
             printf( "Node %d:  Undecided.\n", Pivot );
         else if ( Truth == SBD_SAT_SAT )
@@ -1315,16 +1331,34 @@ int Sbd_ManExplore3( Sbd_Man_t * p, int Pivot, int * pnStrs, Sbd_Str_t * Strs )
         else
             pLeaves[nIters] = -1;
     }
-
     Vec_IntClear( p->vDivSet );
     for ( i = 0; i < nLeaves; i++ )
         if ( pLeaves[i] != -1 )
             Vec_IntPush( p->vDivSet, pLeaves[i] );
-    printf( "Reduced %d -> %d\n", nLeaves, Vec_IntSize(p->vDivSet) );
+    //printf( "Reduced %d -> %d\n", nLeaves, Vec_IntSize(p->vDivSet) );
+    if ( Vec_IntSize(p->vDivSet) <= p->pPars->nLutSize )
+    {
+        *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 );
+        p->timeSat += Abc_Clock() - clk;
+        assert( Truth != SBD_SAT_UNDEC && Truth != SBD_SAT_SAT );
+        // create structure
+        Strs->fLut = 1;
+        Strs->nVarIns = Vec_IntSize( p->vDivSet );
+        for ( i = 0; i < Strs->nVarIns; i++ )
+            Strs->VarIns[i] = i;
+        Strs->Res = Truth;
+        p->nLuts[1]++;
+        //Extra_PrintBinary( stdout, (unsigned *)&Truth, 1 << Strs->nVarIns ), printf( "\n" );
+        return 1;
+    }
     assert( Vec_IntSize(p->vDivSet) > p->pPars->nLutSize );
 
-    //Delay++;
-
     // count number of nodes on each level
     nNodesTop = 0, nNodesBot = 0;
     Vec_IntForEachEntry( p->vDivSet, iObj, i )
@@ -1336,8 +1370,8 @@ int Sbd_ManExplore3( Sbd_Man_t * p, int Pivot, int * pnStrs, Sbd_Str_t * Strs )
             pNodesTop[nNodesTop++] = i;
         else // if ( DelayDiff < -2 )
             pNodesBot[nNodesBot++] = i;
-        Vec_IntWriteEntry( p->vDivSet, iObj, Vec_IntEntry(p->vObj2Var, pLeaves[i]) );
-        pNodeRefs[i] = Gia_ObjRefNumId( p->pGia, iObj );
+        Vec_IntWriteEntry( p->vDivSet, i, Vec_IntEntry(p->vObj2Var, iObj) );
+        //pNodeRefs[i] = Gia_ObjRefNumId( p->pGia, iObj );
     }
     if ( i < Vec_IntSize(p->vDivSet) )
         return 0;
@@ -1379,9 +1413,15 @@ int Sbd_ManExplore3( Sbd_Man_t * p, int Pivot, int * pnStrs, Sbd_Str_t * Strs )
         Strs[2+k].Res = 0;
     }
 
-    return Sbd_ProblemSolve( p->pGia, p->vMirrors, 
-                             Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots,
-                             p->vDivSet, *pnStrs, Strs );
+    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]++;
+    return RetValue;
 }
 
 
@@ -1622,7 +1662,6 @@ int Sbd_ManImplement( Sbd_Man_t * p, int Pivot, word Truth )
     // update delay of the initial node
     assert( Vec_IntEntry(p->vLutLevs, Pivot) == iCurLev );
     Vec_IntWriteEntry( p->vLutLevs, Pivot, iNewLev );
-    p->nChanges++;
     return 0;
 }
 
@@ -1677,13 +1716,14 @@ int Sbd_ManImplement2( Sbd_Man_t * p, int Pivot, int nStrs, Sbd_Str_t * pStrs )
     // remember this function
     assert( Vec_IntEntry(p->vMirrors, Pivot) == -1 );
     Vec_IntWriteEntry( p->vMirrors, Pivot, iLit );
-    if ( p->pPars->fVerbose )
+    if ( p->pPars->fVeryVerbose )
         printf( "Replacing node %d by literal %d.\n", Pivot, iLit );
 
     // extend data-structure to accommodate new nodes
     assert( Vec_IntSize(p->vLutLevs) == iObjLast );
     for ( i = iObjLast; i < Gia_ManObjNum(p->pGia); i++ )
         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++ )
     {
         int Delay = Sbd_StoComputeCutsNode( p->pSto, i );
@@ -1703,7 +1743,6 @@ int Sbd_ManImplement2( Sbd_Man_t * p, int Pivot, int nStrs, Sbd_Str_t * pStrs )
     // update delay of the initial node
     assert( Vec_IntEntry(p->vLutLevs, Pivot) == iCurLev );
     Vec_IntWriteEntry( p->vLutLevs, Pivot, iNewLev );
-    p->nChanges++;
     return 0;
 }
 
@@ -1781,11 +1820,10 @@ Gia_Man_t * Sbd_ManDerive( Gia_Man_t * p, Vec_Int_t * vMirrors )
 ***********************************************************************/
 void Sbd_NtkPerformOne( Sbd_Man_t * p, int Pivot )
 {
-//    extern void Sbd_ManSolveSelect( Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vDivVars, Vec_Int_t * vDivValues, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots );
     Sbd_Str_t Strs[4];
-    int nStrs = 0;
+    int i, RetValue, nStrs = 0;
+    word Truth = 0;
 
-    int RetValue; word Truth = 0;
     if ( !p->pSto )
     {
         if ( Sbd_ManMergeCuts( p, Pivot ) )
@@ -1795,83 +1833,39 @@ void Sbd_NtkPerformOne( Sbd_Man_t * p, int Pivot )
 //    if ( Pivot != 15 )
 //        return;
 
-    if ( p->pPars->fVerbose )
-        printf( "\nLooking at node %d\n", Pivot );
     if ( Sbd_ManWindow( p, Pivot ) )
         return;
 
-//    Sbd_ManSolveSelect( p->pGia, p->vMirrors, Pivot, p->vDivVars, p->vDivValues, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots );
-
     RetValue = Sbd_ManCheckConst( p, Pivot );
     if ( RetValue >= 0 )
     {
         Vec_IntWriteEntry( p->vMirrors, Pivot, RetValue );
-        //printf( "    --> Pivot %4d.  Constant %d.\n", Pivot, RetValue );
+        if ( p->pPars->fVerbose ) printf( "Node %5d:  Detected constant %d.\n", Pivot, RetValue );
     }
-    else if ( Sbd_ManExplore3( p, Pivot, &nStrs, Strs ) )
+    else if ( p->pPars->nLutNum >= 1 && Sbd_ManExplore2( p, Pivot, &Truth ) )
     {
-        //Sbd_ManImplement( p, Pivot, Truth );
-        Sbd_ManImplement2( p, Pivot, nStrs, Strs );
-        //printf( "    --> Pivot %4d.  Supp %d.\n", Pivot, Vec_IntSize(p->vDivSet) );
-    }
-/*
-    else if ( Sbd_ManExplore2( p, Pivot, &Truth ) )
-    {
-        int i;
-        Sbd_Str_t Strs;
-        Strs.fLut = 1;
-        Strs.nVarIns = Vec_IntSize( p->vDivSet );
-        for ( i = 0; i < Strs.nVarIns; i++ )
-            Strs.VarIns[i] = i;
-        Strs.Res = Truth;
-        //Sbd_ManImplement( p, Pivot, Truth );
-        Sbd_ManImplement2( p, Pivot, 1, &Strs );
-        //printf( "    --> Pivot %4d.  Supp %d.\n", Pivot, Vec_IntSize(p->vDivSet) );
+        Strs->fLut = 1;
+        Strs->nVarIns = Vec_IntSize( p->vDivSet );
+        for ( i = 0; i < Strs->nVarIns; i++ )
+            Strs->VarIns[i] = i;
+        Strs->Res = Truth;
+        Sbd_ManImplement2( p, Pivot, 1, Strs );
+        if ( p->pPars->fVerbose ) printf( "Node %5d:  Detected LUT%d\n", Pivot, p->pPars->nLutSize );
     }
-*/
-
-/*
-    else
+    else if ( p->pPars->nLutNum >= 2 && Sbd_ManExplore3( p, Pivot, &nStrs, Strs ) )
     {
-        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 
-                                   );
-
-//        Sbd_Str_t Strs[2] = {   {1, 4, {0, 1, 2, 8}},   {1, 4, {3, 4, 5, 6}}    };
-//        Sbd_Str_t Strs[2] = {   {1, 4, {1, 4, 5, 7}},   {1, 4, {0, 1, 2, 3}}    };
-        Sbd_Str_t Strs[3] = {   {1, 4, {8, 4, 5, 7}},   {1, 4, {0, 1, 2, 3}},   {0, 4, {0, 1, 2, 3}}    };
-
-        Vec_Int_t * vDivSet = Vec_IntAlloc( 8 );
-
-        int i, RetValue;
-        
-        for ( i = 0; i < 6; i++ )
-            Vec_IntPush( vDivSet, i+1 );
-
-        RetValue = Sbd_ProblemSolve( p->pGia, p->vMirrors, 
-                                     Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots,
-                                     vDivSet, 3, Strs );
-        if ( RetValue )
-        {
-            printf( "Solving succeded.\n" );
-            //Sbd_ManImplement2( p, Pivot, Truth, nLuts, nSels, nVarsDivs, pVarsDivs, Truths );
-        }
-        Vec_IntFree( vDivSet );
+        Sbd_ManImplement2( p, Pivot, nStrs, Strs );
+        if ( p->pPars->fVerbose ) printf( "Node %5d:  Detected %d%d\n", Pivot, p->pPars->nLutSize, p->pPars->nLutSize );
     }
-*/
 }
 Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
 {
     Gia_Man_t * pNew;  
     Gia_Obj_t * pObj;
     Sbd_Man_t * p = Sbd_ManStart( pGia, pPars );
-    int nNodesOld = Gia_ManObjNum(pGia);//, Count = 0;
+    int nNodesOld = Gia_ManObjNum(pGia);
     int k, Pivot;
     assert( pPars->nLutSize <= 6 );
-    //Sbd_ManMergeTest( p );
     // prepare references
     Gia_ManForEachObj( p->pGia, pObj, Pivot )
         Sbd_StoRefObj( p->pSto, Pivot, -1 );
@@ -1886,21 +1880,28 @@ Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
         {
             Pivot = Gia_ObjId( pGia, pObj );
             if ( Pivot >= nNodesOld )
-                continue;
+                break;
             if ( Gia_ObjIsAnd(pObj) )
-                Sbd_NtkPerformOne( p, Pivot );
+            {
+                int Delay = Sbd_StoComputeCutsNode( p->pSto, Pivot );
+                Vec_IntWriteEntry( p->vLutLevs, Pivot, Delay );
+                if ( Delay > 1 )
+                    Sbd_NtkPerformOne( p, Pivot );
+            }
             else if ( Gia_ObjIsCi(pObj) )
             {
                 int arrTime = Tim_ManGetCiArrival( (Tim_Man_t*)pGia->pManTime, Gia_ObjCioId(pObj) );
                 Vec_IntWriteEntry( p->vLutLevs, Pivot, arrTime );
+                Sbd_StoComputeCutsCi( p->pSto, Pivot, arrTime, arrTime );
             }
             else if ( Gia_ObjIsCo(pObj) )
             {
                 int arrTime = Vec_IntEntry( p->vLutLevs, Gia_ObjFaninId0(pObj, Pivot) );
                 Tim_ManSetCoArrival( (Tim_Man_t*)pGia->pManTime, Gia_ObjCioId(pObj), arrTime );
             }
-            else if ( !Gia_ObjIsConst0(pObj) )
-                assert( 0 );
+            else if ( Gia_ObjIsConst0(pObj) )
+                Sbd_StoComputeCutsConst0( p->pSto, 0 );
+            else assert( 0 );
         }
         //Tim_ManPrint( pGia->pManTime );
         Tim_ManStop( (Tim_Man_t *)pGia->pManTime );
@@ -1909,34 +1910,39 @@ Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
     }
     else
     {
+        Sbd_StoComputeCutsConst0( p->pSto, 0 );
         Gia_ManForEachObj( pGia, pObj, Pivot )
         {
-            if ( Pivot == nNodesOld )
+            if ( Pivot >= nNodesOld )
                 break;
-            if ( Gia_ObjIsAnd(pObj) )
+            if ( Gia_ObjIsCi(pObj) )
+                Sbd_StoComputeCutsCi( p->pSto, Pivot, 0, 0 );
+            else if ( Gia_ObjIsAnd(pObj) )
             {
                 int Delay = Sbd_StoComputeCutsNode( p->pSto, Pivot );
                 Vec_IntWriteEntry( p->vLutLevs, Pivot, Delay );
                 if ( Delay > 1 )
                     Sbd_NtkPerformOne( p, Pivot );
             }
-            else if ( !Gia_ObjIsCo(pObj) )
-                Sbd_StoComputeCutsCi( p->pSto, Pivot, 0, 0 );
+            //if ( nNodesOld != Gia_ManObjNum(pGia) )
+            //    break;
         }
     }
-    printf( "Found %d constants and %d replacements with delay %d.  ", p->nConsts, p->nChanges, Sbd_ManDelay(p) );
+    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) );
     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;
-    if ( 0 )
+    p->timeOther = p->timeTotal - p->timeWin - p->timeCnf - p->timeSat - p->timeCov - p->timeEnu - p->timeQbf;
+    if ( p->pPars->fVerbose )
     {
         ABC_PRTP( "Win", p->timeWin  ,  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 d4c085a1..9c54c74a 100644
--- a/src/opt/sbd/sbdCut.c
+++ b/src/opt/sbd/sbdCut.c
@@ -40,8 +40,9 @@ struct Sbd_Cut_t_
     int             iFunc;                     // functionality
     int             Cost;                      // cut cost
     int             CostLev;                   // cut cost
-    unsigned        nSlowLeaves  : 14;         // slow leaves
-    unsigned        nTreeLeaves  : 14;         // tree leaves
+    unsigned        nTreeLeaves  :  9;         // tree leaves
+    unsigned        nSlowLeaves  :  9;         // slow leaves
+    unsigned        nTopLeaves   : 10;         // top leaves
     unsigned        nLeaves      :  4;         // leaf count
     int             pLeaves[SBD_MAX_CUTSIZE];  // leaves
 };
@@ -442,13 +443,6 @@ static inline int Sbd_CutCountBits( word i )
     i = ((i + (i >> 4)) & 0x0F0F0F0F0F0F0F0F);
     return (i*(0x0101010101010101))>>56;
 }
-static inline int Sbd_CutSlowLeaves( Sbd_Sto_t * p, int iObj, Sbd_Cut_t * pCut )
-{
-    int i, Count = 0, Delay = Vec_IntEntry(p->vDelays, iObj);
-    for ( i = 0; i < (int)pCut->nLeaves; i++ )
-        Count += (Vec_IntEntry(p->vDelays, pCut->pLeaves[i]) - Delay >= -1);
-    return Count;
-}
 static inline int Sbd_CutCost( Sbd_Sto_t * p, Sbd_Cut_t * pCut )
 {
     int i, Cost = 0;
@@ -470,6 +464,20 @@ static inline int Sbd_CutTreeLeaves( Sbd_Sto_t * p, Sbd_Cut_t * pCut )
         Cost += Vec_IntEntry( p->vRefs, pCut->pLeaves[i] ) == 1;
     return Cost;
 }
+static inline int Sbd_CutSlowLeaves( Sbd_Sto_t * p, int iObj, Sbd_Cut_t * pCut )
+{
+    int i, Count = 0, Delay = Vec_IntEntry(p->vDelays, iObj);
+    for ( i = 0; i < (int)pCut->nLeaves; i++ )
+        Count += (Vec_IntEntry(p->vDelays, pCut->pLeaves[i]) - Delay >= -1);
+    return Count;
+}
+static inline int Sbd_CutTopLeaves( Sbd_Sto_t * p, int iObj, Sbd_Cut_t * pCut )
+{
+    int i, Count = 0, Delay = Vec_IntEntry(p->vDelays, iObj);
+    for ( i = 0; i < (int)pCut->nLeaves; i++ )
+        Count += (Vec_IntEntry(p->vDelays, pCut->pLeaves[i]) - Delay == -2);
+    return Count;
+}
 static inline void Sbd_CutAddUnit( Sbd_Sto_t * p, int iObj )
 {
     Vec_Int_t * vThis = Vec_WecEntry( p->vCuts, iObj );
@@ -481,6 +489,14 @@ static inline void Sbd_CutAddUnit( Sbd_Sto_t * p, int iObj )
     Vec_IntPush( vThis, iObj );
     Vec_IntPush( vThis, 2 );
 }
+static inline void Sbd_CutAddZero( Sbd_Sto_t * p, int iObj )
+{
+    Vec_Int_t * vThis = Vec_WecEntry( p->vCuts, iObj );
+    assert( Vec_IntSize(vThis) == 0 );
+    Vec_IntPush( vThis, 1 );
+    Vec_IntPush( vThis, 0 );
+    Vec_IntPush( vThis, 0 );
+}
 static inline int Sbd_StoPrepareSet( Sbd_Sto_t * p, int iObj, int Index )
 {
     Vec_Int_t * vThis = Vec_WecEntry( p->vCuts, iObj );
@@ -495,8 +511,9 @@ static inline int Sbd_StoPrepareSet( Sbd_Sto_t * p, int iObj, int Index )
         pCutTemp->Sign = Sbd_CutGetSign( pCutTemp );
         pCutTemp->Cost = Sbd_CutCost( p, pCutTemp );
         pCutTemp->CostLev = Sbd_CutCostLev( p, pCutTemp );
-        pCutTemp->nSlowLeaves = Sbd_CutSlowLeaves( p, iObj, pCutTemp );
         pCutTemp->nTreeLeaves = Sbd_CutTreeLeaves( p, pCutTemp );
+        pCutTemp->nSlowLeaves = Sbd_CutSlowLeaves( p, iObj, pCutTemp );
+        pCutTemp->nTopLeaves  = Sbd_CutTopLeaves( p, iObj, pCutTemp );
     }
     return pList[0];
 }
@@ -542,6 +559,7 @@ static inline void Sbd_StoComputeSpec( Sbd_Sto_t * p, int iObj, Sbd_Cut_t ** pCu
     int i;
     for ( i = 0; i < nCuts; i++ )
     {
+        pCuts[i]->nTopLeaves  = Sbd_CutTopLeaves( p, iObj, pCuts[i] );
         pCuts[i]->nSlowLeaves = Sbd_CutSlowLeaves( p, iObj, pCuts[i] );
         p->nCutsSpec += (pCuts[i]->nSlowLeaves == 0);
     }
@@ -555,8 +573,8 @@ static inline void Sbd_CutPrint( Sbd_Sto_t * p, int iObj, Sbd_Cut_t * pCut )
         printf( " %*d", nDigits, pCut->pLeaves[i] );
     for ( ; i < (int)p->nCutSize; i++ )
         printf( " %*s", nDigits, " " );
-    printf( "  }  Cost = %3d  CostL = %3d  Slow = %d  Tree = %d  ", 
-        pCut->Cost, pCut->CostLev, pCut->nSlowLeaves, pCut->nTreeLeaves );
+    printf( "  }  Cost = %3d  CostL = %3d  Tree = %d  Slow = %d  Top = %d  ", 
+        pCut->Cost, pCut->CostLev, pCut->nTreeLeaves, pCut->nSlowLeaves, pCut->nTopLeaves );
     printf( "%c ", pCut->nSlowLeaves == 0 ? '*' : ' ' );
     for ( i = 0; i < (int)pCut->nLeaves; i++ )
         printf( "%3d ", Vec_IntEntry(p->vDelays, pCut->pLeaves[i]) - Delay );
@@ -607,7 +625,7 @@ void Sbd_StoMergeCuts( Sbd_Sto_t * p, int iObj )
     p->nCutsR = nCutsR;
     p->Pivot = iObj;
     // debug printout
-    if ( 1 )
+    if ( 0 )
     {
         printf( "*** Obj = %4d  Delay = %4d  NumCuts = %4d\n", iObj, Vec_IntEntry(p->vDelays, iObj), nCutsR );
         for ( i = 0; i < nCutsR; i++ )
@@ -687,6 +705,11 @@ void Sbd_StoComputeCutsObj( Sbd_Sto_t * p, int iObj, int Delay, int Level )
         Vec_WecPushLevel( p->vCuts );
     }
 }
+void Sbd_StoComputeCutsConst0( Sbd_Sto_t * p, int iObj )
+{
+    Sbd_StoComputeCutsObj( p, iObj, 0, 0 );
+    Sbd_CutAddZero( p, iObj );
+}
 void Sbd_StoComputeCutsCi( Sbd_Sto_t * p, int iObj, int Delay, int Level )
 {
     Sbd_StoComputeCutsObj( p, iObj, Delay, Level );
@@ -732,11 +755,14 @@ int Sbd_StoObjBestCut( Sbd_Sto_t * p, int iObj, int * pLeaves )
     Sbd_Cut_t * pCutBest = NULL;   int i;
     assert( p->Pivot == iObj );
     for ( i = 0; i < p->nCutsR; i++ )
-    {
-        if ( (int)p->ppCuts[i]->nLeaves > p->nLutSize && (pCutBest == NULL || Sbd_CutCompare2(pCutBest, p->ppCuts[i]) == 1) )
+        if ( (int)p->ppCuts[i]->nLeaves > p->nLutSize && 
+             (int)p->ppCuts[i]->nSlowLeaves == 0 &&
+             (int)p->ppCuts[i]->nTopLeaves <= p->nLutSize-1 &&
+             (pCutBest == NULL || Sbd_CutCompare2(pCutBest, p->ppCuts[i]) == 1) )
             pCutBest = p->ppCuts[i];
-    }
-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];
@@ -751,7 +777,7 @@ void Sbd_StoComputeCutsTest( Gia_Man_t * pGia )
     Gia_ManForEachObj( p->pGia, pObj, iObj )
         Sbd_StoRefObj( p, iObj, -1 );
     // compute cuts
-    Sbd_StoComputeCutsObj( p, 0, 0, 0 );
+    Sbd_StoComputeCutsConst0( p, 0 );
     Gia_ManForEachCiId( p->pGia, iObj, i )
         Sbd_StoComputeCutsCi( p, iObj, 0, 0 );
     Gia_ManForEachAnd( p->pGia, pObj, iObj )
diff --git a/src/opt/sbd/sbdInt.h b/src/opt/sbd/sbdInt.h
index 31d0ea06..d54285f8 100644
--- a/src/opt/sbd/sbdInt.h
+++ b/src/opt/sbd/sbdInt.h
@@ -84,7 +84,8 @@ struct Sbd_Str_t_
 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_StoDefefObj( Sbd_Sto_t * p, int iObj );
+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 );
diff --git a/src/opt/sbd/sbdLut.c b/src/opt/sbd/sbdLut.c
index b924a33b..e8aee790 100644
--- a/src/opt/sbd/sbdLut.c
+++ b/src/opt/sbd/sbdLut.c
@@ -157,7 +157,7 @@ void Sbd_ProblemCollectSolution( int nStrs, Sbd_Str_t * pStr0, Vec_Int_t * vLits
             for ( m = 0; m < nIters; m++, iLit++ )
                 if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, iLit)) )
                     Abc_TtSetBit( &pStr->Res, m );
-            Abc_TtStretch6( &pStr->Res, pStr->nVarIns, 6 );
+            pStr->Res = Abc_Tt6Stretch( pStr->Res, pStr->nVarIns );
         }
         else
         {
@@ -192,13 +192,12 @@ int Sbd_ProblemSolve( Gia_Man_t * p, Vec_Int_t * vMirrors,
 {
     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 );
     
-    int fVerbose = 1;
+    int fVerbose = 0;
+    abctime clk = Abc_Clock();
     Vec_Int_t * vLits    = Vec_IntAlloc( 100 );
     sat_solver * pSatCec = Sbd_ManSatSolver( NULL, p, vMirrors, Pivot, vWinObjs, vObj2Var, vTfo, vRoots, 1 );
     sat_solver * pSatQbf = sat_solver_new();
 
-    //int PivotVar   = Vec_IntEntry(vObj2Var, Pivot);
-
     int nVars      = Vec_IntSize( vDivSet );
     int nPars      = Sbd_ProblemCountParams( nStrs, pStr0 );
 
@@ -248,8 +247,6 @@ int Sbd_ProblemSolve( Gia_Man_t * p, Vec_Int_t * vMirrors,
         if ( status == l_False ) // solution found
             break;
         assert( status == l_True );
-//        Vec_IntForEachEntry( vWinObjs, iVar, i )
-//            printf( "Node = %4d.  SatVar = %4d.  Value = %d.\n", iVar, i, sat_solver_var_value(pSatCec, i) );
 
         if ( fVerbose )
         {
@@ -292,16 +289,16 @@ int Sbd_ProblemSolve( Gia_Man_t * p, Vec_Int_t * vMirrors,
     }
     if ( Vec_IntSize(vLits) > 0 )
     {
-        Sbd_ProblemPrintSolution( nStrs, pStr0, vLits );
+        //Sbd_ProblemPrintSolution( nStrs, pStr0, vLits );
         Sbd_ProblemCollectSolution( nStrs, pStr0, vLits );
         RetValue = 1;
     }
-    else 
-        printf( "Solution does not exist.\n" );
-
     sat_solver_delete( pSatCec );
     sat_solver_delete( pSatQbf );
     Vec_IntFree( vLits );
+
+    if ( fVerbose )
+        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
     return RetValue;
 }