New SAT-based optimization package.

2 files changed, 485 insertions, 122 deletions

diff --git a/src/opt/sbd/sbdCore.c b/src/opt/sbd/sbdCore.c
index d83ed231..cf46651e 100644
--- a/src/opt/sbd/sbdCore.c
+++ b/src/opt/sbd/sbdCore.c
@@ -42,6 +42,8 @@ struct Sbd_Man_t_
     Vec_Wrd_t *     vSims[4];    // simulation information (main, backup, controlability)
     Vec_Int_t *     vCover;      // temporary
     Vec_Int_t *     vLits;       // temporary
+    int             nConsts;     // constants
+    int             nChanges;    // changes
     // target node
     int             Pivot;       // target node
     Vec_Int_t *     vTfo;        // TFO (excludes node, includes roots) - precomputed
@@ -82,7 +84,7 @@ void Sbd_ParSetDefault( Sbd_Par_t * pPars )
 {
     memset( pPars, 0, sizeof(Sbd_Par_t) );
     pPars->nLutSize     = 4;  // target LUT size
-    pPars->nTfoLevels   = 3;  // the number of TFO levels (windowing)
+    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 
@@ -145,7 +147,7 @@ Vec_Wec_t * Sbd_ManWindowRoots( Gia_Man_t * p, int nTfoLevels, int nTfoFanMax )
     Vec_BitFree( vPoDrivers );
 
     // print the results
-    if ( 1 )
+    if ( 0 )
     Vec_WecForEachLevel( vTfos, vNodes, i )
     {
         if ( !Gia_ObjIsAnd(Gia_ManObj(p, i)) )
@@ -244,61 +246,9 @@ void Sbd_ManStop( Sbd_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Sbd_ManWindowSim_rec( Sbd_Man_t * p, int Node )
+void Sbd_ManPropagateControlOne( Sbd_Man_t * p, int Node )
 {
-    Gia_Obj_t * pObj;
-    if ( Vec_IntEntry(p->vMirrors, Node) >= 0 )
-        Node = Abc_Lit2Var( Vec_IntEntry(p->vMirrors, Node) );
-    if ( Gia_ObjIsTravIdCurrentId(p->pGia, Node) || Node == 0 )
-        return;
-    Gia_ObjSetTravIdCurrentId(p->pGia, Node);
-    pObj = Gia_ManObj( p->pGia, Node );
-    if ( Gia_ObjIsAnd(pObj) )
-    {
-        Sbd_ManWindowSim_rec( p, Gia_ObjFaninId0(pObj, Node) );
-        Sbd_ManWindowSim_rec( p, Gia_ObjFaninId1(pObj, Node) );
-    }
-    if ( !pObj->fMark0 )
-    {
-        Vec_IntWriteEntry( p->vObj2Var, Node, Vec_IntSize(p->vWinObjs) );
-        Vec_IntPush( p->vWinObjs, Node );
-    }
-    if ( Gia_ObjIsCi(pObj) )
-        return;
-    // simulate
-    assert( Gia_ObjIsAnd(pObj) );
-    if ( Gia_ObjIsXor(pObj) )
-    {
-        Abc_TtXor( Sbd_ObjSim0(p, Node), 
-            Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)), 
-            Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)), 
-            p->pPars->nWords, 
-            Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pObj) );
-
-        if ( pObj->fMark0 )
-            Abc_TtXor( Sbd_ObjSim1(p, Node), 
-                Gia_ObjFanin0(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId0(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)), 
-                Gia_ObjFanin1(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId1(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)), 
-                p->pPars->nWords, 
-                Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pObj) );
-    }
-    else
-    {
-        Abc_TtAndCompl( Sbd_ObjSim0(p, Node), 
-            Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)), Gia_ObjFaninC0(pObj), 
-            Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)), Gia_ObjFaninC1(pObj), 
-            p->pPars->nWords );
-
-        if ( pObj->fMark0 )
-            Abc_TtAndCompl( Sbd_ObjSim1(p, Node), 
-                Gia_ObjFanin0(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId0(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)), Gia_ObjFaninC0(pObj), 
-                Gia_ObjFanin1(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId1(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)), Gia_ObjFaninC1(pObj), 
-                p->pPars->nWords );
-    }
-}
-void Sbd_ManPropagateControl( Sbd_Man_t * p, int Node )
-{
-    Gia_Obj_t * pNode = Gia_ManObj(p->pGia, Node);
+    Gia_Obj_t * pNode = Gia_ManObj(p->pGia, Node);  int w;
     int iObj0 = Gia_ObjFaninId0(pNode, Node);
     int iObj1 = Gia_ObjFaninId1(pNode, Node);
 
@@ -314,20 +264,37 @@ void Sbd_ManPropagateControl( Sbd_Man_t * p, int Node )
     word * pDtrl0 = Sbd_ObjSim3(p, iObj0);
     word * pDtrl1 = Sbd_ObjSim3(p, iObj1);
 
-//    printf( "Node %2d : %d %d\n", Node, (int)(pSims[0] & 1), (int)(pCtrl[0] & 1) );
-    int w;
+//    Gia_ObjPrint( p->pGia, pNode );
+//    printf( "Node %2d : %d %d\n\n", Node, (int)(pSims[0] & 1), (int)(pCtrl[0] & 1) );
+
     for ( w = 0; w < p->pPars->nWords; w++ )
     {
         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);
 
-        pDtrl0[w] = pDtrl[w] & (pSims[w] | Sim1);
-        pDtrl1[w] = pDtrl[w] & (pSims[w] | Sim0 | (~Sim0 & ~Sim1));
+        pDtrl0[w] |= pDtrl[w] & (pSims[w] | Sim1);
+        pDtrl1[w] |= pDtrl[w] & (pSims[w] | Sim0 | (~Sim0 & ~Sim1));
     }
 }
