Improvements to delay-optimization in &satlut.

3 files changed, 330 insertions, 87 deletions

diff --git a/src/aig/gia/giaSatLut.c b/src/aig/gia/giaSatLut.c
index f985eb50..3c8eb320 100644
--- a/src/aig/gia/giaSatLut.c
+++ b/src/aig/gia/giaSatLut.c
@@ -46,6 +46,11 @@ struct Sbl_Man_t_
     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)
     // cuts
     Vec_Wrd_t *      vCutsI;     // input bit patterns
     Vec_Wrd_t *      vCutsN;     // node bit patterns
@@ -54,8 +59,9 @@ struct Sbl_Man_t_
     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 *      vSolCuts;   // cuts belonging to solution
-    Vec_Int_t *      vSolCuts2;  // cuts belonging to solution
+    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
@@ -68,6 +74,155 @@ struct Sbl_Man_t_
 
 /**Function*************************************************************
 
+  Synopsis    [Timing computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sbl_ManComputeDelay( Sbl_Man_t * p, int iLut, Vec_Int_t * vFanins )
+{
+    int k, iFan, Delay = 0;
+    Vec_IntForEachEntry( vFanins, iFan, k )
+        Delay = Abc_MaxInt( Delay, Vec_IntEntry(p->vArrs, iFan) + 1 );
+    return Delay;
+}
+void Sbl_ManCreateTiming( Sbl_Man_t * p, int DelayStart )
+{
+    Vec_Int_t * vFanins;
+    int DelayMax = DelayStart, Delay, iLut, iFan, k;
+    // compute arrival times
+    Vec_IntFill( p->vArrs,  Gia_ManObjNum(p->pGia), 0 );
+    Gia_ManForEachLut2( p->pGia, iLut )
+    {
+        vFanins = Gia_ObjLutFanins2(p->pGia, iLut);
+        Delay = Sbl_ManComputeDelay( p, iLut, vFanins );
+        Vec_IntWriteEntry( p->vArrs,  iLut, Delay );
+        DelayMax = Abc_MaxInt( DelayMax, Delay );
+    }
+    // compute required times
+    Vec_IntFill( p->vReqs, Gia_ManObjNum(p->pGia), ABC_INFINITY );
+    Gia_ManForEachCoDriverId( p->pGia, iLut, k )
+        Vec_IntDowndateEntry( p->vReqs, iLut, DelayMax );
+    Gia_ManForEachLut2Reverse( p->pGia, iLut )
+    {
+        Delay = Vec_IntEntry(p->vReqs, iLut) - 1;
+        vFanins = Gia_ObjLutFanins2(p->pGia, iLut);
+        Vec_IntForEachEntry( vFanins, iFan, k )
+            Vec_IntDowndateEntry( p->vReqs, iFan, Delay );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [For each node in the window, create fanins.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sbl_ManGetCurrentMapping( Sbl_Man_t * p )
+{
+    Vec_Int_t * vObj;
+    word CutI, CutN;
+    int i, c, b, iObj;
+    Vec_WecClear( p->vWindow );
+    Vec_WecInit( p->vWindow, Vec_IntSize(p->vAnds) );
+    assert( Vec_IntSize(p->vSolCur) > 0 );
+    Vec_IntForEachEntry( p->vSolCur, c, i )
+    {
+        CutI = Vec_WrdEntry( p->vCutsI, c );
+        CutN = Vec_WrdEntry( p->vCutsN, c );
+        iObj = Vec_IntEntry( p->vCutsObj, c );
+        //iObj = Vec_IntEntry( p->vAnds, iObj );
+        vObj = Vec_WecEntry( p->vWindow, iObj );
+        assert( Vec_IntSize(vObj) == 0 );
+        for ( b = 0; b < 64; b++ )
+            if ( (CutI >> b) & 1 )
+                Vec_IntPush( vObj, Vec_IntEntry(p->vLeaves, b) );
+        for ( b = 0; b < 64; b++ )
+            if ( (CutN >> b) & 1 )
+                Vec_IntPush( vObj, Vec_IntEntry(p->vAnds, b) );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Given mapping in p->vSolCur, check the critical path.]
+
+  Description [Returns 1 if the mapping satisfies the timing. Returns 0, 
+  if the critical path is detected.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sbl_ManCriticalFanin( Sbl_Man_t * p, int iLut, Vec_Int_t * vFanins )
+{
+    int k, iFan, Delay = Vec_IntEntry(p->vArrs, iLut);
+    Vec_IntForEachEntry( vFanins, iFan, k )
+        if ( Vec_IntEntry(p->vArrs, iFan) + 1 == Delay )
+            return iFan;
+    return -1;
+}
+int Sbl_ManEvaluateMapping( Sbl_Man_t * p, int DelayGlo )
+{
+    Vec_Int_t * vFanins;
+    int i, iLut, iAnd, Delay, Required;
+    Vec_IntClear( p->vPath );
+    // derive timing
+    Sbl_ManCreateTiming( p, DelayGlo );
+    // update new timing
+    Sbl_ManGetCurrentMapping( p );
+    Vec_IntForEachEntry( p->vAnds, iLut, i )
+    {
+        vFanins = Vec_WecEntry( p->vWindow, i );
+        Delay   = Sbl_ManComputeDelay( p, iLut, vFanins );
+        Vec_IntWriteEntry( p->vArrs, iLut, Delay );
+    }
+    // compare timing at the root nodes
+    Vec_IntForEachEntry( p->vRoots, iLut, i )
+    {
+        Delay    = Vec_IntEntry( p->vArrs, iLut );
+        Required = Vec_IntEntry( p->vReqs, iLut );
+        if ( Delay > Required ) // updated timing exceeded original timing
+            break;
+    }
+    if ( i == Vec_IntSize(p->vRoots) )
+        return 1;
+    // derive the critical path
+
+    // find SAT variable of the node whose GIA ID is "iLut"
+    iAnd = Vec_IntFind( p->vAnds, iLut );
+    assert( iAnd >= 0 );
+    // critical path begins in node "iLut", which is i-th root of the window
+    assert( iAnd == Vec_IntEntry(p->vRootVars, i) );
+    while ( 1 )
+    {
+        Vec_IntPush( p->vPath, Abc_Var2Lit(iAnd, 1) );
+        // find fanins of this node
+        vFanins = Vec_WecEntry( p->vWindow, iAnd );
+        // find critical fanin
+        iLut = Sbl_ManCriticalFanin( p, iLut, vFanins );
+        assert( iLut > 0  );
+        // find SAT variable of the node whose GIA ID is "iLut"
+        iAnd = Vec_IntFind( p->vAnds, iLut );
+        if ( iAnd == -1 )
+            break;
+    }
+    return 0;
+}
+
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -83,7 +238,7 @@ void Sbl_ManUpdateMapping( Sbl_Man_t * p )
     Vec_Int_t * vObj;
     word CutI, CutN;
     int i, c, b, iObj, iTemp; 
-    assert( Vec_IntSize(p->vSolCuts2) < Vec_IntSize(p->vSolCuts) );
+    assert( Vec_IntSize(p->vSolBest) < Vec_IntSize(p->vSolInit) );
     Vec_IntForEachEntry( p->vAnds, iObj, i )
     {
         vObj = Vec_WecEntry(p->pGia->vMapping2, iObj);
@@ -91,7 +246,7 @@ void Sbl_ManUpdateMapping( Sbl_Man_t * p )
             Gia_ObjLutRefDecId( p->pGia, iTemp );
         Vec_IntClear( vObj );
     }
-    Vec_IntForEachEntry( p->vSolCuts2, c, i )
+    Vec_IntForEachEntry( p->vSolBest, c, i )
     {
         CutI = Vec_WrdEntry( p->vCutsI, c );
         CutN = Vec_WrdEntry( p->vCutsN, c );
@@ -274,7 +429,7 @@ int Sbl_ManComputeCuts( Sbl_Man_t * p )
     }
     // create current solution
     Vec_IntClear( p->vPolar );
-    Vec_IntClear( p->vSolCuts );
+    Vec_IntClear( p->vSolInit );
     Gia_ManForEachObjVec( p->vAnds, p->pGia, pObj, i )
     {
         word CutI = 0, CutN = 0;
@@ -284,7 +439,7 @@ int Sbl_ManComputeCuts( Sbl_Man_t * p )
         assert( (int)pObj->Value == Vec_IntSize(p->vLeaves) + i );
         // add node
         Vec_IntPush( p->vPolar, i );
-        Vec_IntPush( p->vSolCuts, i );
+        Vec_IntPush( p->vSolInit, i );
         // add its cut
         //Gia_LutForEachFaninObj( p->pGia, Obj, pFanin, k )
         vFanins = Gia_ObjLutFanins2( p->pGia, Obj );
@@ -390,14 +545,20 @@ Sbl_Man_t * Sbl_ManAlloc( Gia_Man_t * pGia, int LogN )
     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 );
     // 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->vSolCuts   = Vec_IntAlloc( 64 );
-    p->vSolCuts2  = Vec_IntAlloc( 64 );
+    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
@@ -419,14 +580,20 @@ void Sbl_ManStop( Sbl_Man_t * p )
     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 );
     // cuts
     Vec_WrdFree( p->vCutsI );
     Vec_WrdFree( p->vCutsN );
     Vec_IntFree( p->vCutsNum );
     Vec_IntFree( p->vCutsStart );
     Vec_IntFree( p->vCutsObj );
-    Vec_IntFree( p->vSolCuts );
-    Vec_IntFree( p->vSolCuts2 );
+    Vec_IntFree( p->vSolInit );
+    Vec_IntFree( p->vSolCur );
+    Vec_IntFree( p->vSolBest );
     Vec_WrdFree( p->vTempI );
     Vec_WrdFree( p->vTempN );
     // temporary
@@ -473,13 +640,15 @@ int Sbl_ManWindow2( Sbl_Man_t * p, int iPivot )
     return Count;
 }
 
-int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int fVerbose )
+int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int DelayMax, int fDelay, int fVeryVerbose, int fVerbose )
 {
     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;
+    Vec_IntClear( p->vSolBest );
+    fVerbose |= fVeryVerbose;
 
     // compute one window
     Count = Sbl_ManWindow2( p, iPivot );
@@ -499,7 +668,7 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int fVerbose )
         return 0;
     }
 
-    if ( Vec_IntSize(p->vAnds) < 20 )
+    if ( Vec_IntSize(p->vAnds) < 10 )
     {
         if ( fVerbose )
         printf( "Skipping.\n" );
@@ -512,10 +681,10 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int fVerbose )
     // derive SAT instance
     Sbl_ManCreateCnf( p );
 
-    if ( fVerbose )
-    Vec_IntPrint( p->vSolCuts );
+    if ( fVeryVerbose )
+    Vec_IntPrint( p->vSolInit );
 
-    if ( fVerbose )
+    if ( 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) );
@@ -532,15 +701,14 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int fVerbose )
         Vec_IntPush( p->vAssump, Abc_Var2Lit(Root, 0) );
 //    Vec_IntPrint( p->vAssump );
 
-    Vec_IntClear( p->vSolCuts2 );
-    StartSol = Vec_IntSize(p->vSolCuts) + 1;
+    StartSol = Vec_IntSize(p->vSolInit) + 1;
 //    StartSol = 30;
     while ( fKeepTrying && StartSol-fKeepTrying > 0 )
     {
         int nConfBef, nConfAft;
         if ( fVerbose )
             printf( "Trying to find mapping with %d gates.\n", StartSol-fKeepTrying );
-    //    for ( i = Vec_IntSize(p->vSolCuts)-5; i < nVars; i++ )
+    //    for ( i = Vec_IntSize(p->vSolInit)-5; i < nVars; i++ )
     //        Vec_IntPush( p->vAssump, Abc_Var2Lit(Vec_IntEntry(p->vCardVars, i), 1) );
         Vec_IntWriteEntry( p->vAssump, 0, Abc_Var2Lit(Vec_IntEntry(p->vCardVars, StartSol-fKeepTrying), 1) );
         // solve the problem
@@ -554,7 +722,7 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int fVerbose )
         if ( status == l_True )
         {
             int Count = 0, LitCount = 0;
-            if ( fVerbose )
+            if ( fVeryVerbose )
             {
                 printf( "Inputs = %d.  ANDs = %d.  Total = %d. All vars = %d.\n", 
                     Vec_IntSize(p->vLeaves), Vec_IntSize(p->vAnds), 
@@ -574,25 +742,52 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int fVerbose )
 //                printf( "%d", sat_solver_var_value(p->pSat, i) );
 //            printf( "\n" );
             Count = 1;
-            Vec_IntClear( p->vSolCuts2 );
+            Vec_IntClear( p->vSolCur );
             for ( i = p->FirstVar; i < sat_solver_nvars(p->pSat); i++ )
                 if ( sat_solver_var_value(p->pSat, i) )
                 {
-                    if ( fVerbose )
+                    if ( 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 ( fVerbose )
+                    if ( fVeryVerbose )
                         LitCount += Sbl_ManFindAndPrintCut( p, i-p->FirstVar );
-                    Vec_IntPush( p->vSolCuts2, i-p->FirstVar );
+                    Vec_IntPush( p->vSolCur, i-p->FirstVar );
                 }
-            if ( fVerbose )
+            if ( fVeryVerbose )
             printf( "LitCount = %d.\n", LitCount );
-            if ( fVerbose )
+            if ( fVeryVerbose )
             Vec_IntPrint( p->vRootVars );
             //Vec_IntPrint( p->vRoots );
             //Vec_IntPrint( p->vAnds );
             //Vec_IntPrint( p->vLeaves );
         }
-        fKeepTrying = status == l_True ? fKeepTrying + 1 : 0;
+
+//        fKeepTrying = status == l_True ? fKeepTrying + 1 : 0;
+        // check the timing
+        if ( status == l_True )
+        {
+            if ( fDelay && !Sbl_ManEvaluateMapping(p, DelayMax) )
+            {
+                int iLit, value;
+                if ( fVerbose )
+                {
+                    printf( "Critical path of length (%d) is detected:   ", Vec_IntSize(p->vPath) );
+                    Vec_IntForEachEntry( p->vPath, iLit, i )
+                        printf( "%d=%d ", i, Vec_IntEntry(p->vAnds, Abc_Lit2Var(iLit)) );
+                    printf( "\n" );
+                }
+                // add the clause
+                value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vPath), Vec_IntLimit(p->vPath)  );
+                assert( value );
+            }
+            else
+            {
+                Vec_IntClear( p->vSolBest );
+                Vec_IntAppend( p->vSolBest, p->vSolCur );
+                fKeepTrying++;
+            }
+        }
+        else
+            fKeepTrying = 0;
         if ( fVerbose )
         {
             if ( status == l_False )
@@ -601,17 +796,21 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int fVerbose )
                 printf( "SAT   " );
             else 
                 printf( "UNDEC " );
+            printf( "confl =%8d.    ", nConfAft - nConfBef );
             Abc_PrintTime( 1, "Time", Abc_Clock() - clk2 );
-            Abc_PrintTime( 1, "Total time", Abc_Clock() - clk );
+
+            printf( "Total " );
+            printf( "confl =%8d.    ", nConfTotal );
+            Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
             printf( "\n" );
         }
     }
 
     // update solution
-    if ( Vec_IntSize(p->vSolCuts2) > 0 && Vec_IntSize(p->vSolCuts2) < Vec_IntSize(p->vSolCuts) )
+    if ( Vec_IntSize(p->vSolBest) > 0 && Vec_IntSize(p->vSolBest) < Vec_IntSize(p->vSolInit) )
     {
         Sbl_ManUpdateMapping( p );
-        printf( "Object %d : Saved %d nodes.  (Conf = %d.)\n", iPivot, Vec_IntSize(p->vSolCuts)-Vec_IntSize(p->vSolCuts2), nConfTotal );
+        printf( "Object %5d : Saved %d nodes.  (Conf =%8d.)\n", iPivot, Vec_IntSize(p->vSolInit)-Vec_IntSize(p->vSolBest), nConfTotal );
         Sbl_ManStop( p );
         return 2;
     }
@@ -619,7 +818,7 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int fVerbose )
     return 1;
 }
 
-void Gia_ManLutSat( Gia_Man_t * pGia, int nNumber, int nConfl, int fReverse, int fVerbose )
+void Gia_ManLutSat( Gia_Man_t * pGia, int nNumber, int nBTLimit, int DelayMax, int fDelay, int fReverse, int fVeryVerbose, int fVerbose )
 {
     int iLut;
     Gia_ManComputeOneWinStart( pGia, fReverse );
@@ -627,7 +826,7 @@ void Gia_ManLutSat( Gia_Man_t * pGia, int nNumber, int nConfl, int fReverse, int
     {
 //        if ( iLut > 259 )
 //            break;
-        if ( Sbl_ManTestSat( pGia, nConfl, iLut, fVerbose ) != 2 )
+        if ( Sbl_ManTestSat( pGia, nBTLimit, iLut, DelayMax, fDelay, fVeryVerbose, fVerbose ) != 2 )
             continue;
 //        break;
     }
diff --git a/src/aig/gia/giaSplit.c b/src/aig/gia/giaSplit.c
index 8bb5d3c0..b402f2ac 100644
--- a/src/aig/gia/giaSplit.c
+++ b/src/aig/gia/giaSplit.c
@@ -209,12 +209,14 @@ void Spl_ManWinFindLeavesRoots( Spl_Man_t * p )
         iFan = Gia_ObjFaninId0( pObj, iObj );
         if ( !Vec_BitEntry(p->vMarksAnd, iFan) )
         {
+            assert( Gia_ObjIsLut2(p->pGia, iFan) || Vec_BitEntry(p->vMarksCIO, iFan) );
             Vec_BitWriteEntry(p->vMarksAnd, iFan, 1);
             Vec_IntPush( p->vLeaves, iFan );
         }
         iFan = Gia_ObjFaninId1( pObj, iObj );
         if ( !Vec_BitEntry(p->vMarksAnd, iFan) )
         {
+            assert( Gia_ObjIsLut2(p->pGia, iFan) || Vec_BitEntry(p->vMarksCIO, iFan) );
             Vec_BitWriteEntry(p->vMarksAnd, iFan, 1);
             Vec_IntPush( p->vLeaves, iFan );
         }
@@ -297,6 +299,28 @@ int Spl_ManCountMarkedFanins( Gia_Man_t * p, int iObj, Vec_Bit_t * vMarks )
             Count++;
     return Count;
 }
+int Spl_ManFindGoodCand( Spl_Man_t * p )
+{
+    int i, iObj;
+    int Res = 0, InCount, InCountMax = -1; 
+    // mark leaves
+    Vec_IntForEachEntry( p->vInputs, iObj, i )
+        Vec_BitWriteEntry( p->vMarksIn, iObj, 1 );
+    // find candidate with maximum input overlap
+    Vec_IntForEachEntry( p->vCands, iObj, i )
+    {
+        InCount = Spl_ManCountMarkedFanins( p->pGia, iObj, p->vMarksIn );
+        if ( InCountMax < InCount )
+        {
+            InCountMax = InCount;
+            Res = iObj;
+        }
+    }
+    // unmark leaves
+    Vec_IntForEachEntry( p->vInputs, iObj, i )
+        Vec_BitWriteEntry( p->vMarksIn, iObj, 0 );
+    return Res;
+}
 
 /**Function*************************************************************
 
@@ -313,45 +337,58 @@ int Spl_ManFindOne( Spl_Man_t * p )
 {
     Vec_Int_t * vVec;
     int nFanouts, iObj, iFan, i, k;
-    int Res = 0, InCount, InCountMax = -1; 
-    Vec_IntClear( p->vCands );
-    Vec_IntClear( p->vInputs );
+    int Res = 0; 
+
     // deref
     Gia_ManForEachLut2Vec( p->vNodes, p->pGia, vVec, iObj, i )
         Vec_IntForEachEntry( vVec, iFan, k )
             Gia_ObjLutRefDecId( p->pGia, iFan );
-    // consider LUT inputs - get one that has no refs
-    if ( p->fReverse )
-    {
-        Gia_ManForEachLut2VecReverse( p->vNodes, p->pGia, vVec, iObj, i )
-            Vec_IntForEachEntry( vVec, iFan, k )
-                if ( !Vec_BitEntry(p->vMarksNo, iFan) && !Vec_BitEntry(p->vMarksCIO, iFan) )
-                {
-                    if ( !Gia_ObjLutRefNumId(p->pGia, iFan) )
-                    {
-                        Res = iFan;
-                        goto finish;
-                    }
-                    Vec_IntPush( p->vCands, iFan );
-                    Vec_IntPush( p->vInputs, iFan );
-                }
-    }
-    else
+
+    // collect external nodes
+    if ( p->fReverse && (Vec_IntSize(p->vNodes) & 1) )
     {
-        Gia_ManForEachLut2Vec( p->vNodes, p->pGia, vVec, iObj, i )
-            Vec_IntForEachEntry( vVec, iFan, k )
-                if ( !Vec_BitEntry(p->vMarksNo, iFan) && !Vec_BitEntry(p->vMarksCIO, iFan) )
-                {
-                    if ( !Gia_ObjLutRefNumId(p->pGia, iFan) )
-                    {
-                        Res = iFan;
-                        goto finish;
-                    }
-                    Vec_IntPush( p->vCands, iFan );
-                    Vec_IntPush( p->vInputs, iFan );
-                }
+        Vec_IntForEachEntry( p->vNodes, iObj, i )
+        {
+            if ( Gia_ObjLutRefNumId(p->pGia, iObj) == 0 )
+                continue;
+            assert( Gia_ObjLutRefNumId(p->pGia, iObj) > 0 );
+            if ( Gia_ObjLutRefNumId(p->pGia, iObj) >= 5 )  // skip nodes with high fanout!
+                continue;
+            nFanouts = Spl_ManLutFanouts( p->pGia, iObj, p->vFanouts, p->vMarksNo, p->vMarksCIO );
+            if ( Gia_ObjLutRefNumId(p->pGia, iObj) == 1 && nFanouts == 1 )
+            {
+                Res = Vec_IntEntry(p->vFanouts, 0);
+                goto finish;
+            }
+            //Vec_IntAppend( p->vCands, p->vFanouts );
+        }
     }
 
+    // consider LUT inputs - get one that has no refs
+    Vec_IntClear( p->vCands );
+    Vec_IntClear( p->vInputs );
+    Gia_ManForEachLut2Vec( p->vNodes, p->pGia, vVec, iObj, i )
+        Vec_IntForEachEntry( vVec, iFan, k )
+            if ( !Vec_BitEntry(p->vMarksNo, iFan) && !Vec_BitEntry(p->vMarksCIO, iFan) && !Gia_ObjLutRefNumId(p->pGia, iFan) )
+            {
+                Vec_IntPush( p->vCands, iFan );
+                Vec_IntPush( p->vInputs, iFan );
+            }
+    Res = Spl_ManFindGoodCand( p );
+    if ( Res )
+        goto finish;
+
+    // collect candidates
+    Vec_IntClear( p->vCands );
+    Vec_IntClear( p->vInputs );
+    Gia_ManForEachLut2Vec( p->vNodes, p->pGia, vVec, iObj, i )
+        Vec_IntForEachEntry( vVec, iFan, k )
+            if ( !Vec_BitEntry(p->vMarksNo, iFan) && !Vec_BitEntry(p->vMarksCIO, iFan) )
+            {
+                Vec_IntPush( p->vCands, iFan );
+                Vec_IntPush( p->vInputs, iFan );
+            }
+
     // all inputs have refs - collect external nodes
     Vec_IntForEachEntry( p->vNodes, iObj, i )
     {
@@ -369,22 +406,10 @@ int Spl_ManFindOne( Spl_Man_t * p )
         Vec_IntAppend( p->vCands, p->vFanouts );
     }
 
-    // mark leaves
-    Vec_IntForEachEntry( p->vInputs, iObj, i )
-        Vec_BitWriteEntry( p->vMarksIn, iObj, 1 );
-    // find candidate with maximum input overlap
-    Vec_IntForEachEntry( p->vCands, iObj, i )
-    {
-        InCount = Spl_ManCountMarkedFanins( p->pGia, iObj, p->vMarksIn );
-        if ( InCountMax < InCount )
-        {
-            InCountMax = InCount;
-            Res = iObj;
-        }
-    }
-    // unmark leaves
-    Vec_IntForEachEntry( p->vInputs, iObj, i )
-        Vec_BitWriteEntry( p->vMarksIn, iObj, 0 );
+    // choose among not-so-good ones
+    Res = Spl_ManFindGoodCand( p );
+    if ( Res )
+        goto finish;
 
     // get the first candidate
     if ( Res == 0 && Vec_IntSize(p->vCands) > 0 )
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 05712ada..5c3a573a 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -34827,10 +34827,11 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9SatLut( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern void Gia_ManLutSat( Gia_Man_t * p, int nNumber, int nConfl, int fReverse, int fVerbose );
-    int c, nNumber = 64, nConfl = 500, fReverse = 0, fVerbose = 0;
+    extern void Gia_ManLutSat( Gia_Man_t * p, int nNumber, int nBTLimit, int DelayMax, int fDelay, int fReverse, int fVeryVerbose, int fVerbose );
+    int c, nNumber = 64, nBTLimit = 500, DelayMax = 0;
+    int fDelay = 0, fReverse = 0, fVeryVerbose = 0, fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "NCrvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "NCDdrwvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -34854,12 +34855,27 @@ int Abc_CommandAbc9SatLut( Abc_Frame_t * pAbc, int argc, char ** argv )
                 Abc_Print( -1, "Command line switch \"-C\" should be followed by a positive integer.\n" );
                 goto usage;
             }
-            nConfl = atoi(argv[globalUtilOptind]);
+            nBTLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            break;
+        case 'D':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-D\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            DelayMax = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
             break;
+        case 'd':
+            fDelay ^= 1;
+            break;
         case 'r':
             fReverse ^= 1;
             break;
+        case 'w':
+            fVeryVerbose ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -34880,15 +34896,18 @@ int Abc_CommandAbc9SatLut( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     if ( Gia_ManLutSizeMax(pAbc->pGia) > 4 )
-        Abc_Print( 0, "Current AIG has mapping into %d-LUTs.\n", Gia_ManLutSizeMax(pAbc->pGia) );
-    Gia_ManLutSat( pAbc->pGia, nNumber, nConfl, fReverse, fVerbose );
+        Abc_Print( 0, "Current AIG is mapped into %d-LUTs (only 4-LUT mapping is currently supported).\n", Gia_ManLutSizeMax(pAbc->pGia) );
+    else
+        Gia_ManLutSat( pAbc->pGia, nNumber, nBTLimit, DelayMax, fDelay, fReverse, fVeryVerbose, fVerbose );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &satlut [-NC num] [-rvh]\n" );
+    Abc_Print( -2, "usage: &satlut [-NCD num] [-drwvh]\n" );
     Abc_Print( -2, "\t           performs SAT-based remapping of the 4-LUT network\n" );
     Abc_Print( -2, "\t-N num   : the limit on the number of AIG nodes in the window [default = %d]\n", nNumber );
-    Abc_Print( -2, "\t-C num   : the limit on the number of conflicts [default = %d]\n", nNumber );
+    Abc_Print( -2, "\t-C num   : the limit on the number of conflicts [default = %d]\n", nBTLimit );
+    Abc_Print( -2, "\t-D num   : the user-specified required times at the outputs [default = %d]\n", DelayMax );
+    Abc_Print( -2, "\t-d       : toggles delay optimization [default = %s]\n", fDelay? "yes": "no" );
     Abc_Print( -2, "\t-r       : toggles using reverse search [default = %s]\n", fReverse? "yes": "no" );
     Abc_Print( -2, "\t-v       : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h       : prints the command usage\n");