New SAT-based optimization package.

2 files changed, 437 insertions, 123 deletions

diff --git a/src/opt/sbd/sbdCore.c b/src/opt/sbd/sbdCore.c
index b391eefa..a35c5594 100644
--- a/src/opt/sbd/sbdCore.c
+++ b/src/opt/sbd/sbdCore.c
@@ -44,6 +44,13 @@ struct Sbd_Man_t_
     Vec_Int_t *     vLits;       // temporary
     int             nConsts;     // constants
     int             nChanges;    // changes
+    abctime         timeWin;
+    abctime         timeCnf;
+    abctime         timeSat;
+    abctime         timeCov;
+    abctime         timeEnu;
+    abctime         timeOther;
+    abctime         timeTotal;
     // target node
     int             Pivot;       // target node
     Vec_Int_t *     vTfo;        // TFO (excludes node, includes roots) - precomputed
@@ -176,6 +183,7 @@ Sbd_Man_t * Sbd_ManStart( Gia_Man_t * pGia, Sbd_Par_t * pPars )
 {
     int i, w, Id;
     Sbd_Man_t * p = ABC_CALLOC( Sbd_Man_t, 1 );  
+    p->timeTotal  = Abc_Clock();
     p->pPars      = pPars;
     p->pGia       = pGia;
     p->vTfos      = Sbd_ManWindowRoots( pGia, pPars->nTfoLevels, pPars->nTfoFanMax );
@@ -207,7 +215,7 @@ Sbd_Man_t * Sbd_ManStart( Gia_Man_t * pGia, Sbd_Par_t * pPars )
     Gia_ManRandom( 1 );
     Gia_ManForEachCiId( pGia, Id, i )
         for ( w = 0; w < p->pPars->nWords; w++ )
-            Sbd_ObjSim0(p, Id)[w] = Gia_ManRandomW( 0 );
+            Sbd_ObjSim0(p, Id)[w] = Gia_ManRandomW( 0 );     
     return p;
 }
 void Sbd_ManStop( Sbd_Man_t * p )
@@ -272,15 +280,16 @@ void Sbd_ManPropagateControlOne( Sbd_Man_t * p, int Node )
         word Sim0 = Gia_ObjFaninC0(pNode) ? ~pSims0[w] : pSims0[w];
         word Sim1 = Gia_ObjFaninC1(pNode) ? ~pSims1[w] : pSims1[w];
 
-        pCtrl0[w] |= pCtrl[w] & (pSims[w] | Sim1 | (~Sim0 & ~Sim1));
-        pCtrl1[w] |= pCtrl[w] & (pSims[w] | Sim0);
+        pCtrl0[w] |= pCtrl[w];// & (pSims[w] | Sim1 | (~Sim0 & ~Sim1));
+        pCtrl1[w] |= pCtrl[w];// & (pSims[w] | Sim0 | (~Sim0 & ~Sim1));
 
-        pDtrl0[w] |= pDtrl[w] & (pSims[w] | Sim1);
-        pDtrl1[w] |= pDtrl[w] & (pSims[w] | Sim0 | (~Sim0 & ~Sim1));
+        pDtrl0[w] |= pDtrl[w];// & (pSims[w] | Sim1 | (~Sim0 & ~Sim1));
+        pDtrl1[w] |= pDtrl[w];// & (pSims[w] | Sim0 | (~Sim0 & ~Sim1));
     }
 }
 void Sbd_ManPropagateControl( Sbd_Man_t * p, int Pivot )
 {
+    abctime clk = Abc_Clock();
     int i, Node;
     Abc_TtCopy( Sbd_ObjSim3(p, Pivot), Sbd_ObjSim2(p, Pivot), p->pPars->nWords, 0 );
     // clean controlability
@@ -294,11 +303,13 @@ void Sbd_ManPropagateControl( Sbd_Man_t * p, int Pivot )
     for ( i = Vec_IntEntry(p->vObj2Var, Pivot); i >= 0 && ((Node = Vec_IntEntry(p->vWinObjs, i)), 1); i-- )
         if ( Gia_ObjIsAnd(Gia_ManObj(p->pGia, Node)) )
             Sbd_ManPropagateControlOne( p, Node );
+    p->timeWin += Abc_Clock() - clk;
 }
 void Sbd_ManUpdateOrder( Sbd_Man_t * p, int Pivot )
 {
     int i, k, Node;
     Vec_Int_t * vLevel;
+    int nTimeValidDivs = 0;
     // collect divisors by logic level
     int LevelMax = Vec_IntEntry(p->vLutLevs, Pivot);
     Vec_WecClear( p->vDivLevels );
@@ -316,10 +327,13 @@ void Sbd_ManUpdateOrder( Sbd_Man_t * p, int Pivot )
             Vec_IntWriteEntry( p->vObj2Var, Node, Vec_IntSize(p->vWinObjs) );
             Vec_IntPush( p->vWinObjs, Node );
         }
-        // detect useful divisors
+        // remember divisor cutoff
         if ( i == LevelMax - 2 )
-            Vec_IntFill( p->vDivValues, Vec_IntSize(p->vWinObjs), 0 );
+            nTimeValidDivs = Vec_IntSize(p->vWinObjs);
     }
