Updates to delay optimization project.

4 files changed, 254 insertions, 48 deletions

diff --git a/src/opt/sbd/sbdCore.c b/src/opt/sbd/sbdCore.c
index 563e6e98..5c5fe35a 100644
--- a/src/opt/sbd/sbdCore.c
+++ b/src/opt/sbd/sbdCore.c
@@ -777,15 +777,15 @@ void Sbd_ManPrintObj( Sbd_Man_t * p, int Pivot )
     }
 }
 
-void Sbd_ManMatrPrint( word Cover[64], int nCol, int nRows )
+void Sbd_ManMatrPrint( Sbd_Man_t * p, word Cover[], int nCol, int nRows )
 {
     int i, k;
     for ( i = 0; i <= nCol; i++ )
     {
         printf( "%2d : ", i );
+        printf( "%d ", i == nCol ? Vec_IntEntry(p->vLutLevs, p->Pivot) : Vec_IntEntry(p->vLutLevs, Vec_IntEntry(p->vWinObjs, Vec_IntEntry(p->vDivVars, i))) );
         for ( k = 0; k < nRows; k++ )
-            for ( k = 0; k < nRows; k++ )
-                printf( "%d", (int)((Cover[i] >> k) & 1) );
+            printf( "%d", (int)((Cover[i] >> k) & 1) );
         printf( "\n"); 
     }
     printf( "\n");
@@ -801,18 +801,18 @@ static inline void Sbd_ManCoverReverseOrder( word Cover[64] )
     }
 }
 
-static inline int Sbd_ManAddCube1( word Cover[64], int nRows, word Cube )
+static inline int Sbd_ManAddCube1( int nRowLimit, word Cover[], int nRows, word Cube )
 {
     int n, m;
     if ( 0 )
     {
         printf( "Adding cube: " );
-        for ( n = 0; n < 64; n++ )
+        for ( n = 0; n < nRowLimit; n++ )
             printf( "%d", (int)((Cube >> n) & 1) );
         printf( "\n" );
     }
     // do not add contained Cube
-    assert( nRows <= 64 );
+    assert( nRows <= nRowLimit );
     for ( n = 0; n < nRows; n++ )
         if ( (Cover[n] & Cube) == Cover[n] ) // Cube is contained
             return nRows;
@@ -820,7 +820,7 @@ static inline int Sbd_ManAddCube1( word Cover[64], int nRows, word 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 )
+    if ( m < nRowLimit )
         Cover[m++] = Cube;
     for ( n = m; n < nRows; n++ )
         Cover[n] = 0;
@@ -855,7 +855,7 @@ static inline int Sbd_ManAddCube2( word Cover[2][64], int nRows, word Cube[2] )
     return nRows;
 }
 
-static inline int Sbd_ManFindCandsSimple( Sbd_Man_t * p, word Cover[64], int nDivs )
+static inline int Sbd_ManFindCandsSimple( Sbd_Man_t * p, word Cover[], int nDivs )
 {
     int c0, c1, c2, c3;
     word Target = Cover[nDivs];
@@ -1052,7 +1052,7 @@ int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth )
     {
         Cube = (Cubes[0][1][i] & Cubes[1][0][k]) | (Cubes[0][0][i] & Cubes[1][1][k]);
         assert( Cube );
-        nRows = Sbd_ManAddCube1( Cover, nRows, Cube );
+        nRows = Sbd_ManAddCube1( 64, Cover, nRows, Cube );
     }
 
     Sbd_ManCoverReverseOrder( Cover );
