Updates to delay optimization project.

6 files changed, 551 insertions, 63 deletions

diff --git a/src/opt/sbd/module.make b/src/opt/sbd/module.make
index d966e577..0320d381 100644
--- a/src/opt/sbd/module.make
+++ b/src/opt/sbd/module.make
@@ -1,5 +1,6 @@
 SRC +=    src/opt/sbd/sbd.c \
     src/opt/sbd/sbdCnf.c \
     src/opt/sbd/sbdCore.c \
+    src/opt/sbd/sbdLut.c \
     src/opt/sbd/sbdSat.c \
     src/opt/sbd/sbdWin.c
diff --git a/src/opt/sbd/sbdCore.c b/src/opt/sbd/sbdCore.c
index b6ec70f9..563e6e98 100644
--- a/src/opt/sbd/sbdCore.c
+++ b/src/opt/sbd/sbdCore.c
@@ -54,10 +54,12 @@ struct Sbd_Man_t_
     abctime         timeTotal;
     // target node
     int             Pivot;       // target node
+    int             DivCutoff;   // the place where D-2 divisors begin
     Vec_Int_t *     vTfo;        // TFO (excludes node, includes roots) - precomputed
     Vec_Int_t *     vRoots;      // TFO root nodes
     Vec_Int_t *     vWinObjs;    // TFI + Pivot + sideTFI + TFO (including roots)
     Vec_Int_t *     vObj2Var;    // SAT variables for the window (indexes of objects in vWinObjs)
+    Vec_Int_t *     vDivSet;     // divisor variables
     Vec_Int_t *     vDivVars;    // divisor variables
     Vec_Int_t *     vDivValues;  // SAT variables values for the divisor variables
     Vec_Wec_t *     vDivLevels;  // divisors collected by levels
@@ -200,6 +202,7 @@ Sbd_Man_t * Sbd_ManStart( Gia_Man_t * pGia, Sbd_Par_t * pPars )
     p->vRoots     = Vec_IntAlloc( 100 );
     p->vWinObjs   = Vec_IntAlloc( Gia_ManObjNum(pGia) );
     p->vObj2Var   = Vec_IntStart( Gia_ManObjNum(pGia) );
+    p->vDivSet    = Vec_IntAlloc( 100 );
     p->vDivVars   = Vec_IntAlloc( 100 );
     p->vDivValues = Vec_IntAlloc( 100 );
     p->vDivLevels = Vec_WecAlloc( 100 );
@@ -234,6 +237,7 @@ void Sbd_ManStop( Sbd_Man_t * p )
     Vec_IntFree( p->vRoots );
     Vec_IntFree( p->vWinObjs );
     Vec_IntFree( p->vObj2Var );
+    Vec_IntFree( p->vDivSet );
     Vec_IntFree( p->vDivVars );
     Vec_IntFree( p->vDivValues );
     Vec_WecFree( p->vDivLevels );
@@ -318,12 +322,11 @@ void Sbd_ManUpdateOrder( Sbd_Man_t * p, int Pivot )
     Vec_WecInit( p->vDivLevels, LevelMax + 1 );
     Vec_IntForEachEntry( p->vWinObjs, Node, i )
         Vec_WecPush( p->vDivLevels, Vec_IntEntry(p->vLutLevs, Node), Node );