+    assert( nTimeValidDivs > 0 );
+    Vec_IntFill( p->vDivValues, Abc_MinInt(63, nTimeValidDivs), 0 );
+    //printf( "%d ", Abc_MinInt(63, nTimeValidDivs) );
 }
 void Sbd_ManWindowSim_rec( Sbd_Man_t * p, int NodeInit )
 {
@@ -378,14 +392,16 @@ void Sbd_ManWindowSim_rec( Sbd_Man_t * p, int NodeInit )
 }
 int Sbd_ManWindow( Sbd_Man_t * p, int Pivot )
 {
+    abctime clk = Abc_Clock();
     int i, Node;
     // assign pivot and TFO (assume siminfo is assigned at the PIs)
     p->Pivot = Pivot;
     p->vTfo = Vec_WecEntry( p->vTfos, Pivot );
-    // simulate TFI cone
+    // add constant node
     Vec_IntClear( p->vWinObjs );
     Vec_IntWriteEntry( p->vObj2Var, 0, Vec_IntSize(p->vWinObjs) );
     Vec_IntPush( p->vWinObjs, 0 );
+    // simulate TFI cone
     Gia_ManIncrementTravId( p->pGia );
     Gia_ObjSetTravIdCurrentId(p->pGia, 0);
     Sbd_ManWindowSim_rec( p, Pivot );
@@ -419,11 +435,10 @@ int Sbd_ManWindow( Sbd_Man_t * p, int Pivot )
     Vec_IntForEachEntry( p->vTfo, Node, i )
         if ( Abc_LitIsCompl(Node) ) // root
             Abc_TtOrXor( Sbd_ObjSim2(p, Pivot), Sbd_ObjSim0(p, Abc_Lit2Var(Node)), Sbd_ObjSim1(p, Abc_Lit2Var(Node)), p->pPars->nWords );
+    p->timeWin += Abc_Clock() - clk;
     // propagate controlability to fanins for the TFI nodes starting from the pivot
     Sbd_ManPropagateControl( p, Pivot );
-    // return 1 if window is too large
-    if ( p->pPars->fVerbose && Vec_IntSize(p->vDivValues) >= 64 )
-        printf( "Window is too large.\n" );
+    assert( Vec_IntSize(p->vDivValues) < 64 );
     return (int)(Vec_IntSize(p->vDivValues) >= 64);
 }
 
@@ -441,15 +456,17 @@ int Sbd_ManWindow( Sbd_Man_t * p, int Pivot )
 int Sbd_ManCheckConst( Sbd_Man_t * p, int Pivot )
 {
     extern void Sbd_ManPrintObj( Sbd_Man_t * p, int Pivot );
-    int nMintCount = 16;
+    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 );
     p->pSat = Sbd_ManSatSolver( p->pSat, p->pGia, p->vMirrors, Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots );
+    p->timeCnf += Abc_Clock() - clk;
     //return -1;
     //Sbd_ManPrintObj( p, Pivot );
 
@@ -508,6 +525,7 @@ int Sbd_ManCheckConst( Sbd_Man_t * p, int Pivot )
     {
         if ( p->pPars->fVerbose )
             printf( "Found stuck-at-%d node %d.\n", RetValue, Pivot );
+        Vec_IntWriteEntry( p->vLutLevs, Pivot, 0 );
         p->nConsts++;
         return RetValue;
     }
@@ -726,24 +744,156 @@ void Sbd_ManPrintObj( Sbd_Man_t * p, int Pivot )
     }
 }
 