@@ -1072,7 +1072,7 @@ int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth )
     for ( nIters = 0; nIters < nItersMax && nRows < 64; nIters++ )
     {
         if ( p->pPars->fVerbose )
-            Sbd_ManMatrPrint( Cover, nDivs, nRows );
+            Sbd_ManMatrPrint( p, Cover, nDivs, nRows );
 
         clk = Abc_Clock();
         if ( !Sbd_ManFindCands( p, Cover, nDivs ) )
@@ -1141,10 +1141,123 @@ 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] )
+int Sbd_ManExplore2( Sbd_Man_t * p, int Pivot, word * pTruth )
 {
+    extern sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots, int fQbf );
+    extern int Sbd_ManCollectConstantsNew( sat_solver * pSat, Vec_Int_t * vDivVars, int nConsts, int PivotVar, word * pOnset, word * pOffset );
+    abctime clk = Abc_Clock();
+    word Onset[64] = {0}, Offset[64] = {0}, Cube;
+    word CoverRows[256] = {0}, CoverCols[64] = {{0}};
+    int nIters, nItersMax = 32;
+    int i, k, nRows = 0;
+
+    int PivotVar = Vec_IntEntry(p->vObj2Var, Pivot);
+    int FreeVar = Vec_IntSize(p->vWinObjs) + Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots);
+    int nDivs = Vec_IntSize( p->vDivVars );
+    int nConsts = 4;
+    int RetValue;
+
+    if ( p->pSat )
+        sat_solver_delete( p->pSat );
+    p->pSat = NULL;
+
+    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;
+
+    assert( nConsts <= 8 );
+    RetValue = Sbd_ManCollectConstantsNew( p->pSat, p->vDivVars, nConsts, PivotVar, Onset, Offset );
+    if ( RetValue >= 0 )
+    {
+        if ( p->pPars->fVerbose )
+            printf( "Found stuck-at-%d node %d.\n", RetValue, Pivot );
+        Vec_IntWriteEntry( p->vLutLevs, Pivot, 0 );
+        p->nConsts++;
+        return RetValue;
+    }
+
+    // create rows of the table
+    nRows = 0;
+    for ( i = 0; i < nConsts; i++ )
+    for ( k = 0; k < nConsts; k++ )
+    {
+        Cube = Onset[i] ^ Offset[k];
+        assert( Cube );
+        nRows = Sbd_ManAddCube1( 256, CoverRows, nRows, Cube );
+    }
+    assert( nRows <= 64 );
+    
+    // create columns of the table
+    for ( i = 0; i < nRows; i++ )
+        for ( k = 0; k <= nDivs; k++ )
+            if ( (CoverRows[i] >> k) & 1 )
+                Abc_TtXorBit(&CoverCols[k], i);
+
+    // solve the covering problem
+    for ( nIters = 0; nIters < nItersMax && nRows < 64; nIters++ )
+    {
+        if ( p->pPars->fVerbose )
+            Sbd_ManMatrPrint( p, CoverCols, nDivs, nRows );
+
+        clk = Abc_Clock();
+        if ( !Sbd_ManFindCands( p, CoverCols, 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 0;
+        }
+        //clkEnu += Abc_Clock() - clk;
+    
+        if ( p->pPars->fVerbose )
+            printf( "Candidate support:  " ),
+            Vec_IntPrint( p->vDivSet );
+
+        clk = Abc_Clock();
+        *pTruth = Sbd_ManSolve( p->pSat, PivotVar, FreeVar+nIters, p->vDivSet, p->vDivVars, p->vDivValues, p->vLits );
+        //clkSat += Abc_Clock() - clk;
+
+        if ( *pTruth == SBD_SAT_UNDEC )
+            printf( "Node %d:  Undecided.\n", Pivot );
+        else if ( *pTruth == SBD_SAT_SAT )
+        {
+            if ( p->pPars->fVerbose )
+            {
+                int i;
+                printf( "Node %d:  SAT.\n", Pivot );
+                for ( i = 0; i < nDivs; i++ )
+                    printf( "%d", Vec_IntEntry(p->vLutLevs, Vec_IntEntry(p->vWinObjs, Vec_IntEntry(p->vDivVars, i))) );
+                printf( "\n" );
+                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 )
+                    CoverCols[i] |= ((word)1 << nRows);
+            CoverCols[nDivs] |= ((word)1 << nRows);
+            nRows++;
+        }
+        else
+        {
+            if ( p->pPars->fVerbose )
+            {
+                printf( "Node %d:  UNSAT.   ", Pivot );
+                Extra_PrintBinary( stdout, (unsigned *)pTruth, 1 << Vec_IntSize(p->vDivSet) ), printf( "\n" );
+            }
+            return 1;
+        }
+    }
     return 0;
 }
 
@@ -1465,7 +1578,7 @@ void Sbd_NtkPerformOne( Sbd_Man_t * p, int Pivot )
     if ( Sbd_ManMergeCuts( p, Pivot ) )
         return;
 
-//    if ( Pivot != 13 )
+//    if ( Pivot != 70 )
 //        return;
 
     if ( p->pPars->fVerbose )
@@ -1481,7 +1594,7 @@ void Sbd_NtkPerformOne( Sbd_Man_t * p, int Pivot )
         Vec_IntWriteEntry( p->vMirrors, Pivot, RetValue );
         //printf( "    --> Pivot %4d.  Constant %d.\n", Pivot, RetValue );
     }