-    // sort primary inputs
-    Vec_IntSort( Vec_WecEntry(p->vDivLevels, 0), 0 );
     // reload divisors
     Vec_IntClear( p->vWinObjs );
     Vec_WecForEachLevel( p->vDivLevels, vLevel, i )
     {
+        Vec_IntSort( vLevel, 0 );
         Vec_IntForEachEntry( vLevel, Node, k )
         {
             Vec_IntWriteEntry( p->vObj2Var, Node, Vec_IntSize(p->vWinObjs) );
@@ -334,8 +337,26 @@ void Sbd_ManUpdateOrder( Sbd_Man_t * p, int Pivot )
             nTimeValidDivs = Vec_IntSize(p->vWinObjs);
     }
     assert( nTimeValidDivs > 0 );
-    Vec_IntFill( p->vDivValues, Abc_MinInt(63, nTimeValidDivs), 0 );
-    //printf( "%d ", Abc_MinInt(63, nTimeValidDivs) );
+    Vec_IntClear( p->vDivVars );
+    p->DivCutoff = -1;
+    Vec_IntForEachEntryStartStop( p->vWinObjs, Node, i, Abc_MaxInt(0, nTimeValidDivs-63), nTimeValidDivs )
+    {
+        if ( p->DivCutoff == -1 && Vec_IntEntry(p->vLutLevs, Node) == LevelMax - 2 )
+            p->DivCutoff = Vec_IntSize(p->vDivVars);
+        Vec_IntPush( p->vDivVars, i );
+    }
+    if ( p->DivCutoff == -1 )
+        p->DivCutoff = 0;
+    // verify
+    assert( Vec_IntSize(p->vDivVars) < 64 );
+    Vec_IntForEachEntryStart( p->vDivVars, Node, i, p->DivCutoff )
+        assert( Vec_IntEntry(p->vLutLevs, Vec_IntEntry(p->vWinObjs, Node)) == LevelMax - 2 );
+    Vec_IntForEachEntryStop( p->vDivVars, Node, i, p->DivCutoff )
+        assert( Vec_IntEntry(p->vLutLevs, Vec_IntEntry(p->vWinObjs, Node)) < LevelMax - 2 );
+    Vec_IntFill( p->vDivValues, Vec_IntSize(p->vDivVars), 0 );
+    //printf( "%d ", Vec_IntSize(p->vDivVars) );
+//    printf( "Node %4d :  Win = %5d.   Divs = %5d.    D1 = %5d.  D2 = %5d.\n",  
+//        Pivot, Vec_IntSize(p->vWinObjs), Vec_IntSize(p->vDivVars), Vec_IntSize(p->vDivVars)-p->DivCutoff, p->DivCutoff );
 }
 void Sbd_ManWindowSim_rec( Sbd_Man_t * p, int NodeInit )
 {
@@ -408,6 +429,8 @@ int Sbd_ManWindow( Sbd_Man_t * p, int Pivot )
     Gia_ObjSetTravIdCurrentId(p->pGia, 0);
     Sbd_ManWindowSim_rec( p, Pivot );
     Sbd_ManUpdateOrder( p, Pivot );
+    assert( Vec_IntSize(p->vDivVars) == Vec_IntSize(p->vDivValues) );
+    assert( Vec_IntSize(p->vDivVars) < Vec_IntSize(p->vWinObjs) );
     // simulate node
     Gia_ManObj(p->pGia, Pivot)->fMark0 = 1;
     Abc_TtCopy( Sbd_ObjSim1(p, Pivot), Sbd_ObjSim0(p, Pivot), p->pPars->nWords, 1 );
@@ -440,8 +463,8 @@ int Sbd_ManWindow( Sbd_Man_t * p, int Pivot )
     p->timeWin += Abc_Clock() - clk;
     // propagate controlability to fanins for the TFI nodes starting from the pivot
     Sbd_ManPropagateControl( p, Pivot );
-    assert( Vec_IntSize(p->vDivValues) < 64 );
-    return (int)(Vec_IntSize(p->vDivValues) >= 64);
+    assert( Vec_IntSize(p->vDivValues) <= 64 );
+    return (int)(Vec_IntSize(p->vDivValues) > 64);
 }
 
 /**Function*************************************************************
@@ -466,8 +489,8 @@ int Sbd_ManCheckConst( Sbd_Man_t * p, int 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 );
+    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 )
     {
@@ -836,11 +859,11 @@ static inline int Sbd_ManFindCandsSimple( Sbd_Man_t * p, word Cover[64], int nDi
 {
     int c0, c1, c2, c3;
     word Target = Cover[nDivs];
-    Vec_IntClear( p->vDivVars );
+    Vec_IntClear( p->vDivSet );
     for ( c0 = 0;    c0 < nDivs; c0++ )
         if ( Cover[c0] == Target )
         {
-            Vec_IntPush( p->vDivVars, c0 );
+            Vec_IntPush( p->vDivSet, c0 );
             return 1;
         }
 
@@ -848,8 +871,8 @@ static inline int Sbd_ManFindCandsSimple( Sbd_Man_t * p, word Cover[64], int nDi
     for ( c1 = c0+1; c1 < nDivs; c1++ )
         if ( (Cover[c0] | Cover[c1]) == Target )
         {
-            Vec_IntPush( p->vDivVars, c0 );
-            Vec_IntPush( p->vDivVars, c1 );
+            Vec_IntPush( p->vDivSet, c0 );
+            Vec_IntPush( p->vDivSet, c1 );
             return 1;
         }
 
@@ -858,9 +881,9 @@ static inline int Sbd_ManFindCandsSimple( Sbd_Man_t * p, word Cover[64], int nDi
     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 );
+            Vec_IntPush( p->vDivSet, c0 );
+            Vec_IntPush( p->vDivSet, c1 );
+            Vec_IntPush( p->vDivSet, c2 );
             return 1;
         }
 
@@ -871,10 +894,10 @@ static inline int Sbd_ManFindCandsSimple( Sbd_Man_t * p, word Cover[64], int nDi
     {
         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 );
+            Vec_IntPush( p->vDivSet, c0 );
+            Vec_IntPush( p->vDivSet, c1 );
+            Vec_IntPush( p->vDivSet, c2 );
+            Vec_IntPush( p->vDivSet, c3 );
             return 1;
         }
     }
@@ -891,11 +914,11 @@ static inline int Sbd_ManFindCands( Sbd_Man_t * p, word Cover[64], int nDivs )
     if ( nDivs < 8 || p->pPars->fCover )
         return Sbd_ManFindCandsSimple( p, Cover, nDivs );
 
-    Vec_IntClear( p->vDivVars );
+    Vec_IntClear( p->vDivSet );
     for ( c0 = 0; c0 < nDivs; c0++ )
         if ( Cover[c0] == Target )
         {
-            Vec_IntPush( p->vDivVars, c0 );
+            Vec_IntPush( p->vDivSet, c0 );
             return 1;
         }
 
@@ -903,8 +926,8 @@ static inline int Sbd_ManFindCands( Sbd_Man_t * p, word Cover[64], int nDivs )
     for ( c1 = c0+1; c1 < nDivs; c1++ )
         if ( (Cover[c0] | Cover[c1]) == Target )
         {
-            Vec_IntPush( p->vDivVars, c0 );
-            Vec_IntPush( p->vDivVars, c1 );
+            Vec_IntPush( p->vDivSet, c0 );
+            Vec_IntPush( p->vDivSet, c1 );
             return 1;
         }
 
@@ -923,9 +946,9 @@ static inline int Sbd_ManFindCands( Sbd_Man_t * p, word Cover[64], int nDivs )
     for ( c2 = c1+1; c2 < Limits[2]; c2++ )
         if ( (Cover[Order[c0]] | Cover[Order[c1]] | Cover[Order[c2]]) == Target )
         {
-            Vec_IntPush( p->vDivVars, Order[c0] );
-            Vec_IntPush( p->vDivVars, Order[c1] );
-            Vec_IntPush( p->vDivVars, Order[c2] );
+            Vec_IntPush( p->vDivSet, Order[c0] );
+            Vec_IntPush( p->vDivSet, Order[c1] );
+            Vec_IntPush( p->vDivSet, Order[c2] );
             return 1;
         }
 
@@ -936,10 +959,10 @@ static inline int Sbd_ManFindCands( Sbd_Man_t * p, word Cover[64], int nDivs )
     {
         if ( (Cover[Order[c0]] | Cover[Order[c1]] | Cover[Order[c2]] | Cover[Order[c3]]) == Target )
         {
-            Vec_IntPush( p->vDivVars, Order[c0] );
-            Vec_IntPush( p->vDivVars, Order[c1] );
-            Vec_IntPush( p->vDivVars, Order[c2] );
-            Vec_IntPush( p->vDivVars, Order[c3] );
+            Vec_IntPush( p->vDivSet, Order[c0] );
+            Vec_IntPush( p->vDivSet, Order[c1] );
+            Vec_IntPush( p->vDivSet, Order[c2] );
+            Vec_IntPush( p->vDivSet, Order[c3] );
             return 1;
         }
     }
@@ -952,10 +975,10 @@ 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 );
+    extern word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDivSet, Vec_Int_t * vDivVars, Vec_Int_t * vDivValues, Vec_Int_t * vTemp );
 
     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 i, k, n, Node, Index, nCubes[2] = {0}, nRows = 0, nRowsOld;
 
     int nDivs = Vec_IntSize(p->vDivValues);
     int PivotVar = Vec_IntEntry(p->vObj2Var, Pivot);
@@ -969,11 +992,11 @@ int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth )
         Sbd_ManPrintObj( p, Pivot );
 
     // collect bit-matrices
-    for ( i = 0; i < nDivs; i++ )
+    Vec_IntForEachEntry( p->vDivVars, Node, 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, Vec_IntEntry(p->vWinObjs, Node) );
+        MatrC[0][63-i] = *Sbd_ObjSim2( p, Vec_IntEntry(p->vWinObjs, Node) );
+        MatrC[1][63-i] = *Sbd_ObjSim3( p, Vec_IntEntry(p->vWinObjs, Node) );
     }
     MatrS[63-i]    = *Sbd_ObjSim0( p, Pivot );
     MatrC[0][63-i] = *Sbd_ObjSim2( p, Pivot );
@@ -1067,10 +1090,10 @@ int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth )
     
         if ( p->pPars->fVerbose )
             printf( "Candidate support:  " ),
-            Vec_IntPrint( p->vDivVars );
+            Vec_IntPrint( p->vDivSet );
 
         clk = Abc_Clock();
-        *pTruth = Sbd_ManSolve( p->pSat, PivotVar, FreeVar+nIters, p->vDivVars, p->vDivValues, p->vLits );
+        *pTruth = Sbd_ManSolve( p->pSat, PivotVar, FreeVar+nIters, p->vDivSet, p->vDivVars, p->vDivValues, p->vLits );
         clkSat += Abc_Clock() - clk;
 
         if ( *pTruth == SBD_SAT_UNDEC )
@@ -1103,7 +1126,7 @@ int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth )
             if ( p->pPars->fVerbose )
             {
                 printf( "Node %d:  UNSAT.\n", Pivot );
-                Extra_PrintBinary( stdout, (unsigned *)pTruth, 1 << Vec_IntSize(p->vDivVars) ), printf( "\n" );
+                Extra_PrintBinary( stdout, (unsigned *)pTruth, 1 << Vec_IntSize(p->vDivSet) ), printf( "\n" );
             }
             RetValue = 1;
             break;
@@ -1118,6 +1141,13 @@ int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth )
     return RetValue;
 }
 
+int Sbd_ManExplore2( Sbd_Man_t * p, int Pivot, 
+                     int nLuts, int nSels, int nVarsDivs[SBD_LUTS_MAX], 
+                     int pVarsDivs[SBD_LUTS_MAX][SBD_SIZE_MAX], word Truths[SBD_LUTS_MAX] )
+{
+    return 0;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Computes delay-oriented k-feasible cut at the node.]
@@ -1233,7 +1263,7 @@ int Sbd_ManMergeCuts( Sbd_Man_t * p, int Node )
     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 );
+//printf( "Setting node %d with delay %d.\n", Node, LevCur );
     return LevCur == 1; // LevCur == Abc_MaxInt(Level0, Level1);
 }
 int Sbd_ManDelay( Sbd_Man_t * p )
@@ -1306,7 +1336,7 @@ int Sbd_ManImplement( Sbd_Man_t * p, int Pivot, word Truth )
     int iNewLev;
     // collect leaf literals
     Vec_IntClear( p->vLits );
-    Vec_IntForEachEntry( p->vDivVars, Node, i )
+    Vec_IntForEachEntry( p->vDivSet, Node, i )
     {
         Node = Vec_IntEntry( p->vWinObjs, Node );
         if ( Vec_IntEntry(p->vMirrors, Node) >= 0 )
@@ -1429,20 +1459,68 @@ 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 );
+
     int RetValue; word Truth = 0;
     if ( Sbd_ManMergeCuts( p, Pivot ) )
         return;
-    //if ( Pivot != 344 )
-    //    continue;
+
+//    if ( Pivot != 13 )
+//        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 );
+    }
     else if ( Sbd_ManExplore( p, Pivot, &Truth ) )
+    {
         Sbd_ManImplement( p, Pivot, Truth );
+        //printf( "    --> Pivot %4d.  Supp %d.\n", Pivot, Vec_IntSize(p->vDivSet) );
+    }
+/*
+    else
+    {
+        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, word Truths[SBD_LUTS_MAX] 
+                                   );
+
+        Sbd_Str_t Strs[2] = {
+            {1, 4, {0, 1, 2, 7}},
+            {1, 4, {3, 4, 5, 6}}
+        };
+
+        word Truths[SBD_LUTS_MAX];
+
+        Vec_Int_t * vDivSet = Vec_IntAlloc( 8 );
+
+        int i, RetValue;
+        
+        for ( i = 0; i < 7; i++ )
+            Vec_IntPush( vDivSet, i+1 );
+
+        RetValue = Sbd_ProblemSolve( p->pGia, p->vMirrors, 
+                                     Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots,
+                                     vDivSet, 2, Strs, Truths );
+        if ( RetValue )
+        {
+            printf( "Solving succeded.\n" );
+            //Sbd_ManImplement2( p, Pivot, Truth, nLuts, nSels, nVarsDivs, pVarsDivs, Truths );
+        }
+        Vec_IntFree( vDivSet );
+    }
+*/
 }
 Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
 {
@@ -1488,8 +1566,10 @@ Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
     else
     {
         Gia_ManForEachAndId( pGia, Pivot )
+        {
             if ( Pivot < nNodesOld )
                 Sbd_NtkPerformOne( p, Pivot );
+        }
     }
     printf( "Found %d constants and %d replacements with delay %d.  ", p->nConsts, p->nChanges, Sbd_ManDelay(p) );
     p->timeTotal = Abc_Clock() - p->timeTotal;
diff --git a/src/opt/sbd/sbdInt.h b/src/opt/sbd/sbdInt.h
index 4c553fb4..3646c6b9 100644
--- a/src/opt/sbd/sbdInt.h
+++ b/src/opt/sbd/sbdInt.h
@@ -52,10 +52,21 @@ ABC_NAMESPACE_HEADER_START
 #define SBD_SAT_UNDEC 0x1234567812345678
 #define SBD_SAT_SAT   0x8765432187654321
 
+#define SBD_LUTS_MAX  2
+#define SBD_SIZE_MAX  4
+#define SBD_DIV_MAX   7
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
 
+typedef struct Sbd_Str_t_ Sbd_Str_t;
+struct Sbd_Str_t_
+{
+    int               fLut;                 // LUT or SEL
+    int               nVarIns;              // input count
+    int               VarIns[SBD_DIV_MAX];  // input vars
+};
 
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
diff --git a/src/opt/sbd/sbdLut.c b/src/opt/sbd/sbdLut.c
new file mode 100644
index 00000000..42bb0955
--- /dev/null
+++ b/src/opt/sbd/sbdLut.c
@@ -0,0 +1,255 @@
+/**CFile****************************************************************
+
+  FileName    [sbdLut.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based optimization using internal don't-cares.]
+
+  Synopsis    [CNF computation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: sbdLut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sbdInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+// count the number of parameter variables in the structure
+int Sbd_ProblemCountParams( int nStrs, Sbd_Str_t * pStr0 )
+{
+    Sbd_Str_t * pStr;  int nPars = 0;
+    for ( pStr = pStr0; pStr < pStr0 + nStrs; pStr++ )
+        nPars += (pStr->fLut ? 1 << pStr->nVarIns : pStr->nVarIns);
+    return nPars;
+}
+// add clauses for the structure
+void Sbd_ProblemAddClauses( sat_solver * pSat, int nVars, int nStrs, int * pVars, Sbd_Str_t * pStr0 )
+{   
+    // variable order:  inputs, structure outputs, parameters
+    Sbd_Str_t * pStr;
+    int VarOut = nVars;
+    int VarPar = nVars + nStrs;
+    int m, k, n, status, pLits[SBD_SIZE_MAX+2];
+    for ( pStr = pStr0; pStr < pStr0 + nStrs; pStr++, VarOut++ )
+    {
+        if ( pStr->fLut )
+        {
+            int nMints = 1 << pStr->nVarIns;
+            assert( pStr->nVarIns <= 6 );
+            for ( m = 0; m < nMints; m++, VarPar++ )
+            {
+                for ( k = 0; k < pStr->nVarIns; k++ )
+                    pLits[k] = Abc_Var2Lit( pVars[pStr->VarIns[k]], (m >> k) & 1 ); 
+                for ( n = 0; n < 2; n++ )
+                {
+                    pLits[pStr->nVarIns]   = Abc_Var2Lit( pVars[VarPar], n );
+                    pLits[pStr->nVarIns+1] = Abc_Var2Lit( pVars[VarOut], !n );
+                    status = sat_solver_addclause( pSat, pLits, pLits + pStr->nVarIns + 2 );
+                    assert( status );
+                }
+            }
+        }
+        else
+        {
+            for ( k = 0; k < pStr->nVarIns; k++, VarPar++ )
+            {
+                for ( n = 0; n < 2; n++ )
+                {
+                    pLits[0] = Abc_Var2Lit( pVars[VarPar], 1 );
+                    pLits[1] = Abc_Var2Lit( pVars[VarOut], n );
+                    pLits[2] = Abc_Var2Lit( pVars[pStr->VarIns[k]], !n );
+                    status = sat_solver_addclause( pSat, pLits, pLits + 3 );
+                    assert( status );
+                }
+            }
+        }
+    }
+}
+void Sbd_ProblemAddClausesInit( sat_solver * pSat, int nVars, int nStrs, int * pVars, Sbd_Str_t * pStr0 )
+{
+    Sbd_Str_t * pStr;
+    int VarPar = nVars + nStrs;
+    int m, m2, pLits[2], status;
+    // make sure selector parameters are mutually exclusive
+    for ( pStr = pStr0; pStr < pStr0 + nStrs; pStr++, VarPar = pStr->fLut ? 1 << pStr->nVarIns : pStr->nVarIns )
+    {
+        if ( pStr->fLut )
+            continue;
+        for ( m = 0; m < pStr->nVarIns; m++ )
+        for ( m2 = m+1; m2 < pStr->nVarIns; m2++ )
+        {
+            pLits[0] = Abc_Var2Lit( pVars[VarPar + m], 1 );
+            pLits[1] = Abc_Var2Lit( pVars[VarPar + m2], 1 );
+            status = sat_solver_addclause( pSat, pLits, pLits + 2 );
+            assert( status );
+        }
+    }
+}
+void Sbd_ProblemPrintSolution( int nStrs, Sbd_Str_t * pStr0, Vec_Int_t * vLits )
+{
+    Sbd_Str_t * pStr;
+    int m, nIters, iLit = 0;
+    printf( "Solution found:\n" );
+    for ( pStr = pStr0; pStr < pStr0 + nStrs; pStr++ )
+    {
+        nIters = pStr->fLut ? 1 << pStr->nVarIns : pStr->nVarIns;
+        printf( "%s%d : ", pStr->fLut ? "LUT":"SEL", pStr-pStr0 );
+        for ( m = 0; m < nIters; m++ )
+            printf( "%d", Abc_LitIsCompl(Vec_IntEntry(vLits, iLit++)) );
+        printf( "\n" );
+    }
+    assert( iLit == Vec_IntSize(vLits) );
+}
+void Sbd_ProblemCollectSolution( int nStrs, Sbd_Str_t * pStr0, Vec_Int_t * vLits, word Truths[SBD_LUTS_MAX] )
+{
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Solves QBF problem for the given window.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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, word Truths[SBD_LUTS_MAX] )  // divisors, structures
+{
+    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 );
+    
+    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 nVars      = Vec_IntSize( vDivSet );
+    int nPars      = Sbd_ProblemCountParams( nStrs, pStr0 );
+
+    int VarCecOut  = Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots);
+    int VarCecPar  = VarCecOut + 1;
+    int VarCecFree = VarCecPar + nPars;
+
+    int VarQbfPar  = 0;
+    int VarQbfFree = nPars;
+
+    int pVarsCec[256];
+    int pVarsQbf[256];
+    int i, iVar, iLit;
+    int RetValue = 0;
+
+    assert( Vec_IntSize(vDivSet) <= SBD_SIZE_MAX );
+    assert( nVars + nStrs + nPars <= 256 );
+
+    // collect CEC variables
+    Vec_IntForEachEntry( vDivSet, iVar, i )
+        pVarsCec[i] = iVar;
+    pVarsCec[nVars] = VarCecOut;
+    for ( i = 1; i < nStrs; i++ )
+        pVarsCec[nVars + i] = VarCecFree++;
+    for ( i = 0; i < nPars; i++ )
+        pVarsCec[nVars + nStrs + i] = VarCecPar + i;
+
+    // collect QBF variables
+    for ( i = 0; i < nVars + nStrs; i++ )
+        pVarsQbf[i] = -1;
+    for ( i = 0; i < nPars; i++ )
+        pVarsQbf[nVars + nStrs + i] = VarQbfPar + i;
+
+    // add clauses to the CEC problem
+    Sbd_ProblemAddClauses( pSatCec, nVars, nStrs, pVarsCec, pStr0 );
+
+    // create QBF solver
+    sat_solver_setnvars( pSatQbf, 1000 );
+    Sbd_ProblemAddClausesInit( pSatQbf, nVars, nStrs, pVarsQbf, pStr0 );
+
+    // assume all parameter variables are 0
+    Vec_IntClear( vLits );
+    for ( i = 0; i < nPars; i++ )
+        Vec_IntPush( vLits, Abc_Var2Lit(VarCecPar + i, 1) );
+    while ( 1 )
+    {
+        // check if these parameters solve the problem
+        int status = sat_solver_solve( pSatCec, Vec_IntArray(vLits), Vec_IntLimit(vLits), 0, 0, 0, 0 );
+        if ( status == l_False ) // solution found
+            break;
+        assert( status == l_True );
+        Vec_IntClear( vLits );
+        // create new QBF variables
+        for ( i = 0; i < nVars + nStrs; i++ )
+            pVarsQbf[i] = VarQbfFree++;
+        // set their values
+        Vec_IntForEachEntry( vDivSet, iVar, i )
+        {
+            iLit = Abc_Var2Lit( pVarsQbf[i], sat_solver_var_value(pSatCec, iVar) );
+            status = sat_solver_addclause( pSatQbf, &iLit, &iLit + 1 );
+            assert( status );
+        }
+        iLit = Abc_Var2Lit( pVarsQbf[nVars], sat_solver_var_value(pSatCec, VarCecOut) );
+        status = sat_solver_addclause( pSatQbf, &iLit, &iLit + 1 );
+        assert( status );
+        // add clauses to the QBF problem
+        Sbd_ProblemAddClauses( pSatQbf, nVars, nStrs, pVarsQbf, pStr0 );
+        // check if solution still exists
+        status = sat_solver_solve( pSatQbf, NULL, NULL, 0, 0, 0, 0 );
+        if ( status == l_False ) // solution does not exist
+            break;
+        assert( status == l_True ); 
+        // find the new values of parameters
+        assert( Vec_IntSize(vLits) == 0 );
+        for ( i = 0; i < nPars; i++ )
+            Vec_IntPush( vLits, Abc_Var2Lit(VarCecPar + i, sat_solver_var_value(pSatQbf, VarQbfPar + i)) );
+    }
+    if ( Vec_IntSize(vLits) > 0 )
+    {
+        Sbd_ProblemPrintSolution( nStrs, pStr0, vLits );
+        Sbd_ProblemCollectSolution( nStrs, pStr0, vLits, Truths );
+        RetValue = 1;
+    }
+    else 
+        printf( "Solution does not exist.\n" );
+
+    sat_solver_delete( pSatCec );
+    sat_solver_delete( pSatQbf );
+    Vec_IntFree( vLits );
+    return RetValue;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/sbd/sbdSat.c b/src/opt/sbd/sbdSat.c
index ae865627..f0de4dbf 100644
--- a/src/opt/sbd/sbdSat.c
+++ b/src/opt/sbd/sbdSat.c
@@ -37,10 +37,6 @@ ABC_NAMESPACE_IMPL_START
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-#define SBD_LUTS_MAX   2
-#define SBD_SIZE_MAX   4
-#define SBD_DIV_MAX   16
-
 // new AIG manager
 typedef struct Sbd_Pro_t_ Sbd_Pro_t;
 struct Sbd_Pro_t_
diff --git a/src/opt/sbd/sbdWin.c b/src/opt/sbd/sbdWin.c
index d722f456..fc79caa7 100644
--- a/src/opt/sbd/sbdWin.c
+++ b/src/opt/sbd/sbdWin.c
@@ -39,19 +39,26 @@ ABC_NAMESPACE_IMPL_START
   a DFS ordered array of objects (vWinObjs) whose indexed in the array
   (which will be used as SAT variables) are given in array vObj2Var.
   The TFO nodes are listed as the last ones in vWinObjs. The root nodes
-  are labeled with Abc_LitIsCompl() in vTfo and also given in vRoots.]
+  are labeled with Abc_LitIsCompl() in vTfo and also given in vRoots.
+  If fQbf is 1, returns the instance meant for QBF solving. It is using
+  the last variable (LastVar) as the placeholder for the second copy
+  of the pivot node.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-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 )
+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 )
 {
     Gia_Obj_t * pObj;
+    int nAddVars = 64;
     int i, iLit = 1, iObj, Fan0, Fan1, Lit0m, Lit1m, Node, fCompl0, fCompl1, RetValue;
     int TfoStart = Vec_IntSize(vWinObjs) - Vec_IntSize(vTfo);
     int PivotVar = Vec_IntEntry(vObj2Var, Pivot);
+    int LastVar = Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots);
     //Vec_IntPrint( vWinObjs );
     //Vec_IntPrint( vTfo );
     //Vec_IntPrint( vRoots );
@@ -60,7 +67,7 @@ sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMi
         pSat = sat_solver_new();
     else
         sat_solver_restart( pSat );
-    sat_solver_setnvars( pSat, Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots) + 32 );
+    sat_solver_setnvars( pSat, Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots) + nAddVars );
     // create constant 0 clause
     sat_solver_addclause( pSat, &iLit, &iLit + 1 );
     // add clauses for all nodes
@@ -100,8 +107,13 @@ sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMi
         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 ( fQbf )
+        {
+            Fan0 = Fan0 == PivotVar ? LastVar : Fan0;
+            Fan1 = Fan1 == PivotVar ? LastVar : Fan1;
+        }
+        fCompl0 = Gia_ObjFaninC0(pObj) ^ (!fQbf && Fan0 == PivotVar) ^ (Lit0m >= 0 && Abc_LitIsCompl(Lit0m));
+        fCompl1 = Gia_ObjFaninC1(pObj) ^ (!fQbf && Fan1 == PivotVar) ^ (Lit1m >= 0 && Abc_LitIsCompl(Lit1m));
         if ( Gia_ObjIsXor(pObj) )
             sat_solver_add_xor( pSat, Node, Fan0, Fan1, fCompl0 ^ fCompl1 );
         else
@@ -127,7 +139,7 @@ sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMi
             sat_solver_delete( pSat );
             return NULL;
         }
-        assert( sat_solver_nvars(pSat) == nVars + 32 );
+        assert( sat_solver_nvars(pSat) == nVars + nAddVars );
     }
     // finalize
     RetValue = sat_solver_simplify( pSat );
@@ -143,7 +155,7 @@ sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMi
 
   Synopsis    [Solves one SAT problem.]
 
-  Description [Computes node function for PivotVar with fanins in vDivVars
+  Description [Computes node function for PivotVar with fanins in vDivSet
   using don't-care represented in the SAT solver. Uses array vValues to 
   return the values of the first Vec_IntSize(vValues) SAT variables in case
   the implementation of the node with the given fanins does not exist.]
@@ -153,12 +165,13 @@ sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMi
   SeeAlso     []
 
 ***********************************************************************/
-word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDivVars, Vec_Int_t * vValues, Vec_Int_t * vTemp )
+word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDivSet, Vec_Int_t * vDivVars, Vec_Int_t * vDivValues, Vec_Int_t * vTemp )
 {
     int nBTLimit = 0;
     word uCube, uTruth = 0;
     int status, i, iVar, nFinal, * pFinal, pLits[2], nIter = 0;
     assert( FreeVar < sat_solver_nvars(pSat) );
+    assert( Vec_IntSize(vDivVars) == Vec_IntSize(vDivValues) );
     pLits[0] = Abc_Var2Lit( PivotVar, 0 ); // F = 1
     pLits[1] = Abc_Var2Lit( FreeVar, 0 );  // iNewLit
     while ( 1 ) 
@@ -171,12 +184,12 @@ word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDi
             return uTruth;
         assert( status == l_True );
         // remember variable values
-        for ( i = 0; i < Vec_IntSize(vValues); i++ )
-            Vec_IntWriteEntry( vValues, i, 2*sat_solver_var_value(pSat, i) );
+        Vec_IntForEachEntry( vDivVars, iVar, i )
+            Vec_IntWriteEntry( vDivValues, i, 2*sat_solver_var_value(pSat, iVar) );
         // collect divisor literals
         Vec_IntClear( vTemp );
         Vec_IntPush( vTemp, Abc_LitNot(pLits[0]) ); // F = 0
-        Vec_IntForEachEntry( vDivVars, iVar, i )
+        Vec_IntForEachEntry( vDivSet, iVar, i )
             Vec_IntPush( vTemp, sat_solver_var_literal(pSat, iVar) );
         // check against offset
         status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntArray(vTemp) + Vec_IntSize(vTemp), nBTLimit, 0, 0, 0 );