+void Sbd_ManMatrPrint( word Cover[64], int nCol, int nRows )
+{
+    int i, k;
+    for ( i = 0; i <= nCol; i++ )
+    {
+        printf( "%2d : ", i );
+        for ( k = 0; k < nRows; k++ )
+            for ( k = 0; k < nRows; k++ )
+                printf( "%d", (int)((Cover[i] >> k) & 1) );
+        printf( "\n"); 
+    }
+    printf( "\n");
+}
+static inline void Sbd_ManCoverReverseOrder( word Cover[64] )
+{
+    int i;
+    for ( i = 0; i < 32; i++ )
+    {
+        word Cube = Cover[i];
+        Cover[i] = Cover[63-i]; 
+        Cover[63-i] = Cube;
+    }
+}
+
+static inline int Sbd_ManAddCube1( word Cover[64], int nRows, word Cube )
+{
+    int n, m;
+    if ( 0 )
+    {
+        printf( "Adding cube: " );
+        for ( n = 0; n < 64; n++ )
+            printf( "%d", (int)((Cube >> n) & 1) );
+        printf( "\n" );
+    }
+    // do not add contained Cube
+    assert( nRows <= 64 );
+    for ( n = 0; n < nRows; n++ )
+        if ( (Cover[n] & Cube) == Cover[n] ) // Cube is contained
+            return nRows;
+    // remove rows contained by Cube
+    for ( n = m = 0; n < nRows; n++ )
+        if ( (Cover[n] & Cube) != Cube ) // Cover[n] is not contained
+            Cover[m++] = Cover[n];
+    if ( m < 64 )
+        Cover[m++] = Cube;
+    for ( n = m; n < nRows; n++ )
+        Cover[n] = 0;
+    nRows = m;
+    return nRows;
+}
+static inline int Sbd_ManAddCube2( word Cover[2][64], int nRows, word Cube[2] )
+{
+    int n, m;
+    // do not add contained Cube
+    assert( nRows <= 64 );
+    for ( n = 0; n < nRows; n++ )
+        if ( (Cover[0][n] & Cube[0]) == Cover[0][n] && (Cover[1][n] & Cube[1]) == Cover[1][n] ) // Cube is contained
+            return nRows;
+    // remove rows contained by Cube
+    for ( n = m = 0; n < nRows; n++ )
+        if ( (Cover[0][n] & Cube[0]) != Cube[0] || (Cover[1][n] & Cube[1]) != Cube[1] ) // Cover[n] is not contained
+        {
+            Cover[0][m] = Cover[0][n];
+            Cover[1][m] = Cover[1][n];
+            m++;
+        }
+    if ( m < 64 )
+    {
+        Cover[0][m] = Cube[0];
+        Cover[1][m] = Cube[1];
+        m++;
+    }
+    for ( n = m; n < nRows; n++ )
+        Cover[0][n] = Cover[1][n] = 0;
+    nRows = m;
+    return nRows;
+}
+
+static inline int Sbd_ManFindCands( Sbd_Man_t * p, word Cover[64], int nDivs )
+{
+    int c0, c1, c2, c3;
+    word Target = Cover[nDivs];
+    Vec_IntClear( p->vDivVars );
+    for ( c0 = 0;    c0 < nDivs; c0++ )
+        if ( Cover[c0] == Target )
+        {
+            Vec_IntPush( p->vDivVars, c0 );
+            return 1;
+        }
+
+    for ( c0 = 0;    c0 < nDivs; c0++ )
+    for ( c1 = c0+1; c1 < nDivs; c1++ )
+        if ( (Cover[c0] | Cover[c1]) == Target )
+        {
+            Vec_IntPush( p->vDivVars, c0 );
+            Vec_IntPush( p->vDivVars, c1 );
+            return 1;
+        }
+
+    for ( c0 = 0;    c0 < nDivs; c0++ )
+    for ( c1 = c0+1; c1 < nDivs; c1++ )
+    for ( c2 = c1+1; c2 < nDivs; c2++ )
+        if ( (Cover[c0] | Cover[c1] | Cover[c2]) == Target )
+        {
+            Vec_IntPush( p->vDivVars, c0 );
+            Vec_IntPush( p->vDivVars, c1 );
+            Vec_IntPush( p->vDivVars, c2 );
+            return 1;
+        }
+
+    for ( c0 = 0;    c0 < nDivs; c0++ )
+    for ( c1 = c0+1; c1 < nDivs; c1++ )
+    for ( c2 = c1+1; c2 < nDivs; c2++ )
+    for ( c3 = c2+1; c3 < nDivs; c3++ )
+    {
+        if ( (Cover[c0] | Cover[c1] | Cover[c2] | Cover[c3]) == Target )
+        {
+            Vec_IntPush( p->vDivVars, c0 );
+            Vec_IntPush( p->vDivVars, c1 );
+            Vec_IntPush( p->vDivVars, c2 );
+            Vec_IntPush( p->vDivVars, c3 );
+            return 1;
+        }
+    }
+    return 0;
+}
 
 int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth )
 {
     int fVerbose = 0;
+    abctime clk, clkSat = 0, clkEnu = 0, clkAll = Abc_Clock();
+    int nIters, nItersMax = 32;
     extern word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDivVars, Vec_Int_t * vValues, Vec_Int_t * vTemp );
 
-    word MatrS[64] = {0}, MatrC[2][64] = {{0}}, Cubes[2][2][64] = {{{0}}}, Cover[64] = {0}, Cube, Cube0, Cube1, Target;
-    int c0 = 0, c1 = 0, c2 = 0, c3 = 0, i, k, n, Index, nCubes[2] = {0}, nRows = 0;
+    word MatrS[64] = {0}, MatrC[2][64] = {{0}}, Cubes[2][2][64] = {{{0}}}, Cover[64] = {0}, Cube, CubeNew[2];
+    int i, k, n, Index, nCubes[2] = {0}, nRows = 0, nRowsOld;
 
+    int nDivs = Vec_IntSize(p->vDivValues);
     int PivotVar = Vec_IntEntry(p->vObj2Var, Pivot);
     int FreeVar = Vec_IntSize(p->vWinObjs) + Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots);
     int RetValue = 0;
 
+    if ( p->pPars->fVerbose )
+        printf( "Node %d.  Useful divisors = %d.\n", Pivot, nDivs );
+
     if ( fVerbose )
         Sbd_ManPrintObj( p, Pivot );
 
     // collect bit-matrices