-    else if ( Sbd_ManExplore( p, Pivot, &Truth ) )
+    else if ( Sbd_ManExplore2( p, Pivot, &Truth ) )
     {
         Sbd_ManImplement( p, Pivot, Truth );
         //printf( "    --> Pivot %4d.  Supp %d.\n", Pivot, Vec_IntSize(p->vDivSet) );
@@ -1493,26 +1606,23 @@ void Sbd_NtkPerformOne( Sbd_Man_t * p, int Pivot )
                                        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] 
+                                       Vec_Int_t * vDivSet, int nStrs, Sbd_Str_t * pStr0 
                                    );
 
-        Sbd_Str_t Strs[2] = {
-            {1, 4, {0, 1, 2, 7}},
-            {1, 4, {3, 4, 5, 6}}
-        };
-
-        word Truths[SBD_LUTS_MAX];
+//        Sbd_Str_t Strs[2] = {   {1, 4, {0, 1, 2, 8}},   {1, 4, {3, 4, 5, 6}}    };
+//        Sbd_Str_t Strs[2] = {   {1, 4, {1, 4, 5, 7}},   {1, 4, {0, 1, 2, 3}}    };
+        Sbd_Str_t Strs[3] = {   {1, 4, {8, 4, 5, 7}},   {1, 4, {0, 1, 2, 3}},   {0, 4, {0, 1, 2, 3}}    };
 
         Vec_Int_t * vDivSet = Vec_IntAlloc( 8 );
 
         int i, RetValue;
         
-        for ( i = 0; i < 7; i++ )
+        for ( i = 0; i < 6; i++ )
             Vec_IntPush( vDivSet, i+1 );
 
         RetValue = Sbd_ProblemSolve( p->pGia, p->vMirrors, 
                                      Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots,
-                                     vDivSet, 2, Strs, Truths );
+                                     vDivSet, 3, Strs );
         if ( RetValue )
         {
             printf( "Solving succeded.\n" );
diff --git a/src/opt/sbd/sbdInt.h b/src/opt/sbd/sbdInt.h
index 3646c6b9..5395e148 100644
--- a/src/opt/sbd/sbdInt.h
+++ b/src/opt/sbd/sbdInt.h
@@ -66,6 +66,7 @@ struct Sbd_Str_t_
     int               fLut;                 // LUT or SEL
     int               nVarIns;              // input count
     int               VarIns[SBD_DIV_MAX];  // input vars
+    word              Res;                  // result of solving
 };
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/sbd/sbdLut.c b/src/opt/sbd/sbdLut.c
index 42bb0955..b68ecc26 100644
--- a/src/opt/sbd/sbdLut.c
+++ b/src/opt/sbd/sbdLut.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "sbdInt.h"
+#include "misc/util/utilTruth.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -46,17 +47,18 @@ 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);
+        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 )
+int 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];
+//printf( "Start par = %d.  ", VarPar );
     for ( pStr = pStr0; pStr < pStr0 + nStrs; pStr++, VarOut++ )
     {
         if ( pStr->fLut )
@@ -72,12 +74,14 @@ void Sbd_ProblemAddClauses( sat_solver * pSat, int nVars, int nStrs, int * pVars
                     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 );
+                    if ( !status )
+                        return 0;
                 }
             }
         }
         else
         {
+            assert( pStr->nVarIns <= SBD_DIV_MAX );
             for ( k = 0; k < pStr->nVarIns; k++, VarPar++ )
             {
                 for ( n = 0; n < 2; n++ )
@@ -86,22 +90,32 @@ void Sbd_ProblemAddClauses( sat_solver * pSat, int nVars, int nStrs, int * pVars
                     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 );
+                    if ( !status )
+                        return 0;
                 }
             }
         }
     }
+//printf( "Stop par = %d.\n", VarPar );
+    return 1;
 }
 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;
+    int m, m2, status, pLits[SBD_DIV_MAX];
     // make sure selector parameters are mutually exclusive
