initial commit of public abc

16 files changed, 4351 insertions, 0 deletions

diff --git a/src/aig/llb/llb.c b/src/aig/llb/llb.c
new file mode 100644
index 00000000..348c0622
--- /dev/null
+++ b/src/aig/llb/llb.c
@@ -0,0 +1,52 @@
+/**CFile****************************************************************
+
+  FileName    [llb.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [BDD based reachability.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: llb.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "llbInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/llb/llb.h b/src/aig/llb/llb.h
new file mode 100644
index 00000000..2c8d1c19
--- /dev/null
+++ b/src/aig/llb/llb.h
@@ -0,0 +1,92 @@
+/**CFile****************************************************************
+
+  FileName    [llb.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [BDD-based reachability.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 8, 2010.]
+
+  Revision    [$Id: llb.h,v 1.00 2010/05/08 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __LLB_H__
+#define __LLB_H__
+
+ 
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+
+
+ABC_NAMESPACE_HEADER_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+  
+typedef struct Gia_ParLlb_t_ Gia_ParLlb_t;
+struct Gia_ParLlb_t_
+{
+    int         nBddMax;       // maximum BDD size
+    int         nIterMax;      // maximum iteration count
+    int         nClusterMax;   // maximum cluster size
+    int         nHintDepth;    // the number of times to cofactor
+    int         HintFirst;     // the number of first hint to use
+    int         fUseFlow;      // use flow computation
+    int         nVolumeMax;    // the largest volume
+    int         nVolumeMin;    // the smallest volume
+    int         fReorder;      // enable dynamic variable reordering
+    int         fIndConstr;    // extract inductive constraints
+    int         fUsePivots;    // use internal pivot variables
+    int         fCluster;      // use partition clustering
+    int         fSchedule;     // use cluster scheduling
+    int         fVerbose;      // print verbose information
+    int         fVeryVerbose;  // print dependency matrices
+    int         fSilent;       // do not print any infomation
+    int         fSkipReach;    // skip reachability (preparation phase only)
+    int         fSkipOutCheck; // does not check the property output
+    int         TimeLimit;     // time limit for one reachability run
+    int         TimeLimitGlo;  // time limit for all reachability runs
+    // internal parameters
+    int         TimeTarget;    // the time to stop
+    int         iFrame;        // explored up to this frame
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== llbCore.c ==========================================================*/
+extern void     Llb_ManSetDefaultParams( Gia_ParLlb_t * pPars );
+
+
+
+ABC_NAMESPACE_HEADER_END
+
+
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/llb/llbCex.c b/src/aig/llb/llbCex.c
new file mode 100644
index 00000000..87059c0c
--- /dev/null
+++ b/src/aig/llb/llbCex.c
@@ -0,0 +1,56 @@
+/**CFile****************************************************************
+
+  FileName    [llbCex.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [BDD based reachability.]
+
+  Synopsis    [Deriving counter-example.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: llbCex.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "llbInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Cex_t * Llb_ManDeriveCex( Llb_Man_t * p, DdNode * bInter, int iOutFail, int iIter )
+{
+    return NULL;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/llb/llbCluster.c b/src/aig/llb/llbCluster.c
new file mode 100644
index 00000000..1d0153ce
--- /dev/null
+++ b/src/aig/llb/llbCluster.c
@@ -0,0 +1,357 @@
+/**CFile****************************************************************
+
+  FileName    [llbCluster.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [BDD based reachability.]
+
+  Synopsis    [Clustering algorithm.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: llbCluster.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "llbInt.h"
+#include "extra.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Llb_ManComputeCommonQuant( Llb_Mtr_t * p, int iCol1, int iCol2 )
+{
+    int iVar, Weight = 0;
+    for ( iVar = 0; iVar < p->nRows - p->nFfs; iVar++ )
+    {
+        // count each removed variable as 2
+        if ( p->pMatrix[iCol1][iVar] == 1 && p->pMatrix[iCol2][iVar] == 1 && p->pRowSums[iVar] == 2 )
+            Weight += 2;
+        // count each added variale as -1
+        else if ( (p->pMatrix[iCol1][iVar] == 1 && p->pMatrix[iCol2][iVar] == 0) || 
+                  (p->pMatrix[iCol1][iVar] == 0 && p->pMatrix[iCol2][iVar] == 1) )
+            Weight--;
+    }
+    return Weight;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Llb_ManComputeBestQuant( Llb_Mtr_t * p )
+{
+    int i, k, WeightBest = -100000, WeightCur, RetValue = -1;
+    for ( i = 1; i < p->nCols-1; i++ )
+    for ( k = i+1; k < p->nCols-1; k++ )
+    {
+        if ( p->pColSums[i] == 0 || p->pColSums[i] > p->pMan->pPars->nClusterMax )
+            continue;
+        if ( p->pColSums[k] == 0 || p->pColSums[k] > p->pMan->pPars->nClusterMax )
+            continue;
+
+        WeightCur = Llb_ManComputeCommonQuant( p, i, k );
+        if ( WeightCur <= 0 )
+            continue;
+        if ( WeightBest < WeightCur )
+        {
+            WeightBest = WeightCur;
+            RetValue   = (i << 16) | k;
+        }
+    }
+//    printf( "Choosing best quant Weight %4d\n", WeightCur );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float ** Llb_ManComputeQuant( Llb_Mtr_t * p )
+{
+    float ** pCosts;
+    int i, k;
+    // alloc and clean
+    pCosts = (float **)Extra_ArrayAlloc( p->nCols, p->nCols, sizeof(float) );
+    for ( i = 0; i < p->nCols; i++ )
+    for ( k = 0; k < p->nCols; k++ )
+        pCosts[i][i] = 0.0;
+    // fill up
+    for ( i = 1; i < p->nCols-1; i++ )
+    for ( k = i+1; k < p->nCols-1; k++ )
+        pCosts[i][k] = pCosts[k][i] = Llb_ManComputeCommonQuant( p, i, k );
+    return pCosts;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Llb_ManComputeCommonAttr( Llb_Mtr_t * p, int iCol1, int iCol2 )
+{
+    int iVar, CountComm = 0, CountDiff = 0;
+    for ( iVar = 0; iVar < p->nRows - p->nFfs; iVar++ )
+    {
+        if ( p->pMatrix[iCol1][iVar] == 1 && p->pMatrix[iCol2][iVar] == 1 )
+            CountComm++;
+        else if ( p->pMatrix[iCol1][iVar] == 1 || p->pMatrix[iCol2][iVar] == 1 )
+            CountDiff++;
+    }
+/*
+    printf( "Attr cost for %4d and %4d:  %4d %4d (%5.2f)\n", 
+        iCol1, iCol2, 
+        CountDiff, CountComm, 
+        -1.0 * CountDiff / ( CountComm + CountDiff ) );
+*/
+    return -1.0 * CountDiff / ( CountComm + CountDiff );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Llb_ManComputeBestAttr( Llb_Mtr_t * p )
+{
+    float WeightBest = -100000, WeightCur;
+    int i, k, RetValue = -1;
+    for ( i = 1; i < p->nCols-1; i++ )
+    for ( k = i+1; k < p->nCols-1; k++ )
+    {
+        if ( p->pColSums[i] == 0 || p->pColSums[i] > p->pMan->pPars->nClusterMax )
+            continue;
+        if ( p->pColSums[k] == 0 || p->pColSums[k] > p->pMan->pPars->nClusterMax )
+            continue;
+        WeightCur = Llb_ManComputeCommonAttr( p, i, k );
+        if ( WeightBest < WeightCur )
+        {
+            WeightBest = WeightCur;
+            RetValue   = (i << 16) | k;
+        }
+    }
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float ** Llb_ManComputeAttr( Llb_Mtr_t * p )
+{
+    float ** pCosts;
+    int i, k;
+    // alloc and clean
+    pCosts = (float **)Extra_ArrayAlloc( p->nCols, p->nCols, sizeof(float) );
+    for ( i = 0; i < p->nCols; i++ )
+    for ( k = 0; k < p->nCols; k++ )
+        pCosts[i][i] = 0.0;
+    // fill up
+    for ( i = 1; i < p->nCols-1; i++ )
+    for ( k = i+1; k < p->nCols-1; k++ )
+        pCosts[i][k] = pCosts[k][i] = Llb_ManComputeCommonAttr( p, i, k );
+    return pCosts;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of variables that will be saved.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_MtrCombineSelectedColumns( Llb_Mtr_t * p, int iGrp1, int iGrp2 )
+{
+    int iVar;
+    assert( iGrp1 >= 1 && iGrp1 < p->nCols - 1 );
+    assert( iGrp2 >= 1 && iGrp2 < p->nCols - 1 );
+    assert( p->pColGrps[iGrp1] != NULL );
+    assert( p->pColGrps[iGrp2] != NULL );
+    for ( iVar = 0; iVar < p->nRows; iVar++ )
+    {
+        if ( p->pMatrix[iGrp1][iVar] == 1 && p->pMatrix[iGrp2][iVar] == 1 )
+            p->pRowSums[iVar]--;
+        if ( p->pMatrix[iGrp1][iVar] == 0 && p->pMatrix[iGrp2][iVar] == 1 )
+        {
+            p->pMatrix[iGrp1][iVar] = 1;
+            p->pColSums[iGrp1]++;
+        }
+        if ( p->pMatrix[iGrp2][iVar] == 1 )
+            p->pMatrix[iGrp2][iVar] = 0;
+    }
+    p->pColSums[iGrp2] = 0;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Combines one pair of columns.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_ManClusterOne( Llb_Mtr_t * p, int iCol1, int iCol2 )
+{
+    int fVerbose = 0;
+    Llb_Grp_t * pGrp;
+    int iVar;
+
+    if ( fVerbose )
+    {
+        printf( "Combining %d and %d\n", iCol1, iCol2 );
+        for ( iVar = 0; iVar < p->nRows; iVar++ )
+        {
+            if ( p->pMatrix[iCol1][iVar] == 0 && p->pMatrix[iCol2][iVar] == 0 )
+                continue;
+            printf( "%3d : %c%c\n", iVar, 
+                p->pMatrix[iCol1][iVar]? '*':' ', 
+                p->pMatrix[iCol2][iVar]? '*':' ' );
+        }
+    }
+    pGrp = Llb_ManGroupsCombine( p->pColGrps[iCol1], p->pColGrps[iCol2] );
+    Llb_MtrCombineSelectedColumns( p, iCol1, iCol2 );
+    p->pColGrps[iCol1] = pGrp;
+    p->pColGrps[iCol2] = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes empty columns.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_ManClusterCompress( Llb_Mtr_t * p )
+{
+    int i, k = 0;
+    for ( i = 0; i < p->nCols; i++ )
+    {
+        if ( p->pColGrps[i] == NULL )
+        {
+            assert( p->pColSums[i] == 0 );
+            assert( p->pMatrix[i] != NULL );
+            ABC_FREE( p->pMatrix[i] );
+            continue;
+        }
+        p->pMatrix[k]  = p->pMatrix[i];
+        p->pColGrps[k] = p->pColGrps[i];
+        p->pColSums[k] = p->pColSums[i];
+        k++;
+    }
+    p->nCols = k;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Combines one pair of columns.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_ManCluster( Llb_Mtr_t * p )
+{
+    int RetValue;
+    do
+    {
+        do {
+            RetValue = Llb_ManComputeBestQuant( p );
+            if ( RetValue > 0 )
+                Llb_ManClusterOne( p, RetValue >> 16, RetValue & 0xffff );
+        }
+        while ( RetValue > 0 );
+
+        RetValue = Llb_ManComputeBestAttr( p );
+        if ( RetValue > 0 )
+            Llb_ManClusterOne( p, RetValue >> 16, RetValue & 0xffff );
+
+        Llb_MtrVerifyMatrix( p );
+    }
+    while ( RetValue > 0 );
+
+    Llb_ManClusterCompress( p );
+
+    Llb_MtrVerifyMatrix( p );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/llb/llbConstr.c b/src/aig/llb/llbConstr.c
new file mode 100644
index 00000000..eabae3bc
--- /dev/null
+++ b/src/aig/llb/llbConstr.c
@@ -0,0 +1,313 @@
+/**CFile****************************************************************
+
+  FileName    [llbConstr.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [BDD based reachability.]
+
+  Synopsis    [Computing inductive constraints.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: llbConstr.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "llbInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the array of constraint candidates.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Llb_ManCountEntries( Vec_Int_t * vCands )
+{
+    int i, Entry, Counter = 0;
+    Vec_IntForEachEntry( vCands, Entry, i )
+        Counter += ((Entry == 0) || (Entry == 1));
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the array of constraint candidates.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_ManPrintEntries( Aig_Man_t * p, Vec_Int_t * vCands )
+{
+    int i, Entry;
+    if ( vCands == NULL )
+    {
+        printf( "There is no hints.\n" );
+        return;
+    }
+    Entry = Llb_ManCountEntries(vCands);
+    printf( "\n*** Using %d hint%s:\n", Entry, (Entry != 1 ? "s":"") );
+    Vec_IntForEachEntry( vCands, Entry, i )
+    {
+        if ( Entry != 0 && Entry != 1 )
+            continue;
+        printf( "%c", Entry ? '+' : '-' );
+        printf( "%-6d : ", i );
+        Aig_ObjPrint( p, Aig_ManObj(p, i) );
+        printf( "\n" );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Dereference BDD nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_ManDerefenceBdds( Aig_Man_t * p, DdManager * dd )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    Aig_ManForEachObj( p, pObj, i )
+        Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the array of constraint candidates.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Llb_ManComputeIndCase_rec( Aig_Man_t * p, Aig_Obj_t * pObj, DdManager * dd, Vec_Ptr_t * vBdds )
+{
+    DdNode * bBdd0, * bBdd1;
+    DdNode * bFunc = (DdNode *)Vec_PtrEntry( vBdds, Aig_ObjId(pObj) );
+    if ( bFunc != NULL )
+        return bFunc;
+    assert( Aig_ObjIsNode(pObj) );
+    bBdd0 = Llb_ManComputeIndCase_rec( p, Aig_ObjFanin0(pObj), dd, vBdds ); 
+    bBdd1 = Llb_ManComputeIndCase_rec( p, Aig_ObjFanin1(pObj), dd, vBdds ); 
+    bBdd0 = Cudd_NotCond( bBdd0, Aig_ObjFaninC0(pObj) );
+    bBdd1 = Cudd_NotCond( bBdd1, Aig_ObjFaninC1(pObj) );
+    bFunc = Cudd_bddAnd( dd, bBdd0, bBdd1 );  Cudd_Ref( bFunc );
+    Vec_PtrWriteEntry( vBdds, Aig_ObjId(pObj), bFunc );
+    return bFunc;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the array of constraint candidates.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_ManComputeIndCase( Aig_Man_t * p, DdManager * dd, Vec_Int_t * vNodes )
+{
+    Vec_Ptr_t * vBdds;
+    Aig_Obj_t * pObj;
+    DdNode * bFunc;
+    int i, Entry;
+    vBdds = Vec_PtrStart( Aig_ManObjNumMax(p) );
+    bFunc = Cudd_ReadOne(dd); Cudd_Ref( bFunc );
+    Vec_PtrWriteEntry( vBdds, Aig_ObjId(Aig_ManConst1(p)), bFunc );
+    Saig_ManForEachPi( p, pObj, i )
+    {
+        bFunc = Cudd_bddIthVar( dd, Aig_ManPiNum(p) + i );  Cudd_Ref( bFunc );
+        Vec_PtrWriteEntry( vBdds, Aig_ObjId(pObj), bFunc );
+    }
+    Saig_ManForEachLi( p, pObj, i )
+    {
+        bFunc = (DdNode *)pObj->pData;  Cudd_Ref( bFunc );
+        Vec_PtrWriteEntry( vBdds, Aig_ObjId(Saig_ObjLiToLo(p, pObj)), bFunc );
+    }
+    Vec_IntForEachEntry( vNodes, Entry, i )
+    { 
+        if ( Entry != 0 && Entry != 1 )
+            continue;
+        pObj = Aig_ManObj( p, i );
+        bFunc = Llb_ManComputeIndCase_rec( p, pObj, dd, vBdds );
+        if ( Entry == 0 )
+        {
+//            Extra_bddPrint( dd, Cudd_Not(pObj->pData) );  printf( "\n" );
+//            Extra_bddPrint( dd, Cudd_Not(bFunc) );        printf( "\n" );
+            if ( !Cudd_bddLeq( dd, Cudd_Not(pObj->pData), Cudd_Not(bFunc) ) )
+                Vec_IntWriteEntry( vNodes, i, -1 );
+        }
+        else if ( Entry == 1 )
+        {
+//            Extra_bddPrint( dd, pObj->pData );  printf( "\n" );
+//            Extra_bddPrint( dd, bFunc );        printf( "\n" );
+            if ( !Cudd_bddLeq( dd, (DdNode *)pObj->pData, bFunc ) )
+                Vec_IntWriteEntry( vNodes, i, -1 );
+        }
+    }
+    Vec_PtrForEachEntry( DdNode *, vBdds, bFunc, i )
+        if ( bFunc )
+            Cudd_RecursiveDeref( dd, bFunc );
+    Vec_PtrFree( vBdds );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the array of constraint candidates.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Llb_ManComputeBaseCase( Aig_Man_t * p, DdManager * dd )
+{
+    Vec_Int_t * vNodes;
+    Aig_Obj_t * pObj, * pRoot;
+    int i;
+    pRoot = Aig_ManPo( p, 0 );
+    vNodes = Vec_IntStartFull( Aig_ManObjNumMax(p) );
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+            continue;
+        if ( Cudd_bddLeq( dd, (DdNode *)pObj->pData, Cudd_Not(pRoot->pData) ) )
+            Vec_IntWriteEntry( vNodes, i, 1 );
+        else if ( Cudd_bddLeq( dd, Cudd_Not((DdNode *)pObj->pData), Cudd_Not(pRoot->pData) ) )
+            Vec_IntWriteEntry( vNodes, i, 0 );
+    }
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Constructs global BDDs for each object in the AIG manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdManager * Llb_ManConstructGlobalBdds( Aig_Man_t * p )
+{
+    DdManager * dd;
+    DdNode * bBdd0, * bBdd1;
+    Aig_Obj_t * pObj;
+    int i;
+    dd = Cudd_Init( Aig_ManPiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    Cudd_AutodynEnable( dd,  CUDD_REORDER_SYMM_SIFT );
+    pObj = Aig_ManConst1(p);
+    pObj->pData = Cudd_ReadOne(dd);  Cudd_Ref( (DdNode *)pObj->pData );
+    Aig_ManForEachPi( p, pObj, i )
+    {
+        pObj->pData = Cudd_bddIthVar(dd, i);  Cudd_Ref( (DdNode *)pObj->pData );
+    }
+    Aig_ManForEachNode( p, pObj, i )
+    {
+        bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
+        bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
+        pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 );   Cudd_Ref( (DdNode *)pObj->pData );
+    }
+    Aig_ManForEachPo( p, pObj, i )
+    {
+        pObj->pData = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );  Cudd_Ref( (DdNode *)pObj->pData );
+    }
+    return dd;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives inductive constraints.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Llb_ManDeriveConstraints( Aig_Man_t * p )
+{
+    DdManager * dd;
+    Vec_Int_t * vNodes;
+    if ( Saig_ManPoNum(p) != 1 )
+    {
+        printf( "The AIG has %d property outputs.\n", Saig_ManPoNum(p) );
+        return NULL;
+    }
+    assert( Saig_ManPoNum(p) == 1 );
+    dd = Llb_ManConstructGlobalBdds( p );
+    vNodes = Llb_ManComputeBaseCase( p, dd );
+    if ( Llb_ManCountEntries(vNodes) > 0 )
+        Llb_ManComputeIndCase( p, dd, vNodes );
+    if ( Llb_ManCountEntries(vNodes) == 0 )
+        Vec_IntFreeP( &vNodes );
+    Llb_ManDerefenceBdds( p, dd );
+    Extra_StopManager( dd );
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Tests derived constraints.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_ManConstrTest( Aig_Man_t * p )
+{
+    Vec_Int_t * vNodes;
+    vNodes = Llb_ManDeriveConstraints( p );
+    Llb_ManPrintEntries( p, vNodes );
+    Vec_IntFreeP( &vNodes );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/llb/llbCore.c b/src/aig/llb/llbCore.c
new file mode 100644
index 00000000..562a9800
--- /dev/null
+++ b/src/aig/llb/llbCore.c
@@ -0,0 +1,219 @@
+/**CFile****************************************************************
+
+  FileName    [llbCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [BDD based reachability.]
+
+  Synopsis    [Top-level procedure.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: llbCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "llbInt.h"
+#include "gia.h"
+#include "giaAig.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+ 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_ManSetDefaultParams( Gia_ParLlb_t * p )
+{
+    memset( p, 0, sizeof(Gia_ParLlb_t) );
+    p->nBddMax       =  1000000;
+    p->nIterMax      =     1000;
+    p->nClusterMax   =       20;
+    p->nHintDepth    =        0;
+    p->HintFirst     =        0;
+    p->fUseFlow      =        0;  // use flow 
+    p->nVolumeMax    =      100;  // max volume
+    p->nVolumeMin    =       30;  // min volume
+    p->fReorder      =        1;
+    p->fIndConstr    =        0;
+    p->fUsePivots    =        0;
+    p->fCluster      =        0;
+    p->fSchedule     =        0;
+    p->fVerbose      =        0;
+    p->fVeryVerbose  =        0;
+    p->fSilent       =        0;
+    p->TimeLimit     =        0;
+//    p->TimeLimit     =        0;
+    p->TimeLimitGlo  =        0;
+    p->TimeTarget    =        0;
+    p->iFrame        =       -1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Prints statistics about MFFCs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_ManPrintAig( Llb_Man_t * p )
+{
+    Abc_Print( 1, "pi =%3d  ",    Saig_ManPiNum(p->pAig) );
+    Abc_Print( 1, "po =%3d  ",    Saig_ManPoNum(p->pAig) );
+    Abc_Print( 1, "ff =%3d  ",    Saig_ManRegNum(p->pAig) );
+    Abc_Print( 1, "int =%5d  ",   Vec_IntSize(p->vVar2Obj)-Aig_ManPiNum(p->pAig)-Saig_ManRegNum(p->pAig) );
+    Abc_Print( 1, "var =%5d  ",   Vec_IntSize(p->vVar2Obj) );
+    Abc_Print( 1, "part =%5d  ",  Vec_PtrSize(p->vGroups)-2 );
+    Abc_Print( 1, "and =%5d  ",   Aig_ManNodeNum(p->pAig) );
+    Abc_Print( 1, "lev =%4d  ",   Aig_ManLevelNum(p->pAig) );
+//    Abc_Print( 1, "cut =%4d  ",   Llb_ManCrossCut(p->pAig) );
+    Abc_Print( 1, "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Llb_ManModelCheckAig( Aig_Man_t * pAigGlo, Gia_ParLlb_t * pPars, Vec_Int_t * vHints, DdManager ** pddGlo )
+{
+    Llb_Man_t * p = NULL; 
+    Aig_Man_t * pAig;
+    int RetValue = -1;
+    int clk = clock();
+
+    if ( pPars->fIndConstr )
+    {
+        assert( vHints == NULL );
+        vHints = Llb_ManDeriveConstraints( pAigGlo );
+    }
+
+    // derive AIG for hints
+    if ( vHints == NULL )
+        pAig = Aig_ManDupSimple( pAigGlo );
+    else
+    {
+        if ( pPars->fVerbose )
+            Llb_ManPrintEntries( pAigGlo, vHints );
+        pAig = Aig_ManDupSimpleWithHints( pAigGlo, vHints );
+    }
+
+
+    if ( pPars->fUseFlow )
+    {
+//        p = Llb_ManStartFlow( pAigGlo, pAig, pPars );
+    }
+    else
+    {
+        p = Llb_ManStart( pAigGlo, pAig, pPars );
+        if ( pPars->fVerbose )
+        {
+            Llb_ManPrintAig( p );
+            printf( "Original matrix:          " );
+            Llb_MtrPrintMatrixStats( p->pMatrix );
+            if ( pPars->fVeryVerbose )
+                Llb_MtrPrint( p->pMatrix, 1 );
+        }
+        if ( pPars->fCluster )
+        {
+            Llb_ManCluster( p->pMatrix );
+            if ( pPars->fVerbose )
+            {
+                printf( "Matrix after clustering:  " );
+                Llb_MtrPrintMatrixStats( p->pMatrix );
+                if ( pPars->fVeryVerbose )
+                    Llb_MtrPrint( p->pMatrix, 1 );
+            }
+        }
+        if ( pPars->fSchedule )
+        {
+            Llb_MtrSchedule( p->pMatrix );
+            if ( pPars->fVerbose )
+            {
+                printf( "Matrix after scheduling:  " );
+                Llb_MtrPrintMatrixStats( p->pMatrix );
+                if ( pPars->fVeryVerbose )
+                    Llb_MtrPrint( p->pMatrix, 1 );
+            }
+        }
+    }
+    
+    if ( !p->pPars->fSkipReach ) 
+        RetValue = Llb_ManReachability( p, vHints, pddGlo );
+    Llb_ManStop( p );
+
+    Abc_PrintTime( 1, "Time", clock() - clk );
+
+    if ( pPars->fIndConstr )
+        Vec_IntFreeP( &vHints );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Llb_ManModelCheckGia( Gia_Man_t * pGia, Gia_ParLlb_t * pPars )
+{
+    Gia_Man_t * pGia2;
+    Aig_Man_t * pAig;
+    int RetValue = -1;
+    pGia2 = Gia_ManDupDfs( pGia );
+    pAig  = Gia_ManToAigSimple( pGia2 );
+    Gia_ManStop( pGia2 );
+//Aig_ManShow( pAig, 0, NULL ); 
+
+    if ( pPars->nHintDepth == 0 )
+        RetValue = Llb_ManModelCheckAig( pAig, pPars, NULL, NULL );
+    else
+        RetValue = Llb_ManModelCheckAigWithHints( pAig, pPars );
+    Aig_ManStop( pAig );
+    return RetValue;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/llb/llbFlow.c b/src/aig/llb/llbFlow.c
new file mode 100644
index 00000000..55405c09
--- /dev/null
+++ b/src/aig/llb/llbFlow.c
@@ -0,0 +1,639 @@
+/**CFile****************************************************************
+
+  FileName    [llbFlow.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [BDD based reachability.]
+
+  Synopsis    [Flow computation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: llbFlow.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "llbInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Llb_Flw_t_ Llb_Flw_t;
+struct Llb_Flw_t_
+{
+    unsigned    Source  :    1;  // source of the graph
+    unsigned    Sink    :    1;  // sink of the graph
+    unsigned    Flow    :    1;  // node has flow
+    unsigned    Mark    :    1;  // visited node
+    unsigned    Id      :   14;  // ID of the corresponding node
+    unsigned    nFanins :   14;  // number of fanins
+    Llb_Flw_t * Fanins[0];       // fanins
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Llb_Flw_t * Llb_FlwAlloc( Vec_Int_t * vMem, Vec_Ptr_t * vStore, int Id, int nFanins )
+{
+    Llb_Flw_t * p;
+    int nWords = (sizeof(Llb_Flw_t) + nFanins * sizeof(void *)) / sizeof(int);
+    p = (Llb_Flw_t *)Vec_IntFetch( vMem, nWords );
+    memset( p, 1, nWords * sizeof(int) );
+    p->Id      = Id;
+    p->nFanins = 0;//nFanins;
+    Vec_PtrWriteEntry( vStore, Id, p );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_FlwAddFanin( Llb_Flw_t * pFrom, Llb_Flw_t * pTo )
+{
+    pFrom->Fanins[pFrom->nFanins++] = pTo;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_AigCreateFlw( Aig_Man_t * p, Vec_Int_t ** pvMem, Vec_Ptr_t ** pvTops, Vec_Ptr_t ** pvBots )
+{
+    Llb_Flw_t * pFlwTop, * pFlwBot;
+    Vec_Ptr_t * vTops, * vBots;
+    Vec_Int_t * vMem;
+    Aig_Obj_t * pObj;
+    int i;
+    vMem  = Vec_IntAlloc( Aig_ManObjNumMax(p) * (sizeof(Llb_Flw_t) + sizeof(void *) * 8) );
+    vBots = Vec_PtrStart( Aig_ManObjNumMax(p) );
+    vTops = Vec_PtrStart( Aig_ManObjNumMax(p) );
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        pFlwBot = Llb_FlwAlloc( vMem, vBots, i, Aig_ObjIsPo(pObj) + 2 * Aig_ObjIsNode(pObj) );
+        pFlwTop = Llb_FlwAlloc( vMem, vTops, i, Aig_ObjRefs(pObj) + 1 );
+        Llb_FlwAddFanin( pFlwBot, pFlwTop );
+        Llb_FlwAddFanin( pFlwTop, pFlwBot );
+        Llb_FlwAddFanin( pFlwBot, (Llb_Flw_t *)Vec_PtrEntry(vTops, Aig_ObjFaninId0(pObj)) );
+        Llb_FlwAddFanin( pFlwBot, (Llb_Flw_t *)Vec_PtrEntry(vTops, Aig_ObjFaninId1(pObj)) );
+        Llb_FlwAddFanin( (Llb_Flw_t *)Vec_PtrEntry(vTops, Aig_ObjFaninId0(pObj)), pFlwBot );
+        Llb_FlwAddFanin( (Llb_Flw_t *)Vec_PtrEntry(vTops, Aig_ObjFaninId1(pObj)), pFlwBot );
+    }
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        pFlwBot = (Llb_Flw_t *)Vec_PtrEntry( vBots, i );
+        pFlwTop = (Llb_Flw_t *)Vec_PtrEntry( vTops, i );
+        assert( pFlwBot->nFanins == (unsigned)Aig_ObjIsPo(pObj) + 2 * Aig_ObjIsNode(pObj) );
+        assert( pFlwTop->nFanins == (unsigned)Aig_ObjRefs(pObj) + 1 );
+    }
+    *pvMem  = vMem;
+    *pvTops = vTops;
+    *pvBots = vBots;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_AigCleanMarks( Vec_Ptr_t * vFlw )
+{
+    Llb_Flw_t * pFlw;
+    int i;
+    Vec_PtrForEachEntry( Llb_Flw_t *, vFlw, pFlw, i )
+        pFlw->Mark = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_AigCleanFlow( Vec_Ptr_t * vFlw )
+{
+    Llb_Flw_t * pFlw;
+    int i;
+    Vec_PtrForEachEntry( Llb_Flw_t *, vFlw, pFlw, i )
+        pFlw->Flow = 0;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Llb_AigCollectCut( Vec_Ptr_t * vNodes, Vec_Ptr_t * vBots, Vec_Ptr_t * vTops )
+{
+    Vec_Int_t * vCut;
+    Llb_Flw_t * pFlwBot, * pFlwTop;
+    Aig_Obj_t * pObj;
+    int i;
+    vCut = Vec_IntAlloc( 100 );
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
+    {
+        pFlwBot = (Llb_Flw_t *)Vec_PtrEntry( vBots, i );
+        pFlwTop = (Llb_Flw_t *)Vec_PtrEntry( vTops, i );
+        if ( pFlwBot->Mark && !pFlwTop->Mark )
+            Vec_IntPush( vCut, i );
+    }
+    return vCut;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Llb_AigPushFlow_rec( Llb_Flw_t * pFlw, Llb_Flw_t * pFlwPrev, Vec_Ptr_t * vMarked, Vec_Ptr_t * vFlowed )
+{
+    int i;
+    if ( pFlw->Mark )
+        return 0;
+    pFlw->Mark = 1;
+    Vec_PtrPush( vMarked, pFlw );
+    if ( pFlw->Source )
+        return 0;
+    if ( pFlw->Sink )
+    {
+        pFlw->Flow = 1;
+        Vec_PtrPush( vFlowed, pFlw );
+        return 1;
+    }
+//    assert( Aig_ObjIsNode(pObj) );
+    for ( i = 0; i < (int)pFlw->nFanins; i++ )
+    {
+        if ( pFlw->Fanins[i] == pFlwPrev )
+            continue;
+        if ( Llb_AigPushFlow_rec( pFlw->Fanins[i], pFlw, vMarked, vFlowed ) )
+            break;
+    }
+    if ( i == (int)pFlw->nFanins )
+        return 0;
+    if ( i == 0 )
+    {
+        pFlw->Flow = 1;
+        Vec_PtrPush( vFlowed, pFlw );
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Llb_AigPushFlow( Vec_Ptr_t * vFlwBots, Vec_Ptr_t * vMarked, Vec_Ptr_t * vFlowed )
+{
+    Llb_Flw_t * pFlw;
+    int i, Counter = 0;
+    Vec_PtrForEachEntry( Llb_Flw_t *, vFlwBots, pFlw, i )
+    {
+        pFlw->Mark = 1;
+        if ( Llb_AigPushFlow_rec( pFlw->Fanins[0], pFlw, vMarked, vFlowed ) )
+        {
+            Counter++;
+            pFlw->Flow = 1;
+            Vec_PtrPush( vFlowed, pFlw );
+        }
+    }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Llb_AigFindMinCut( Vec_Ptr_t * vNodes, Vec_Ptr_t * vFlwBots, Vec_Ptr_t * vFlwTop, Vec_Ptr_t * vFlwBots2, Vec_Ptr_t * vFlwTop2 )
+{
+    Vec_Int_t * vCut;
+    Vec_Ptr_t * vMarked, * vFlowed;
+    int Value;
+    vMarked = Vec_PtrAlloc( 100 );
+    vFlowed = Vec_PtrAlloc( 100 );
+    Value = Llb_AigPushFlow( vFlwBots2, vMarked, vFlowed );
+    Llb_AigCleanMarks( vMarked );
+    Value = Llb_AigPushFlow( vFlwBots2, vMarked, vFlowed );
+    assert( Value == 0 );
+    vCut = Llb_AigCollectCut( vNodes, vFlwBots, vFlwTop );
+    Llb_AigCleanMarks( vMarked );
+    Llb_AigCleanFlow( vFlowed );
+    return vCut;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Llb_AigCollectFlowTerminals( Aig_Man_t * p, Vec_Ptr_t * vFlws, Vec_Int_t * vCut )
+{
+    Vec_Ptr_t * pFlwRes;
+    Aig_Obj_t * pObj;
+    int i;
+    pFlwRes = Vec_PtrAlloc( Vec_IntSize(vCut) );
+    Aig_ManForEachNodeVec( p, vCut, pObj, i )
+        Vec_PtrPush( pFlwRes, Vec_PtrEntry( vFlws, Aig_ObjId(pObj) ) );
+    return pFlwRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_AigMarkFlowTerminals( Vec_Ptr_t * vFlws, int fSource, int fSink )
+{
+    Llb_Flw_t * pFlw;
+    int i;
+    Vec_PtrForEachEntry( Llb_Flw_t *, vFlws, pFlw, i )
+    {
+        pFlw->Source = fSource;
+        pFlw->Sink   = fSink;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects internal nodes in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_ManCollectNodes_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
+{
+    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Aig_ObjSetTravIdCurrent(p, pObj);
+    assert( Aig_ObjIsNode(pObj) );
+    Llb_ManCollectNodes_rec( p, Aig_ObjFanin0(pObj), vNodes );
+    Llb_ManCollectNodes_rec( p, Aig_ObjFanin1(pObj), vNodes );
+    Vec_PtrPush( vNodes, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Llb_ManCollectNodes( Aig_Man_t * p, Vec_Int_t * vCut1, Vec_Int_t * vCut2 )
+{
+    Vec_Ptr_t * vNodes;
+    Aig_Obj_t * pObj;
+    int i;
+    Aig_ManIncrementTravId( p );
+    Aig_ManForEachNodeVec( p, vCut1, pObj, i )
+        Aig_ObjSetTravIdCurrent( p, pObj );
+    vNodes = Vec_PtrAlloc( Aig_ManObjNumMax(p) );
+    Aig_ManForEachNodeVec( p, vCut2, pObj, i )
+        Llb_ManCollectNodes_rec( p, pObj, vNodes );
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects internal nodes in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Llb_ManCountNodes_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+        return 0;
+    Aig_ObjSetTravIdCurrent(p, pObj);
+    assert( Aig_ObjIsNode(pObj) );
+    return 1 + Llb_ManCountNodes_rec( p, Aig_ObjFanin0(pObj) ) +
+               Llb_ManCountNodes_rec( p, Aig_ObjFanin1(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Llb_ManCountNodes( Aig_Man_t * p, Vec_Int_t * vCut1, Vec_Int_t * vCut2 )
+{
+    Aig_Obj_t * pObj;
+    int i, Counter = 0;
+    Aig_ManIncrementTravId( p );
+    Aig_ManForEachNodeVec( p, vCut1, pObj, i )
+        Aig_ObjSetTravIdCurrent( p, pObj );
+    Aig_ManForEachNodeVec( p, vCut2, pObj, i )
+        Counter += Llb_ManCountNodes_rec( p, pObj );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes starting cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Llb_ManComputeCioCut( Aig_Man_t * pAig, int fCollectCos )
+{
+    Vec_Int_t * vCut;
+    Aig_Obj_t * pObj;
+    int i;
+    vCut = Vec_IntAlloc( 500 );
+    if ( fCollectCos )
+        Aig_ManForEachPo( pAig, pObj, i )
+            Vec_IntPush( vCut, Aig_ObjId(pObj) );
+    else
+        Aig_ManForEachPi( pAig, pObj, i )
+            Vec_IntPush( vCut, Aig_ObjId(pObj) );
+    return vCut;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts the new cut into the array.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_ManCutInsert( Aig_Man_t * p, Vec_Ptr_t * vCuts, Vec_Int_t * vVols, int iEntry, Vec_Int_t * vCutNew )
+{
+    Vec_Int_t * vCut1, * vCut2; 
+    int Vol1, Vol2;
+    Vec_PtrInsert( vCuts, iEntry, vCutNew );
+    Vec_IntInsert( vVols, iEntry, -1 );
+    vCut1 = (Vec_Int_t *)Vec_PtrEntry( vCuts, iEntry );
+    vCut2 = (Vec_Int_t *)Vec_PtrEntry( vCuts, iEntry+1 );
+    Vol1  = Llb_ManCountNodes( p, vCut1, vCutNew );
+    Vol2  = Llb_ManCountNodes( p, vCutNew, vCut2 );
+    Vec_IntWriteEntry( vVols, iEntry-1, Vol1 );
+    Vec_IntWriteEntry( vVols, iEntry,   Vol2 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the set of cuts resulting from the flow computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Llb_ManComputePartitioning( Aig_Man_t * p, int nVolumeMin, int nVolumeMax )
+{ 
+    Vec_Ptr_t * vCuts, * vFlwTops, * vFlwBots;
+    Vec_Int_t * vVols, * vCut1, * vCut2, * vCut, * vMem; 
+    int nMaxValue, iEntry;
+    vCuts = Vec_PtrAlloc( 1000 );
+    vVols = Vec_IntAlloc( 1000 );
+    // prepare flow computation
+    Llb_AigCreateFlw( p, &vMem, &vFlwTops, &vFlwBots );
+    // start with regular cuts
+    Vec_PtrPush( vCuts, Llb_ManComputeCioCut(p, 0) );
+    Vec_PtrPush( vCuts, Llb_ManComputeCioCut(p, 1) );
+    Vec_IntPush( vVols, Aig_ManNodeNum(p) );
+    // split cuts with the largest volume
+    while ( (nMaxValue = Vec_IntFindMax(vVols)) > nVolumeMax )
+    {
+        Vec_Ptr_t * vNodes, * vFlwBots2, * vFlwTops2; 
+        iEntry = Vec_IntFind( vVols, nMaxValue );  assert( iEntry >= 0 );
+        vCut1  = (Vec_Int_t *)Vec_PtrEntry( vCuts, iEntry );
+        vCut2  = (Vec_Int_t *)Vec_PtrEntry( vCuts, iEntry+1 );
+        // collect nodes
+        vNodes = Llb_ManCollectNodes( p, vCut1, vCut1 );
+        assert( Vec_PtrSize(vNodes) == nMaxValue );
+        assert( Llb_ManCountNodes(p, vCut1, vCut2) == nMaxValue );
+        // collect sources and sinks
+        vFlwBots2 = Llb_AigCollectFlowTerminals( p, vFlwBots, vCut1 );
+        vFlwTops2 = Llb_AigCollectFlowTerminals( p, vFlwTops, vCut2 );
+        // mark sources and sinks
+        Llb_AigMarkFlowTerminals( vFlwBots2, 1, 0 );
+        Llb_AigMarkFlowTerminals( vFlwTops2, 0, 1 );
+        vCut = Llb_AigFindMinCut( vNodes, vFlwBots, vFlwTops, vFlwBots2, vFlwTops2 );
+        Llb_AigMarkFlowTerminals( vFlwBots2, 0, 0 );
+        Llb_AigMarkFlowTerminals( vFlwTops2, 0, 0 );
+        // insert new cut
+        Llb_ManCutInsert( p, vCuts, vVols, iEntry+1, vCut );
+        // deallocate
+        Vec_PtrFree( vNodes );
+        Vec_PtrFree( vFlwBots2 );
+        Vec_PtrFree( vFlwTops2 );
+    }
+    Vec_IntFree( vMem );
+    Vec_PtrFree( vFlwTops );
+    Vec_PtrFree( vFlwBots );
+    return vCuts;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Llb_ManMarkPivotNodesFlow( Aig_Man_t * p, Vec_Ptr_t * vCuts )
+{
+    Vec_Int_t * vVar2Obj, * vCut;
+    Aig_Obj_t * pObj;
+    int i, k;
+    // mark inputs/outputs
+    Aig_ManForEachPi( p, pObj, i )
+        pObj->fMarkA = 1;
+    Saig_ManForEachLi( p, pObj, i )
+        pObj->fMarkA = 1;
+
+    // mark internal pivot nodes
+    Vec_PtrForEachEntry( Vec_Int_t *, vCuts, vCut, i )
+        Aig_ManForEachNodeVec( p, vCut, pObj, k )
+            pObj->fMarkA = 1;
+
+    // assign variable numbers
+    Aig_ManConst1(p)->fMarkA = 0;
+    vVar2Obj = Vec_IntAlloc( 100 );
+    Aig_ManForEachPi( p, pObj, i )
+        Vec_IntPush( vVar2Obj, Aig_ObjId(pObj) );
+    Aig_ManForEachNode( p, pObj, i )
+        if ( pObj->fMarkA )
+            Vec_IntPush( vVar2Obj, Aig_ObjId(pObj) );
+    Saig_ManForEachLi( p, pObj, i )
+        Vec_IntPush( vVar2Obj, Aig_ObjId(pObj) );
+    return vVar2Obj;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the set of cuts resulting from the flow computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_ManPartitionUsingFlow( Llb_Man_t * p, Vec_Ptr_t * vCuts )
+{ 
+    Vec_Int_t * vCut1, * vCut2;
+    int i;
+    vCut1 = (Vec_Int_t *)Vec_PtrEntry( vCuts, 0 );
+    Vec_PtrForEachEntryStart( Vec_Int_t *, vCuts, vCut1, i, 1 )
+    {
+        vCut2 = (Vec_Int_t *)Vec_PtrEntry( vCuts, i );
+        Llb_ManGroupCreateFromCuts( p, vCut1, vCut2 );
+        vCut1 = vCut2;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Llb_Man_t * Llb_ManStartFlow( Aig_Man_t * pAigGlo, Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
+{
+    Vec_Ptr_t * vCuts;
+    Llb_Man_t * p;
+    vCuts = Llb_ManComputePartitioning( pAig, pPars->nVolumeMin, pPars->nVolumeMax );
+    Aig_ManCleanMarkA( pAig );
+    p = ABC_CALLOC( Llb_Man_t, 1 );
+    p->pAigGlo  = pAigGlo;
+    p->pPars    = pPars;
+    p->pAig     = pAig;
+    p->vVar2Obj = Llb_ManMarkPivotNodesFlow( p->pAig, vCuts );
+    p->vObj2Var = Vec_IntInvert( p->vVar2Obj, -1 );
+    Llb_ManPrepareVarMap( p );
+    Aig_ManCleanMarkA( pAig );
+    Llb_ManPartitionUsingFlow( p, vCuts );
+    Vec_VecFreeP( (Vec_Vec_t **)&vCuts );
+    return p;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/llb/llbHint.c b/src/aig/llb/llbHint.c
new file mode 100644
index 00000000..acc674c8
--- /dev/null
+++ b/src/aig/llb/llbHint.c
@@ -0,0 +1,226 @@
+/**CFile****************************************************************
+
+  FileName    [llbHint.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [BDD based reachability.]
+
+  Synopsis    [Cofactors the circuit w.r.t. the high-fanout variables.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: llbHint.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "llbInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Returns CI index with the largest number of fanouts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Llb_ManMaxFanoutCi( Aig_Man_t * pAig )
+{
+    Aig_Obj_t * pObj; 
+    int i, WeightMax = -ABC_INFINITY, iInput = -1;
+    Aig_ManForEachPi( pAig, pObj, i )
+        if ( WeightMax < Aig_ObjRefs(pObj) )
+        {
+            WeightMax = Aig_ObjRefs(pObj);
+            iInput = i;
+        }
+    assert( iInput >= 0 );
+    return iInput;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives AIG whose PI is substituted by a constant.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Llb_ManPerformHints( Aig_Man_t * pAig, int nHintDepth )
+{
+    Aig_Man_t * pNew, * pTemp;
+    int i, iInput;
+    pNew = Aig_ManDupDfs( pAig );
+    for ( i = 0; i < nHintDepth; i++ )
+    {
+        iInput = Llb_ManMaxFanoutCi( pNew );
+        Abc_Print( 1, "%d %3d\n", i, iInput );
+        pNew = Aig_ManDupCof( pTemp = pNew, iInput, 1 );
+        Aig_ManStop( pTemp );
+    }
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns CI index with the largest number of fanouts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Llb_ManCollectHighFanoutObjects( Aig_Man_t * pAig, int nCandMax, int fCisOnly )
+{
+    Vec_Int_t * vFanouts, * vResult;
+    Aig_Obj_t * pObj; 
+    int i, fChanges, PivotValue;
+//    int Entry;
+    // collect fanout counts
+    vFanouts = Vec_IntAlloc( 100 );
+    Aig_ManForEachObj( pAig, pObj, i )
+    {
+//        if ( !Aig_ObjIsPi(pObj) && (fCisOnly || !Aig_ObjIsNode(pObj)) )
+        if ( !Saig_ObjIsLo(pAig,pObj) && (fCisOnly || !Aig_ObjIsNode(pObj)) )
+            continue;
+        Vec_IntPush( vFanouts, Aig_ObjRefs(pObj) );
+    }
+    Vec_IntSort( vFanouts, 1 );
+    // pick the separator
+    nCandMax = ABC_MIN( nCandMax, Vec_IntSize(vFanouts) - 1 );
+    PivotValue = Vec_IntEntry( vFanouts, nCandMax );
+    Vec_IntFree( vFanouts );
+    // collect obj satisfying the constraints
+    vResult = Vec_IntAlloc( 100 );
+    Aig_ManForEachObj( pAig, pObj, i )
+    {
+//        if ( !Aig_ObjIsPi(pObj) && (fCisOnly || !Aig_ObjIsNode(pObj)) )
+        if ( !Saig_ObjIsLo(pAig,pObj) && (fCisOnly || !Aig_ObjIsNode(pObj)) )
+            continue;
+        if ( Aig_ObjRefs(pObj) < PivotValue )
+            continue;
+        Vec_IntPush( vResult, Aig_ObjId(pObj) );
+    }
+    assert( Vec_IntSize(vResult) >= nCandMax );
+    // order in the decreasing order of fanouts
+    do
+    {
+        fChanges = 0;
+        for ( i = 0; i < Vec_IntSize(vResult) - 1; i++ )
+            if ( Aig_ObjRefs(Aig_ManObj(pAig, Vec_IntEntry(vResult, i))) < 
+                 Aig_ObjRefs(Aig_ManObj(pAig, Vec_IntEntry(vResult, i+1))) )
+            {
+                int Temp = Vec_IntEntry( vResult, i );
+                Vec_IntWriteEntry( vResult, i, Vec_IntEntry(vResult, i+1) );
+                Vec_IntWriteEntry( vResult, i+1, Temp );
+                fChanges = 1;
+            }
+    }
+    while ( fChanges );
+/*
+    Vec_IntForEachEntry( vResult, Entry, i )
+        printf( "%d ", Aig_ObjRefs(Aig_ManObj(pAig, Entry)) );
+printf( "\n" );
+*/
+    return vResult;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives AIG whose PI is substituted by a constant.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Llb_ManModelCheckAigWithHints( Aig_Man_t * pAigGlo, Gia_ParLlb_t * pPars )
+{
+    DdManager * ddGlo = NULL;
+    Vec_Int_t * vHints;
+    Vec_Int_t * vHFCands;
+    int i, Entry, RetValue = -1;
+    int clk = clock();
+    assert( pPars->nHintDepth > 0 );
+/*
+    // perform reachability without hints
+    RetValue = Llb_ManModelCheckAig( pAigGlo, pPars, NULL, NULL );
+    if ( RetValue >= 0 )
+        return RetValue;
+*/
+    // create hints representation
+    vHFCands = Llb_ManCollectHighFanoutObjects( pAigGlo, pPars->nHintDepth+pPars->HintFirst, 1 );
+    vHints   = Vec_IntStartFull( Aig_ManObjNumMax(pAigGlo) );
+    // add one hint at a time till the problem is solved
+    Vec_IntForEachEntryStart( vHFCands, Entry, i, pPars->HintFirst )
+    {
+        Vec_IntWriteEntry( vHints, Entry, 1 );   // change to 1 to start from zero cof!!!
+        // solve under hints
+        RetValue = Llb_ManModelCheckAig( pAigGlo, pPars, vHints, &ddGlo );
+        if ( RetValue == 0 )
+            goto Finish;
+        if ( RetValue == 1 )
+            break;
+    }
+    if ( RetValue == -1 )
+        goto Finish;
+    // undo the hints one at a time
+    for ( ; i >= pPars->HintFirst; i-- )
+    {
+        Entry = Vec_IntEntry( vHFCands, i );
+        Vec_IntWriteEntry( vHints, Entry, -1 );        
+        // solve under relaxed hints
+        RetValue = Llb_ManModelCheckAig( pAigGlo, pPars, vHints, &ddGlo );
+        if ( RetValue == 0 )
+            goto Finish;
+        if ( RetValue == 1 )
+            continue;
+        break;
+    }
+Finish:
+    if ( ddGlo )
+    {
+        if ( ddGlo->bReached )
+            Cudd_RecursiveDeref( ddGlo, ddGlo->bReached ); 
+        Extra_StopManager( ddGlo );
+    }
+    Vec_IntFreeP( &vHFCands );
+    Vec_IntFreeP( &vHints );
+    if ( pPars->fVerbose )
+        Abc_PrintTime( 1, "Total runtime", clock() - clk );
+    return RetValue;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/llb/llbInt.h b/src/aig/llb/llbInt.h
new file mode 100644
index 00000000..dc448954
--- /dev/null
+++ b/src/aig/llb/llbInt.h
@@ -0,0 +1,162 @@
+/**CFile****************************************************************
+
+  FileName    [llbInt.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [BDD-based reachability.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 8, 2010.]
+
+  Revision    [$Id: llbInt.h,v 1.00 2010/05/08 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __LLB_INT_H__
+#define __LLB_INT_H__
+
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+#include "aig.h"
+#include "saig.h"
+#include "cuddInt.h"
+#include "extra.h"
+#include "llb.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+
+
+ABC_NAMESPACE_HEADER_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Llb_Man_t_ Llb_Man_t;
+typedef struct Llb_Mtr_t_ Llb_Mtr_t;
+typedef struct Llb_Grp_t_ Llb_Grp_t;
+
+struct Llb_Man_t_
+{
+    Gia_ParLlb_t *  pPars;          // parameters
+    Aig_Man_t *     pAigGlo;        // initial AIG manager (owned by the caller)
+    Aig_Man_t *     pAig;           // derived AIG manager (created in this package)
+    DdManager *     dd;             // BDD manager
+    DdManager *     ddG;            // BDD manager
+    Vec_Int_t *     vObj2Var;       // mapping AIG ObjId into BDD var index
+    Vec_Int_t *     vVar2Obj;       // mapping BDD var index into AIG ObjId
+    Vec_Ptr_t *     vGroups;        // group Id into group pointer
+    Llb_Mtr_t *     pMatrix;        // dependency matrix
+    // image computation
+    Vec_Int_t *     vVarBegs;       // the first group where the var appears  
+    Vec_Int_t *     vVarEnds;       // the last group where the var appears 
+    // variable mapping
+    Vec_Int_t *     vNs2Glo;        // next state variables into global variables
+    Vec_Int_t *     vGlo2Cs;        // global variables into current state variables
+    // flow computation
+//    Vec_Int_t *     vMem;
+//    Vec_Ptr_t *     vTops;
+//    Vec_Ptr_t *     vBots;
+//    Vec_Ptr_t *     vCuts;
+};
+
+struct Llb_Mtr_t_
+{
+    int             nPis;           // number of primary inputs
+    int             nFfs;           // number of flip-flops
+    int             nRows;          // number of rows
+    int             nCols;          // number of columns
+    int *           pColSums;       // sum of values in a column
+    Llb_Grp_t **    pColGrps;       // group structure for each col
+    int *           pRowSums;       // sum of values in a row
+    char **         pMatrix;        // dependency matrix
+    Llb_Man_t *     pMan;           // manager
+    // partial product
+    char *          pProdVars;      // variables in the partial product
+    int *           pProdNums;      // var counts in the remaining partitions
+};
+
+struct Llb_Grp_t_
+{
+    int             Id;             // group ID
+    Vec_Ptr_t *     vIns;           // input AIG objs
+    Vec_Ptr_t *     vOuts;          // output AIG objs
+    Vec_Ptr_t *     vNodes;         // internal AIG objs
+    Llb_Man_t *     pMan;           // manager
+    Llb_Grp_t *     pPrev;          // previous group
+    Llb_Grp_t *     pNext;          // next group
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== llbCex.c =======================================================*/
+extern Abc_Cex_t *     Llb_ManDeriveCex( Llb_Man_t * p, DdNode * bInter, int iOutFail, int iIter );
+/*=== llbConstr.c ======================================================*/
+extern Vec_Int_t *     Llb_ManDeriveConstraints( Aig_Man_t * p );
+extern void            Llb_ManPrintEntries( Aig_Man_t * p, Vec_Int_t * vCands );
+/*=== llbCore.c ======================================================*/
+extern int             Llb_ManModelCheckAig( Aig_Man_t * pAigGlo, Gia_ParLlb_t * pPars, Vec_Int_t * vHints, DdManager ** pddGlo );
+/*=== llbCluster.c ======================================================*/
+extern void            Llb_ManCluster( Llb_Mtr_t * p );
+/*=== llbFlow.c ======================================================*/
+extern Llb_Man_t *     Llb_ManStartFlow( Aig_Man_t * pAigGlo, Aig_Man_t * pAig, Gia_ParLlb_t * pPars );
+/*=== llbHint.c ======================================================*/
+extern int             Llb_ManReachabilityWithHints( Llb_Man_t * p );
+extern int             Llb_ManModelCheckAigWithHints( Aig_Man_t * pAigGlo, Gia_ParLlb_t * pPars );
+/*=== llbMan.c =======================================================*/
+extern void            Llb_ManPrepareVarMap( Llb_Man_t * p );
+extern Llb_Man_t *     Llb_ManStart( Aig_Man_t * pAigGlo, Aig_Man_t * pAig, Gia_ParLlb_t *  pPars );
+extern void            Llb_ManStop( Llb_Man_t * p );
+/*=== llbMatrix.c ====================================================*/
+extern void            Llb_MtrVerifyMatrix( Llb_Mtr_t * p );
+extern Llb_Mtr_t *     Llb_MtrCreate( Llb_Man_t * p );
+extern void            Llb_MtrFree( Llb_Mtr_t * p );
+extern void            Llb_MtrPrint( Llb_Mtr_t * p, int fOrder );
+extern void            Llb_MtrPrintMatrixStats( Llb_Mtr_t * p );
+/*=== llbPart.c ======================================================*/
+extern Llb_Grp_t *     Llb_ManGroupAlloc( Llb_Man_t * pMan );
+extern void            Llb_ManGroupStop( Llb_Grp_t * p );
+extern void            Llb_ManPrepareGroups( Llb_Man_t * pMan );
+extern Llb_Grp_t *     Llb_ManGroupsCombine( Llb_Grp_t * p1, Llb_Grp_t * p2 );
+extern Llb_Grp_t *     Llb_ManGroupCreateFromCuts( Llb_Man_t * pMan, Vec_Int_t * vCut1, Vec_Int_t * vCut2 );
+extern void            Llb_ManPrepareVarLimits( Llb_Man_t * p );
+/*=== llbPivot.c =====================================================*/
+extern int             Llb_ManTracePaths( Aig_Man_t * p, Aig_Obj_t * pPivot );
+extern Vec_Int_t *     Llb_ManMarkPivotNodes( Aig_Man_t * p, int fUseInternal );
+/*=== llbReach.c =====================================================*/
+extern int             Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo );
+/*=== llbSched.c =====================================================*/
+extern void            Llb_MtrSchedule( Llb_Mtr_t * p );
+
+
+
+ABC_NAMESPACE_HEADER_END
+
+
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/llb/llbMan.c b/src/aig/llb/llbMan.c
new file mode 100644
index 00000000..cd6fd3ff
--- /dev/null
+++ b/src/aig/llb/llbMan.c
@@ -0,0 +1,189 @@
+/**CFile****************************************************************
+
+  FileName    [llbMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [BDD based reachability.]
+
+  Synopsis    [Reachability manager.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: llbMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "llbInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_ManPrepareVarMap( Llb_Man_t * p )
+{
+    Aig_Obj_t * pObjLi, * pObjLo;
+    int i, iVarLi, iVarLo;
+    assert( p->vNs2Glo == NULL );
+    assert( p->vGlo2Cs == NULL );
+    p->vNs2Glo = Vec_IntStartFull( Vec_IntSize(p->vVar2Obj) );
+    p->vGlo2Cs = Vec_IntStartFull( Aig_ManRegNum(p->pAig) );
+    Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
+    {
+        iVarLi = Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObjLi));
+        iVarLo = Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObjLo));
+        assert( iVarLi >= 0 && iVarLi < Vec_IntSize(p->vVar2Obj) );
+        assert( iVarLo >= 0 && iVarLo < Vec_IntSize(p->vVar2Obj) );
+        Vec_IntWriteEntry( p->vNs2Glo, iVarLi, i );
+        Vec_IntWriteEntry( p->vGlo2Cs, i, iVarLo );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_ManPrepareVarLimits( Llb_Man_t * p )
+{
+    Llb_Grp_t * pGroup;
+    Aig_Obj_t * pVar;
+    int i, k;
+    assert( p->vVarBegs == NULL );
+    assert( p->vVarEnds == NULL );
+    p->vVarEnds = Vec_IntStart( Aig_ManObjNumMax(p->pAig) ); 
+    p->vVarBegs = Vec_IntStart( Aig_ManObjNumMax(p->pAig) ); 
+    Vec_IntFill( p->vVarBegs, Aig_ManObjNumMax(p->pAig), p->pMatrix->nCols );
+
+    for ( i = 0; i < p->pMatrix->nCols; i++ )
+    {
+        pGroup = p->pMatrix->pColGrps[i];
+
+        Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pVar, k )
+            if ( Vec_IntEntry(p->vVarBegs, pVar->Id) > i )
+                Vec_IntWriteEntry( p->vVarBegs, pVar->Id, i );
+        Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pVar, k )
+            if ( Vec_IntEntry(p->vVarBegs, pVar->Id) > i )
+                Vec_IntWriteEntry( p->vVarBegs, pVar->Id, i );
+
+        Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pVar, k )
+            if ( Vec_IntEntry(p->vVarEnds, pVar->Id) < i )
+                Vec_IntWriteEntry( p->vVarEnds, pVar->Id, i );
+        Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pVar, k )
+            if ( Vec_IntEntry(p->vVarEnds, pVar->Id) < i )
+                Vec_IntWriteEntry( p->vVarEnds, pVar->Id, i );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_ManStop( Llb_Man_t * p )
+{
+    Llb_Grp_t * pGrp;
+    int i;
+
+//    Vec_IntFreeP( &p->vMem );
+//    Vec_PtrFreeP( &p->vTops );
+//    Vec_PtrFreeP( &p->vBots );
+//    Vec_VecFreeP( (Vec_Vec_t **)&p->vCuts );
+
+    if ( p->pMatrix )
+        Llb_MtrFree( p->pMatrix );
+    Vec_PtrForEachEntry( Llb_Grp_t *, p->vGroups, pGrp, i )
+        Llb_ManGroupStop( pGrp );
+    Vec_PtrFreeP( &p->vGroups );
+    Vec_IntFreeP( &p->vVar2Obj );
+    Vec_IntFreeP( &p->vObj2Var );
+    Vec_IntFreeP( &p->vVarBegs );
+    Vec_IntFreeP( &p->vVarEnds );
+    Vec_IntFreeP( &p->vNs2Glo );
+    Vec_IntFreeP( &p->vGlo2Cs );
+//    Vec_IntFreeP( &p->vHints );
+    if ( p->dd )
+    {
+        Extra_StopManager( p->dd );
+    }
+    if ( p->ddG )
+    {
+        if ( p->ddG->bReached )
+            Cudd_RecursiveDeref( p->ddG, p->ddG->bReached ); 
+        Extra_StopManager( p->ddG );
+    }
+    Aig_ManStop( p->pAig );
+    ABC_FREE( p );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Llb_Man_t * Llb_ManStart( Aig_Man_t * pAigGlo, Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
+{
+    Llb_Man_t * p;
+    Aig_ManCleanMarkA( pAig );
+    p = ABC_CALLOC( Llb_Man_t, 1 );
+    p->pAigGlo  = pAigGlo;
+    p->pPars    = pPars;
+    p->pAig     = pAig;
+    p->vVar2Obj = Llb_ManMarkPivotNodes( p->pAig, pPars->fUsePivots );
+    p->vObj2Var = Vec_IntInvert( p->vVar2Obj, -1 );
+    Llb_ManPrepareVarMap( p );
+    Llb_ManPrepareGroups( p );
+    Aig_ManCleanMarkA( pAig );
+    p->pMatrix = Llb_MtrCreate( p );
+    p->pMatrix->pMan = p;
+    return p;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/llb/llbMatrix.c b/src/aig/llb/llbMatrix.c
new file mode 100644
index 00000000..484ee690
--- /dev/null
+++ b/src/aig/llb/llbMatrix.c
@@ -0,0 +1,430 @@
+/**CFile****************************************************************
+
+  FileName    [llbMatrix.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [BDD based reachability.]
+
+  Synopsis    [Partition clustering as a matrix problem.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: llbMatrix.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "llbInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+//              0123              nCols
+//             +--------------------->  
+// pi        0 |  111             row0   pRowSums[0]  
+// pi        1 | 1     11         row1   pRowSums[1] 
+// pi        2 |   1  11          row2   pRowSums[2] 
+// CS          |1       1
+// CS          |1      111
+// CS          |111    111
+// int         |  11111           
+// int         |     111          
+// int         |       111        
+// int         |         111      
+// NS          |           11 11
+// NS          |            11 1
+// NS          |             111
+//       nRows |
+//             v    
+//              cccc   pColSums[0]
+//              oooo   pColSums[1]
+//              llll   pColSums[2]
+//              0123   pColSums[3]
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Verify columns.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_MtrVerifyRowsAll( Llb_Mtr_t * p )
+{
+    int iRow, iCol, Counter;
+    for ( iCol = 0; iCol < p->nCols; iCol++ )
+    {
+        Counter = 0;
+        for ( iRow = 0; iRow < p->nRows; iRow++ )
+            if ( p->pMatrix[iCol][iRow] == 1 )
+                Counter++;
+        assert( Counter == p->pColSums[iCol] );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Verify columns.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_MtrVerifyColumnsAll( Llb_Mtr_t * p )
+{
+    int iRow, iCol, Counter;
+    for ( iRow = 0; iRow < p->nRows; iRow++ )
+    {
+        Counter = 0;
+        for ( iCol = 0; iCol < p->nCols; iCol++ )
+            if ( p->pMatrix[iCol][iRow] == 1 )
+                Counter++;
+        assert( Counter == p->pRowSums[iRow] );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Verify columns.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_MtrVerifyMatrix( Llb_Mtr_t * p )
+{
+    Llb_MtrVerifyRowsAll( p );
+    Llb_MtrVerifyColumnsAll( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sort variables in the order of removal.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int * Llb_MtrFindVarOrder( Llb_Mtr_t * p )
+{
+    int * pOrder, * pLast;
+    int i, k, fChanges, Temp;
+    pOrder = ABC_CALLOC( int, p->nRows );
+    pLast  = ABC_CALLOC( int, p->nRows );
+    for ( i = 0; i < p->nRows; i++ )
+    {
+        pOrder[i] = i;
+        for ( k = p->nCols - 1; k >= 0; k-- )
+            if ( p->pMatrix[k][i] )
+            {
+                pLast[i] = k;
+                break;
+            }
+    }
+    do
+    {
+        fChanges = 0;
+        for ( i = 0; i < p->nRows - 1; i++ )
+            if ( pLast[i] > pLast[i+1] )
+            {
+                Temp = pOrder[i];
+                pOrder[i] = pOrder[i+1];
+                pOrder[i+1] = Temp;
+
+                Temp = pLast[i];
+                pLast[i] = pLast[i+1];
+                pLast[i+1] = Temp;
+
+                fChanges = 1;
+            }
+    }
+    while ( fChanges );
+    ABC_FREE( pLast );
+    return pOrder;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns type of a variable.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Llb_MtrVarName( Llb_Mtr_t * p, int iVar )
+{
+    static char Buffer[10];
+    if ( iVar < p->nPis )
+        strcpy( Buffer, "pi" );
+    else if ( iVar < p->nPis + p->nFfs )
+        strcpy( Buffer, "CS" );
+    else if ( iVar >= p->nRows - p->nFfs )
+        strcpy( Buffer, "NS" );
+    else 
+        strcpy( Buffer, "int" );
+    return Buffer;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates one column with vars in the array.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_MtrPrint( Llb_Mtr_t * p, int fOrder )
+{
+    int * pOrder = NULL;
+    int i, iRow, iCol;
+    if ( fOrder )
+        pOrder = Llb_MtrFindVarOrder( p );
+    for ( i = 0; i < p->nRows; i++ )
+    {
+        iRow = pOrder ? pOrder[i] : i;
+        printf( "%3d : ", iRow );
+        printf( "%3d ", p->pRowSums[iRow] );
+        printf( "%3s ", Llb_MtrVarName(p, iRow) );
+        for ( iCol = 0; iCol < p->nCols; iCol++ )
+            printf( "%c", p->pMatrix[iCol][iRow] ? '*' : ' ' );
+        printf( "\n" );
+    }
+    ABC_FREE( pOrder );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Verify columns.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_MtrPrintMatrixStats( Llb_Mtr_t * p )
+{
+    int iVar, iGrp, iGrp1, iGrp2, Span = 0, nCutSize = 0, nCutSizeMax = 0;
+    int * pGrp1 = ABC_CALLOC( int, p->nRows ); 
+    int * pGrp2 = ABC_CALLOC( int, p->nRows ); 
+    for ( iVar = 0; iVar < p->nRows; iVar++ )
+    {
+        if ( p->pRowSums[iVar] == 0 )
+            continue;
+        for ( iGrp1 = 0; iGrp1 < p->nCols; iGrp1++ )
+            if ( p->pMatrix[iGrp1][iVar] == 1 )
+                break;
+        for ( iGrp2 = p->nCols - 1; iGrp2 >= 0; iGrp2-- )
+            if ( p->pMatrix[iGrp2][iVar] == 1 )
+                break;
+        assert( iGrp1 <= iGrp2 );
+        pGrp1[iVar] = iGrp1;
+        pGrp2[iVar] = iGrp2;
+        Span += iGrp2 - iGrp1;
+    }
+    // compute span
+    for ( iGrp = 0; iGrp < p->nCols; iGrp++ )
+    {
+        for ( iVar = 0; iVar < p->nRows; iVar++ )
+            if ( pGrp1[iVar] == iGrp )
+                nCutSize++;
+        if ( nCutSizeMax < nCutSize )
+            nCutSizeMax = nCutSize;
+        for ( iVar = 0; iVar < p->nRows; iVar++ )
+            if ( pGrp2[iVar] == iGrp )
+                nCutSize--;
+    }
+    ABC_FREE( pGrp1 );
+    ABC_FREE( pGrp2 );
+    printf( "[%4d x %4d]  Life-span =%6.2f  Max-cut =%5d\n", 
+        p->nCols, p->nRows, 1.0*Span/p->nRows, nCutSizeMax );
+    if ( nCutSize )
+        Abc_Print( -1, "Cut size is not zero (%d).\n", nCutSize );
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the matrix representation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Llb_Mtr_t * Llb_MtrAlloc( int nPis, int nFfs, int nCols, int nRows )
+{
+    Llb_Mtr_t * p;
+    int i;
+    p = ABC_CALLOC( Llb_Mtr_t, 1 );
+    p->nPis  = nPis;
+    p->nFfs  = nFfs;
+    p->nRows = nRows;
+    p->nCols = nCols;
+    p->pRowSums = ABC_CALLOC( int, nRows );
+    p->pColSums = ABC_CALLOC( int, nCols );
+    p->pColGrps = ABC_CALLOC( Llb_Grp_t *, nCols );
+    p->pMatrix  = ABC_CALLOC( char *, nCols );
+    for ( i = 0; i < nCols; i++ )
+        p->pMatrix[i] = ABC_CALLOC( char, nRows );
+    // partial product
+    p->pProdVars = ABC_CALLOC( char, nRows );  // variables in the partial product
+    p->pProdNums = ABC_CALLOC( int, nRows );   // var counts in the remaining partitions
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the matrix representation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_MtrFree( Llb_Mtr_t * p )
+{
+    int i;
+    ABC_FREE( p->pProdVars );
+    ABC_FREE( p->pProdNums );
+    for ( i = 0; i < p->nCols; i++ )
+        ABC_FREE( p->pMatrix[i] );
+    ABC_FREE( p->pRowSums );
+    ABC_FREE( p->pColSums );
+    ABC_FREE( p->pMatrix );
+    ABC_FREE( p->pColGrps );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates one column with vars in the array.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_MtrAddColumn( Llb_Mtr_t * p, Llb_Grp_t * pGrp )
+{
+    Aig_Obj_t * pVar;
+    int i, iRow, iCol = pGrp->Id;
+    assert( iCol >= 0 && iCol < p->nCols );
+    p->pColGrps[iCol] = pGrp;
+    Vec_PtrForEachEntry( Aig_Obj_t *, pGrp->vIns, pVar, i )
+    {
+        iRow = Vec_IntEntry( pGrp->pMan->vObj2Var, Aig_ObjId(pVar) );
+        assert( iRow >= 0 && iRow < p->nRows );
+        p->pMatrix[iCol][iRow] = 1;
+        p->pColSums[iCol]++;
+        p->pRowSums[iRow]++;
+    }
+    Vec_PtrForEachEntry( Aig_Obj_t *, pGrp->vOuts, pVar, i )
+    {
+        iRow = Vec_IntEntry( pGrp->pMan->vObj2Var, Aig_ObjId(pVar) );
+        assert( iRow >= 0 && iRow < p->nRows );
+        p->pMatrix[iCol][iRow] = 1;
+        p->pColSums[iCol]++;
+        p->pRowSums[iRow]++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Matrix reduce.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_MtrRemoveSingletonRows( Llb_Mtr_t * p )
+{
+    int i, k;
+    for ( i = 0; i < p->nRows; i++ )
+        if ( p->pRowSums[i] < 2 )
+        {
+            p->pRowSums[i] = 0;
+            for ( k = 0; k < p->nCols; k++ )
+            {
+                if ( p->pMatrix[k][i] == 1 )
+                {
+                    p->pMatrix[k][i] = 0;
+                    p->pColSums[k]--;
+                }
+            }
+        }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Matrix reduce.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Llb_Mtr_t * Llb_MtrCreate( Llb_Man_t * p )
+{
+    Llb_Mtr_t * pMatrix;
+    Llb_Grp_t * pGroup;
+    int i;
+    pMatrix = Llb_MtrAlloc( Saig_ManPiNum(p->pAig), Saig_ManRegNum(p->pAig), 
+        Vec_PtrSize(p->vGroups), Vec_IntSize(p->vVar2Obj) );
+    Vec_PtrForEachEntry( Llb_Grp_t *, p->vGroups, pGroup, i )
+        Llb_MtrAddColumn( pMatrix, pGroup );
+//    Llb_MtrRemoveSingletonRows( pMatrix );
+    return pMatrix;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/llb/llbPart.c b/src/aig/llb/llbPart.c
new file mode 100644
index 00000000..41de27d8
--- /dev/null
+++ b/src/aig/llb/llbPart.c
@@ -0,0 +1,474 @@
+/**CFile****************************************************************
+
+  FileName    [llbPart.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [BDD based reachability.]
+
+  Synopsis    [Initial partition computation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: llbPart.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "llbInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Llb_Grp_t * Llb_ManGroupAlloc( Llb_Man_t * pMan )
+{
+    Llb_Grp_t * p;
+    p = ABC_CALLOC( Llb_Grp_t, 1 );
+    p->pMan   = pMan;
+    p->vIns   = Vec_PtrAlloc( 8 );
+    p->vOuts  = Vec_PtrAlloc( 8 );
+    p->Id     = Vec_PtrSize( pMan->vGroups );
+    Vec_PtrPush( pMan->vGroups, p );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_ManGroupStop( Llb_Grp_t * p )
+{
+    if ( p == NULL )
+        return;
+    Vec_PtrWriteEntry( p->pMan->vGroups, p->Id, NULL );
+    Vec_PtrFreeP( &p->vIns );
+    Vec_PtrFreeP( &p->vOuts );
+    Vec_PtrFreeP( &p->vNodes );
+    ABC_FREE( p );
+}
+
+ 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_ManGroupCollect_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
+{
+    if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
+        return;
+    Aig_ObjSetTravIdCurrent(pAig, pObj);
+    if ( Aig_ObjIsConst1(pObj) )
+        return;
+    if ( Aig_ObjIsPo(pObj) )
+    {
+        Llb_ManGroupCollect_rec( pAig, Aig_ObjFanin0(pObj), vNodes );
+        return;
+    }
+    assert( Aig_ObjIsAnd(pObj) );
+    Llb_ManGroupCollect_rec( pAig, Aig_ObjFanin0(pObj), vNodes );
+    Llb_ManGroupCollect_rec( pAig, Aig_ObjFanin1(pObj), vNodes );
+    Vec_PtrPush( vNodes, pObj );
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    [Collects the support of MFFC.]
+
+  Description [Returns the number of internal nodes in the MFFC.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Llb_ManGroupCollect( Llb_Grp_t * pGroup )
+{
+    Vec_Ptr_t * vNodes;
+    Aig_Obj_t * pObj;
+    int i;
+    vNodes = Vec_PtrAlloc( 100 );
+    Aig_ManIncrementTravId( pGroup->pMan->pAig );
+    Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i )
+        Aig_ObjSetTravIdCurrent( pGroup->pMan->pAig, pObj );
+    Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i )
+        Aig_ObjSetTravIdPrevious( pGroup->pMan->pAig, pObj );
+    Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i )
+        Llb_ManGroupCollect_rec( pGroup->pMan->pAig, pObj, vNodes );
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_ManGroupCreate_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Ptr_t * vSupp )
+{ 
+    if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
+        return;
+    Aig_ObjSetTravIdCurrent(pAig, pObj);
+    if ( Aig_ObjIsConst1(pObj) )
+        return;
+    if ( pObj->fMarkA )
+    {
+        Vec_PtrPush( vSupp, pObj );
+        return;
+    }
+    assert( Aig_ObjIsAnd(pObj) );
+    Llb_ManGroupCreate_rec( pAig, Aig_ObjFanin0(pObj), vSupp );
+    Llb_ManGroupCreate_rec( pAig, Aig_ObjFanin1(pObj), vSupp );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Llb_Grp_t * Llb_ManGroupCreate( Llb_Man_t * pMan, Aig_Obj_t * pObj )
+{
+    Llb_Grp_t * p;
+    assert( pObj->fMarkA == 1 );
+    // derive group
+    p = Llb_ManGroupAlloc( pMan );
+    Vec_PtrPush( p->vOuts, pObj );
+    Aig_ManIncrementTravId( pMan->pAig );
+    if ( Aig_ObjIsPo(pObj) )
+        Llb_ManGroupCreate_rec( pMan->pAig, Aig_ObjFanin0(pObj), p->vIns );
+    else
+    {
+        Llb_ManGroupCreate_rec( pMan->pAig, Aig_ObjFanin0(pObj), p->vIns );
+        Llb_ManGroupCreate_rec( pMan->pAig, Aig_ObjFanin1(pObj), p->vIns );
+    }
+    // derive internal objects
+    assert( p->vNodes == NULL );
+    p->vNodes = Llb_ManGroupCollect( p );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Llb_Grp_t * Llb_ManGroupCreateFirst( Llb_Man_t * pMan )
+{
+    Llb_Grp_t * p;
+    Aig_Obj_t * pObj;
+    int i;
+    p = Llb_ManGroupAlloc( pMan );
+    Saig_ManForEachLo( pMan->pAig, pObj, i )
+        Vec_PtrPush( p->vOuts, pObj );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Llb_Grp_t * Llb_ManGroupCreateLast( Llb_Man_t * pMan )
+{
+    Llb_Grp_t * p;
+    Aig_Obj_t * pObj;
+    int i;
+    p = Llb_ManGroupAlloc( pMan );
+    Saig_ManForEachLi( pMan->pAig, pObj, i )
+        Vec_PtrPush( p->vIns, pObj );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Llb_Grp_t * Llb_ManGroupsCombine( Llb_Grp_t * p1, Llb_Grp_t * p2 )
+{
+    Llb_Grp_t * p;
+    Aig_Obj_t * pObj;
+    int i;
+    p = Llb_ManGroupAlloc( p1->pMan );
+    // create inputs
+    Vec_PtrForEachEntry( Aig_Obj_t *, p1->vIns, pObj, i )
+        Vec_PtrPush( p->vIns, pObj );
+    Vec_PtrForEachEntry( Aig_Obj_t *, p2->vIns, pObj, i )
+        Vec_PtrPushUnique( p->vIns, pObj );
+    // create outputs
+    Vec_PtrForEachEntry( Aig_Obj_t *, p1->vOuts, pObj, i )
+        Vec_PtrPush( p->vOuts, pObj );
+    Vec_PtrForEachEntry( Aig_Obj_t *, p2->vOuts, pObj, i )
+        Vec_PtrPushUnique( p->vOuts, pObj );
+
+    // derive internal objects
+    assert( p->vNodes == NULL );
+    p->vNodes = Llb_ManGroupCollect( p );
+    return p;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_ManGroupMarkNodes_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    if ( Aig_ObjIsTravIdPrevious(p, pObj) )
+    {
+        Aig_ObjSetTravIdCurrent(p, pObj);
+        return;
+    }
+    Aig_ObjSetTravIdCurrent(p, pObj);
+    assert( Aig_ObjIsNode(pObj) );
+    Llb_ManGroupMarkNodes_rec( p, Aig_ObjFanin0(pObj) );
+    Llb_ManGroupMarkNodes_rec( p, Aig_ObjFanin1(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates group from two cuts derived by the flow computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Llb_Grp_t * Llb_ManGroupCreateFromCuts( Llb_Man_t * pMan, Vec_Int_t * vCut1, Vec_Int_t * vCut2 )
+{
+    Llb_Grp_t * p;
+    Aig_Obj_t * pObj;
+    int i;
+    p = Llb_ManGroupAlloc( pMan );
+
+    // mark Cut1
+    Aig_ManIncrementTravId( pMan->pAig );
+    Aig_ManForEachNodeVec( pMan->pAig, vCut1, pObj, i )
+        Aig_ObjSetTravIdCurrent( pMan->pAig, pObj );
+    // collect unmarked Cut2
+    Aig_ManForEachNodeVec( pMan->pAig, vCut2, pObj, i )
+        if ( !Aig_ObjIsTravIdCurrent( pMan->pAig, pObj ) )
+            Vec_PtrPush( p->vOuts, pObj );
+
+    // mark nodes reachable from Cut2
+    Aig_ManIncrementTravId( pMan->pAig );
+    Aig_ManForEachNodeVec( pMan->pAig, vCut2, pObj, i )
+        Llb_ManGroupMarkNodes_rec( pMan->pAig, pObj );
+    // collect marked Cut1
+    Aig_ManForEachNodeVec( pMan->pAig, vCut1, pObj, i )
+        if ( Aig_ObjIsTravIdCurrent( pMan->pAig, pObj ) )
+            Vec_PtrPush( p->vIns, pObj );
+
+    // derive internal objects
+    assert( p->vNodes == NULL );
+    p->vNodes = Llb_ManGroupCollect( p );
+    return p;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_ManPrepareGroups( Llb_Man_t * pMan )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    assert( pMan->vGroups == NULL );
+    pMan->vGroups = Vec_PtrAlloc( 1000 );
+    Llb_ManGroupCreateFirst( pMan );
+    Aig_ManForEachNode( pMan->pAig, pObj, i )
+    {
+        if ( pObj->fMarkA )
+            Llb_ManGroupCreate( pMan, pObj );
+    }
+    Saig_ManForEachLi( pMan->pAig, pObj, i )
+    {
+        if ( pObj->fMarkA )
+            Llb_ManGroupCreate( pMan, pObj );
+    }
+    Llb_ManGroupCreateLast( pMan );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_ManPrintSpan( Llb_Man_t * p )
+{
+    Llb_Grp_t * pGroup;
+    Aig_Obj_t * pVar;
+    int i, k, Span = 0, SpanMax = 0;
+    Vec_PtrForEachEntry( Llb_Grp_t *, p->vGroups, pGroup, i )
+    {
+        Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pVar, k )
+            if ( Vec_IntEntry(p->vVarBegs, pVar->Id) == i )
+                Span++;
+        Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pVar, k )
+            if ( Vec_IntEntry(p->vVarBegs, pVar->Id) == i )
+                Span++;
+
+        SpanMax = ABC_MAX( SpanMax, Span );
+printf( "%d ", Span );
+
+        Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pVar, k )
+            if ( Vec_IntEntry(p->vVarEnds, pVar->Id) == i )
+                Span--;
+        Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pVar, k )
+            if ( Vec_IntEntry(p->vVarEnds, pVar->Id) == i )
+                Span--;
+    }
+printf( "\n" );
+printf( "Max = %d\n", SpanMax );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Llb_ManGroupHasVar( Llb_Man_t * p, int iGroup, int iVar )
+{
+    Llb_Grp_t * pGroup = (Llb_Grp_t *)Vec_PtrEntry( p->vGroups, iGroup );
+    Aig_Obj_t * pObj;
+    int i;
+    Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i )
+        if ( pObj->Id == iVar )
+            return 1;
+    Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i )
+        if ( pObj->Id == iVar )
+            return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_ManPrintHisto( Llb_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i, k;
+    Aig_ManForEachObj( p->pAig, pObj, i )
+    {
+        if ( Vec_IntEntry(p->vObj2Var, i) < 0 )
+            continue;
+        printf( "%3d :", i );
+        for ( k = 0; k < Vec_IntEntry(p->vVarBegs, i); k++ )
+            printf( " " );
+        for (      ; k <= Vec_IntEntry(p->vVarEnds, i); k++ )
+            printf( "%c", Llb_ManGroupHasVar(p, k, i)? '*':'-' );
+        printf( "\n" );
+    }
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/llb/llbPivot.c b/src/aig/llb/llbPivot.c
new file mode 100644
index 00000000..6a6fb321
--- /dev/null
+++ b/src/aig/llb/llbPivot.c
@@ -0,0 +1,254 @@
+/**CFile****************************************************************
+
+  FileName    [llbPivot.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [BDD based reachability.]
+
+  Synopsis    [Determining pivot variables.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: llbPivot.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "llbInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Llb_ManTracePaths_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pPivot )
+{
+    Aig_Obj_t * pFanout;
+    int k, iFan;
+    if ( Aig_ObjIsTravIdPrevious(p, pObj) )
+        return 0;
+    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+        return 1;
+    if ( Saig_ObjIsLi(p, pObj) )
+        return 0;
+    if ( Saig_ObjIsPo(p, pObj) )
+        return 0;
+    if ( pObj == pPivot )
+        return 1;
+    assert( Aig_ObjIsCand(pObj) );
+    Aig_ObjForEachFanout( p, pObj, pFanout, iFan, k )
+        if ( !Llb_ManTracePaths_rec( p, pFanout, pPivot ) )
+        {
+            Aig_ObjSetTravIdPrevious(p, pObj);
+            return 0;
+        }
+    Aig_ObjSetTravIdCurrent(p, pObj);
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Llb_ManTracePaths( Aig_Man_t * p, Aig_Obj_t * pPivot )
+{
+    Aig_Obj_t * pObj;
+    int i, Counter = 0;
+    Aig_ManIncrementTravId( p ); // prev = visited with path to LI  (value 0)
+    Aig_ManIncrementTravId( p ); // cur  = visited w/o  path to LI  (value 1)
+    Saig_ManForEachLo( p, pObj, i )
+        Counter += Llb_ManTracePaths_rec( p, pObj, pPivot );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_ManTestCuts( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i, Count;
+    Aig_ManFanoutStart( p );
+    Aig_ManForEachNode( p, pObj, i )
+    {
+        if ( Aig_ObjRefs(pObj) <= 1 )
+            continue;
+        Count = Llb_ManTracePaths( p, pObj );
+        printf( "Obj =%5d.  Lev =%3d.  Fanout =%5d.  Count = %3d.\n", 
+            i, Aig_ObjLevel(pObj), Aig_ObjRefs(pObj), Count );
+    }
+    Aig_ManFanoutStop( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_ManLabelLiCones_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    if ( pObj->fMarkB )
+        return;
+    pObj->fMarkB = 1;
+    assert( Aig_ObjIsNode(pObj) );
+    Llb_ManLabelLiCones_rec( p, Aig_ObjFanin0(pObj) );
+    Llb_ManLabelLiCones_rec( p, Aig_ObjFanin1(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Determine starting cut-points.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_ManLabelLiCones( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    // mark const and PIs
+    Aig_ManConst1(p)->fMarkB = 1;
+    Aig_ManForEachPi( p, pObj, i )
+        pObj->fMarkB = 1;
+    // mark cones
+    Saig_ManForEachLi( p, pObj, i )
+        Llb_ManLabelLiCones_rec( p, Aig_ObjFanin0(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Determine starting cut-points.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_ManMarkInternalPivots( Aig_Man_t * p )
+{
+    Vec_Ptr_t * vMuxes;
+    Aig_Obj_t * pObj;
+    int i, Counter = 0;
+
+    // remove refs due to MUXes
+    vMuxes = Aig_ManMuxesCollect( p );
+    Aig_ManMuxesDeref( p, vMuxes );
+
+    // mark nodes feeding into LIs
+    Aig_ManCleanMarkB( p );
+    Llb_ManLabelLiCones( p );
+
+    // mark internal nodes
+    Aig_ManFanoutStart( p );
+    Aig_ManForEachNode( p, pObj, i )
+        if ( pObj->fMarkB && pObj->nRefs > 1 )
+        {
+            if ( Llb_ManTracePaths(p, pObj) > 0 )
+                pObj->fMarkA = 1;
+            Counter++;
+        }
+    Aig_ManFanoutStop( p );
+//    printf( "TracePath tried = %d.\n", Counter );
+
+    // mark nodes feeding into LIs
+    Aig_ManCleanMarkB( p );
+
+    // add refs due to MUXes
+    Aig_ManMuxesRef( p, vMuxes );
+    Vec_PtrFree( vMuxes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Determine starting cut-points.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Llb_ManMarkPivotNodes( Aig_Man_t * p, int fUseInternal )
+{
+    Vec_Int_t * vVar2Obj;
+    Aig_Obj_t * pObj;
+    int i;
+    // mark inputs/outputs
+    Aig_ManForEachPi( p, pObj, i )
+        pObj->fMarkA = 1;
+    Saig_ManForEachLi( p, pObj, i )
+        pObj->fMarkA = 1;
+
+    // mark internal pivot nodes
+    if ( fUseInternal )
+        Llb_ManMarkInternalPivots( p );
+
+    // assign variable numbers
+    Aig_ManConst1(p)->fMarkA = 0;
+    vVar2Obj = Vec_IntAlloc( 100 );
+    Aig_ManForEachPi( p, pObj, i )
+        Vec_IntPush( vVar2Obj, Aig_ObjId(pObj) );
+    Aig_ManForEachNode( p, pObj, i )
+        if ( pObj->fMarkA )
+            Vec_IntPush( vVar2Obj, Aig_ObjId(pObj) );
+    Saig_ManForEachLi( p, pObj, i )
+        Vec_IntPush( vVar2Obj, Aig_ObjId(pObj) );
+    return vVar2Obj;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/llb/llbReach.c b/src/aig/llb/llbReach.c
new file mode 100644
index 00000000..7c12a88c
--- /dev/null
+++ b/src/aig/llb/llbReach.c
@@ -0,0 +1,620 @@
+/**CFile****************************************************************
+
+  FileName    [llbReach.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [BDD based reachability.]
+
+  Synopsis    [Reachability analysis.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: llbReach.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "llbInt.h"
+#include "extra.h"
+
+ABC_NAMESPACE_IMPL_START
+
+ 
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Derives global BDD for the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Llb_ManConstructOutBdd( Aig_Man_t * pAig, Aig_Obj_t * pNode, DdManager * dd )
+{
+    DdNode * bBdd0, * bBdd1, * bFunc;
+    Vec_Ptr_t * vNodes;
+    Aig_Obj_t * pObj;
+    int i;
+    if ( Aig_ObjFanin0(pNode) == Aig_ManConst1(pAig) )
+        return Cudd_NotCond( Cudd_ReadOne(dd), Aig_ObjFaninC0(pNode) );
+    vNodes = Aig_ManDfsNodes( pAig, &pNode, 1 );
+    assert( Vec_PtrSize(vNodes) > 0 );
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
+    {
+        if ( !Aig_ObjIsNode(pObj) )
+            continue;
+        bBdd0 = Cudd_NotCond( Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
+        bBdd1 = Cudd_NotCond( Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
+        pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 );  Cudd_Ref( (DdNode *)pObj->pData );
+    }
+    bFunc = (DdNode *)pObj->pData; Cudd_Ref( bFunc );
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
+    {
+        if ( !Aig_ObjIsNode(pObj) )
+            continue;
+        Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
+    }
+    Vec_PtrFree( vNodes );
+    if ( Aig_ObjIsPo(pNode) )
+        bFunc = Cudd_NotCond( bFunc, Aig_ObjFaninC0(pNode) );
+    Cudd_Deref( bFunc );
+    return bFunc;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives BDD for the group.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Llb_ManConstructGroupBdd( Llb_Man_t * p, Llb_Grp_t * pGroup )
+{
+    Aig_Obj_t * pObj;
+    DdNode * bBdd0, * bBdd1, * bRes, * bXor, * bTemp;
+    int i;
+    Aig_ManConst1(p->pAig)->pData = Cudd_ReadOne( p->dd );
+    Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i )
+        pObj->pData = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) );
+    Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vNodes, pObj, i )
+    {
+        bBdd0 = Cudd_NotCond( Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
+        bBdd1 = Cudd_NotCond( Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
+        pObj->pData = Cudd_bddAnd( p->dd, bBdd0, bBdd1 );  Cudd_Ref( (DdNode *)pObj->pData );
+    }
+    bRes = Cudd_ReadOne( p->dd );   Cudd_Ref( bRes );
+    Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i )
+    {
+        if ( Aig_ObjIsPo(pObj) )
+            bBdd0 = Cudd_NotCond( Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
+        else
+            bBdd0 = (DdNode *)pObj->pData;
+        bBdd1 = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) );
+        bXor  = Cudd_bddXor( p->dd, bBdd0, bBdd1 );                  Cudd_Ref( bXor );
+        bRes  = Cudd_bddAnd( p->dd, bTemp = bRes, Cudd_Not(bXor) );  Cudd_Ref( bRes );
+        Cudd_RecursiveDeref( p->dd, bTemp );
+        Cudd_RecursiveDeref( p->dd, bXor );
+    }
+    Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vNodes, pObj, i )
+        Cudd_RecursiveDeref( p->dd, (DdNode *)pObj->pData );
+    Cudd_Deref( bRes );
+    return bRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives quantification cube.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Llb_ManConstructQuantCubeIntern( Llb_Man_t * p, Llb_Grp_t * pGroup, int iGrpPlace )
+{
+    Aig_Obj_t * pObj;
+    DdNode * bRes, * bTemp, * bVar;
+    int i, iGroupFirst, iGroupLast;
+    bRes = Cudd_ReadOne( p->dd );   Cudd_Ref( bRes );
+    Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i )
+    {
+        iGroupFirst = Vec_IntEntry(p->vVarBegs, Aig_ObjId(pObj));
+        iGroupLast  = Vec_IntEntry(p->vVarEnds, Aig_ObjId(pObj));
+        assert( iGroupFirst <= iGroupLast );
+        if ( iGroupFirst < iGroupLast )
+            continue;
+        bVar  = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) );
+        bRes  = Cudd_bddAnd( p->dd, bTemp = bRes, bVar );  Cudd_Ref( bRes );
+        Cudd_RecursiveDeref( p->dd, bTemp );
+    }
+    Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i )
+    {
+        iGroupFirst = Vec_IntEntry(p->vVarBegs, Aig_ObjId(pObj));
+        iGroupLast  = Vec_IntEntry(p->vVarEnds, Aig_ObjId(pObj));
+        assert( iGroupFirst <= iGroupLast );
+        if ( iGroupFirst < iGroupLast )
+            continue;
+        bVar  = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) );
+        bRes  = Cudd_bddAnd( p->dd, bTemp = bRes, bVar );  Cudd_Ref( bRes );
+        Cudd_RecursiveDeref( p->dd, bTemp );
+    }
+    Cudd_Deref( bRes );
+    return bRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives quantification cube.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Llb_ManConstructQuantCube( Llb_Man_t * p, Llb_Grp_t * pGroup, int iGrpPlace )
+{
+    Aig_Obj_t * pObj;
+    DdNode * bRes, * bTemp, * bVar;
+    int i, iGroupLast;
+    bRes = Cudd_ReadOne( p->dd );   Cudd_Ref( bRes );
+    Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i )
+    {
+        iGroupLast = Vec_IntEntry(p->vVarEnds, Aig_ObjId(pObj));
+        assert( iGroupLast >= iGrpPlace );
+        if ( iGroupLast > iGrpPlace )
+            continue;
+        bVar  = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) );
+        bRes  = Cudd_bddAnd( p->dd, bTemp = bRes, bVar );  Cudd_Ref( bRes );
+        Cudd_RecursiveDeref( p->dd, bTemp );
+    }
+    Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i )
+    {
+        iGroupLast = Vec_IntEntry(p->vVarEnds, Aig_ObjId(pObj));
+        assert( iGroupLast >= iGrpPlace );
+        if ( iGroupLast > iGrpPlace )
+            continue;
+        bVar  = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) );
+        bRes  = Cudd_bddAnd( p->dd, bTemp = bRes, bVar );  Cudd_Ref( bRes );
+        Cudd_RecursiveDeref( p->dd, bTemp );
+    }
+    Cudd_Deref( bRes );
+    return bRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Llb_ManComputeInitState( Llb_Man_t * p, DdManager * dd )
+{
+    Aig_Obj_t * pObj;
+    DdNode * bRes, * bVar, * bTemp;
+    int i, iVar;
+    bRes = Cudd_ReadOne( dd );   Cudd_Ref( bRes );
+    Saig_ManForEachLo( p->pAig, pObj, i )
+    {
+        iVar  = (dd == p->ddG) ? i : Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj));
+        bVar  = Cudd_bddIthVar( dd, iVar );
+        bRes  = Cudd_bddAnd( dd, bTemp = bRes, Cudd_Not(bVar) );  Cudd_Ref( bRes );
+        Cudd_RecursiveDeref( dd, bTemp );
+    }
+    Cudd_Deref( bRes );
+    return bRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Llb_ManComputeImage( Llb_Man_t * p, DdNode * bInit )
+{
+    int fCheckSupport = 0;
+    Llb_Grp_t * pGroup;
+    DdNode * bImage, * bGroup, * bCube, * bTemp;
+    int i;
+    bImage = bInit;  Cudd_Ref( bImage );
+    for ( i = 1; i < p->pMatrix->nCols-1; i++ )
+    {
+        // compute group BDD
+        pGroup = p->pMatrix->pColGrps[i];
+        bGroup = Llb_ManConstructGroupBdd( p, pGroup );                          Cudd_Ref( bGroup );
+        // quantify variables appearing only in this group
+        bCube  = Llb_ManConstructQuantCubeIntern( p, pGroup, i );                Cudd_Ref( bCube );
+        bGroup = Cudd_bddExistAbstract( p->dd, bTemp = bGroup, bCube );         Cudd_Ref( bGroup );
+        Cudd_RecursiveDeref( p->dd, bTemp );
+        Cudd_RecursiveDeref( p->dd, bCube );
+        // perform partial product
+        bCube  = Llb_ManConstructQuantCube( p, pGroup, i );                      Cudd_Ref( bCube );
+        bImage = Cudd_bddAndAbstract( p->dd, bTemp = bImage, bGroup, bCube );   Cudd_Ref( bImage );
+        Cudd_RecursiveDeref( p->dd, bTemp );
+        Cudd_RecursiveDeref( p->dd, bGroup );
+        Cudd_RecursiveDeref( p->dd, bCube );
+        // chech runtime
+        if ( p->pPars->TimeTarget && clock() >= p->pPars->TimeTarget )
+        {
+            Cudd_RecursiveDeref( p->dd, bImage );
+            return NULL;
+        }
+    }
+
+    // make sure image depends on next state vars
+    if ( fCheckSupport )
+    {
+        bCube = Cudd_Support( p->dd, bImage );    Cudd_Ref( bCube );
+        for ( bTemp = bCube; bTemp != p->dd->one; bTemp = cuddT(bTemp) )
+        {
+            int ObjId = Vec_IntEntry( p->vVar2Obj, bTemp->index );
+            Aig_Obj_t * pObj = Aig_ManObj( p->pAig, ObjId );
+            if ( !Saig_ObjIsLi(p->pAig, pObj) )
+                printf( "Var %d assigned to obj %d that is not LI\n", bTemp->index, ObjId );
+        }
+        Cudd_RecursiveDeref( p->dd, bCube );
+    }
+    Cudd_Deref( bImage );
+    return bImage;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Llb_ManCreateConstraints( Llb_Man_t * p, Vec_Int_t * vHints, int fUseNsVars )
+{
+    DdNode * bConstr, * bFunc, * bTemp;
+    Aig_Obj_t * pObj;
+    int i, Entry;
+    if ( vHints == NULL )
+        return Cudd_ReadOne( p->dd );
+    assert( Aig_ManPiNum(p->pAig) == Aig_ManPiNum(p->pAigGlo) );
+    // assign const and PI nodes to the original AIG
+    Aig_ManCleanData( p->pAig );
+    Aig_ManConst1( p->pAig )->pData = Cudd_ReadOne( p->dd );
+    Saig_ManForEachPi( p->pAig, pObj, i )
+        pObj->pData = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var,Aig_ObjId(pObj)) );
+    Saig_ManForEachLo( p->pAig, pObj, i )
+    {
+        if ( fUseNsVars )
+            Entry = Vec_IntEntry( p->vObj2Var, Aig_ObjId(Saig_ObjLoToLi(p->pAig, pObj)) );
+        else
+            Entry = Vec_IntEntry( p->vObj2Var, Aig_ObjId(pObj) );
+        pObj->pData = Cudd_bddIthVar( p->dd, Entry );
+    }
+    // transfer them to the global AIG
+    Aig_ManCleanData( p->pAigGlo );
+    Aig_ManConst1( p->pAigGlo )->pData = Cudd_ReadOne( p->dd );
+    Aig_ManForEachPi( p->pAigGlo, pObj, i )
+        pObj->pData = Aig_ManPi(p->pAig, i)->pData;
+    // derive consraints
+    bConstr = Cudd_ReadOne( p->dd );   Cudd_Ref( bConstr );
+    Vec_IntForEachEntry( vHints, Entry, i )
+    {
+        if ( Entry != 0 && Entry != 1 )
+            continue;
+        bFunc = Llb_ManConstructOutBdd( p->pAigGlo, Aig_ManObj(p->pAigGlo, i), p->dd );  Cudd_Ref( bFunc );
+        bFunc = Cudd_NotCond( bFunc, Entry ); // restrict to not constraint
+        // make the product
+        bConstr = Cudd_bddAnd( p->dd, bTemp = bConstr, bFunc );                          Cudd_Ref( bConstr );
+        Cudd_RecursiveDeref( p->dd, bTemp );
+        Cudd_RecursiveDeref( p->dd, bFunc );
+    }
+    Cudd_Deref( bConstr );
+    return bConstr;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Perform reachability with hints and returns reached states in ppGlo.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo )
+{
+    int fCheckOutputs    = !p->pPars->fSkipOutCheck;  
+    int fInternalReorder = 0;
+    int * pNs2Glo = Vec_IntArray( p->vNs2Glo );
+    int * pGlo2Cs = Vec_IntArray( p->vGlo2Cs );
+    DdNode * bCurrent, * bReached, * bNext, * bTemp, * bCube;
+    DdNode * bConstrCs, * bConstrNs;
+    int clk2, clk = clock(), nIters, nBddSize = 0, iOutFail = -1;
+    int nThreshold = 10000;
+
+    // compute time to stop
+    if ( p->pPars->TimeLimit )
+        p->pPars->TimeTarget = clock() + p->pPars->TimeLimit * CLOCKS_PER_SEC;
+    else
+        p->pPars->TimeTarget = 0;
+
+    // define variable limits
+    Llb_ManPrepareVarLimits( p );
+
+    // start the managers
+    assert( p->dd == NULL );
+    assert( p->ddG == NULL );
+    p->dd  = Cudd_Init( Vec_IntSize(p->vVar2Obj), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    if ( pddGlo && *pddGlo )
+        p->ddG = *pddGlo, *pddGlo = NULL; 
+    else
+        p->ddG = Cudd_Init( Aig_ManRegNum(p->pAig),   0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+
+    if ( p->pPars->fReorder )
+    {
+        Cudd_AutodynEnable( p->dd,  CUDD_REORDER_SYMM_SIFT );
+        Cudd_AutodynEnable( p->ddG, CUDD_REORDER_SYMM_SIFT );
+    }
+    else
+    {
+        Cudd_AutodynDisable( p->dd );
+        Cudd_AutodynDisable( p->ddG );
+    }
+
+    // derive constraints
+    bConstrCs = Llb_ManCreateConstraints( p, vHints, 0 );   Cudd_Ref( bConstrCs );
+    bConstrNs = Llb_ManCreateConstraints( p, vHints, 1 );   Cudd_Ref( bConstrNs );
+//Extra_bddPrint( p->dd, bConstrCs ); printf( "\n" );
+//Extra_bddPrint( p->dd, bConstrNs ); printf( "\n" );
+
+    // perform reachability analysis
+    // compute the starting set of states
+    if ( p->ddG->bReached )
+    {
+        bReached = p->ddG->bReached; p->ddG->bReached = NULL;
+        bCurrent = Extra_TransferPermute( p->ddG, p->dd, bReached, pGlo2Cs );    Cudd_Ref( bCurrent );
+    }
+    else
+    {
+        bReached = Llb_ManComputeInitState( p, p->ddG );                         Cudd_Ref( bReached );
+        bCurrent = Llb_ManComputeInitState( p, p->dd  );                         Cudd_Ref( bCurrent );
+    }
+//Extra_bddPrintSupport( p->ddG, bReached ); printf( "\n" );
+//Extra_bddPrintSupport( p->dd,  bCurrent ); printf( "\n" );
+
+//Extra_bddPrintSupport( p->dd, bCurrent ); printf( "\n" );
+    for ( nIters = 0; nIters < p->pPars->nIterMax; nIters++ )
+    { 
+        clk2 = clock();
+        // check the runtime limit
+        if ( p->pPars->TimeLimit && clock() >= p->pPars->TimeTarget )
+        {
+            if ( !p->pPars->fSilent )
+                printf( "Reached timeout during image computation (%d seconds).\n",  p->pPars->TimeLimit );
+            p->pPars->iFrame = nIters - 1;
+            Cudd_RecursiveDeref( p->dd,  bCurrent );  bCurrent = NULL;
+            Cudd_RecursiveDeref( p->dd,  bConstrCs ); bConstrCs = NULL;
+            Cudd_RecursiveDeref( p->dd,  bConstrNs ); bConstrNs = NULL;
+            Cudd_RecursiveDeref( p->ddG, bReached );  bReached = NULL;
+            return -1;
+        }
+
+        // check outputs
+        if ( fCheckOutputs )
+        {
+            Aig_Obj_t * pObj;
+            int i;
+            Aig_ManConst1( p->pAigGlo )->pData = Cudd_ReadOne( p->dd );
+            Aig_ManForEachPi( p->pAig, pObj, i )
+                pObj->pData = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var,Aig_ObjId(pObj)) );
+            Aig_ManForEachPi( p->pAigGlo, pObj, i )
+                pObj->pData = Aig_ManPi(p->pAig, i)->pData;
+
+//Extra_bddPrintSupport( p->dd, bCurrent ); printf( "\n" );
+            for ( iOutFail = 0; iOutFail < Saig_ManPoNum(p->pAig); iOutFail++ )
+            {
+                DdNode * bFunc, * bInter;
+                bFunc = Llb_ManConstructOutBdd( p->pAigGlo, Aig_ManPo(p->pAigGlo, iOutFail), p->dd );  Cudd_Ref( bFunc );
+//Extra_bddPrint( p->dd, bFunc ); printf( "\n" );
+                if ( Cudd_bddLeq( p->dd, bCurrent, Cudd_Not(bFunc) ) ) // no cex
+                {
+                    Cudd_RecursiveDeref( p->dd, bFunc );
+                    continue;
+                }
+                bInter = Cudd_bddIntersect( p->dd, bCurrent, bFunc );  Cudd_Ref( bInter );
+                assert( p->pAig->pSeqModel == NULL );
+                p->pAig->pSeqModel = Llb_ManDeriveCex( p, bInter, iOutFail, nIters ); 
+                Cudd_RecursiveDeref( p->dd, bInter );
+                Cudd_RecursiveDeref( p->dd, bFunc );
+                break;
+            }
+            if ( iOutFail < Saig_ManPoNum(p->pAig) )
+            {
+                if ( !p->pPars->fSilent )
+                    printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness).  ", iOutFail, nIters );
+                Cudd_RecursiveDeref( p->ddG, bReached );  bReached = NULL;
+                Cudd_RecursiveDeref( p->dd,  bCurrent );  bCurrent = NULL;
+                p->pPars->iFrame = nIters;
+                break;
+            }
+        }
+
+        // restrict reachable states using constraints
+        if ( vHints )
+        {
+            bCurrent = Cudd_bddAnd( p->dd, bTemp = bCurrent, bConstrCs );               Cudd_Ref( bCurrent );
+            Cudd_RecursiveDeref( p->dd, bTemp );
+        }
+
+        // quantify variables appearing only in the init state
+        bCube    = Llb_ManConstructQuantCubeIntern( p, (Llb_Grp_t *)Vec_PtrEntry(p->vGroups,0), 0 ); Cudd_Ref( bCube );
+        bCurrent = Cudd_bddExistAbstract( p->dd, bTemp = bCurrent, bCube );             Cudd_Ref( bCurrent );
+        Cudd_RecursiveDeref( p->dd, bTemp );
+        Cudd_RecursiveDeref( p->dd, bCube );
+
+        // compute the next states
+        bNext = Llb_ManComputeImage( p, bCurrent );
+        if ( bNext == NULL )
+        {
+            if ( !p->pPars->fSilent )
+                printf( "Reached timeout during image computation (%d seconds).\n",  p->pPars->TimeLimit );
+            p->pPars->iFrame = nIters - 1;
+            Cudd_RecursiveDeref( p->dd,  bCurrent );   bCurrent = NULL;
+            Cudd_RecursiveDeref( p->dd,  bConstrCs );  bConstrCs = NULL;
+            Cudd_RecursiveDeref( p->dd,  bConstrNs );  bConstrNs = NULL;
+            Cudd_RecursiveDeref( p->ddG, bReached );   bReached = NULL;
+            return -1;
+        }
+        Cudd_Ref( bNext );
+        Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
+
+        // restrict reachable states using constraints
+        if ( vHints )
+        {
+            bNext = Cudd_bddAnd( p->dd, bTemp = bNext, bConstrNs );                Cudd_Ref( bNext );
+            Cudd_RecursiveDeref( p->dd, bTemp );
+        }
+//Extra_bddPrintSupport( p->dd, bNext ); printf( "\n" );
+
+        // remap these states into the current state vars
+        bNext = Extra_TransferPermute( p->dd, p->ddG, bTemp = bNext, pNs2Glo );    Cudd_Ref( bNext );
+        Cudd_RecursiveDeref( p->dd, bTemp );
+
+        // check if there are any new states
+        if ( Cudd_bddLeq( p->ddG, bNext, bReached ) ) // implication = no new states
+        {
+            Cudd_RecursiveDeref( p->ddG,  bNext );     bNext = NULL;
+            break;
+        }
+
+        // check the BDD size
+        nBddSize = Cudd_DagSize(bNext);
+        if ( nBddSize > p->pPars->nBddMax )
+        {
+            Cudd_RecursiveDeref( p->ddG,  bNext );     bNext = NULL;
+            break;
+        }
+
+        // get the new states
+        bCurrent = Cudd_bddAnd( p->ddG, bNext, Cudd_Not(bReached) );                    Cudd_Ref( bCurrent );
+        // minimize the new states with the reached states
+//        bCurrent = Cudd_bddConstrain( p->ddG, bTemp = bCurrent, Cudd_Not(bReached) ); Cudd_Ref( bCurrent );
+//        bCurrent = Cudd_bddRestrict( p->ddG, bTemp = bCurrent, Cudd_Not(bReached) );  Cudd_Ref( bCurrent );
+//        Cudd_RecursiveDeref( p->ddG, bTemp );
+//printf( "Initial BDD =%7d. Constrained BDD =%7d.\n", Cudd_DagSize(bTemp), Cudd_DagSize(bCurrent) );
+        // remap these states into the current state vars
+        bCurrent = Extra_TransferPermute( p->ddG, p->dd, bTemp = bCurrent, pGlo2Cs );   Cudd_Ref( bCurrent );
+        Cudd_RecursiveDeref( p->ddG, bTemp );
+
+        // add to the reached states
+        bReached = Cudd_bddOr( p->ddG, bTemp = bReached, bNext );                       Cudd_Ref( bReached );
+        Cudd_RecursiveDeref( p->ddG, bTemp );
+        Cudd_RecursiveDeref( p->ddG, bNext );
+        bNext = NULL;
+
+        if ( p->pPars->fVerbose )
+        {
+            fprintf( stdout, "F =%3d : ",    nIters );
+            fprintf( stdout, "Image =%6d  ", nBddSize );
+            fprintf( stdout, "%8d (%4d %3d)     ", 
+                Cudd_ReadKeys(p->dd),  Cudd_ReadReorderings(p->dd),  Cudd_ReadGarbageCollections(p->dd) );
+            fprintf( stdout, "Reach =%6d  ", Cudd_DagSize(bReached) );
+            fprintf( stdout, "%8d (%4d %3d)  ", 
+                Cudd_ReadKeys(p->ddG), Cudd_ReadReorderings(p->ddG), Cudd_ReadGarbageCollections(p->ddG) );
+        }
+        if ( fInternalReorder && p->pPars->fReorder && nBddSize > nThreshold )
+        {
+            if ( p->pPars->fVerbose )
+                fprintf( stdout, "Reordering... Before = %5d. ", Cudd_DagSize(bReached) );
+            Cudd_ReduceHeap( p->dd, CUDD_REORDER_SYMM_SIFT, 100 );
+//            Cudd_AutodynDisable( p->dd );
+            if ( p->pPars->fVerbose )
+                fprintf( stdout, "After = %5d.\r", Cudd_DagSize(bReached) );
+            nThreshold *= 2;
+        }
+        if ( p->pPars->fVerbose )
+//            fprintf( stdout, "\r" );
+//            fprintf( stdout, "\n" );
+            Abc_PrintTime( 1, "T", clock() - clk2 );
+    }
+    Cudd_RecursiveDeref( p->dd, bConstrCs ); bConstrCs = NULL;
+    Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL;
+    if ( bReached == NULL )
+        return 0; // reachable
+    assert( bCurrent == NULL );
+    if ( bCurrent )
+        Cudd_RecursiveDeref( p->dd, bCurrent );
+    // report the stats
+    if ( p->pPars->fVerbose )
+    {
+        double nMints = Cudd_CountMinterm(p->ddG, bReached, Saig_ManRegNum(p->pAig) );
+        if ( nIters >= p->pPars->nIterMax || nBddSize > p->pPars->nBddMax )
+            fprintf( stdout, "Reachability analysis is stopped after %d frames.\n", nIters );
+        else
+            fprintf( stdout, "Reachability analysis completed after %d frames.\n", nIters );
+        fprintf( stdout, "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p->pAig)) );
+        fflush( stdout ); 
+    }
+    if ( nIters >= p->pPars->nIterMax || nBddSize > p->pPars->nBddMax )
+    {
+        if ( !p->pPars->fSilent )
+            printf( "Verified only for states reachable in %d frames.  ", nIters );
+        Cudd_RecursiveDeref( p->ddG, bReached );
+        return -1; // undecided
+    }
+    if ( pddGlo ) 
+    {
+        assert( p->ddG->bReached == NULL );
+        p->ddG->bReached = bReached; bReached = NULL;
+        assert( *pddGlo == NULL );
+        *pddGlo = p->ddG;  p->ddG = NULL;
+    }
+    else
+        Cudd_RecursiveDeref( p->ddG, bReached );
+    if ( !p->pPars->fSilent )
+        printf( "The miter is proved unreachable after %d iterations.  ", nIters );
+    p->pPars->iFrame = nIters - 1;
+    return 1; // unreachable
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/llb/llbSched.c b/src/aig/llb/llbSched.c
new file mode 100644
index 00000000..0f7b9fab
--- /dev/null
+++ b/src/aig/llb/llbSched.c
@@ -0,0 +1,257 @@
+/**CFile****************************************************************
+
+  FileName    [llb.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [BDD based reachability.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: llb.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "llbInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Swaps two rows.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_MtrSwapColumns( Llb_Mtr_t * p, int iCol1, int iCol2 )
+{
+    Llb_Grp_t * pGemp;
+    char * pTemp;
+    int iTemp;
+    assert( iCol1 >= 0 && iCol1 < p->nCols );
+    assert( iCol2 >= 0 && iCol2 < p->nCols );
+    if ( iCol1 == iCol2 )
+        return;
+    assert( iCol1 != iCol2 );
+    // swap col groups
+    pGemp = p->pColGrps[iCol1];
+    p->pColGrps[iCol1] = p->pColGrps[iCol2];
+    p->pColGrps[iCol2] = pGemp;
+    // swap col vectors
+    pTemp = p->pMatrix[iCol1];
+    p->pMatrix[iCol1] = p->pMatrix[iCol2];
+    p->pMatrix[iCol2] = pTemp;
+    // swap col sums
+    iTemp = p->pColSums[iCol1];
+    p->pColSums[iCol1] = p->pColSums[iCol2];
+    p->pColSums[iCol2] = iTemp;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Find columns which brings as few vars as possible.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Llb_MtrFindBestColumn( Llb_Mtr_t * p, int iGrpStart )
+{
+    int Cost, Cost2, CostBest = ABC_INFINITY, Cost2Best = ABC_INFINITY;
+    int WeightCur, WeightBest = -ABC_INFINITY, iGrp, iGrpBest = -1;
+    int k, c, iVar, Counter;
+    // find partition that reduces partial product as much as possible
+    for ( iVar = 0; iVar < p->nRows - p->nFfs; iVar++ )
+    { 
+        if ( p->pRowSums[iVar] < 2 )
+            continue;
+        // look at present variables that can be quantified
+        if ( !(p->pProdVars[iVar] == 1 && p->pProdNums[iVar] == 1) )
+            continue;
+        // check that it appears in one partition only
+        Counter = 0;
+        for ( c = iGrpStart; c < p->nCols-1; c++ )
+            if ( p->pMatrix[c][iVar] == 1 )
+            {
+                iGrp = c;
+                Counter++;
+            }
+        assert( Counter == 1 );
+        if ( Counter != 1 )
+            Abc_Print( -1, "Llb_MtrFindBestColumn() Internal error!\n" );
+        // find weight of this column
+        WeightCur = 0;
+        for ( k = 0; k < p->nRows; k++ )
+        {
+            // increase weight if variable k will be quantified from partial product
+            if ( p->pProdVars[k] == 1 && p->pMatrix[iGrp][k] == 1 && p->pProdNums[k] == 1 ) 
+                WeightCur += 2;
+            // decrease weight if variable k will be added to partial product
+            if ( p->pProdVars[k] == 0 && p->pMatrix[iGrp][k] == 1 )
+                WeightCur--;
+        }
+        if ( WeightCur > 0 && WeightBest < WeightCur )
+        {
+            WeightBest = WeightCur;
+            iGrpBest   = iGrp;
+        }
+    }
+    if ( iGrpBest >= 0 )
+        return iGrpBest;
+    // could not find the group with any vars to quantify
+    // select the group that contains as few extra variables as possible
+    // if there is a tie, select variables that appear in less groups than others
+    for ( iGrp = iGrpStart; iGrp < p->nCols-1; iGrp++ )
+    {
+        Cost = Cost2 = 0;
+        for ( k = 0; k < p->nRows; k++ )
+            if ( p->pProdVars[k] == 0 && p->pMatrix[iGrp][k] == 1 )
+            {
+                Cost++;
+                Cost2 += p->pProdNums[k];
+            }
+        if ( CostBest >  Cost || 
+            (CostBest == Cost && Cost2 > Cost2Best) )
+        {
+            CostBest  = Cost;
+            Cost2Best = Cost2;
+            iGrpBest  = iGrp;
+        }
+    }
+    return iGrpBest;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of variables that will be saved.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_MtrUseSelectedColumn( Llb_Mtr_t * p, int iCol )
+{
+    int iVar;
+    assert( iCol >= 1 && iCol < p->nCols - 1 );
+    for ( iVar = 0; iVar < p->nRows; iVar++ )
+    {
+        if ( p->pMatrix[iCol][iVar] == 0 )
+            continue;
+        if ( p->pProdVars[iVar] == 1 && p->pProdNums[iVar] == 1 )
+        {
+            p->pProdVars[iVar] = 0;
+            p->pProdNums[iVar] = 0;
+            continue;
+        }
+        if ( p->pProdVars[iVar] == 0 )
+        {
+            p->pProdVars[iVar] = 1;
+            p->pProdNums[iVar] = p->pRowSums[iVar];
+        }
+        p->pProdNums[iVar]--;
+        assert( p->pProdNums[iVar] >= 0 );
+        if ( p->pProdNums[iVar] < 0 )
+            Abc_Print( -1, "Llb_MtrUseSelectedColumn() Internal error!\n" );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Verify columns.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_MtrVerifyColumns( Llb_Mtr_t * p, int iGrpStart )
+{
+    int iVar, iGrp, Counter;
+    for ( iVar = 0; iVar < p->nRows; iVar++ )
+    {
+        if ( p->pProdVars[iVar] == 0 )
+            continue;
+        Counter = 0;
+        for ( iGrp = iGrpStart; iGrp < p->nCols; iGrp++ )
+            if ( p->pMatrix[iGrp][iVar] == 1 )
+                Counter++;
+        assert( Counter == p->pProdNums[iVar] );
+        if ( Counter != p->pProdNums[iVar] )
+            Abc_Print( -1, "Llb_MtrVerifyColumns(): Internal error.\n" );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Matrix reduce.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_MtrSchedule( Llb_Mtr_t * p )
+{
+    int iGrp, iGrpBest, i;
+    // start partial product
+    for ( i = 0; i < p->nRows; i++ )
+    {
+        if ( i >= p->nPis && i < p->nPis + p->nFfs )
+        {
+            p->pProdVars[i] = 1;
+            p->pProdNums[i] = p->pRowSums[i] - 1;
+        }
+        else 
+        {
+            p->pProdVars[i] = 0;
+            p->pProdNums[i] = p->pRowSums[i];
+        }
+    }
+    // order the partitions
+    Llb_MtrVerifyMatrix( p );
+    for ( iGrp = 1; iGrp < p->nCols-1; iGrp++ )
+    {
+        Llb_MtrVerifyColumns( p, iGrp );
+        iGrpBest = Llb_MtrFindBestColumn( p, iGrp );
+        Llb_MtrUseSelectedColumn( p, iGrpBest );
+        Llb_MtrSwapColumns( p, iGrp, iGrpBest );
+    }
+    Llb_MtrVerifyMatrix( p );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/llb/module.make b/src/aig/llb/module.make
new file mode 100644
index 00000000..60b6ce07
--- /dev/null
+++ b/src/aig/llb/module.make
@@ -0,0 +1,11 @@
+SRC +=    src/aig/llb/llbCex.c \
+    src/aig/llb/llbCluster.c \
+    src/aig/llb/llbConstr.c \
+    src/aig/llb/llbCore.c \
+    src/aig/llb/llbHint.c \
+    src/aig/llb/llbMan.c \
+    src/aig/llb/llbMatrix.c \
+    src/aig/llb/llbPart.c \
+    src/aig/llb/llbPivot.c \
+    src/aig/llb/llbReach.c \
+    src/aig/llb/llbSched.c