Improvements to delay-optimization in &satlut.

1 files changed, 249 insertions, 150 deletions

diff --git a/src/aig/gia/giaSatLut.c b/src/aig/gia/giaSatLut.c
index 44b5e2e1..23d1b407 100644
--- a/src/aig/gia/giaSatLut.c
+++ b/src/aig/gia/giaSatLut.c
@@ -33,49 +33,193 @@ ABC_NAMESPACE_IMPL_START
 typedef struct Sbl_Man_t_ Sbl_Man_t;
 struct Sbl_Man_t_
 {
-    sat_solver *     pSat;       // SAT solver
-    Vec_Int_t *      vCardVars;  // candinality variables
-    int              LogN;       // max vars
-    int              FirstVar;   // first variable to be used
-    int              LitShift;   // shift in terms of literals (2*Gia_ManCiNum(pGia)+2)
-    int              nInputs;    // the number of inputs
-    int              nEdges;     // the number of edges
+    sat_solver *   pSat;         // SAT solver
+    Vec_Int_t *    vCardVars;    // candinality variables
+    int            nVars;        // max vars
+    int            LogN;         // base-2 log of max vars
+    int            Power2;       // power-2 of LogN
+    int            FirstVar;     // first variable to be used
+    int            nRuns;        // the number of runs
+    // parameters
+    int            nBTLimit;     // conflicts
+    int            DelayMax;     // external delay
+    int            nEdges;       // the number of edges
+    int            fDelay;       // delay mode
+    int            fReverse;     // reverse windowing
+    int            fVeryVerbose; // verbose
+    int            fVerbose;     // verbose
     // window
-    Gia_Man_t *      pGia;
-    Vec_Int_t *      vLeaves;    // leaf nodes
-    Vec_Int_t *      vAnds;      // AND-gates
-    Vec_Int_t *      vNodes;     // internal LUTs
-    Vec_Int_t *      vRoots;     // driver nodes (a subset of vAnds)
-    Vec_Int_t *      vRootVars;  // driver nodes (as SAT variables)
+    Gia_Man_t *    pGia;
+    Vec_Int_t *    vLeaves;      // leaf nodes
+    Vec_Int_t *    vAnds;        // AND-gates
+    Vec_Int_t *    vNodes;       // internal LUTs
+    Vec_Int_t *    vRoots;       // driver nodes (a subset of vAnds)
+    Vec_Int_t *    vRootVars;    // driver nodes (as SAT variables)
     // timing 
-    Vec_Int_t *      vArrs;      // arrival times  
-    Vec_Int_t *      vReqs;      // required times  
-    Vec_Wec_t *      vWindow;    // fanins of each node in the window
-    Vec_Int_t *      vPath;      // critical path (as SAT variables)
-    Vec_Int_t *      vEdges;     // fanin edges
+    Vec_Int_t *    vArrs;        // arrival times  
+    Vec_Int_t *    vReqs;        // required times  
+    Vec_Wec_t *    vWindow;      // fanins of each node in the window
+    Vec_Int_t *    vPath;        // critical path (as SAT variables)
+    Vec_Int_t *    vEdges;       // fanin edges
     // cuts
-    Vec_Wrd_t *      vCutsI;     // input bit patterns
-    Vec_Wrd_t *      vCutsN;     // node bit patterns
-    Vec_Int_t *      vCutsNum;   // cut counts for each obj
-    Vec_Int_t *      vCutsStart; // starting cuts for each obj
-    Vec_Int_t *      vCutsObj;   // object to which this cut belongs
-    Vec_Wrd_t *      vTempI;     // temporary cuts
-    Vec_Wrd_t *      vTempN;     // temporary cuts
-    Vec_Int_t *      vSolInit;   // initial solution
-    Vec_Int_t *      vSolCur;    // current solution
-    Vec_Int_t *      vSolBest;   // best solution
+    Vec_Wrd_t *    vCutsI;       // input bit patterns
+    Vec_Wrd_t *    vCutsN;       // node bit patterns
+    Vec_Int_t *    vCutsNum;     // cut counts for each obj
+    Vec_Int_t *    vCutsStart;   // starting cuts for each obj
+    Vec_Int_t *    vCutsObj;     // object to which this cut belongs
+    Vec_Wrd_t *    vTempI;       // temporary cuts
+    Vec_Wrd_t *    vTempN;       // temporary cuts
+    Vec_Int_t *    vSolInit;     // initial solution
+    Vec_Int_t *    vSolCur;      // current solution
+    Vec_Int_t *    vSolBest;     // best solution
     // temporary
-    Vec_Int_t *      vLits;      // literals
-    Vec_Int_t *      vAssump;    // literals
-    Vec_Int_t *      vPolar;     // variables polarity
+    Vec_Int_t *    vLits;        // literals
+    Vec_Int_t *    vAssump;      // literals
+    Vec_Int_t *    vPolar;       // variables polarity
+    // statistics
+    abctime        timeWin;      // windowing
+    abctime        timeCut;      // cut computation
+    abctime        timeSat;      // SAT runtime
+    abctime        timeSatSat;   // satisfiable time
+    abctime        timeSatUns;   // unsatisfiable time
+    abctime        timeSatUnd;   // undecided time
+    abctime        timeTime;     // timing time
+    abctime        timeStart;    // starting time
+    abctime        timeTotal;    // all runtime
+    abctime        timeOther;    // other time
 };
 