-    for ( i = 0; i < Vec_IntSize(p->vDivValues); i++ )
+    for ( i = 0; i < nDivs; i++ )
     {
         MatrS[63-i]    = *Sbd_ObjSim0( p, Vec_IntEntry(p->vWinObjs, i) );
         MatrC[0][63-i] = *Sbd_ObjSim2( p, Vec_IntEntry(p->vWinObjs, i) );
@@ -762,34 +912,26 @@ int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth )
     // collect cubes
     for ( i = 0; i < 64; i++ )
     {
-        assert( Abc_TtGetBit(&MatrC[0][i], Vec_IntSize(p->vDivValues)) == Abc_TtGetBit(&MatrC[1][i], Vec_IntSize(p->vDivValues)) );
-        if ( !Abc_TtGetBit(&MatrC[0][i], Vec_IntSize(p->vDivValues)) )
+        assert( Abc_TtGetBit(&MatrC[0][i], nDivs) == Abc_TtGetBit(&MatrC[1][i], nDivs) );
+        if ( !Abc_TtGetBit(&MatrC[0][i], nDivs) )
             continue;
-        Index = Abc_TtGetBit(&MatrS[i], Vec_IntSize(p->vDivValues)); // Index==0 offset; Index==1 onset
+        Index = Abc_TtGetBit(&MatrS[i], nDivs); // Index==0 offset; Index==1 onset
         for ( n = 0; n < 2; n++ )
         {
             if ( n && MatrC[0][i] == MatrC[1][i] )
                 continue;
             assert( MatrC[n][i] );
-            Cube0 = ~MatrS[i] & MatrC[n][i];
-            Cube1 =  MatrS[i] & MatrC[n][i];
-            assert( Cube0 || Cube1 );
-            for ( k = 0; k < nCubes[Index]; k++ )
-                if ( Cubes[Index][0][k] == Cube0 && Cubes[Index][1][k] == Cube1 )
-                    break;
-            if ( k == nCubes[Index] && k < 64 )
-            {
-                Cubes[Index][0][nCubes[Index]] = Cube0;
-                Cubes[Index][1][nCubes[Index]] = Cube1;
-                nCubes[Index]++;
-            }
+            CubeNew[0] = ~MatrS[i] & MatrC[n][i];
+            CubeNew[1] =  MatrS[i] & MatrC[n][i];
+            assert( CubeNew[0] || CubeNew[1] );
+            nCubes[Index] = Sbd_ManAddCube2( Cubes[Index], nCubes[Index], CubeNew );
         }
     }
 
     if ( p->pPars->fVerbose )
         printf( "Generated matrix with %d x %d entries.\n", nCubes[0], nCubes[1] );
 
-    if ( fVerbose )
+    if ( p->pPars->fVerbose )
     for ( n = 0; n < 2; n++ )
     {
         printf( "%s:\n", n ? "Onset" : "Offset" );
@@ -804,96 +946,99 @@ int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth )
         printf( "\n" );
     }
 
-    // collect cover
-    for ( i = 0; i < nCubes[0]; i++ )
-    for ( k = 0; k < nCubes[1]; k++ )
+    // create covering table
+    nRows = 0;
+    for ( i = 0; i < nCubes[0] && nRows < 32; i++ )
+    for ( k = 0; k < nCubes[1] && nRows < 32; k++ )
     {
         Cube = (Cubes[0][1][i] & Cubes[1][0][k]) | (Cubes[0][0][i] & Cubes[1][1][k]);
         assert( Cube );
-        for ( n = 0; n < nRows; n++ )
-            if ( Cover[63-n] == Cube )
-                break;
-        if ( n == nRows && n < 64 )
-            Cover[63-nRows++] = Cube;
+        nRows = Sbd_ManAddCube1( Cover, nRows, Cube );
     }
 
+    Sbd_ManCoverReverseOrder( Cover );
+
     if ( p->pPars->fVerbose )
         printf( "Generated cover with %d entries.\n", nRows );
 
-
+    //if ( p->pPars->fVerbose )
     //Sbd_PrintMatrix64( Cover );
     Sbd_TransposeMatrix64( Cover );
+    //if ( p->pPars->fVerbose )
     //Sbd_PrintMatrix64( Cover );
 
-    // swap
-    for ( i = 0; i < 32; i++ )
-    {
-        Cube = Cover[i];
-        Cover[i] = Cover[63-i]; 
-        Cover[63-i] = Cube;
-    }
-
-    if ( fVerbose )
-    {
-        for ( i = 0; i <= nRows; i++, printf( "\n") )
-            for ( k = 0; k < 64; k++ )
-                printf( "%d", (int)((Cover[i] >> k) & 1) );
-    }
+    Sbd_ManCoverReverseOrder( Cover );
 
-    Target = Cover[Vec_IntSize(p->vDivValues)];
-    for ( c0 = 0;    c0 < Vec_IntSize(p->vDivValues); c0++ )
-    for ( c1 = c0+1; c1 < Vec_IntSize(p->vDivValues); c1++ )
-    for ( c2 = c1+1; c2 < Vec_IntSize(p->vDivValues); c2++ )
-    for ( c3 = c2+1; c3 < Vec_IntSize(p->vDivValues); c3++ )
-    {
-        if ( (Cover[c0] | Cover[c1] | Cover[c2] | Cover[c3]) == Target )
-            goto finish;
-    }
-finish:
-    if ( c0 == Vec_IntSize(p->vDivValues) )
+    nRowsOld = nRows;
+    for ( nIters = 0; nIters < nItersMax && nRows < 64; nIters++ )
     {
         if ( p->pPars->fVerbose )
-            printf( "Cannot find a feasible cover.\n" );
-        return RetValue;
-    }
+            Sbd_ManMatrPrint( Cover, nDivs, nRows );
 
-    Vec_IntClear( p->vDivVars );
-    Vec_IntPush( p->vDivVars, c0 );
-    Vec_IntPush( p->vDivVars, c1 );
-    Vec_IntPush( p->vDivVars, c2 );
-    Vec_IntPush( p->vDivVars, c3 );
+        clk = Abc_Clock();
+        if ( !Sbd_ManFindCands( p, Cover, nDivs ) )
+        {
+            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;
+            return RetValue;
+        }
+        clkEnu += Abc_Clock() - clk;
     