-    for ( pStr = pStr0; pStr < pStr0 + nStrs; pStr++, VarPar = pStr->fLut ? 1 << pStr->nVarIns : pStr->nVarIns )
+    for ( pStr = pStr0; pStr < pStr0 + nStrs; VarPar += pStr->fLut ? 1 << pStr->nVarIns : pStr->nVarIns, pStr++ )
     {
         if ( pStr->fLut )
             continue;
+        // one variable should be selected
+        assert( pStr->nVarIns <= SBD_DIV_MAX );
+        for ( m = 0; m < pStr->nVarIns; m++ )
+            pLits[m] = Abc_Var2Lit( pVars[VarPar + m], 0 );
+        status = sat_solver_addclause( pSat, pLits, pLits + pStr->nVarIns );
+        assert( status );
+        // two variables cannot be selected
         for ( m = 0; m < pStr->nVarIns; m++ )
         for ( m2 = m+1; m2 < pStr->nVarIns; m2++ )
         {
@@ -120,15 +134,44 @@ void Sbd_ProblemPrintSolution( int nStrs, Sbd_Str_t * pStr0, Vec_Int_t * vLits )
     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" );
+        printf( "%s%d : ", pStr->fLut ? "LUT":"SEL", (int)(pStr-pStr0) );
+        for ( m = 0; m < nIters; m++, iLit++ )
+            printf( "%d", !Abc_LitIsCompl(Vec_IntEntry(vLits, iLit)) );
+        printf( "    {" );
+        for ( m = 0; m < pStr->nVarIns; m++ )
+            printf( " %d", pStr->VarIns[m] );
+        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] )
+void Sbd_ProblemCollectSolution( int nStrs, Sbd_Str_t * pStr0, Vec_Int_t * vLits )
 {
+    Sbd_Str_t * pStr;
+    int m, nIters, iLit = 0;
+    for ( pStr = pStr0; pStr < pStr0 + nStrs; pStr++ )
+    {
+        pStr->Res = 0;
+        if ( pStr->fLut )
+        {
+            nIters = 1 << pStr->nVarIns;
+            for ( m = 0; m < nIters; m++, iLit++ )
+                if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, iLit)) )
+                    Abc_TtSetBit( &pStr->Res, m );
+            Abc_TtStretch6( &pStr->Res, pStr->nVarIns, 6 );
+        }
+        else
+        {
+            nIters = 0;
+            for ( m = 0; m < pStr->nVarIns; m++, iLit++ )
+                if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, iLit)) )
+                {
+                    pStr->Res = pStr->VarIns[m];
+                    nIters++;
+                }
+            assert( nIters == 1 );
+        }
+    }
+    assert( iLit == Vec_IntSize(vLits) );
 }
 
 /**Function*************************************************************
@@ -145,38 +188,39 @@ void Sbd_ProblemCollectSolution( int nStrs, Sbd_Str_t * pStr0, Vec_Int_t * vLits
 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
+                       Vec_Int_t * vDivSet, int nStrs, Sbd_Str_t * pStr0 )  // 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 );
     
+    int fVerbose = 1;
     Vec_Int_t * vLits    = Vec_IntAlloc( 100 );
     sat_solver * pSatCec = Sbd_ManSatSolver( NULL, p, vMirrors, Pivot, vWinObjs, vObj2Var, vTfo, vRoots, 1 );
     sat_solver * pSatQbf = sat_solver_new();
 
+    int PivotVar   = Vec_IntEntry(vObj2Var, Pivot);
+
     int nVars      = Vec_IntSize( vDivSet );
     int nPars      = Sbd_ProblemCountParams( nStrs, pStr0 );
 
     int VarCecOut  = Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots);
-    int VarCecPar  = VarCecOut + 1;
-    int VarCecFree = VarCecPar + nPars;
+    int VarCecPar  = VarCecOut + nStrs;
 
     int VarQbfPar  = 0;
     int VarQbfFree = nPars;
 
     int pVarsCec[256];
     int pVarsQbf[256];
-    int i, iVar, iLit;
+    int i, iVar, iLit, nIters;
     int RetValue = 0;
 
-    assert( Vec_IntSize(vDivSet) <= SBD_SIZE_MAX );
+    assert( Vec_IntSize(vDivSet) <= SBD_DIV_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 < nStrs; i++ )
+        pVarsCec[nVars + i] = VarCecOut + i;
     for ( i = 0; i < nPars; i++ )
         pVarsCec[nVars + nStrs + i] = VarCecPar + i;
 
@@ -197,13 +241,24 @@ int Sbd_ProblemSolve( Gia_Man_t * p, Vec_Int_t * vMirrors,
     Vec_IntClear( vLits );
     for ( i = 0; i < nPars; i++ )
         Vec_IntPush( vLits, Abc_Var2Lit(VarCecPar + i, 1) );
-    while ( 1 )
+    for ( nIters = 0; nIters < (1 << nVars); nIters++ )
     {
         // 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_IntForEachEntry( vWinObjs, iVar, i )
+//            printf( "Node = %4d.  SatVar = %4d.  Value = %d.\n", iVar, i, sat_solver_var_value(pSatCec, i) );
+
+        if ( fVerbose )
+        {
+            printf( "Iter %3d : ", nIters );
+            for ( i = 0; i < nPars; i++ )
+                printf( "%d", !Abc_LitIsCompl(Vec_IntEntry(vLits, i)) );
+            printf( "    " );
+        }
+
         Vec_IntClear( vLits );
         // create new QBF variables
         for ( i = 0; i < nVars + nStrs; i++ )
@@ -211,15 +266,20 @@ int Sbd_ProblemSolve( Gia_Man_t * p, Vec_Int_t * vMirrors,
         // set their values
         Vec_IntForEachEntry( vDivSet, iVar, i )
         {
-            iLit = Abc_Var2Lit( pVarsQbf[i], sat_solver_var_value(pSatCec, iVar) );
+            iLit = Abc_Var2Lit( pVarsQbf[i], !sat_solver_var_value(pSatCec, iVar) );
             status = sat_solver_addclause( pSatQbf, &iLit, &iLit + 1 );
             assert( status );
+            if ( fVerbose )
+                printf( "%d", sat_solver_var_value(pSatCec, iVar) );
         }
         iLit = Abc_Var2Lit( pVarsQbf[nVars], sat_solver_var_value(pSatCec, VarCecOut) );
         status = sat_solver_addclause( pSatQbf, &iLit, &iLit + 1 );
         assert( status );
+        if ( fVerbose )
+            printf( " %d\n", !sat_solver_var_value(pSatCec, VarCecOut) );
         // add clauses to the QBF problem
-        Sbd_ProblemAddClauses( pSatQbf, nVars, nStrs, pVarsQbf, pStr0 );
+        if ( !Sbd_ProblemAddClauses( pSatQbf, nVars, nStrs, pVarsQbf, pStr0 ) )
+            break; // solution does not exist
         // check if solution still exists
         status = sat_solver_solve( pSatQbf, NULL, NULL, 0, 0, 0, 0 );
         if ( status == l_False ) // solution does not exist
@@ -228,12 +288,12 @@ int Sbd_ProblemSolve( Gia_Man_t * p, Vec_Int_t * vMirrors,
         // 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)) );
+            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 );
+        Sbd_ProblemCollectSolution( nStrs, pStr0, vLits );
         RetValue = 1;
     }
     else 
diff --git a/src/opt/sbd/sbdWin.c b/src/opt/sbd/sbdWin.c
index fc79caa7..d5b7dd9d 100644
--- a/src/opt/sbd/sbdWin.c
+++ b/src/opt/sbd/sbdWin.c
@@ -141,6 +141,17 @@ sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMi
         }
         assert( sat_solver_nvars(pSat) == nVars + nAddVars );
     }
+    else if ( fQbf )
+    {
+        int n, pLits[2];
+        for ( n = 0; n < 2; n++ )
+        {
+            pLits[0] = Abc_Var2Lit( PivotVar, n );
+            pLits[1] = Abc_Var2Lit( LastVar, n );
+            RetValue = sat_solver_addclause( pSat, pLits, pLits + 2 );
+            assert( RetValue );
+        }
+    }
     // finalize
     RetValue = sat_solver_simplify( pSat );
     if ( RetValue == 0 )
@@ -418,6 +429,30 @@ int Sbd_ManCollectConstants( sat_solver * pSat, int nCareMints[2], int PivotVar,
     return -1;
 }
 
+int Sbd_ManCollectConstantsNew( sat_solver * pSat, Vec_Int_t * vDivVars, int nConsts, int PivotVar, word * pOnset, word * pOffset )
+{
+    int nBTLimit = 0;
+    int n, i, k, status, iLit, iVar; 
+    word * pPats[2] = {pOnset, pOffset};
+    assert( Vec_IntSize(vDivVars) < 64 );
+    for ( n = 0; n < 2; n++ )
+    for ( i = 0; i < nConsts; i++ )
+    {
+        sat_solver_random_polarity( pSat );
+        iLit = Abc_Var2Lit( PivotVar, n );
+        status = sat_solver_solve( pSat, &iLit, &iLit + 1, nBTLimit, 0, 0, 0 );
+        if ( status == l_Undef )
+            return -2;
+        if ( status == l_False )
+            return n;
+        pPats[n][i] = ((word)!n) << Vec_IntSize(vDivVars);
+        Vec_IntForEachEntry( vDivVars, iVar, k )
+            if ( sat_solver_var_value(pSat, iVar) )
+                Abc_TtXorBit(&pPats[n][i], k);
+    }
+    return -1;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///