Further improvements to reachability.

4 files changed, 191 insertions, 52 deletions

diff --git a/src/aig/llb/llb4Cluster.c b/src/aig/llb/llb4Cluster.c
index 71e044be..8697a01d 100644
--- a/src/aig/llb/llb4Cluster.c
+++ b/src/aig/llb/llb4Cluster.c
@@ -70,7 +70,8 @@ void Llb_Nonlin4FindOrder_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * v
         Llb_Nonlin4FindOrder_rec( pAig, pFanin1, vOrder, pCounter );
         Llb_Nonlin4FindOrder_rec( pAig, pFanin0, vOrder, pCounter );
     }
-    Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ );
+    if ( pObj->fMarkA )
+        Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ );
 }
 
 /**Function*************************************************************
@@ -84,19 +85,27 @@ void Llb_Nonlin4FindOrder_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * v
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Llb_Nonlin4FindOrder( Aig_Man_t * pAig )
+Vec_Int_t * Llb_Nonlin4FindOrder( Aig_Man_t * pAig, int * pCounter )
 {
     Vec_Int_t * vNodes = NULL;
     Vec_Int_t * vOrder;
     Aig_Obj_t * pObj;
     int i, Counter = 0;
+    // mark nodes to exclude:  AND with low level and CO drivers
+    Aig_ManCleanMarkA( pAig );
+    Aig_ManForEachNode( pAig, pObj, i )
+        if ( Aig_ObjLevel(pObj) > 3 )
+            pObj->fMarkA = 1;
+    Aig_ManForEachPo( pAig, pObj, i )
+        Aig_ObjFanin0(pObj)->fMarkA = 0;
+
     // collect nodes in the order
     vOrder = Vec_IntStartFull( Aig_ManObjNumMax(pAig) );
     Aig_ManIncrementTravId( pAig );
     Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) );
-    Aig_ManForEachPo( pAig, pObj, i )
+//    Aig_ManForEachPo( pAig, pObj, i )
+    Saig_ManForEachLi( pAig, pObj, i )
     {
-printf( "PO %d Var %d\n", i, Counter );
         Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
         Llb_Nonlin4FindOrder_rec( pAig, Aig_ObjFanin0(pObj), vOrder, &Counter );
     }
@@ -105,7 +114,27 @@ printf( "PO %d Var %d\n", i, Counter );
             Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
     Aig_ManCleanMarkA( pAig );
     Vec_IntFreeP( &vNodes );
-    assert( Counter == Aig_ManObjNum(pAig) - 1 );
+//    assert( Counter == Aig_ManObjNum(pAig) - 1 );
+
+/*
+    Saig_ManForEachPi( pAig, pObj, i )
+        printf( "pi%d ", Llb_MnxBddVar(vOrder, pObj) );
+    printf( "\n" );
+    Saig_ManForEachLo( pAig, pObj, i )
+        printf( "lo%d ", Llb_MnxBddVar(vOrder, pObj) );
+    printf( "\n" );
+    Saig_ManForEachPo( pAig, pObj, i )
+        printf( "po%d ", Llb_MnxBddVar(vOrder, pObj) );
+    printf( "\n" );
+    Saig_ManForEachLi( pAig, pObj, i )
+        printf( "li%d ", Llb_MnxBddVar(vOrder, pObj) );
+    printf( "\n" );
+    Aig_ManForEachNode( pAig, pObj, i )
+        printf( "n%d ", Llb_MnxBddVar(vOrder, pObj) );
+    printf( "\n" );
+*/
+    if ( pCounter )
+        *pCounter = Counter;
     return vOrder;
 }
 
@@ -137,7 +166,8 @@ Vec_Ptr_t * Llb_Nonlin4FindPartitions( DdManager * dd, Aig_Man_t * pAig, Vec_Int
             pObj->pData = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObj) );
             Cudd_Ref( (DdNode *)pObj->pData );
         }