-    if ( p->pPars->fVerbose )
-        printf( "Feasible cover:  " );
-    if ( p->pPars->fVerbose )
-        Vec_IntPrint( p->vDivVars );
-
-    *pTruth = Sbd_ManSolve( p->pSat, PivotVar, FreeVar, p->vDivVars, p->vDivValues, p->vLits );
-    if ( *pTruth == SBD_SAT_UNDEC )
-        printf( "Node %d:  Undecided.\n", Pivot );
-    else if ( *pTruth == SBD_SAT_SAT )
-    {
         if ( p->pPars->fVerbose )
+            printf( "Candidate support:  " ),
+            Vec_IntPrint( p->vDivVars );
+
+        clk = Abc_Clock();
+        *pTruth = Sbd_ManSolve( p->pSat, PivotVar, FreeVar+nIters, p->vDivVars, p->vDivValues, p->vLits );
+        clkSat += Abc_Clock() - clk;
+
+        if ( *pTruth == SBD_SAT_UNDEC )
+            printf( "Node %d:  Undecided.\n", Pivot );
+        else if ( *pTruth == SBD_SAT_SAT )
         {
-            int i;
-            printf( "Node %d:  SAT.\n", Pivot );
-            for ( i = 0; i < Vec_IntSize(p->vDivValues); i++ )
-                printf( "%d", Vec_IntEntry(p->vDivValues, i) & 1 );
-            printf( "\n" );
-            for ( i = 0; i < Vec_IntSize(p->vDivValues); i++ )
-                printf( "%d", Vec_IntEntry(p->vDivValues, i) >> 1 );
-            printf( "\n" );
+            if ( p->pPars->fVerbose )
+            {
+                int i;
+                printf( "Node %d:  SAT.\n", Pivot );
+                for ( i = 0; i < nDivs; i++ )
+                    printf( "%d", i % 10 );
+                printf( "\n" );
+                for ( i = 0; i < nDivs; i++ )
+                    printf( "%c", (Vec_IntEntry(p->vDivValues, i) & 0x4) ? '0' + (Vec_IntEntry(p->vDivValues, i) & 1) : 'x' );
+                printf( "\n" );
+                for ( i = 0; i < nDivs; i++ )
+                    printf( "%c", (Vec_IntEntry(p->vDivValues, i) & 0x8) ? '0' + ((Vec_IntEntry(p->vDivValues, i) >> 1) & 1) : 'x' );
+                printf( "\n" );
+            }
+            // add row to the covering table
+            for ( i = 0; i < nDivs; i++ )
+                if ( Vec_IntEntry(p->vDivValues, i) == 0xE || Vec_IntEntry(p->vDivValues, i) == 0xD )
+                    Cover[i] |= ((word)1 << nRows);
+            Cover[nDivs] |= ((word)1 << nRows);
+            nRows++;
         }
+        else
+        {
+            if ( p->pPars->fVerbose )
+            {
+                printf( "Node %d:  UNSAT.\n", Pivot );
+                Extra_PrintBinary( stdout, (unsigned *)pTruth, 1 << Vec_IntSize(p->vDivVars) ), printf( "\n" );
+            }
+            RetValue = 1;
+            break;
+        }
+        //break;
     }
-    else
-    {
-        if ( p->pPars->fVerbose )
-            printf( "Node %d:  UNSAT.\n", Pivot );
-        if ( p->pPars->fVerbose )
-            Extra_PrintBinary( stdout, (unsigned *)pTruth, 1 << Vec_IntSize(p->vDivVars) ), printf( "\n" );
-        RetValue = 1;
-    }
-
+    //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;
 }
 
@@ -930,9 +1075,11 @@ int Sbd_CutMergeSimple( Sbd_Man_t * p, int * pCut1, int * pCut2, int * pCut )
         *pBeg++ = *pBeg2++;
     return (pCut[0] = pBeg - pCut - 1);
 }