+void Sbd_ManPropagateControl( Sbd_Man_t * p, int Pivot )
+{
+    int i, Node;
+    Abc_TtCopy( Sbd_ObjSim3(p, Pivot), Sbd_ObjSim2(p, Pivot), p->pPars->nWords, 0 );
+    // clean controlability
+    for ( i = 0; i < Vec_IntEntry(p->vObj2Var, Pivot) && ((Node = Vec_IntEntry(p->vWinObjs, i)), 1); i++ )
+    {
+        Abc_TtClear( Sbd_ObjSim2(p, Node), p->pPars->nWords );
+        Abc_TtClear( Sbd_ObjSim3(p, Node), p->pPars->nWords );
+        //printf( "Clearing node %d.\n", Node );
+    }
+    // propagate controlability to fanins for the TFI nodes starting from the 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 );
+}
 void Sbd_ManUpdateOrder( Sbd_Man_t * p, int Pivot )
 {
     int i, k, Node;
@@ -354,7 +321,62 @@ void Sbd_ManUpdateOrder( Sbd_Man_t * p, int Pivot )
             Vec_IntFill( p->vDivValues, Vec_IntSize(p->vWinObjs), 0 );
     }
 }
-void Sbd_ManWindow( Sbd_Man_t * p, int Pivot )
+void Sbd_ManWindowSim_rec( Sbd_Man_t * p, int NodeInit )
+{
+    Gia_Obj_t * pObj;
+    int Node = NodeInit;
+    if ( Vec_IntEntry(p->vMirrors, Node) >= 0 )
+        Node = Abc_Lit2Var( Vec_IntEntry(p->vMirrors, Node) );
+    if ( Gia_ObjIsTravIdCurrentId(p->pGia, Node) )
+        return;
+    Gia_ObjSetTravIdCurrentId(p->pGia, Node);
+    pObj = Gia_ManObj( p->pGia, Node );
+    if ( Gia_ObjIsAnd(pObj) )
+    {
+        Sbd_ManWindowSim_rec( p, Gia_ObjFaninId0(pObj, Node) );
+        Sbd_ManWindowSim_rec( p, Gia_ObjFaninId1(pObj, Node) );
+    }
+    if ( !pObj->fMark0 )
+    {
+        Vec_IntWriteEntry( p->vObj2Var, Node, Vec_IntSize(p->vWinObjs) );
+        Vec_IntPush( p->vWinObjs, Node );
+    }
+    if ( Gia_ObjIsCi(pObj) )
+        return;
+    // simulate
+    assert( Gia_ObjIsAnd(pObj) );
+    if ( Gia_ObjIsXor(pObj) )
+    {
+        Abc_TtXor( Sbd_ObjSim0(p, Node), 
+            Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)), 
+            Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)), 
+            p->pPars->nWords, 
+            Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pObj) );
+
+        if ( pObj->fMark0 )
+            Abc_TtXor( Sbd_ObjSim1(p, Node), 
+                Gia_ObjFanin0(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId0(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)), 
+                Gia_ObjFanin1(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId1(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)), 
+                p->pPars->nWords, 
+                Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pObj) );
+    }
+    else
+    {
+        Abc_TtAndCompl( Sbd_ObjSim0(p, Node), 
+            Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)), Gia_ObjFaninC0(pObj), 
+            Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)), Gia_ObjFaninC1(pObj), 
+            p->pPars->nWords );
+
+        if ( pObj->fMark0 )
+            Abc_TtAndCompl( Sbd_ObjSim1(p, Node), 
+                Gia_ObjFanin0(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId0(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)), Gia_ObjFaninC0(pObj), 
+                Gia_ObjFanin1(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId1(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)), Gia_ObjFaninC1(pObj), 
+                p->pPars->nWords );
+    }
+    if ( Node != NodeInit )
+        Abc_TtCopy( Sbd_ObjSim0(p, NodeInit), Sbd_ObjSim0(p, Node), p->pPars->nWords, Abc_LitIsCompl(Vec_IntEntry(p->vMirrors, NodeInit)) );
+}
+int Sbd_ManWindow( Sbd_Man_t * p, int Pivot )
 {
     int i, Node;
     // assign pivot and TFO (assume siminfo is assigned at the PIs)
@@ -362,7 +384,10 @@ void Sbd_ManWindow( Sbd_Man_t * p, int Pivot )
     p->vTfo = Vec_WecEntry( p->vTfos, Pivot );
     // simulate TFI cone
     Vec_IntClear( p->vWinObjs );
+    Vec_IntWriteEntry( p->vObj2Var, 0, Vec_IntSize(p->vWinObjs) );
+    Vec_IntPush( p->vWinObjs, 0 );
     Gia_ManIncrementTravId( p->pGia );
+    Gia_ObjSetTravIdCurrentId(p->pGia, 0);
     Sbd_ManWindowSim_rec( p, Pivot );
     Sbd_ManUpdateOrder( p, Pivot );
     // simulate node
@@ -394,11 +419,143 @@ void 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 );
-    Abc_TtCopy( Sbd_ObjSim3(p, Pivot), Sbd_ObjSim2(p, Pivot), p->pPars->nWords, 0 );
     // propagate controlability to fanins for the TFI nodes starting from the 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_ManPropagateControl( p, Node );