+extern sat_solver * Sbm_AddCardinSolver( int LogN, Vec_Int_t ** pvVars );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Sbl_Man_t * Sbl_ManAlloc( Gia_Man_t * pGia, int Number )
+{
+    Sbl_Man_t * p = ABC_CALLOC( Sbl_Man_t, 1 );
+    p->nVars      = Number;
+    p->LogN       = Abc_Base2Log(Number);
+    p->Power2     = 1 << p->LogN;
+    p->pSat       = Sbm_AddCardinSolver( p->LogN, &p->vCardVars );
+    p->FirstVar   = sat_solver_nvars( p->pSat );
+    sat_solver_bookmark( p->pSat );
+    // window
+    p->pGia       = pGia;
+    p->vLeaves    = Vec_IntAlloc( p->nVars );
+    p->vAnds      = Vec_IntAlloc( p->nVars );
+    p->vNodes     = Vec_IntAlloc( p->nVars );
+    p->vRoots     = Vec_IntAlloc( p->nVars );
+    p->vRootVars  = Vec_IntAlloc( p->nVars );
+    // timing
+    p->vArrs      = Vec_IntAlloc( 0 );
+    p->vReqs      = Vec_IntAlloc( 0 );
+    p->vWindow    = Vec_WecAlloc( 128 );
+    p->vPath      = Vec_IntAlloc( 32 );
+    p->vEdges     = Vec_IntAlloc( 32 );
+    // cuts
+    p->vCutsI     = Vec_WrdAlloc( 1000 );     // input bit patterns
+    p->vCutsN     = Vec_WrdAlloc( 1000 );     // node bit patterns
+    p->vCutsNum   = Vec_IntAlloc( 64 );       // cut counts for each obj
+    p->vCutsStart = Vec_IntAlloc( 64 );       // starting cuts for each obj
+    p->vCutsObj   = Vec_IntAlloc( 1000 );
+    p->vSolInit   = Vec_IntAlloc( 64 );
+    p->vSolCur    = Vec_IntAlloc( 64 );
+    p->vSolBest   = Vec_IntAlloc( 64 );
+    p->vTempI     = Vec_WrdAlloc( 32 ); 
+    p->vTempN     = Vec_WrdAlloc( 32 ); 
+    // internal
+    p->vLits      = Vec_IntAlloc( 64 );
+    p->vAssump    = Vec_IntAlloc( 64 );
+    p->vPolar     = Vec_IntAlloc( 1000 );
+    // other
+    Gia_ManFillValue( pGia );
+    return p;
+}
+void Sbl_ManClean( Sbl_Man_t * p )
+{
+    p->timeStart = Abc_Clock();
+    sat_solver_rollback( p->pSat );
+    sat_solver_bookmark( p->pSat );
+    // internal
+    Vec_IntClear( p->vLeaves );
+    Vec_IntClear( p->vAnds );
+    Vec_IntClear( p->vNodes );
+    Vec_IntClear( p->vRoots );
+    Vec_IntClear( p->vRootVars );
+    // timing
+    Vec_IntClear( p->vArrs );
+    Vec_IntClear( p->vReqs );
+    Vec_WecClear( p->vWindow );
+    Vec_IntClear( p->vPath );
+    Vec_IntClear( p->vEdges );
+    // cuts
+    Vec_WrdClear( p->vCutsI );
+    Vec_WrdClear( p->vCutsN );
+    Vec_IntClear( p->vCutsNum );
+    Vec_IntClear( p->vCutsStart );
+    Vec_IntClear( p->vCutsObj );
+    Vec_IntClear( p->vSolInit );
+    Vec_IntClear( p->vSolCur );
+    Vec_IntClear( p->vSolBest );
+    Vec_WrdClear( p->vTempI );
+    Vec_WrdClear( p->vTempN );
+    // temporary
+    Vec_IntClear( p->vLits );
+    Vec_IntClear( p->vAssump );
+    Vec_IntClear( p->vPolar );
+    // other
+    Gia_ManFillValue( p->pGia );
+    p->nRuns++;
+}
+void Sbl_ManStop( Sbl_Man_t * p )
+{
+    sat_solver_delete( p->pSat );
+    Vec_IntFree( p->vCardVars );
+    // internal
+    Vec_IntFree( p->vLeaves );
+    Vec_IntFree( p->vAnds );
+    Vec_IntFree( p->vNodes );
+    Vec_IntFree( p->vRoots );
+    Vec_IntFree( p->vRootVars );
+    // timing
+    Vec_IntFree( p->vArrs );
+    Vec_IntFree( p->vReqs );
+    Vec_WecFree( p->vWindow );
+    Vec_IntFree( p->vPath );
+    Vec_IntFree( p->vEdges );
+    // cuts
+    Vec_WrdFree( p->vCutsI );
+    Vec_WrdFree( p->vCutsN );
+    Vec_IntFree( p->vCutsNum );
+    Vec_IntFree( p->vCutsStart );
+    Vec_IntFree( p->vCutsObj );
+    Vec_IntFree( p->vSolInit );
+    Vec_IntFree( p->vSolCur );
+    Vec_IntFree( p->vSolBest );
+    Vec_WrdFree( p->vTempI );
+    Vec_WrdFree( p->vTempN );
+    // temporary
+    Vec_IntFree( p->vLits );
+    Vec_IntFree( p->vAssump );
+    Vec_IntFree( p->vPolar );
+    // other
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Timing computation.]
 
   Description []