-int Sbd_ManComputeCut( Sbd_Man_t * p, int Node )
+/*
+int Sbd_ManMergeCuts( Sbd_Man_t * p, int Node )
 {
-    int pCut[2*SBD_MAX_LUTSIZE];     
+    int Result  = 1; // no need to resynthesize
+    int pCut[2*SBD_MAX_LUTSIZE+1];     
     int iFan0   = Gia_ObjFaninId0( Gia_ManObj(p->pGia, Node), Node );
     int iFan1   = Gia_ObjFaninId1( Gia_ManObj(p->pGia, Node), Node );
     int Level0  = Vec_IntEntry( p->vLutLevs, iFan0 );
@@ -940,30 +1087,147 @@ int Sbd_ManComputeCut( Sbd_Man_t * p, int Node )
     int LevMax  = (Level0 || Level1) ? Abc_MaxInt(Level0, Level1) : 1;
     int * pCut0 = Sbd_ObjCut( p, iFan0 );
     int * pCut1 = Sbd_ObjCut( p, iFan1 );
-    int Cut0[2] = {1, iFan0}, * pCut0Temp = Level0 < LevMax ? Cut0 : pCut0; 
-    int Cut1[2] = {1, iFan1}, * pCut1Temp = Level1 < LevMax ? Cut1 : pCut1; 
-    int nSize   = Sbd_CutMergeSimple( p, pCut0Temp, pCut1Temp, pCut );
-    int Result  = 1; // no need to resynthesize
-    assert( iFan0 != iFan1 );
+    int nSize   = Sbd_CutMergeSimple( p, pCut0, pCut1, pCut );
     if ( nSize > p->pPars->nLutSize )
     {
-        pCut[0] = 2;
-        pCut[1] = iFan0 < iFan1 ? iFan0 : iFan1;
-        pCut[2] = iFan0 < iFan1 ? iFan1 : iFan0;
-        Result  = LevMax ? 0 : 1;
-        LevMax++;
+        if ( Level0 != Level1 )
+        {
+            int Cut0[2] = {1, iFan0}, * pCut0Temp = Level0 < LevMax ? Cut0 : pCut0; 
+            int Cut1[2] = {1, iFan1}, * pCut1Temp = Level1 < LevMax ? Cut1 : pCut1; 
+            nSize = Sbd_CutMergeSimple( p, pCut0Temp, pCut1Temp, pCut );
+        }
+        if ( nSize > p->pPars->nLutSize )
+        {
+            pCut[0] = 2;
+            pCut[1] = iFan0 < iFan1 ? iFan0 : iFan1;
+            pCut[2] = iFan0 < iFan1 ? iFan1 : iFan0;
+            Result  = LevMax ? 0 : 1;
+            LevMax++;
+        }
     }
+    assert( iFan0 != iFan1 );
     assert( Vec_IntEntry(p->vLutLevs, Node) == 0 );
     Vec_IntWriteEntry( p->vLutLevs, Node, LevMax );
     memcpy( Sbd_ObjCut(p, Node), pCut, sizeof(int) * (pCut[0] + 1) );
     //printf( "Setting node %d with delay %d (result = %d).\n", Node, LevMax, Result );
     return Result;
 }
+*/
+int Sbd_ManMergeCuts( Sbd_Man_t * p, int Node )
+{
+    int pCut11[2*SBD_MAX_LUTSIZE+1];     
+    int pCut01[2*SBD_MAX_LUTSIZE+1];     
+    int pCut10[2*SBD_MAX_LUTSIZE+1];     
+    int pCut00[2*SBD_MAX_LUTSIZE+1];     
+    int iFan0   = Gia_ObjFaninId0( Gia_ManObj(p->pGia, Node), Node );
+    int iFan1   = Gia_ObjFaninId1( Gia_ManObj(p->pGia, Node), Node );
+    int Level0  = Vec_IntEntry( p->vLutLevs, iFan0 ) ? Vec_IntEntry( p->vLutLevs, iFan0 ) : 1;
+    int Level1  = Vec_IntEntry( p->vLutLevs, iFan1 ) ? Vec_IntEntry( p->vLutLevs, iFan1 ) : 1;
+    int * pCut0 = Sbd_ObjCut( p, iFan0 );
+    int * pCut1 = Sbd_ObjCut( p, iFan1 );
+    int Cut0[2] = {1, iFan0}; 
+    int Cut1[2] = {1, iFan1}; 
+    int nSize11 = Sbd_CutMergeSimple( p, pCut0, pCut1, pCut11 );
+    int nSize01 = Sbd_CutMergeSimple( p,  Cut0, pCut1, pCut01 );
+    int nSize10 = Sbd_CutMergeSimple( p, pCut0,  Cut1, pCut10 );
+    int nSize00 = Sbd_CutMergeSimple( p,  Cut0,  Cut1, pCut00 );
+    int Lev11   = nSize11 <= p->pPars->nLutSize ? Abc_MaxInt(Level0,   Level1)   : ABC_INFINITY;
+    int Lev01   = nSize01 <= p->pPars->nLutSize ? Abc_MaxInt(Level0+1, Level1)   : ABC_INFINITY;
+    int Lev10   = nSize10 <= p->pPars->nLutSize ? Abc_MaxInt(Level0,   Level1+1) : ABC_INFINITY;
+    int Lev00   = nSize00 <= p->pPars->nLutSize ? Abc_MaxInt(Level0+1, Level1+1) : ABC_INFINITY;
+    int * pCutRes = pCut11;
+    int LevCur    = Lev11;
+    if ( Lev01 < LevCur || (Lev01 == LevCur && pCut01[0] < pCutRes[0]) )
+    {
+        pCutRes = pCut01;
+        LevCur  = Lev01;
+    }
+    if ( Lev10 < LevCur || (Lev10 == LevCur && pCut10[0] < pCutRes[0]) )
+    {
+        pCutRes = pCut10;
+        LevCur  = Lev10;
+    }
+    if ( Lev00 < LevCur || (Lev00 == LevCur && pCut00[0] < pCutRes[0]) )
+    {
+        pCutRes = pCut00;
+        LevCur  = Lev00;
+    }
+    assert( iFan0 != iFan1 );
+    assert( Vec_IntEntry(p->vLutLevs, Node) == 0 );
+    Vec_IntWriteEntry( p->vLutLevs, Node, LevCur );
+    assert( pCutRes[0] <= p->pPars->nLutSize );
+    memcpy( Sbd_ObjCut(p, Node), pCutRes, sizeof(int) * (pCutRes[0] + 1) );
+    //printf( "Setting node %d with delay %d.\n", Node, LevCur );
+    return LevCur == Abc_MaxInt(Level0, Level1);
+}
+int Sbd_ManDelay( Sbd_Man_t * p )
+{
+    int i, Id, Delay = 0;
+    Gia_ManForEachCoDriverId( p->pGia, Id, i )
+        Delay = Abc_MaxInt( Delay, Vec_IntEntry(p->vLutLevs, Id) );
+    return Delay;
+}
+void Sbd_ManMergeTest( Sbd_Man_t * p )
+{
+    int Node;
+    Gia_ManForEachAndId( p->pGia, Node )
+        Sbd_ManMergeCuts( p, Node );
+    printf( "Delay %d.\n", Sbd_ManDelay(p) );
+}
+
+void Sbd_ManFindCut_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    if ( pObj->fMark1 )
+        return;
+    pObj->fMark1 = 1;
+    if ( pObj->fMark0 )
+        return;
+    assert( Gia_ObjIsAnd(pObj) );
+    Sbd_ManFindCut_rec( p, Gia_ObjFanin0(pObj) );
+    Sbd_ManFindCut_rec( p, Gia_ObjFanin1(pObj) );
+}
+void Sbd_ManFindCutUnmark_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    if ( !pObj->fMark1 )
+        return;
+    pObj->fMark1 = 0;
+    if ( pObj->fMark0 )
+        return;
+    assert( Gia_ObjIsAnd(pObj) );
+    Sbd_ManFindCutUnmark_rec( p, Gia_ObjFanin0(pObj) );
+    Sbd_ManFindCutUnmark_rec( p, Gia_ObjFanin1(pObj) );
+}
+void Sbd_ManFindCut( Sbd_Man_t * p, int Node, Vec_Int_t * vCutLits )
+{
+    int pCut[SBD_MAX_LUTSIZE+1];     
+    int i, LevelMax = 0;
+    // label reachable nodes 
+    Gia_Obj_t * pTemp, * pObj = Gia_ManObj(p->pGia, Node);
+    Sbd_ManFindCut_rec( p->pGia, pObj );
+    // collect 
+    pCut[0] = 0;
+    Gia_ManForEachObjVec( vCutLits, p->pGia, pTemp, i )
+        if ( pTemp->fMark1 )
+        {
+            LevelMax = Abc_MaxInt( LevelMax, Vec_IntEntry(p->vLutLevs, Gia_ObjId(p->pGia, pTemp)) );
+            pCut[1+pCut[0]++] = Gia_ObjId(p->pGia, pTemp);
+        }
+    assert( pCut[0] <= p->pPars->nLutSize );
+    // unlabel reachable nodes
+    Sbd_ManFindCutUnmark_rec( p->pGia, pObj );
+    // create cut
+    assert( Vec_IntEntry(p->vLutLevs, Node) == 0 );
+    Vec_IntWriteEntry( p->vLutLevs, Node, LevelMax+1 );
+    memcpy( Sbd_ObjCut(p, Node), pCut, sizeof(int) * (pCut[0] + 1) );
+}
+
 int Sbd_ManImplement( Sbd_Man_t * p, int Pivot, word Truth )
 {
-    int i, k, w, iLit, Node;
+    int i, k, w, iLit, Entry, Node;
     int iObjLast = Gia_ManObjNum(p->pGia);
     int iCurLev = Vec_IntEntry(p->vLutLevs, Pivot);
+    int iNewLev;
+    Gia_Obj_t * pObj;
     // collect leaf literals
     Vec_IntClear( p->vLits );
     Vec_IntForEachEntry( p->vDivVars, Node, i )
@@ -986,7 +1250,13 @@ int Sbd_ManImplement( Sbd_Man_t * p, int Pivot, word Truth )
     Vec_IntWriteEntry( p->vMirrors, Pivot, iLit );
     if ( p->pPars->fVerbose )
         printf( "Replacing node %d by literal %d.\n", Pivot, iLit );
-    // extend data-structure for new nodes
+    // translate literals into variables
+    Vec_IntForEachEntry( p->vLits, Entry, i )
+        Vec_IntWriteEntry( p->vLits, i, Abc_Lit2Var(Entry) );
+    // label inputs
+    Gia_ManForEachObjVec( p->vLits, p->pGia, pObj, i )
+        pObj->fMark0 = 1;
+    // extend data-structure to accommodate new nodes
     assert( Vec_IntSize(p->vLutLevs) == iObjLast );
     for ( i = iObjLast; i < Gia_ManObjNum(p->pGia); i++ )
     {
@@ -994,13 +1264,20 @@ int Sbd_ManImplement( Sbd_Man_t * p, int Pivot, word Truth )
         Vec_IntPush( p->vObj2Var, 0 );
         Vec_IntPush( p->vMirrors, -1 );
         Vec_IntFillExtra( p->vLutCuts, Vec_IntSize(p->vLutCuts) + p->pPars->nLutSize + 1, 0 );
-        Sbd_ManComputeCut( p, i );
+        Sbd_ManFindCut( p, i, p->vLits );
         for ( k = 0; k < 4; k++ )
             for ( w = 0; w < p->pPars->nWords; w++ )
                 Vec_WrdPush( p->vSims[k], 0 );
     }
+    // unlabel inputs
+    Gia_ManForEachObjVec( p->vLits, p->pGia, pObj, i )
+        pObj->fMark0 = 0;
     // make sure delay reduction is achieved
-    assert( Vec_IntEntry(p->vLutLevs, Abc_Lit2Var(iLit)) < iCurLev );
+    iNewLev = Vec_IntEntry( p->vLutLevs, Abc_Lit2Var(iLit) );
+    assert( iNewLev < iCurLev );
+    // update delay of the initial node
+    assert( Vec_IntEntry(p->vLutLevs, Pivot) == iCurLev );
+    Vec_IntWriteEntry( p->vLutLevs, Pivot, iNewLev );
     p->nChanges++;
     return 0;
 }