+    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" );
+    return (int)(Vec_IntSize(p->vDivValues) >= 64);
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sbd_ManCheckConst( Sbd_Man_t * p, int Pivot )
+{
+    extern void Sbd_ManPrintObj( Sbd_Man_t * p, int Pivot );
+    int nMintCount = 16;
+    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};
+    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 );
+    //return -1;
+    //Sbd_ManPrintObj( p, Pivot );
+
+    // count the number of on-set and off-set care-set minterms
+    Vec_IntClear( p->vLits );
+    for ( i = 0; i < 64; i++ )
+        if ( Abc_TtGetBit(pCtrl, i) )
+            nCares[Abc_TtGetBit(pSims, i)]++;
+        else
+            Vec_IntPush( p->vLits, i );
+    fFindOnset = (int)(nCares[0] < nCares[1]);
+    if ( nCares[0] >= nMintCount && nCares[1] >= nMintCount )
+        return -1;
+    // find how many do we need
+    nCares[0] = nCares[0] < nMintCount ? nMintCount - nCares[0] : 0;
+    nCares[1] = nCares[1] < nMintCount ? nMintCount - nCares[1] : 0;
+
+    if ( p->pPars->fVerbose )
+        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] )
+        Vec_IntShrink( p->vLits, nCares[0] + nCares[1] );
+    else
+    {
+        // collect places to insert new minterms
+        for ( i = 0; i < 64 && Vec_IntSize(p->vLits) < nCares[0] + nCares[1]; i++ )
+            if ( fFindOnset == Abc_TtGetBit(pSims, i) )
+                Vec_IntPush( p->vLits, i );
+    }
+    // collect simulation pointers
+    vSims = Vec_PtrAlloc( PivotVar + 1 );
+    Vec_IntForEachEntry( p->vWinObjs, iObj, i )
+    {
+        Vec_PtrPush( vSims, Sbd_ObjSim0(p, iObj) );
+        if ( iObj == Pivot )
+            break;
+    }
+    assert( i == PivotVar );
+    // compute patterns
+    RetValue = Sbd_ManCollectConstants( p->pSat, nCares, PivotVar, (word **)Vec_PtrArray(vSims), p->vLits );
+    // print computed miterms
+    if ( 0 && RetValue < 0 )
+    {
+        Vec_Int_t * vPis = Vec_WecEntry(p->vDivLevels, 0);
+        int i, k, Ind;
+        printf( "Additional minterms:\n" );
+        Vec_IntForEachEntry( p->vLits, Ind, k )
+        {
+            for ( i = 0; i < Vec_IntSize(vPis); i++ )
+                printf( "%d", Abc_TtGetBit( (word *)Vec_PtrEntry(vSims, Vec_IntEntry(p->vWinObjs, i)), Ind ) );
+            printf( "\n" );
+        }
+    }
+    Vec_PtrFree( vSims );
+    if ( RetValue >= 0 )
+    {
+        if ( p->pPars->fVerbose )
+            printf( "Found stuck-at-%d node %d.\n", RetValue, Pivot );
+        p->nConsts++;
+        return RetValue;
+    }
+    // set controlability of these minterms
+    Vec_IntForEachEntry( p->vLits, Ind, i )
+        Abc_TtSetBit( pCtrl, Ind );
+    // propagate controlability to fanins for the TFI nodes starting from the pivot
+    Sbd_ManPropagateControl( p, Pivot );
+    // double check that we now have enough minterms
+    for ( i = 0; i < 64; i++ )
+        if ( Abc_TtGetBit(pCtrl, i) )
+            nCares[Abc_TtGetBit(pSims, i)]++;
+    assert( nCares[0] >= nMintCount && nCares[1] >= nMintCount );
+    return -1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transposing 64-bit matrix.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Sbd_TransposeMatrix64( word A[64] )
+{
+    int j, k;
+    word t, m = 0x00000000FFFFFFFF;
+    for ( j = 32; j != 0; j = j >> 1, m = m ^ (m << j) )
+    {
+        for ( k = 0; k < 64; k = (k + j + 1) & ~j )
+        {
+            t = (A[k] ^ (A[k+j] >> j)) & m;
+            A[k] = A[k] ^ t;
+            A[k+j] = A[k+j] ^ (t << j);
+        }
+    }
+}
+static inline void Sbd_PrintMatrix64( word A[64] )
+{
+    int j, k;
+    for ( j = 0; j < 64; j++, printf("\n") )
+    for ( k = 0; k < 64; k++ )
+        printf( "%d", (int)((A[j] >> k) & 1) );
+    printf( "\n" );
 }
 
 /**Function*************************************************************
@@ -418,7 +575,7 @@ void Sbd_ManPrintObj( Sbd_Man_t * p, int Pivot )
     int i, k, k0, k1, Id, Bit0, Bit1;
 
     Vec_IntForEachEntryStop( p->vWinObjs, Id, i, nDivs )
-        printf( "%d : ", Id ), Extra_PrintBinary( stdout, (unsigned *)Sbd_ObjSim0(p, Id), 64 ), printf( "\n" );
+        printf( "%3d : ", Id ), Extra_PrintBinary( stdout, (unsigned *)Sbd_ObjSim0(p, Id), 64 ), printf( "\n" );
 
     assert( p->Pivot == Pivot );
     Vec_IntClear( p->vCounts[0] );
@@ -561,52 +718,182 @@ void Sbd_ManPrintObj( Sbd_Man_t * p, int Pivot )
             if ( Abc_TtGetBit(pCtrl, Bit0) && Abc_TtGetBit(pCtrl, Bit1) && Abc_TtGetBit(pSims, Bit0) != Abc_TtGetBit(pSims, Bit1) )
                 Abc_TtXorBit( &Row, i );
         }
-        if ( !Vec_WrdPushUnique( p->vMatrix, Row ) )
-            Extra_PrintBinary( stdout, (unsigned *)&Row, nDivs ), printf( "\n" );
+        if ( Vec_WrdPushUnique( p->vMatrix, Row ) )
+            continue;
+        for ( i = 0; i < nDivs; i++ )
+            printf( "%d", (int)((Row >> i) & 1) );
+        printf( "\n" );
     }
-
 }
+
+
 int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth )
 {
-    extern sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots );
+    int fVerbose = 0;
     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, c1, c2, c3, i, k, n, Index, nCubes[2] = {0}, nRows = 0, fFound = 0;
+
     int PivotVar = Vec_IntEntry(p->vObj2Var, Pivot);
     int FreeVar = Vec_IntSize(p->vWinObjs) + Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots);
     int RetValue = 0;
 
-//    Sbd_ManPrintObj( p, Pivot );
-    Vec_IntPrint( p->vObj2Var );
+    if ( fVerbose )
+        Sbd_ManPrintObj( p, Pivot );
+
+    // collect bit-matrices
+    for ( i = 0; i < Vec_IntSize(p->vDivValues); i++ )
+    {
+        MatrS[63-i]    = *Sbd_ObjSim0( p, Vec_IntEntry(p->vWinObjs, i) );
+        MatrC[0][63-i] = *Sbd_ObjSim2( p, Vec_IntEntry(p->vWinObjs, i) );
+        MatrC[1][63-i] = *Sbd_ObjSim3( p, Vec_IntEntry(p->vWinObjs, i) );
+    }
+    MatrS[63-i]    = *Sbd_ObjSim0( p, Pivot );
+    MatrC[0][63-i] = *Sbd_ObjSim2( p, Pivot );
+    MatrC[1][63-i] = *Sbd_ObjSim3( p, Pivot );
+
+    //Sbd_PrintMatrix64( MatrS );
+    Sbd_TransposeMatrix64( MatrS );
+    Sbd_TransposeMatrix64( MatrC[0] );
+    Sbd_TransposeMatrix64( MatrC[1] );
+    //Sbd_PrintMatrix64( MatrS );
+
+    // 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)) )
+            continue;
+        Index = Abc_TtGetBit(&MatrS[i], Vec_IntSize(p->vDivValues)); // 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]++;
+            }
+        }
+    }
+
+    if ( p->pPars->fVerbose )
+        printf( "Generated matrix with %d x %d entries.\n", nCubes[0], nCubes[1] );
+
+    if ( fVerbose )
+    for ( n = 0; n < 2; n++ )
+    {
+        printf( "%s:\n", n ? "Onset" : "Offset" );
+        for ( i = 0; i < nCubes[n]; i++, printf( "\n" ) )
+            for ( k = 0; k < 64; k++ )
+                if ( Abc_TtGetBit(&Cubes[n][0][i], k) )
+                    printf( "0" );
+                else if ( Abc_TtGetBit(&Cubes[n][1][i], k) )
+                    printf( "1" );
+                else 
+                    printf( "." );
+        printf( "\n" );
+    }
+
+    // collect cover
+    for ( i = 0; i < nCubes[0]; i++ )
+    for ( k = 0; k < nCubes[1]; 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;
+    }
+
+    if ( p->pPars->fVerbose )
+        printf( "Generated cover with %d entries.\n", nRows );
+
+
+    //Sbd_PrintMatrix64( Cover );
+    Sbd_TransposeMatrix64( Cover );
+    //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) );
+    }
+
+    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) )
+    {
+        if ( p->pPars->fVerbose )
+            printf( "Cannot find a feasible cover.\n" );
+        return RetValue;
+    }
 
     Vec_IntClear( p->vDivVars );
-    Vec_IntPush( p->vDivVars, 0 );
-    Vec_IntPush( p->vDivVars, 1 );
-    Vec_IntPush( p->vDivVars, 2 );
-    Vec_IntPush( p->vDivVars, 4 );
+    Vec_IntPush( p->vDivVars, c0 );
+    Vec_IntPush( p->vDivVars, c1 );
+    Vec_IntPush( p->vDivVars, c2 );
+    Vec_IntPush( p->vDivVars, c3 );
+    
+    if ( p->pPars->fVerbose )
+        printf( "Feasible cover:  " );
+    if ( p->pPars->fVerbose )
+        Vec_IntPrint( p->vDivVars );
 
-    p->pSat = Sbd_ManSatSolver( p->pSat, p->pGia, Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots );
     *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 )
     {
-        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 < 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" );
+        }
     }
     else
     {
-        printf( "Node %d:  UNSAT.\n", Pivot );
+        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;
     }
 
-    Extra_PrintBinary( stdout, (unsigned *)pTruth, 1 << Vec_IntSize(p->vDivVars) ), printf( "\n" );
-
     return RetValue;
 }
 
@@ -669,7 +956,7 @@ int Sbd_ManComputeCut( Sbd_Man_t * p, int Node )
     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 );
+    //printf( "Setting node %d with delay %d (result = %d).\n", Node, LevMax, Result );
     return Result;
 }
 int Sbd_ManImplement( Sbd_Man_t * p, int Pivot, word Truth )
@@ -697,11 +984,15 @@ int Sbd_ManImplement( Sbd_Man_t * p, int Pivot, word Truth )
     // remember this function
     assert( Vec_IntEntry(p->vMirrors, Pivot) == -1 );
     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
     assert( Vec_IntSize(p->vLutLevs) == iObjLast );
     for ( i = iObjLast; i < Gia_ManObjNum(p->pGia); i++ )
     {
         Vec_IntPush( p->vLutLevs, 0 );
+        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 );
         for ( k = 0; k < 4; k++ )
@@ -710,6 +1001,7 @@ int Sbd_ManImplement( Sbd_Man_t * p, int Pivot, word Truth )
     }
     // make sure delay reduction is achieved
     assert( Vec_IntEntry(p->vLutLevs, Abc_Lit2Var(iLit)) < iCurLev );
+    p->nChanges++;
     return 0;
 }
 
@@ -728,18 +1020,19 @@ void Sbd_ManDerive_rec( Gia_Man_t * pNew, Gia_Man_t * p, int Node, Vec_Int_t * v
 {
     Gia_Obj_t * pObj;
     int Obj = Node;
-    if ( Node < Vec_IntSize(vMirrors) && Vec_IntEntry(vMirrors, Node) >= 0 )
+    if ( Vec_IntEntry(vMirrors, Node) >= 0 )
         Obj = Abc_Lit2Var( Vec_IntEntry(vMirrors, Node) );
     pObj = Gia_ManObj( p, Obj );
-    if ( ~pObj->Value )
-        return;
-    assert( Gia_ObjIsAnd(pObj) );
-    Sbd_ManDerive_rec( pNew, p, Gia_ObjFaninId0(pObj, Obj), vMirrors );
-    Sbd_ManDerive_rec( pNew, p, Gia_ObjFaninId1(pObj, Obj), vMirrors );
-    if ( Gia_ObjIsXor(pObj) )
-        pObj->Value = Gia_ManHashXorReal( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
-    else
-        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    if ( !~pObj->Value )
+    {
+        assert( Gia_ObjIsAnd(pObj) );
+        Sbd_ManDerive_rec( pNew, p, Gia_ObjFaninId0(pObj, Obj), vMirrors );
+        Sbd_ManDerive_rec( pNew, p, Gia_ObjFaninId1(pObj, Obj), vMirrors );
+        if ( Gia_ObjIsXor(pObj) )
+            pObj->Value = Gia_ManHashXorReal( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        else
+            pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    }
     // set the original node as well
     if ( Obj != Node )
         Gia_ManObj(p, Node)->Value = Abc_LitNotCond( pObj->Value, Abc_LitIsCompl(Vec_IntEntry(vMirrors, Node)) );
@@ -766,7 +1059,6 @@ Gia_Man_t * Sbd_ManDerive( Gia_Man_t * p, Vec_Int_t * vMirrors )
     return pNew;
 }
 
-
 /**Function*************************************************************
 
   Synopsis    [Performs delay optimization for the given LUT size.]
@@ -782,18 +1074,28 @@ 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 Pivot; word Truth = 0;
+    int nNodesOld = Gia_ManObjNum(pGia);
+    int RetValue, Pivot; word Truth = 0;
     assert( pPars->nLutSize <= 6 );
     Gia_ManForEachAndId( pGia, Pivot )
     {
+        if ( Pivot >= nNodesOld )
+            break;
         if ( Sbd_ManComputeCut( p, Pivot ) )
             continue;
-        printf( "Looking at node %d\n", Pivot );
-        Sbd_ManWindow( p, Pivot );
-        if ( Sbd_ManExplore( p, Pivot, &Truth ) )
+        //if ( Pivot != 313 )
+        //    continue;
+        if ( p->pPars->fVerbose )
+            printf( "\nLooking at node %d\n", Pivot );
+        if ( Sbd_ManWindow( p, Pivot ) )
+            continue;
+        RetValue = Sbd_ManCheckConst( p, Pivot );
+        if ( RetValue >= 0 )
+            Vec_IntWriteEntry( p->vMirrors, Pivot, RetValue );
+        else if ( Sbd_ManExplore( p, Pivot, &Truth ) )
             Sbd_ManImplement( p, Pivot, Truth );
-        break;
     }
+    printf( "Found %d constants and %d replacements.\n", p->nConsts, p->nChanges );
     pNew = Sbd_ManDerive( pGia, p->vMirrors );
     Sbd_ManStop( p );
     return pNew;
diff --git a/src/opt/sbd/sbdWin.c b/src/opt/sbd/sbdWin.c
index 8f320038..50837e1f 100644
--- a/src/opt/sbd/sbdWin.c
+++ b/src/opt/sbd/sbdWin.c
@@ -46,46 +46,62 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots )
+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 )
 {
     Gia_Obj_t * pObj;
-    int i, iObj, Fan0, Fan1, Node, fCompl0, fCompl1, RetValue;
+    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);
+    //Vec_IntPrint( vWinObjs );
+    //Vec_IntPrint( vTfo );
+    //Vec_IntPrint( vRoots );
     // create SAT solver
     if ( pSat == NULL )
         pSat = sat_solver_new();
     else
         sat_solver_restart( pSat );
     sat_solver_setnvars( pSat, Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots) + 32 );
+    // create constant 0 clause
+    sat_solver_addclause( pSat, &iLit, &iLit + 1 );
     // add clauses for all nodes
-    Vec_IntForEachEntry( vWinObjs, iObj, i )
+    Vec_IntForEachEntryStart( vWinObjs, iObj, i, 1 )
     {
         pObj = Gia_ManObj( p, iObj );
         if ( Gia_ObjIsCi(pObj) )
             continue;
         assert( Gia_ObjIsAnd(pObj) );
+        assert( Vec_IntEntry( vMirrors, iObj ) < 0 );
         Node = Vec_IntEntry( vObj2Var, iObj );
-        Fan0 = Vec_IntEntry( vObj2Var, Gia_ObjFaninId0(pObj, iObj) );
-        Fan1 = Vec_IntEntry( vObj2Var, Gia_ObjFaninId1(pObj, iObj) );
-        fCompl0 = Gia_ObjFaninC0(pObj);
-        fCompl1 = Gia_ObjFaninC1(pObj);
+        Lit0m = Vec_IntEntry( vMirrors, Gia_ObjFaninId0(pObj, iObj) );
+        Lit1m = Vec_IntEntry( 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);
+        Fan0 = Vec_IntEntry( vObj2Var, Fan0 );
+        Fan1 = Vec_IntEntry( vObj2Var, Fan1 );
+        fCompl0 = Gia_ObjFaninC0(pObj) ^ (Lit0m >= 0 && Abc_LitIsCompl(Lit0m));
+        fCompl1 = Gia_ObjFaninC1(pObj) ^ (Lit1m >= 0 && Abc_LitIsCompl(Lit1m));
         if ( Gia_ObjIsXor(pObj) )
             sat_solver_add_xor( pSat, Node, Fan0, Fan1, fCompl0 ^ fCompl1 );
         else
             sat_solver_add_and( pSat, Node, Fan0, Fan1, fCompl0, fCompl1, 0 );
     }
     // add second clauses for the TFO
-    Vec_IntForEachEntryStart( vWinObjs, iObj, i, Vec_IntSize(vWinObjs) - Vec_IntSize(vTfo) )
+    Vec_IntForEachEntryStart( vWinObjs, iObj, i, TfoStart )
     {
         pObj = Gia_ManObj( p, iObj );
         assert( Gia_ObjIsAnd(pObj) );
+        assert( Vec_IntEntry( vMirrors, iObj ) < 0 );
         Node = Vec_IntEntry( vObj2Var, iObj ) + Vec_IntSize(vTfo);
-        Fan0 = Vec_IntEntry( vObj2Var, Gia_ObjFaninId0(pObj, iObj) );
-        Fan1 = Vec_IntEntry( vObj2Var, Gia_ObjFaninId1(pObj, iObj) );
-        Fan0 = Fan0 <= PivotVar ? Fan0 : Fan0 + Vec_IntSize(vTfo);
-        Fan1 = Fan1 <= PivotVar ? Fan1 : Fan1 + Vec_IntSize(vTfo);
-        fCompl0 = Gia_ObjFaninC0(pObj) ^ (Fan0 == PivotVar);
-        fCompl1 = Gia_ObjFaninC1(pObj) ^ (Fan1 == PivotVar);
+        Lit0m = Vec_IntEntry( vMirrors, Gia_ObjFaninId0(pObj, iObj) );
+        Lit1m = Vec_IntEntry( 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);
+        Fan0 = Vec_IntEntry( vObj2Var, Fan0 );
+        Fan1 = Vec_IntEntry( vObj2Var, Fan1 );
+        Fan0 = Fan0 < TfoStart ? Fan0 : Fan0 + Vec_IntSize(vTfo);
+        Fan1 = Fan1 < TfoStart ? Fan1 : Fan1 + Vec_IntSize(vTfo);
+        fCompl0 = Gia_ObjFaninC0(pObj) ^ (Fan0 == PivotVar) ^ (Lit0m >= 0 && Abc_LitIsCompl(Lit0m));
+        fCompl1 = Gia_ObjFaninC1(pObj) ^ (Fan1 == PivotVar) ^ (Lit1m >= 0 && Abc_LitIsCompl(Lit1m));
         if ( Gia_ObjIsXor(pObj) )
             sat_solver_add_xor( pSat, Node, Fan0, Fan1, fCompl0 ^ fCompl1 );
         else
@@ -98,8 +114,9 @@ sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, int Pivot, Vec_
         Vec_Int_t * vFaninVars = Vec_IntAlloc( Vec_IntSize(vRoots) );
         Vec_IntForEachEntry( vRoots, iObj, i )
         {
-            Vec_IntPush( vFaninVars, Abc_Var2Lit(nVars, 0) );
+            assert( Vec_IntEntry( vMirrors, iObj ) < 0 );
             Node = Vec_IntEntry( vObj2Var, iObj );
+            Vec_IntPush( vFaninVars, Abc_Var2Lit(nVars, 0) );
             sat_solver_add_xor( pSat, Node, Node + Vec_IntSize(vTfo), nVars++, 0 );
         }
         // make OR clause for the last nRoots variables
@@ -190,6 +207,50 @@ word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDi
     return SBD_SAT_SAT;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Returns a bunch of positive/negative random care minterms.]
+
+  Description [Returns 0/1 if the functions is const 0/1.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void sat_solver_random_polarity(sat_solver* s)
+{
+    int i, k;
+    for ( i = 0; i < s->size; i += 64 )
+    {
+        word Polar = Gia_ManRandomW(0);
+        for ( k = 0; k < 64 && (i << 6) + k < s->size; k++ )
+            s->polarity[(i << 6) + k] = Abc_TtGetBit(&Polar, k);
+    }
+}
+int Sbd_ManCollectConstants( sat_solver * pSat, int nCareMints[2], int PivotVar, word * pVarSims[], Vec_Int_t * vInds )
+{
+    int nBTLimit = 0;
+    int i, Ind; 
+    assert( Vec_IntSize(vInds) == nCareMints[0] + nCareMints[1] );
+    Vec_IntForEachEntry( vInds, Ind, i )
+    {
+        int fOffSet = (int)(i < nCareMints[0]);
+        int status, k, iLit = Abc_Var2Lit( PivotVar, fOffSet );
+        sat_solver_random_polarity( pSat );
+        status = sat_solver_solve( pSat, &iLit, &iLit + 1, nBTLimit, 0, 0, 0 );
+        if ( status == l_Undef )
+            return -2;
+        if ( status == l_False )
+            return fOffSet;
+        for ( k = 0; k <= PivotVar; k++ )
+            if ( Abc_TtGetBit(pVarSims[k], Ind) != sat_solver_var_value(pSat, k) )
+                Abc_TtXorBit(pVarSims[k], Ind);
+    }
+    return -1;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////