@@ -211,6 +355,7 @@ int Sbl_ManCriticalFanin( Sbl_Man_t * p, int iLut, Vec_Int_t * vFanins )
 }
 int Sbl_ManEvaluateMapping( Sbl_Man_t * p, int DelayGlo )
 {
+    abctime clk = Abc_Clock();
     Vec_Int_t * vFanins;
     int i, iLut = -1, iAnd, Delay, Required, Edges;
     Vec_IntClear( p->vPath );
@@ -233,6 +378,7 @@ int Sbl_ManEvaluateMapping( Sbl_Man_t * p, int DelayGlo )
         if ( Delay > Required ) // updated timing exceeded original timing
             break;
     }
+    p->timeTime += Abc_Clock() - clk;
     if ( i == Vec_IntSize(p->vRoots) )
         return 1;
     // derive the critical path
@@ -332,7 +478,7 @@ void Sbl_ManUpdateMapping( Sbl_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-static int Sbl_ManPrintCut( word CutI, word CutN, int nInputs )
+static int Sbl_ManPrintCut( word CutI, word CutN )
 {
     int b, Count = 0; 
     printf( "{ " );
@@ -348,7 +494,7 @@ static int Sbl_ManPrintCut( word CutI, word CutN, int nInputs )
 }
 static int Sbl_ManFindAndPrintCut( Sbl_Man_t * p, int c )
 {
-    return Sbl_ManPrintCut( Vec_WrdEntry(p->vCutsI, c), Vec_WrdEntry(p->vCutsN, c), Vec_IntSize(p->vLeaves) );
+    return Sbl_ManPrintCut( Vec_WrdEntry(p->vCutsI, c), Vec_WrdEntry(p->vCutsN, c) );
 }
 static inline int Sbl_CutIsFeasible( word CutI, word CutN )
 {
@@ -411,11 +557,11 @@ static inline int Sbl_ManFindCut( Sbl_Man_t * p, int Obj, word CutI, word CutN )
     int Limit0 = Start0 + Vec_IntEntry( p->vCutsNum, Obj );
     int i;
     //printf( "\nLooking for:\n" );
-    //Sbl_ManPrintCut( CutI, CutN, p->nInputs );
+    //Sbl_ManPrintCut( CutI, CutN );
     //printf( "\n" );
     for ( i = Start0; i < Limit0; i++ )
     {
-        //Sbl_ManPrintCut( pCutsI[i], pCutsN[i], p->nInputs );
+        //Sbl_ManPrintCut( pCutsI[i], pCutsN[i] );
         if ( pCutsI[i] == CutI && pCutsN[i] == CutN )
             return i;
     }
@@ -423,9 +569,10 @@ static inline int Sbl_ManFindCut( Sbl_Man_t * p, int Obj, word CutI, word CutN )
 }
 int Sbl_ManComputeCuts( Sbl_Man_t * p )
 {
+    abctime clk = Abc_Clock();
     Gia_Obj_t * pObj; Vec_Int_t * vFanins;
     int i, k, Index, Fanin, nObjs = Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vAnds);
-    assert( Vec_IntSize(p->vLeaves) <= 64 && Vec_IntSize(p->vAnds) <= 64 );
+    assert( Vec_IntSize(p->vLeaves) <= p->nVars && Vec_IntSize(p->vAnds) <= p->nVars );
     // assign leaf cuts
     Vec_IntClear( p->vCutsStart );
     Vec_IntClear( p->vCutsObj );
@@ -510,6 +657,7 @@ int Sbl_ManComputeCuts( Sbl_Man_t * p )
         pObj->Value = ~0;
     Gia_ManForEachObjVec( p->vAnds, p->pGia, pObj, i )
         pObj->Value = ~0;
+    p->timeCut += Abc_Clock() - clk;
     return Vec_WrdSize(p->vCutsI);
 }
 int Sbl_ManCreateCnf( Sbl_Man_t * p )