@@ -1074,16 +1351,18 @@ Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
 {
     Gia_Man_t * pNew;  
     Sbd_Man_t * p = Sbd_ManStart( pGia, pPars );
-    int nNodesOld = Gia_ManObjNum(pGia);
+    int nNodesOld = Gia_ManObjNum(pGia);//, Count = 0;
     int RetValue, Pivot; word Truth = 0;
     assert( pPars->nLutSize <= 6 );
+    //Sbd_ManMergeTest( p );
+    //return NULL;
     Gia_ManForEachAndId( pGia, Pivot )
     {
         if ( Pivot >= nNodesOld )
             break;
-        if ( Sbd_ManComputeCut( p, Pivot ) )
+        if ( Sbd_ManMergeCuts( p, Pivot ) )
             continue;
-        //if ( Pivot != 313 )
+        //if ( Pivot != 344 )
         //    continue;
         if ( p->pPars->fVerbose )
             printf( "\nLooking at node %d\n", Pivot );
@@ -1093,10 +1372,25 @@ Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
         if ( RetValue >= 0 )
             Vec_IntWriteEntry( p->vMirrors, Pivot, RetValue );
         else if ( Sbd_ManExplore( p, Pivot, &Truth ) )
+        {
             Sbd_ManImplement( p, Pivot, Truth );
+            //if ( Count++ == 1 )
+            //    break;
+        }
     }
-    printf( "Found %d constants and %d replacements.\n", p->nConsts, p->nChanges );
+    printf( "Found %d constants and %d replacements with delay %d.  ", p->nConsts, p->nChanges, 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;
+    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( "Oth", p->timeOther,  p->timeTotal );
+    ABC_PRTP( "ALL", p->timeTotal,  p->timeTotal );
     Sbd_ManStop( p );
     return pNew;
 }
diff --git a/src/opt/sbd/sbdWin.c b/src/opt/sbd/sbdWin.c
index 50837e1f..7100462b 100644
--- a/src/opt/sbd/sbdWin.c
+++ b/src/opt/sbd/sbdWin.c
@@ -155,9 +155,9 @@ word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDi
     int nBTLimit = 0;
     word uCube, uTruth = 0;
     int status, i, iVar, nFinal, * pFinal, pLits[2], nIter = 0;
+    assert( FreeVar < sat_solver_nvars(pSat) );
     pLits[0] = Abc_Var2Lit( PivotVar, 0 ); // F = 1
     pLits[1] = Abc_Var2Lit( FreeVar, 0 );  // iNewLit
-    assert( Vec_IntSize(vValues) <= sat_solver_nvars(pSat) );
     while ( 1 ) 
     {
         // find onset minterm
@@ -169,7 +169,7 @@ word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDi
         assert( status == l_True );
         // remember variable values
         for ( i = 0; i < Vec_IntSize(vValues); i++ )
-            Vec_IntWriteEntry( vValues, i, sat_solver_var_value(pSat, i) );
+            Vec_IntWriteEntry( vValues, i, 2*sat_solver_var_value(pSat, i) );
         // collect divisor literals
         Vec_IntClear( vTemp );
         Vec_IntPush( vTemp, Abc_LitNot(pLits[0]) ); // F = 0
@@ -203,7 +203,27 @@ word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDi
     assert( status == l_True );
     // store the counter-example
     for ( i = 0; i < Vec_IntSize(vValues); i++ )
-        Vec_IntAddToEntry( vValues, i, 2*sat_solver_var_value(pSat, i) );
+        Vec_IntAddToEntry( vValues, i, sat_solver_var_value(pSat, i) );
+
+    for ( i = 0; i < Vec_IntSize(vValues); i++ )
+        Vec_IntAddToEntry( vValues, i, 0xC );
+/*
+    // reduce the counter example
+    for ( n = 0; n < 2; n++ )
+    {
+        Vec_IntClear( vTemp );
+        Vec_IntPush( vTemp, Abc_Var2Lit(PivotVar, n) ); // n = 0 => F = 1  (expanding offset against onset)
+        for ( i = 0; i < Vec_IntSize(vValues); i++ )
+            Vec_IntPush( vTemp, Abc_Var2Lit(i, !((Vec_IntEntry(vValues, i) >> n) & 1)) );
+        status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntArray(vTemp) + Vec_IntSize(vTemp), nBTLimit, 0, 0, 0 );
+        assert( status == l_False );
+        // compute cube and add clause
+        nFinal = sat_solver_final( pSat, &pFinal );
+        for ( i = 0; i < nFinal; i++ )
+            if ( Abc_Lit2Var(pFinal[i]) != PivotVar )
+                Vec_IntAddToEntry( vValues, Abc_Lit2Var(pFinal[i]), 1 << (n+2) );
+    }
+*/
     return SBD_SAT_SAT;
 }