-    Aig_ManForEachPo( pAig, pObj, i )
+//    Aig_ManForEachPo( pAig, pObj, i )
+    Saig_ManForEachLi( pAig, pObj, i )
         pObj->pData = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObj) );
     // compute intermediate BDDs
     vRoots = Vec_PtrAlloc( 100 );
@@ -161,7 +191,8 @@ Vec_Ptr_t * Llb_Nonlin4FindPartitions( DdManager * dd, Aig_Man_t * pAig, Vec_Int
         Vec_PtrPush( vRoots, bPart );
     }
     // compute register output BDDs
-    Aig_ManForEachPo( pAig, pObj, i )
+//    Aig_ManForEachPo( pAig, pObj, i )
+    Saig_ManForEachLi( pAig, pObj, i )
     {
         bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
         bPart = Cudd_bddXnor( dd, (DdNode *)pObj->pData, bBdd0 );  
@@ -206,7 +237,8 @@ Vec_Int_t * Llb_Nonlin4FindVars2Q( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t *
     Vec_IntFill( vVars2Q, Cudd_ReadSize(dd), 1 );
     Saig_ManForEachLo( pAig, pObj, i )
         Vec_IntWriteEntry( vVars2Q, Llb_MnxBddVar(vOrder, pObj), 0 );
-    Aig_ManForEachPo( pAig, pObj, i )
+//    Aig_ManForEachPo( pAig, pObj, i )
+    Saig_ManForEachLi( pAig, pObj, i )
         Vec_IntWriteEntry( vVars2Q, Llb_MnxBddVar(vOrder, pObj), 0 );
     return vVars2Q;
 }
@@ -227,28 +259,32 @@ int Llb_Nonlin4CountTerms( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder,
     DdNode * bSupp;
     Aig_Obj_t * pObj;
     int i, Counter = 0;
-    bSupp = Cudd_Support( dd, bFunc );  Cudd_Ref( bFunc );
+    bSupp = Cudd_Support( dd, bFunc );  Cudd_Ref( bSupp );
     if ( !fCo && !fFlop )
     {
         Saig_ManForEachPi( pAig, pObj, i )
-            Counter += Cudd_bddLeq( dd, bSupp, Cudd_bddIthVar(dd, Llb_MnxBddVar(vOrder, pObj)) );
+            if ( Llb_MnxBddVar(vOrder, pObj) >= 0 )
+                Counter += Cudd_bddLeq( dd, bSupp, Cudd_bddIthVar(dd, Llb_MnxBddVar(vOrder, pObj)) );
     }
     else if ( fCo && !fFlop )
     {
         Saig_ManForEachPo( pAig, pObj, i )
-            Counter += Cudd_bddLeq( dd, bSupp, Cudd_bddIthVar(dd, Llb_MnxBddVar(vOrder, pObj)) );
+            if ( Llb_MnxBddVar(vOrder, pObj) >= 0 )
+                Counter += Cudd_bddLeq( dd, bSupp, Cudd_bddIthVar(dd, Llb_MnxBddVar(vOrder, pObj)) );
     }
     else if ( !fCo && fFlop )
     {
         Saig_ManForEachLo( pAig, pObj, i )
-            Counter += Cudd_bddLeq( dd, bSupp, Cudd_bddIthVar(dd, Llb_MnxBddVar(vOrder, pObj)) );
+            if ( Llb_MnxBddVar(vOrder, pObj) >= 0 )
+                Counter += Cudd_bddLeq( dd, bSupp, Cudd_bddIthVar(dd, Llb_MnxBddVar(vOrder, pObj)) );
     }
     else if ( fCo && fFlop )
     {
         Saig_ManForEachLi( pAig, pObj, i )
-            Counter += Cudd_bddLeq( dd, bSupp, Cudd_bddIthVar(dd, Llb_MnxBddVar(vOrder, pObj)) );
+            if ( Llb_MnxBddVar(vOrder, pObj) >= 0 )
+                Counter += Cudd_bddLeq( dd, bSupp, Cudd_bddIthVar(dd, Llb_MnxBddVar(vOrder, pObj)) );
     }
-    Cudd_RecursiveDeref( dd, bFunc );
+    Cudd_RecursiveDeref( dd, bSupp );
     return Counter;
 }
 
@@ -269,6 +305,7 @@ void Llb_Nonlin4PrintGroups( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrde
     int i, nSuppAll, nSuppPi, nSuppPo, nSuppLi, nSuppLo, nSuppAnd;
     Vec_PtrForEachEntry( DdNode *, vGroups, bTemp, i )
     {
+//Extra_bddPrintSupport(dd, bTemp);  printf("\n" );
         nSuppAll = Cudd_SupportSize(dd,bTemp);
         nSuppPi  = Llb_Nonlin4CountTerms(dd, pAig, vOrder, bTemp, 0, 0);
         nSuppPo  = Llb_Nonlin4CountTerms(dd, pAig, vOrder, bTemp, 1, 0);
@@ -276,6 +313,9 @@ void Llb_Nonlin4PrintGroups( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrde
         nSuppLo  = Llb_Nonlin4CountTerms(dd, pAig, vOrder, bTemp, 1, 1);
         nSuppAnd = nSuppAll - (nSuppPi+nSuppPo+nSuppLi+nSuppLo);
 
+        if ( Cudd_DagSize(bTemp) <= 10 )
+            continue;
+
         printf( "%4d : bdd =%6d  supp =%3d  ", i, Cudd_DagSize(bTemp), nSuppAll );
         printf( "pi =%3d ",  nSuppPi );
         printf( "po =%3d ",  nSuppPo );
@@ -288,6 +328,60 @@ void Llb_Nonlin4PrintGroups( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrde
 
 /**Function*************************************************************
 
+  Synopsis    [Creates quantifiable varaibles for both types of traversal.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_Nonlin4PrintSuppProfile( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, Vec_Ptr_t * vGroups )
+{
+    Aig_Obj_t * pObj;
+    int i, * pSupp;
+    int nSuppAll = 0, nSuppPi = 0, nSuppPo = 0, nSuppLi = 0, nSuppLo = 0, nSuppAnd = 0;
+
+    pSupp = ABC_CALLOC( int, Cudd_ReadSize(dd) );
+    Extra_VectorSupportArray( dd, (DdNode **)Vec_PtrArray(vGroups), Vec_PtrSize(vGroups), pSupp );
+
+    Aig_ManForEachObj( pAig, pObj, i )
+    {
+        if ( Llb_MnxBddVar(vOrder, pObj) < 0 )
+            continue;
+        // remove variables that do not participate
+        if ( pSupp[Llb_MnxBddVar(vOrder, pObj)] == 0 )
+        {
+            if ( Aig_ObjIsNode(pObj) )
+                Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), -1 );
+            continue;
+        }
+        nSuppAll++;
+        if ( Saig_ObjIsPi(pAig, pObj) )
+            nSuppPi++;
+        else if ( Saig_ObjIsLo(pAig, pObj) )
+            nSuppLo++;
+        else if ( Saig_ObjIsPo(pAig, pObj) )
+            nSuppPo++;
+        else if ( Saig_ObjIsLi(pAig, pObj) )
+            nSuppLi++;
+        else
+            nSuppAnd++;
+    }
+    ABC_FREE( pSupp );
+
+    printf( "Variable counts: all =%4d ",  nSuppAll );
+    printf( "pi =%4d ",  nSuppPi );
+    printf( "po =%4d ",  nSuppPo );
+    printf( "lo =%4d ",  nSuppLo );
+    printf( "li =%4d ",  nSuppLi );
+    printf( "and =%4d",  nSuppAnd );
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -297,37 +391,60 @@ void Llb_Nonlin4PrintGroups( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrde
   SeeAlso     []
 
 ***********************************************************************/
-void Llb_Nonlin4Cluster( Aig_Man_t * pAig )
+void Llb_Nonlin4Cluster( Aig_Man_t * pAig, DdManager ** pdd, Vec_Int_t ** pvOrder, Vec_Ptr_t ** pvGroups, int nBddMax, int fVerbose )
 {
     DdManager * dd;
     Vec_Int_t * vOrder, * vVars2Q;
     Vec_Ptr_t * vParts, * vGroups;
     DdNode * bTemp;
-    int i;
+    int i, nVarNum;
 
     // create the BDD manager
-    dd      = Cudd_Init( Aig_ManObjNumMax(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
-//    Cudd_AutodynEnable( p->dd,  CUDD_REORDER_SYMM_SIFT );
-    vOrder  = Llb_Nonlin4FindOrder( pAig );
+    vOrder  = Llb_Nonlin4FindOrder( pAig, &nVarNum );
+    dd      = Cudd_Init( nVarNum, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+//    Cudd_AutodynEnable( dd,  CUDD_REORDER_SYMM_SIFT );
+
     vVars2Q = Llb_Nonlin4FindVars2Q( dd, pAig, vOrder );
     vParts  = Llb_Nonlin4FindPartitions( dd, pAig, vOrder );
 
-    vGroups = Llb_Nonlin4Group( dd, vParts, vVars2Q, 500 );
+    vGroups = Llb_Nonlin4Group( dd, vParts, vVars2Q, nBddMax );
+    Vec_IntFree( vVars2Q );
+
+    Vec_PtrForEachEntry( DdNode *, vParts, bTemp, i )
+        Cudd_RecursiveDeref( dd, bTemp );
+    Vec_PtrFree( vParts );
+
 
+//    if ( fVerbose )
+    Llb_Nonlin4PrintSuppProfile( dd, pAig, vOrder, vGroups );
+    if ( fVerbose )
+    printf( "Before reordering\n" );
+    if ( fVerbose )
     Llb_Nonlin4PrintGroups( dd, pAig, vOrder, vGroups );
 
-    Vec_PtrForEachEntry( DdNode *, vGroups, bTemp, i )
-        Cudd_RecursiveDeref( dd, bTemp );
+//    Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 1 );
+//    printf( "After reordering\n" );
+//    Llb_Nonlin4PrintGroups( dd, pAig, vOrder, vGroups );
 
-    Vec_PtrForEachEntry( DdNode *, vParts, bTemp, i )
-        Cudd_RecursiveDeref( dd, bTemp );
-    Extra_StopManager( dd );
-//    Cudd_Quit( dd );
+    if ( pvOrder )
+        *pvOrder = vOrder;
+    else
+        Vec_IntFree( vOrder );
 
-    Vec_IntFree( vOrder );
-    Vec_IntFree( vVars2Q );
-    Vec_PtrFree( vParts );
-    Vec_PtrFree( vGroups );
+    if ( pvGroups )
+        *pvGroups = vGroups;
+    else
+    {
+        Vec_PtrForEachEntry( DdNode *, vGroups, bTemp, i )
+            Cudd_RecursiveDeref( dd, bTemp );
+        Vec_PtrFree( vGroups );
+    }
+
+    if ( pdd )
+        *pdd = dd;
+    else
+        Extra_StopManager( dd );
+//    Cudd_Quit( dd );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/llb/llb4Image.c b/src/aig/llb/llb4Image.c
index 45efaead..acc34b22 100644
--- a/src/aig/llb/llb4Image.c
+++ b/src/aig/llb/llb4Image.c
@@ -116,6 +116,7 @@ void Llb_Nonlin4RemoveVar( Llb_Mgr_t * p, Llb_Var_t * pVar )
 ***********************************************************************/
 void Llb_Nonlin4RemovePart( Llb_Mgr_t * p, Llb_Prt_t * pPart )
 {
+//printf( "Removing %d\n", pPart->iPart );
     assert( p->pParts[pPart->iPart] == pPart );
     p->pParts[pPart->iPart] = NULL;
     Vec_IntFree( pPart->vVars );
@@ -329,7 +330,7 @@ int Llb_Nonlin4Quantify2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * pPart2
     // create cube to be quantified
     bCube = Llb_Nonlin4CreateCube2( p, pPart1, pPart2 );   Cudd_Ref( bCube );
 
-printf( "Quantifying  " ); Extra_bddPrintSupport( p->dd, bCube );  printf( "\n" );
+//printf( "Quantifying  " ); Extra_bddPrintSupport( p->dd, bCube );  printf( "\n" );
 
 if ( fVerbose )
 {
@@ -352,7 +353,9 @@ liveEnd = p->dd->keys - p->dd->dead;
     Cudd_Ref( bFunc );
     Cudd_RecursiveDeref( p->dd, bCube );
 
-printf( "Createing part %d ", p->iPartFree ); Extra_bddPrintSupport( p->dd, bFunc );  printf( "\n" );
+//printf( "Creating part %d ", p->iPartFree ); Extra_bddPrintSupport( p->dd, bFunc );  printf( "\n" );
+
+//printf( "Creating %d\n", p->iPartFree );
 
     // create new partition
     pTemp = p->pParts[p->iPartFree] = ABC_CALLOC( Llb_Prt_t, 1 );
@@ -530,6 +533,7 @@ void Llb_Nonlin4AddPartition( Llb_Mgr_t * p, int i, DdNode * bFunc )
 {
     int k, nSuppSize;
     assert( !Cudd_IsConstant(bFunc) );
+//printf( "Creating init %d\n", i );
     // create partition
     p->pParts[i] = ABC_CALLOC( Llb_Prt_t, 1 );
     p->pParts[i]->iPart = i;
@@ -610,9 +614,9 @@ int Llb_Nonlin4NextPartitions( Llb_Mgr_t * p, Llb_Prt_t ** ppPart1, Llb_Prt_t **
                 pPart2Best = pPart;
         }
     }
-printf( "Selecting %d and parts %d and %d\n", pVarBest->iVar, pPart1Best->nSize, pPart2Best->nSize );
-Extra_bddPrintSupport( p->dd, pPart1Best->bFunc ); printf( "\n" );
-Extra_bddPrintSupport( p->dd, pPart2Best->bFunc ); printf( "\n" );
+//printf( "Selecting %d and parts %d and %d\n", pVarBest->iVar, pPart1Best->nSize, pPart2Best->nSize );
+//Extra_bddPrintSupport( p->dd, pPart1Best->bFunc ); printf( "\n" );
+//Extra_bddPrintSupport( p->dd, pPart2Best->bFunc ); printf( "\n" );
 
     *ppPart1 = pPart1Best;
     *ppPart2 = pPart2Best;
@@ -802,7 +806,7 @@ Vec_Ptr_t * Llb_Nonlin4Group( DdManager * dd, Vec_Ptr_t * vParts, Vec_Int_t * vV
     Vec_Ptr_t * vGroups;
     Llb_Prt_t * pPart, * pPart1, * pPart2;
     Llb_Mgr_t * p;
-    int i, nReorders;
+    int i, nReorders, clk = clock();
     // start the manager
     p = Llb_Nonlin4Alloc( dd, vParts, NULL, vVars2Q, nSizeMax );
     // remove singles
@@ -822,24 +826,28 @@ Vec_Ptr_t * Llb_Nonlin4Group( DdManager * dd, Vec_Ptr_t * vParts, Vec_Int_t * vV
         }
         if ( nReorders < Cudd_ReadReorderings(dd) )
             Llb_Nonlin4RecomputeScores( p );
-        else
-            Llb_Nonlin4VerifyScores( p );
+//        else
+//            Llb_Nonlin4VerifyScores( p );
     }
     // load partitions
     vGroups = Vec_PtrAlloc( 1000 );
     Llb_MgrForEachPart( p, pPart, i )
     {
+//printf( "Iteration %d ", pPart->iPart );
         if ( Cudd_IsConstant(pPart->bFunc) )
         {
+//printf( "Constant\n" );
             assert( !Cudd_IsComplement(pPart->bFunc) );
             continue;
         }
+//printf( "\n" );
         Vec_PtrPush( vGroups, pPart->bFunc );
         Cudd_Ref( pPart->bFunc );
-printf( "Part %d  ", pPart->iPart );
-Extra_bddPrintSupport( p->dd, pPart->bFunc ); printf( "\n" );
+//printf( "Part %d  ", pPart->iPart );
+//Extra_bddPrintSupport( p->dd, pPart->bFunc ); printf( "\n" );
     }
     Llb_Nonlin4Free( p );
+Abc_PrintTime( 1, "Reparametrization time", clock() - clk );
     return vGroups;
 }
 
diff --git a/src/aig/llb/llb4Nonlin.c b/src/aig/llb/llb4Nonlin.c
index d7b3c6c3..a432179f 100644
--- a/src/aig/llb/llb4Nonlin.c
+++ b/src/aig/llb/llb4Nonlin.c
@@ -246,7 +246,7 @@ Vec_Int_t * Llb_Nonlin4CreateOrderSimple( Aig_Man_t * pAig )
   SeeAlso     []
 
 ***********************************************************************/
-void Llb_Nonlin4CreateOrderSmart_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vOrder, int * pCounter )
+void Llb_Nonlin4CreateOrder_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vOrder, int * pCounter )
 {
     Aig_Obj_t * pFanin0, * pFanin1;
     if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
@@ -266,13 +266,13 @@ void Llb_Nonlin4CreateOrderSmart_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_In
 //    if ( pFanin0->Level > pFanin1->Level || (pFanin0->Level == pFanin1->Level && pFanin0->Id < pFanin1->Id) )
     if ( pFanin0->Level > pFanin1->Level )
     {
-        Llb_Nonlin4CreateOrderSmart_rec( pAig, pFanin0, vOrder, pCounter );
-        Llb_Nonlin4CreateOrderSmart_rec( pAig, pFanin1, vOrder, pCounter );
+        Llb_Nonlin4CreateOrder_rec( pAig, pFanin0, vOrder, pCounter );
+        Llb_Nonlin4CreateOrder_rec( pAig, pFanin1, vOrder, pCounter );
     }
     else
     {
-        Llb_Nonlin4CreateOrderSmart_rec( pAig, pFanin1, vOrder, pCounter );
-        Llb_Nonlin4CreateOrderSmart_rec( pAig, pFanin0, vOrder, pCounter );
+        Llb_Nonlin4CreateOrder_rec( pAig, pFanin1, vOrder, pCounter );
+        Llb_Nonlin4CreateOrder_rec( pAig, pFanin0, vOrder, pCounter );
     }
     if ( pObj->fMarkA )
         Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ );
@@ -321,7 +321,7 @@ Vec_Int_t * Llb_Nonlin4CollectHighRefNodes( Aig_Man_t * pAig, int nFans )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Llb_Nonlin4CreateOrderSmart( Aig_Man_t * pAig )
+Vec_Int_t * Llb_Nonlin4CreateOrder( Aig_Man_t * pAig )
 {
     Vec_Int_t * vNodes = NULL;
     Vec_Int_t * vOrder;
@@ -335,7 +335,6 @@ Vec_Int_t * Llb_Nonlin4CreateOrderSmart( Aig_Man_t * pAig )
         pObj->fMarkA = 1;
 printf( "Techmapping added %d pivots.\n", Vec_IntSize(vNodes) );
 */
-
     // collect nodes in the order
     vOrder = Vec_IntStartFull( Aig_ManObjNumMax(pAig) );
     Aig_ManIncrementTravId( pAig );
@@ -343,7 +342,7 @@ printf( "Techmapping added %d pivots.\n", Vec_IntSize(vNodes) );
     Saig_ManForEachLi( pAig, pObj, i )
     {
         Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
-        Llb_Nonlin4CreateOrderSmart_rec( pAig, Aig_ObjFanin0(pObj), vOrder, &Counter );
+        Llb_Nonlin4CreateOrder_rec( pAig, Aig_ObjFanin0(pObj), vOrder, &Counter );
     }
     Aig_ManForEachPi( pAig, pObj, i )
         if ( Llb_MnxBddVar(vOrder, pObj) < 0 )
@@ -410,6 +409,8 @@ void Llb_Nonlin4SetupVarMap( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrde
     pVarsY = ABC_ALLOC( DdNode *, Cudd_ReadSize(dd) );
     Saig_ManForEachLiLo( pAig, pObjLo, pObjLi, i )
     {
+        assert( Llb_MnxBddVar(vOrder, pObjLo) >= 0 );
+        assert( Llb_MnxBddVar(vOrder, pObjLi) >= 0 );
         pVarsX[i] = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObjLo) );
         pVarsY[i] = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObjLi) );
     }
@@ -830,14 +831,25 @@ Llb_Mnx_t * Llb_MnxStart( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
     p = ABC_CALLOC( Llb_Mnx_t, 1 );
     p->pAig    = pAig;
     p->pPars   = pPars;
+
+    if ( pPars->fCluster )
+    {
+        Llb_Nonlin4Cluster( p->pAig, &p->dd, &p->vOrder, &p->vRoots, pPars->nBddMax, pPars->fVerbose );
+        Cudd_AutodynEnable( p->dd,  CUDD_REORDER_SYMM_SIFT );
+    }
+    else
+    {
 //    p->vOrder  = Llb_Nonlin4CreateOrderSimple( pAig );
-    p->vOrder  = Llb_Nonlin4CreateOrderSmart( pAig );
-    p->dd      = Cudd_Init( Vec_IntSize(p->vOrder), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+        p->vOrder  = Llb_Nonlin4CreateOrder( pAig );
+        p->dd      = Cudd_Init( Vec_IntSize(p->vOrder), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+        Cudd_AutodynEnable( p->dd,  CUDD_REORDER_SYMM_SIFT );
+        p->vRoots  = Llb_Nonlin4DerivePartitions( p->dd, pAig, p->vOrder );
+    }
+
     Llb_Nonlin4SetupVarMap( p->dd, pAig, p->vOrder );
-    Cudd_AutodynEnable( p->dd,  CUDD_REORDER_SYMM_SIFT );
     p->vVars2Q = Llb_Nonlin4CreateVars2Q( p->dd, pAig, p->vOrder, 1 );
-    p->vRoots  = Llb_Nonlin4DerivePartitions( p->dd, pAig, p->vOrder );
     p->vRings  = Vec_PtrAlloc( 100 );
+
     if ( pPars->fReorder )
         Llb_Nonlin4Reorder( p->dd, 0, 1 );
     return p;
diff --git a/src/aig/llb/llbInt.h b/src/aig/llb/llbInt.h
index 5d145831..d3fd2e49 100644
--- a/src/aig/llb/llbInt.h
+++ b/src/aig/llb/llbInt.h
@@ -182,6 +182,8 @@ extern DdNode *        Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, V
 /*=== llb3Nonlin.c ======================================================*/
 extern DdNode *        Llb_NonlinComputeInitState( Aig_Man_t * pAig, DdManager * dd );
 
+/*=== llb4Cluster.c =======================================================*/
+extern void            Llb_Nonlin4Cluster( Aig_Man_t * pAig, DdManager ** pdd, Vec_Int_t ** pvOrder, Vec_Ptr_t ** pvGroups, int nBddMax, int fVerbose );
 /*=== llb4Image.c =======================================================*/
 extern DdNode *        Llb_Nonlin4Image( DdManager * dd, Vec_Ptr_t * vParts, DdNode * bCurrent, Vec_Int_t * vVars2Q );
 extern Vec_Ptr_t *     Llb_Nonlin4Group( DdManager * dd, Vec_Ptr_t * vParts, Vec_Int_t * vVars2Q, int nSizeMax );