@@ -195,7 +208,7 @@ word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDi
             if ( pFinal[i] == pLits[0] )
                 continue;
             Vec_IntPush( vTemp, pFinal[i] );
-            iVar = Vec_IntFind( vDivVars, Abc_Lit2Var(pFinal[i]) );   assert( iVar >= 0 );
+            iVar = Vec_IntFind( vDivSet, Abc_Lit2Var(pFinal[i]) );   assert( iVar >= 0 );
             uCube &= Abc_LitIsCompl(pFinal[i]) ? s_Truths6[iVar] : ~s_Truths6[iVar];
         }
         uTruth |= uCube;
@@ -205,11 +218,11 @@ 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, sat_solver_var_value(pSat, i) );
+    Vec_IntForEachEntry( vDivVars, iVar, i )
+        Vec_IntAddToEntry( vDivValues, i, sat_solver_var_value(pSat, iVar) );
 
-    for ( i = 0; i < Vec_IntSize(vValues); i++ )
-        Vec_IntAddToEntry( vValues, i, 0xC );
+    for ( i = 0; i < Vec_IntSize(vDivValues); i++ )
+        Vec_IntAddToEntry( vDivValues, i, 0xC );
 /*
     // reduce the counter example
     for ( n = 0; n < 2; n++ )
@@ -232,6 +245,138 @@ word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDi
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sbd_ManSolve2( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDivVars, Vec_Int_t * vDivValues, Vec_Int_t * vTemp, Vec_Int_t * vSop )
+{
+    int nBTLimit = 0;
+    int status, i, iVar, nFinal, * pFinal, pLits[2], nIter = 0;
+    assert( FreeVar < sat_solver_nvars(pSat) );
+    assert( Vec_IntSize(vDivVars) == Vec_IntSize(vDivValues) );
+    pLits[0] = Abc_Var2Lit( PivotVar, 0 ); // F = 1
+    pLits[1] = Abc_Var2Lit( FreeVar, 0 );  // iNewLit
+    Vec_IntClear( vSop );
+    while ( 1 ) 
+    {
+        // find onset minterm
+        status = sat_solver_solve( pSat, pLits, pLits + 2, nBTLimit, 0, 0, 0 );
+        if ( status == l_Undef )
+            return 0;
+        if ( status == l_False )
+            return 1;
+        assert( status == l_True );
+        // remember variable values
+        //for ( i = 0; i < Vec_IntSize(vValues); 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
+        //Vec_IntForEachEntry( vDivSet, iVar, i )
+        Vec_IntForEachEntry( vDivVars, iVar, i )
+            Vec_IntPush( vTemp, sat_solver_var_literal(pSat, iVar) );
+        // check against offset
+        status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntArray(vTemp) + Vec_IntSize(vTemp), nBTLimit, 0, 0, 0 );
+        if ( status == l_Undef )
+            return 0;
+        if ( status == l_True )
+            break;
+        assert( status == l_False );
+        // compute cube and add clause
+        nFinal = sat_solver_final( pSat, &pFinal );
+        Vec_IntClear( vTemp );
+        Vec_IntPush( vTemp, Abc_LitNot(pLits[1]) ); // NOT(iNewLit)
+        for ( i = 0; i < nFinal; i++ )
+        {
+            if ( pFinal[i] == pLits[0] )
+                continue;
+            Vec_IntPush( vTemp, pFinal[i] );
+            iVar = Vec_IntFind( vDivVars, Abc_Lit2Var(pFinal[i]) );   assert( iVar >= 0 );
+            //uCube &= Abc_LitIsCompl(pFinal[i]) ? s_Truths6[iVar] : ~s_Truths6[iVar];
+            Vec_IntPush( vSop, Abc_Var2Lit( iVar, !Abc_LitIsCompl(pFinal[i]) ) );
+        }
+        //uTruth |= uCube;
+        Vec_IntPush( vSop, -1 );
+        status = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntArray(vTemp) + Vec_IntSize(vTemp) );
+        assert( status );
+        nIter++;
+    }
+    assert( status == l_True );
+    // store the counter-example
+    //for ( i = 0; i < Vec_IntSize(vValues); i++ )
+    //    Vec_IntAddToEntry( vValues, i, sat_solver_var_value(pSat, i) );
+    return 0;
+}
+
+word Sbd_ManSolverSupp( Vec_Int_t * vSop, int * pInds, int * pnVars )
+{
+    word Supp = 0;
+    int i, Entry, nVars = 0;
+    Vec_IntForEachEntry( vSop, Entry, i )
+    {
+        if ( Entry == -1 )
+            continue;
+        assert( Abc_Lit2Var(Entry) < 64 );
+        if ( (Supp >> Abc_Lit2Var(Entry)) & 1 )
+            continue;
+        pInds[Abc_Lit2Var(Entry)] = nVars++;
+        Supp |= (word)1 << Abc_Lit2Var(Entry);
+    }
+    *pnVars = nVars;
+    return Supp;
+}
+void Sbd_ManSolverPrint( Vec_Int_t * vSop )
+{
+    int v, i, Entry, nVars, pInds[64];
+    word Supp = Sbd_ManSolverSupp( vSop, pInds, &nVars );
+    char Cube[65] = {'\0'};
+    assert( Cube[nVars] == '\0' );
+    for ( v = 0; v < nVars; v++ )
+        Cube[v] = '-';
+    Vec_IntForEachEntry( vSop, Entry, i )
+    {
+        if ( Entry == -1 )
+        {
+            printf( "%s\n", Cube );
+            for ( v = 0; v < nVars; v++ )
+                Cube[v] = '-';
+            continue;
+        }
+        Cube[pInds[Abc_Lit2Var(Entry)]] = '1' - (char)Abc_LitIsCompl(Entry);
+    }
+}
+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 )
+{
+    Vec_Int_t * vSop = Vec_IntAlloc( 100 );
+    Vec_Int_t * vTemp = Vec_IntAlloc( 100 );
+    sat_solver * pSat = Sbd_ManSatSolver( NULL, p, vMirrors, Pivot, vWinObjs, vObj2Var, vTfo, vRoots, 0 );
+    int PivotVar = Vec_IntEntry(vObj2Var, Pivot);
+    int FreeVar = Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots);
+    int Status = Sbd_ManSolve2( pSat, PivotVar, FreeVar, vDivVars, vDivValues, vTemp, vSop );
+    printf( "Pivot = %4d. Divs = %4d.  ", Pivot, Vec_IntSize(vDivVars) );
+    if ( Status == 0 )
+        printf( "UNSAT.\n" );
+    else
+    {
+        int nVars, pInds[64];
+        word Supp = Sbd_ManSolverSupp( vSop, pInds, &nVars );
+        //Sbd_ManSolverPrint( vSop );
+        printf( "SAT with %d vars and %d cubes.\n", nVars, Vec_IntCountEntry(vSop, -1) );
+    }
+    Vec_IntFree( vTemp );
+    Vec_IntFree( vSop );
+    sat_solver_delete( pSat );
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Returns a bunch of positive/negative random care minterms.]
 
   Description [Returns 0/1 if the functions is const 0/1.]