@@ -573,80 +721,6 @@ int Sbl_ManCreateCnf( Sbl_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Sbl_Man_t * Sbl_ManAlloc( Gia_Man_t * pGia, int LogN )
-{
-    Sbl_Man_t * p = ABC_CALLOC( Sbl_Man_t, 1 );
-    extern sat_solver * Sbm_AddCardinSolver( int LogN, Vec_Int_t ** pvVars );
-    p->pSat = Sbm_AddCardinSolver( LogN, &p->vCardVars );
-    p->LogN = LogN;
-    p->FirstVar  = sat_solver_nvars( p->pSat );
-    // window
-    p->pGia       = pGia;
-    p->vLeaves    = Vec_IntAlloc( 64 );
-    p->vAnds      = Vec_IntAlloc( 64 );
-    p->vNodes     = Vec_IntAlloc( 64 );
-    p->vRoots     = Vec_IntAlloc( 64 );
-    p->vRootVars  = Vec_IntAlloc( 64 );
-    // timing
-    p->vArrs      = Vec_IntAlloc( 0 );
-    p->vReqs      = Vec_IntAlloc( 0 );
-    p->vWindow    = Vec_WecAlloc( 128 );
-    p->vPath      = Vec_IntAlloc( 32 );
-    p->vEdges     = Vec_IntAlloc( 32 );
-    // cuts
-    p->vCutsI     = Vec_WrdAlloc( 1000 );     // input bit patterns
-    p->vCutsN     = Vec_WrdAlloc( 1000 );     // node bit patterns
-    p->vCutsNum   = Vec_IntAlloc( 64 );       // cut counts for each obj
-    p->vCutsStart = Vec_IntAlloc( 64 );       // starting cuts for each obj
-    p->vCutsObj   = Vec_IntAlloc( 1000 );
-    p->vSolInit   = Vec_IntAlloc( 64 );
-    p->vSolCur    = Vec_IntAlloc( 64 );
-    p->vSolBest   = Vec_IntAlloc( 64 );
-    p->vTempI     = Vec_WrdAlloc( 32 ); 
-    p->vTempN     = Vec_WrdAlloc( 32 ); 
-    // internal
-    p->vLits      = Vec_IntAlloc( 64 );
-    p->vAssump    = Vec_IntAlloc( 64 );
-    p->vPolar     = Vec_IntAlloc( 1000 );
-    // other
-    Gia_ManFillValue( pGia );
-    return p;
-}
-
-void Sbl_ManStop( Sbl_Man_t * p )
-{
-    sat_solver_delete( p->pSat );
-    Vec_IntFree( p->vCardVars );
-    // internal
-    Vec_IntFree( p->vLeaves );
-    Vec_IntFree( p->vAnds );
-    Vec_IntFree( p->vNodes );
-    Vec_IntFree( p->vRoots );
-    Vec_IntFree( p->vRootVars );
-    // timing
-    Vec_IntFree( p->vArrs );
-    Vec_IntFree( p->vReqs );
-    Vec_WecFree( p->vWindow );
-    Vec_IntFree( p->vPath );
-    Vec_IntFree( p->vEdges );
-    // cuts
-    Vec_WrdFree( p->vCutsI );
-    Vec_WrdFree( p->vCutsN );
-    Vec_IntFree( p->vCutsNum );
-    Vec_IntFree( p->vCutsStart );
-    Vec_IntFree( p->vCutsObj );
-    Vec_IntFree( p->vSolInit );
-    Vec_IntFree( p->vSolCur );
-    Vec_IntFree( p->vSolBest );
-    Vec_WrdFree( p->vTempI );
-    Vec_WrdFree( p->vTempN );
-    // temporary
-    Vec_IntFree( p->vLits );
-    Vec_IntFree( p->vAssump );
-    Vec_IntFree( p->vPolar );
-    // other
-    ABC_FREE( p );
-}
 
 void Sbl_ManWindow( Sbl_Man_t * p )
 {
@@ -667,8 +741,10 @@ void Sbl_ManWindow( Sbl_Man_t * p )
 
 int Sbl_ManWindow2( Sbl_Man_t * p, int iPivot )
 {
+    abctime clk = Abc_Clock();
     Vec_Int_t * vRoots, * vNodes, * vLeaves, * vAnds;
     int Count = Gia_ManComputeOneWin( p->pGia, iPivot, &vRoots, &vNodes, &vLeaves, &vAnds );
+    p->timeWin += Abc_Clock() - clk;
     if ( Count == 0 )
         return 0;
     Vec_IntClear( p->vRoots );   Vec_IntAppend( p->vRoots,  vRoots );
@@ -684,41 +760,34 @@ int Sbl_ManWindow2( Sbl_Man_t * p, int iPivot )
     return Count;
 }
 
-int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int DelayMax, int nEdges, int fDelay, int fVeryVerbose, int fVerbose )
+int Sbl_ManTestSat( Sbl_Man_t * p, int iPivot )
 {
     int fKeepTrying = 1;
     abctime clk = Abc_Clock(), clk2;
-    int i, LogN = 6, nVars = 1 << LogN, status, Root;
-    Sbl_Man_t * p = Sbl_ManAlloc( pGia, LogN );
-    int StartSol, Count, nConfTotal = 0, nIters = 0;
+    int i, status, Root, Count, StartSol, nConfTotal = 0, nIters = 0;
 
-    p->nEdges = nEdges;
-    fVerbose |= fVeryVerbose;
-    Vec_IntClear( p->vSolBest );
+    Sbl_ManClean( p );
 
     // compute one window
     Count = Sbl_ManWindow2( p, iPivot );
     if ( Count == 0 )
     {
         printf( "Obj %d: Window with less than %d inputs does not exist.\n", iPivot, 64 );
-        Sbl_ManStop( p );
         return 0;
     }
-    if ( fVerbose )
+    if ( p->fVerbose )
     printf( "\nObj = %6d : Leaf = %2d.  LUT = %2d.  AND = %2d.  Root = %2d.\n", 
         iPivot, Vec_IntSize(p->vLeaves), Vec_IntSize(p->vNodes), Vec_IntSize(p->vAnds), Vec_IntSize(p->vRoots) ); 
-    if ( Vec_IntSize(p->vLeaves) > 64 || Vec_IntSize(p->vAnds) > 64 )
+
+    if ( Vec_IntSize(p->vLeaves) > p->nVars || Vec_IntSize(p->vAnds) > p->nVars )
     {
         printf( "Obj %d: Encountered window with %d inputs and %d internal nodes.\n", iPivot, Vec_IntSize(p->vLeaves), Vec_IntSize(p->vAnds) );
-        Sbl_ManStop( p );
         return 0;
     }
-
     if ( Vec_IntSize(p->vAnds) < 10 )
     {
-        if ( fVerbose )
+        if ( p->fVerbose )
         printf( "Skipping.\n" );
-        Sbl_ManStop( p );
         return 0;
     }
 
@@ -727,10 +796,10 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int DelayMax, in
     // derive SAT instance
     Sbl_ManCreateCnf( p );
 
-    if ( fVeryVerbose )
+    if ( p->fVeryVerbose )
     Vec_IntPrint( p->vSolInit );
 
-    if ( fVeryVerbose )
+    if ( p->fVeryVerbose )
     printf( "All clauses = %d.  Multi clauses = %d.  Binary clauses = %d.  Other clauses = %d.\n\n", 
         sat_solver_nclauses(p->pSat), Vec_IntSize(p->vAnds), Vec_WrdSize(p->vCutsI) - Vec_IntSize(p->vAnds), 
         sat_solver_nclauses(p->pSat) - Vec_WrdSize(p->vCutsI) );
@@ -740,7 +809,7 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int DelayMax, in
     Vec_IntClear( p->vAssump );
     Vec_IntPush( p->vAssump, -1 );
     // unused variables
-    for ( i = Vec_IntSize(p->vAnds); i < nVars; i++ )
+    for ( i = Vec_IntSize(p->vAnds); i < p->Power2; i++ )
         Vec_IntPush( p->vAssump, Abc_Var2Lit(i, 1) );
     // root variables
     Vec_IntForEachEntry( p->vRootVars, Root, i )
@@ -752,7 +821,7 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int DelayMax, in
     while ( fKeepTrying && StartSol-fKeepTrying > 0 )
     {
         int nConfBef, nConfAft;
-        if ( fVerbose )
+        if ( p->fVerbose )
             printf( "Trying to find mapping with %d gates.\n", StartSol-fKeepTrying );
     //    for ( i = Vec_IntSize(p->vSolInit)-5; i < nVars; i++ )
     //        Vec_IntPush( p->vAssump, Abc_Var2Lit(Vec_IntEntry(p->vCardVars, i), 1) );
@@ -760,20 +829,27 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int DelayMax, in
         // solve the problem
         clk2 = Abc_Clock();
         nConfBef = (int)p->pSat->stats.conflicts;
-        status = sat_solver_solve( p->pSat, Vec_IntArray(p->vAssump), Vec_IntLimit(p->vAssump), nBTLimit, 0, 0, 0 );
+        status = sat_solver_solve( p->pSat, Vec_IntArray(p->vAssump), Vec_IntLimit(p->vAssump), p->nBTLimit, 0, 0, 0 );
+        p->timeSat += Abc_Clock() - clk2;
         nConfAft = (int)p->pSat->stats.conflicts;
         nConfTotal += nConfAft - nConfBef;
         nIters++;
+        if ( status == l_True )
+            p->timeSatSat += Abc_Clock() - clk2;
+        else if ( status == l_False )
+            p->timeSatUns += Abc_Clock() - clk2;
+        else 
+            p->timeSatUnd += Abc_Clock() - clk2;
         if ( status == l_Undef )
             break;
         if ( status == l_True )
         {
             int Count = 0, LitCount = 0;
-            if ( fVeryVerbose )
+            if ( p->fVeryVerbose )
             {
                 printf( "Inputs = %d.  ANDs = %d.  Total = %d. All vars = %d.\n", 
                     Vec_IntSize(p->vLeaves), Vec_IntSize(p->vAnds), 
-                    Vec_IntSize(p->vLeaves)+Vec_IntSize(p->vAnds), nVars );
+                    Vec_IntSize(p->vLeaves)+Vec_IntSize(p->vAnds), p->nVars );
                 for ( i = 0; i < Vec_IntSize(p->vAnds); i++ )
                     printf( "%d", sat_solver_var_value(p->pSat, i) );
                 printf( "\n" );
@@ -793,15 +869,15 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int DelayMax, in
             for ( i = p->FirstVar; i < sat_solver_nvars(p->pSat); i++ )
                 if ( sat_solver_var_value(p->pSat, i) )
                 {
-                    if ( fVeryVerbose )
+                    if ( p->fVeryVerbose )
                         printf( "Cut %3d : Node = %3d  Node = %6d  ", Count++, Vec_IntEntry(p->vCutsObj, i-p->FirstVar), Vec_IntEntry(p->vAnds, Vec_IntEntry(p->vCutsObj, i-p->FirstVar)) );
-                    if ( fVeryVerbose )
+                    if ( p->fVeryVerbose )
                         LitCount += Sbl_ManFindAndPrintCut( p, i-p->FirstVar );
                     Vec_IntPush( p->vSolCur, i-p->FirstVar );
                 }
-            if ( fVeryVerbose )
+            if ( p->fVeryVerbose )
             printf( "LitCount = %d.\n", LitCount );
-            if ( fVeryVerbose )
+            if ( p->fVeryVerbose )
             Vec_IntPrint( p->vRootVars );
             //Vec_IntPrint( p->vRoots );
             //Vec_IntPrint( p->vAnds );
@@ -812,10 +888,10 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int DelayMax, in
         // check the timing
         if ( status == l_True )
         {
-            if ( fDelay && !Sbl_ManEvaluateMapping(p, DelayMax) )
+            if ( p->fDelay && !Sbl_ManEvaluateMapping(p, p->DelayMax) )
             {
                 int iLit, value;
-                if ( fVerbose )
+                if ( p->fVerbose )
                 {
                     printf( "Critical path of length (%d) is detected:   ", Vec_IntSize(p->vPath) );
                     Vec_IntForEachEntry( p->vPath, iLit, i )
@@ -835,7 +911,7 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int DelayMax, in
         }
         else
             fKeepTrying = 0;
-        if ( fVerbose )
+        if ( p->fVerbose )
         {
             if ( status == l_False )
                 printf( "UNSAT " );
@@ -856,31 +932,54 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int DelayMax, in
     // update solution
     if ( Vec_IntSize(p->vSolBest) > 0 && Vec_IntSize(p->vSolBest) < Vec_IntSize(p->vSolInit) )
     {
-        int nDelay, nEdges;
-        nDelay = Sbl_ManCreateTiming( p, DelayMax, &nEdges );
+        int nDelayCur, nEdgesCur;
+        nDelayCur = Sbl_ManCreateTiming( p, p->DelayMax, &nEdgesCur );
         Sbl_ManUpdateMapping( p );
         printf( "Object %5d : Saved %d nodes  (Conf =%8d)  Iter =%3d  Delay = %d  Edges = %4d\n", 
-            iPivot, Vec_IntSize(p->vSolInit)-Vec_IntSize(p->vSolBest), nConfTotal, nIters, nDelay, nEdges );
-        Sbl_ManStop( p );
+            iPivot, Vec_IntSize(p->vSolInit)-Vec_IntSize(p->vSolBest), nConfTotal, nIters, nDelayCur, nEdgesCur );
+        p->timeTotal += Abc_Clock() - p->timeStart;
         return 2;
     }
-    Sbl_ManStop( p );
+    p->timeTotal += Abc_Clock() - p->timeStart;
     return 1;
 }
-
-void Gia_ManLutSat( Gia_Man_t * pGia, int nNumber, int nBTLimit, int DelayMax, int nEdges, int fDelay, int fReverse, int fVeryVerbose, int fVerbose )
+void Sbl_ManPrintRuntime( Sbl_Man_t * p )
+{
+    p->timeOther = p->timeTotal - p->timeWin - p->timeCut - p->timeSat - p->timeTime;
+
+    ABC_PRTP( "Win   ", p->timeWin  ,   p->timeTotal );
+    ABC_PRTP( "Cut   ", p->timeCut  ,   p->timeTotal );
+    ABC_PRTP( "Sat   ", p->timeSat,     p->timeTotal );
+    ABC_PRTP( " Sat  ", p->timeSatSat,  p->timeTotal );
+    ABC_PRTP( " Unsat", p->timeSatUns,  p->timeTotal );
+    ABC_PRTP( " Undec", p->timeSatUnd,  p->timeTotal );
+    ABC_PRTP( "Timing", p->timeTime ,   p->timeTotal );
+    ABC_PRTP( "Other ", p->timeOther,   p->timeTotal );
+    ABC_PRTP( "ALL   ", p->timeTotal,   p->timeTotal );
+    printf( "Total runs = %d.\n", p->nRuns );
+}
+void Gia_ManLutSat( Gia_Man_t * pGia, int nNumber, int nImproves, int nBTLimit, int DelayMax, int nEdges, int fDelay, int fReverse, int fVeryVerbose, int fVerbose )
 {
-    int iLut;
+    int iLut, nImproveCount = 0;
+    Sbl_Man_t * p   = Sbl_ManAlloc( pGia, nNumber );
+    p->nBTLimit     = nBTLimit;     // conflicts
+    p->DelayMax     = DelayMax;     // external delay
+    p->nEdges       = nEdges;       // the number of edges
+    p->fDelay       = fDelay;       // delay mode
+    p->fReverse     = fReverse;     // reverse windowing
+    p->fVeryVerbose = fVeryVerbose; // verbose
+    p->fVerbose     = fVerbose | fVeryVerbose;
     Gia_ManComputeOneWinStart( pGia, fReverse );
     Gia_ManForEachLut2( pGia, iLut )
     {
-//        if ( iLut > 259 )
-//            break;
-        if ( Sbl_ManTestSat( pGia, nBTLimit, iLut, DelayMax, nEdges, fDelay, fVeryVerbose, fVerbose ) != 2 )
+        if ( Sbl_ManTestSat( p, iLut ) != 2 )
             continue;
-//        break;
+        if ( ++nImproveCount == nImproves )
+            break;
     }
     Gia_ManComputeOneWin( pGia, -1, NULL, NULL, NULL, NULL );
+    Sbl_ManPrintRuntime( p );
+    Sbl_ManStop( p );
 }
 
 ////////////////////////////////////////////////////////////////////////