Version abc70705

25 files changed, 3328 insertions, 1955 deletions

diff --git a/Makefile b/Makefile
index 6d0919fb..28131069 100644
--- a/Makefile
+++ b/Makefile
@@ -6,12 +6,21 @@ CP   := cp
 
 PROG := abc
 
-MODULES := src/base/abc src/base/abci src/base/cmd src/base/io src/base/main src/base/ver \
-	src/aig/ivy src/aig/hop src/aig/rwt src/aig/deco src/aig/mem src/aig/ec \
-	src/bdd/cudd src/bdd/dsd src/bdd/epd src/bdd/mtr src/bdd/parse src/bdd/reo src/bdd/cas \
-	src/map/fpga src/map/mapper src/map/mio src/map/super src/map/if \
-	src/misc/extra src/misc/mvc src/misc/st src/misc/util src/misc/espresso src/misc/nm src/misc/vec src/misc/hash \
-	src/opt/cut src/opt/dec src/opt/fxu src/opt/rwr src/opt/sim src/opt/ret src/opt/res src/opt/kit \
+MODULES := src/base/abc src/base/abci src/base/cmd \
+	src/base/io src/base/main src/base/ver \
+	src/aig/ivy src/aig/hop src/aig/rwt src/aig/deco \
+	src/aig/mem src/aig/dar src/aig/fra src/aig/cnf \
+	src/aig/ec \
+	src/bdd/cudd src/bdd/dsd src/bdd/epd src/bdd/mtr \
+	src/bdd/parse src/bdd/reo src/bdd/cas \
+	src/map/fpga src/map/mapper src/map/mio \
+	src/map/super src/map/if \
+	src/misc/extra src/misc/mvc src/misc/st src/misc/util \
+	src/misc/espresso src/misc/nm src/misc/vec \
+	src/misc/hash \
+	src/opt/cut src/opt/dec src/opt/fxu src/opt/rwr \
+	src/opt/sim src/opt/ret src/opt/res src/opt/kit \
+	src/opt/lpk \
 	src/sat/bsat src/sat/csat src/sat/msat src/sat/fraig \
 	src/phys/place 	
 
diff --git a/abc.dsp b/abc.dsp
index 30ebec3f..e1ea15fb 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -42,7 +42,7 @@ RSC=rc.exe
 # PROP Ignore_Export_Lib 0
 # PROP Target_Dir ""
 # ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c
-# ADD CPP /nologo /W3 /GX /O2 /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\bsat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\opt\kit" /I "src\opt\res" /I "src\map\fpga" /I "src\map\if" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /I "src\misc\hash" /I "src\aig\ivy" /I "src\aig\hop" /I "src\aig\rwt" /I "src\aig\deco" /I "src\aig\mem" /I "src\aig\dar" /I "src\aig\cnf" /I "src\aig\fra" /I "src\temp\esop" /I "src\phys\place" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /c
+# ADD CPP /nologo /W3 /GX /O2 /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\bsat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\opt\kit" /I "src\opt\res" /I "src\opt\lpk" /I "src\opt\bdc" /I "src\map\fpga" /I "src\map\if" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /I "src\misc\hash" /I "src\aig\ivy" /I "src\aig\hop" /I "src\aig\rwt" /I "src\aig\deco" /I "src\aig\mem" /I "src\aig\dar" /I "src\aig\cnf" /I "src\aig\fra" /I "src\temp\esop" /I "src\phys\place" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /c
 # ADD BASE RSC /l 0x409 /d "NDEBUG"
 # ADD RSC /l 0x409 /d "NDEBUG"
 BSC32=bscmake.exe
@@ -66,7 +66,7 @@ LINK32=link.exe
 # PROP Ignore_Export_Lib 0
 # PROP Target_Dir ""
 # ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c
-# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\bsat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\opt\kit" /I "src\opt\res" /I "src\map\fpga" /I "src\map\if" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /I "src\misc\hash" /I "src\aig\ivy" /I "src\aig\hop" /I "src\aig\rwt" /I "src\aig\deco" /I "src\aig\mem" /I "src\aig\dar" /I "src\aig\cnf" /I "src\aig\fra" /I "src\temp\esop" /I "src\phys\place" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /GZ /c
+# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\bsat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\opt\kit" /I "src\opt\res" /I "src\opt\lpk" /I "src\opt\bdc" /I "src\map\fpga" /I "src\map\if" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /I "src\misc\hash" /I "src\aig\ivy" /I "src\aig\hop" /I "src\aig\rwt" /I "src\aig\deco" /I "src\aig\mem" /I "src\aig\dar" /I "src\aig\cnf" /I "src\aig\fra" /I "src\temp\esop" /I "src\phys\place" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /GZ /c
 # SUBTRACT CPP /X
 # ADD BASE RSC /l 0x409 /d "_DEBUG"
 # ADD RSC /l 0x409 /d "_DEBUG"
@@ -230,10 +230,6 @@ SOURCE=.\src\base\abci\abcDsd.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\base\abci\abcDsdRes.c
-# End Source File
-# Begin Source File
-
 SOURCE=.\src\base\abci\abcEspresso.c
 # End Source File
 # Begin Source File
@@ -1937,6 +1933,46 @@ SOURCE=.\src\opt\bdc\bdcInt.h
 SOURCE=.\src\opt\bdc\bdcTable.c
 # End Source File
 # End Group
+# Begin Group "lpk"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\opt\lpk\lpk.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\lpk\lpkCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\lpk\lpkCut.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\lpk\lpkInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\lpk\lpkMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\lpk\lpkMap.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\lpk\lpkMulti.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\lpk\lpkMux.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\lpk\lpkSets.c
+# End Source File
+# End Group
 # End Group
 # Begin Group "map"
 
diff --git a/abc.rc b/abc.rc
index a6efab40..b9cb6ff4 100644
--- a/abc.rc
+++ b/abc.rc
@@ -31,6 +31,7 @@ alias fsto fraig_store
 alias fres fraig_restore
 alias ft fraig_trust
 alias lp lutpack
+alias pd print_dsd
 alias pex print_exdc -d
 alias pf print_factor
 alias pfan print_fanio
@@ -169,6 +170,8 @@ alias tst6     "r i10_if6.blif; st; ps; r x/rec6_16_.blif; st; rec_start; r i10_
 alias bug      "r pj1_if3.blif; lp"
 alias table    "r lutexp.baf; test"
 
-alias t        "r c.blif; st; wc c.cnf"
+#alias t        "r c.blif; st; wc c.cnf"
+#alias t        "r test/dsdmap6.blif; lutpack -vw; cec"
+alias t        "r i10_if4.blif; lp"
 
 
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 3b309b43..30557259 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -227,23 +227,6 @@ struct Abc_Lib_t_
     void *            pGenlib;       // the genlib library used to map this design
 };
 
-typedef struct Lut_Par_t_ Lut_Par_t;
-struct Lut_Par_t_
-{
-    // user-controlled parameters
-    int               nLutsMax;      // (N) the maximum number of LUTs in the structure
-    int               nLutsOver;     // (Q) the maximum number of LUTs not in the MFFC
-    int               nVarsShared;   // (S) the maximum number of shared variables (crossbars)
-    int               nGrowthLevel;  // (L) the maximum increase in the node level after resynthesis
-    int               fSatur;        // iterate till saturation
-    int               fZeroCost;     // accept zero-cost replacements
-    int               fVerbose;      // the verbosiness flag
-    int               fVeryVerbose;  // additional verbose info printout
-    // internal parameters
-    int               nLutSize;      // (K) the LUT size (determined by the input network)
-    int               nVarsMax;      // (V) the largest number of variables: V = N * (K-1) + 1
-};
-
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c
index 2bfad15b..f3297d8f 100644
--- a/src/base/abc/abcFunc.c
+++ b/src/base/abc/abcFunc.c
@@ -881,12 +881,20 @@ unsigned * Abc_ConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, V
     Hop_Obj_t * pObj;
     unsigned * pTruth, * pTruth2;
     int i, nWords, nNodes;
+    Vec_Ptr_t * vTtElems;
+
+    // if the number of variables is more than 8, allocate truth tables
+    if ( nVars > 8 )
+        vTtElems = Vec_PtrAllocTruthTables( nVars );
+    else
+        vTtElems = NULL;
+
     // clear the data fields and set marks
     nNodes = Abc_ConvertAigToTruth_rec1( pRoot );
     // prepare memory
     nWords = Hop_TruthWordNum( nVars );
     Vec_IntClear( vTruth );
-    Vec_IntGrow( vTruth, nWords * nNodes );
+    Vec_IntGrow( vTruth, nWords * (nNodes+1) );
     pTruth = Vec_IntFetch( vTruth, nWords );
     // check the case of a constant
     if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
@@ -900,21 +908,33 @@ unsigned * Abc_ConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, V
     }
     // set elementary truth tables at the leaves
     assert( nVars <= Hop_ManPiNum(p) );
-    assert( Hop_ManPiNum(p) <= 8 ); 
+//    assert( Hop_ManPiNum(p) <= 8 ); 
     if ( fMsbFirst )
     {
         Hop_ManForEachPi( p, pObj, i )
-            pObj->pData = (void *)uTruths[nVars-1-i];
+        {
+            if ( vTtElems )
+                pObj->pData = Vec_PtrEntry(vTtElems, nVars-1-i);
+            else               
+                pObj->pData = (void *)uTruths[nVars-1-i];
+        }
     }
     else
     {
         Hop_ManForEachPi( p, pObj, i )
-            pObj->pData = (void *)uTruths[i];
+        {
+            if ( vTtElems )
+                pObj->pData = Vec_PtrEntry(vTtElems, i);
+            else               
+                pObj->pData = (void *)uTruths[i];
+        }
     }
     // clear the marks and compute the truth table
     pTruth2 = Abc_ConvertAigToTruth_rec2( pRoot, vTruth, nWords );
     // copy the result
     Extra_TruthCopy( pTruth, pTruth2, nVars );
+    if ( vTtElems )
+        Vec_PtrFree( vTtElems );
     return pTruth;
 }
 
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index d5bdd444..53566b7d 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -26,7 +26,7 @@
 #include "fpga.h"
 #include "if.h"
 #include "res.h"
-//#include "dar.h"
+#include "lpk.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -1509,23 +1509,37 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
     int c;
-    int fUseLibrary;
+    int fCofactor;
+    int nCofLevel;
 
     extern void Kit_DsdTest( unsigned * pTruth, int nVars );
+    extern void Kit_DsdPrintCofactors( unsigned * pTruth, int nVars, int nCofLevel, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fUseLibrary = 1;
+    nCofLevel = 1;
+    fCofactor = 1;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "lh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Nch" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'l':
-            fUseLibrary ^= 1;
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nCofLevel = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nCofLevel < 0 ) 
+                goto usage;
+            break;
+        case 'c':
+            fCofactor ^= 1;
             break;
         case 'h':
             goto usage;
@@ -1549,16 +1563,16 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
     // convert it to truth table
     {
         Abc_Obj_t * pObj = Abc_ObjFanin0( Abc_NtkPo(pNtk, 0) );
-        Vec_Int_t * vMemory = Vec_IntAlloc( 10000 );
+        Vec_Int_t * vMemory = Vec_IntAlloc(0);
         unsigned * pTruth;
         if ( !Abc_ObjIsNode(pObj) )
         {
             fprintf( pErr, "The fanin of the first PO node does not have a logic function.\n" );
             return 1;
         }
-        if ( Abc_ObjFaninNum(pObj) > 8 )
+        if ( Abc_ObjFaninNum(pObj) > 16 )
         {
-            fprintf( pErr, "Currently works only for up to 8 inputs.\n" );
+            fprintf( pErr, "Currently works only for up to 16 inputs.\n" );
             return 1;
         }
         pTruth = Abc_ConvertAigToTruth( pNtk->pManFunc, Hop_Regular(pObj->pData), Abc_ObjFaninNum(pObj), vMemory, 0 );
@@ -1566,16 +1580,20 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
             Extra_TruthNot( pTruth, pTruth, Abc_ObjFaninNum(pObj) );
         Extra_PrintBinary( stdout, pTruth, 1 << Abc_ObjFaninNum(pObj) );
         printf( "\n" );
-        Kit_DsdTest( pTruth, Abc_ObjFaninNum(pObj) );
+        if ( fCofactor )
+            Kit_DsdPrintCofactors( pTruth, Abc_ObjFaninNum(pObj), nCofLevel, 1 );
+        else
+            Kit_DsdTest( pTruth, Abc_ObjFaninNum(pObj) );
         Vec_IntFree( vMemory );
     }
     return 0;
 
 usage:
-    fprintf( pErr, "usage: print_dsd [-h]\n" );
-    fprintf( pErr, "\t        print DSD formula for a single-output function with less than 16 variables\n" );
-//    fprintf( pErr, "\t-l    : used library gate names (if mapped) [default = %s]\n", fUseLibrary? "yes": "no" );
-    fprintf( pErr, "\t-h    : print the command usage\n");
+    fprintf( pErr, "usage: print_dsd [-ch] [-N num]\n" );
+    fprintf( pErr, "\t         print DSD formula for a single-output function with less than 16 variables\n" );
+    fprintf( pErr, "\t-c     : toggle recursive cofactoring [default = %s]\n", fCofactor? "yes": "no" );
+    fprintf( pErr, "\t-N num : the number of levels to cofactor [default = %d]\n", nCofLevel );
+    fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
 }
 
@@ -2906,26 +2924,22 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
-    Lut_Par_t Pars, * pPars = &Pars;
+    Lpk_Par_t Pars, * pPars = &Pars;
     int c;
-    extern int Abc_LutResynthesize( Abc_Ntk_t * pNtk, Lut_Par_t * pPars );
-
-//    printf( "Implementation of this command is not finished.\n" );
-//    return 1;
-
+ 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    memset( pPars, 0, sizeof(Lut_Par_t) );
+    memset( pPars, 0, sizeof(Lpk_Par_t) );
     pPars->nLutsMax     =  4; // (N) the maximum number of LUTs in the structure
     pPars->nLutsOver    =  3; // (Q) the maximum number of LUTs not in the MFFC
-    pPars->nVarsShared  =  3; // (S) the maximum number of shared variables (crossbars)
-    pPars->nGrowthLevel =  1;
+    pPars->nVarsShared  =  0; // (S) the maximum number of shared variables (crossbars)
+    pPars->nGrowthLevel =  9; // (L) the maximum number of increased levels
     pPars->fSatur       =  1;
     pPars->fZeroCost    =  0; 
-    pPars->fVerbose     =  0;
+    pPars->fVerbose     =  1;
     pPars->fVeryVerbose =  0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "NQSLszvwh" ) ) != EOF )
@@ -3007,7 +3021,7 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // modify the current network
-    if ( !Abc_LutResynthesize( pNtk, pPars ) )
+    if ( !Lpk_Resynthesize( pNtk, pPars ) )
     {
         fprintf( pErr, "Resynthesis has failed.\n" );
         return 1;
diff --git a/src/base/abci/abcDsdRes.c b/src/base/abci/abcDsdRes.c
deleted file mode 100644
index 3aa71a15..00000000
--- a/src/base/abci/abcDsdRes.c
+++ /dev/null
@@ -1,1774 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [abcDsdRes.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Network and node package.]
-
-  Synopsis    []
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: abcDsdRes.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "abc.h"
-#include "kit.h"
-#include "if.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-#define LUT_SIZE_MAX     16   // the largest size of the function
-#define LUT_CUTS_MAX   1024   // the largest number of cuts considered
-
-typedef struct Lut_Man_t_ Lut_Man_t;
-typedef struct Lut_Cut_t_ Lut_Cut_t;
-
-struct Lut_Cut_t_
-{
-    unsigned     nLeaves       : 6;     // (L) the number of leaves
-    unsigned     nNodes        : 6;     // (M) the number of nodes
-    unsigned     nNodesDup     : 6;     // (Q) nodes outside of MFFC
-    unsigned     nLuts         : 6;     // (N) the number of LUTs to try
-    unsigned     unused        : 6;     // unused
-    unsigned     fHasDsd       : 1;     // set to 1 if the cut has structural DSD (and so cannot be used)
-    unsigned     fMark         : 1;     // multipurpose mark
-    unsigned     uSign[2];              // the signature
-    float        Weight;                // the weight of the cut: (M - Q)/N(V)   (the larger the better)
-    int          Gain;                  // the gain achieved using this cut
-    int          pLeaves[LUT_SIZE_MAX]; // the leaves of the cut
-    int          pNodes[LUT_SIZE_MAX];  // the nodes of the cut
-};
-
-struct Lut_Man_t_
-{
-    // parameters
-    Lut_Par_t *  pPars;                 // the set of parameters
-    // current representation
-    Abc_Ntk_t *  pNtk;                  // the network
-    Abc_Obj_t *  pObj;                  // the node to resynthesize 
-    // cut representation
-    int          nMffc;                 // the size of MFFC of the node
-    int          nCuts;                 // the total number of cuts    
-    int          nCutsMax;              // the largest possible number of cuts
-    int          nEvals;                // the number of good cuts
-    Lut_Cut_t    pCuts[LUT_CUTS_MAX];   // the storage for cuts
-    int          pEvals[LUT_CUTS_MAX];  // the good cuts
-    // visited nodes 
-    Vec_Vec_t *  vVisited;
-    // mapping manager
-    If_Man_t *   pIfMan;
-    Vec_Int_t *  vCover; 
-    Vec_Vec_t *  vLevels;
-    // temporary variables
-    int          fCofactoring;          // working in the cofactoring mode
-    int          pRefs[LUT_SIZE_MAX];   // fanin reference counters 
-    int          pCands[LUT_SIZE_MAX];  // internal nodes pointing only to the leaves
-    // truth table representation
-    Vec_Ptr_t *  vTtElems;              // elementary truth tables
-    Vec_Ptr_t *  vTtNodes;              // storage for temporary truth tables of the nodes 
-    // statistics
-    int          nNodesTotal;           // total number of nodes
-    int          nNodesOver;            // nodes with cuts over the limit 
-    int          nCutsTotal;            // total number of cuts
-    int          nCutsUseful;           // useful cuts 
-    int          nGainTotal;            // the gain in LUTs
-    int          nChanges;              // the number of changed nodes
-    // counter of non-DSD blocks
-    int          nBlocks[17];
-    // rutime
-    int          timeCuts;
-    int          timeTruth;
-    int          timeEval;
-    int          timeMap;
-    int          timeOther;
-    int          timeTotal;
-};
-
-#define Abc_LutCutForEachLeaf( pNtk, pCut, pObj, i )                                        \
-    for ( i = 0; (i < (int)(pCut)->nLeaves) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pLeaves[i])), 1); i++ )
-#define Abc_LutCutForEachNode( pNtk, pCut, pObj, i )                                        \
-    for ( i = 0; (i < (int)(pCut)->nNodes) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pNodes[i])), 1); i++ )
-#define Abc_LutCutForEachNodeReverse( pNtk, pCut, pObj, i )                                 \
-    for ( i = (int)(pCut)->nNodes - 1; (i >= 0) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pNodes[i])), 1); i-- )
-
-static inline If_Obj_t *  If_Regular( If_Obj_t * p )        { return (If_Obj_t *)((unsigned long)(p) & ~01);  }
-static inline If_Obj_t *  If_Not( If_Obj_t * p )            { return (If_Obj_t *)((unsigned long)(p) ^  01);  }
-static inline If_Obj_t *  If_NotCond( If_Obj_t * p, int c ) { return (If_Obj_t *)((unsigned long)(p) ^ (c));  }
-static inline int         If_IsComplement( If_Obj_t * p )   { return (int )(((unsigned long)p) & 01);         }
-
-extern void Res_UpdateNetworkLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels );
-
-static If_Obj_t * Abc_LutIfManMapMulti( Lut_Man_t * p, unsigned * pTruth, int nLeaves, If_Obj_t ** ppLeaves );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Lut_Man_t * Abc_LutManStart( Lut_Par_t * pPars )
-{
-    Lut_Man_t * p;
-    assert( pPars->nLutsMax <= 16 );
-    assert( pPars->nVarsMax > 0 );
-    p = ALLOC( Lut_Man_t, 1 );
-    memset( p, 0, sizeof(Lut_Man_t) );
-    p->pPars = pPars;
-    p->nCutsMax = LUT_CUTS_MAX;
-    p->vTtElems = Vec_PtrAllocTruthTables( pPars->nVarsMax );
-    p->vTtNodes = Vec_PtrAllocSimInfo( 256, Abc_TruthWordNum(pPars->nVarsMax) );
-    p->vCover = Vec_IntAlloc( 1 << 12 );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_LutManStop( Lut_Man_t * p )
-{
-    if ( p->pIfMan )
-    {
-        void * pPars = p->pIfMan->pPars;
-        If_ManStop( p->pIfMan );
-        free( pPars );
-    }
-    if ( p->vLevels )
-        Vec_VecFree( p->vLevels );
-    if ( p->vVisited )
-        Vec_VecFree( p->vVisited );
-    Vec_IntFree( p->vCover );
-    Vec_PtrFree( p->vTtElems );
-    Vec_PtrFree( p->vTtNodes );
-    free( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if at least one entry has changed.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_LutNodeHasChanged( Lut_Man_t * p, int iNode )
-{
-    Vec_Ptr_t * vNodes;
-    Abc_Obj_t * pTemp;
-    int i;
-    vNodes = Vec_VecEntry( p->vVisited, iNode );
-    if ( Vec_PtrSize(vNodes) == 0 )
-        return 1;
-    Vec_PtrForEachEntry( vNodes, pTemp, i )
-    {
-        // check if the node has changed
-        pTemp = Abc_NtkObj( p->pNtk, (int)pTemp );
-        if ( pTemp == NULL )
-            return 1;
-        // check if the number of fanouts has changed
-//        if ( Abc_ObjFanoutNum(pTemp) != (int)Vec_PtrEntry(vNodes, i+1) )
-//            return 1;
-        i++;
-    }
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if at least one entry has changed.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_LutNodeRecordImpact( Lut_Man_t * p )
-{
-    Lut_Cut_t * pCut;
-    Vec_Ptr_t * vNodes = Vec_VecEntry( p->vVisited, p->pObj->Id );
-    Abc_Obj_t * pNode;
-    int i, k;
-    // collect the nodes that impact the given node
-    Vec_PtrClear( vNodes );
-    for ( i = 0; i < p->nCuts; i++ )
-    {
-        pCut = p->pCuts + i;
-        for ( k = 0; k < (int)pCut->nLeaves; k++ )
-        {
-            pNode = Abc_NtkObj( p->pNtk, pCut->pLeaves[k] );
-            if ( pNode->fMarkC )
-                continue;
-            pNode->fMarkC = 1;
-            Vec_PtrPush( vNodes, (void *)pNode->Id );
-            Vec_PtrPush( vNodes, (void *)Abc_ObjFanoutNum(pNode) );
-        }
-    }
-    // clear the marks
-    Vec_PtrForEachEntry( vNodes, pNode, i )
-    {
-        pNode = Abc_NtkObj( p->pNtk, (int)pNode );
-        pNode->fMarkC = 0;
-        i++;
-    }
-//printf( "%d ", Vec_PtrSize(vNodes) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if the cut has structural DSD.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_LutNodeCutsCheckDsd( Lut_Man_t * p, Lut_Cut_t * pCut )
-{
-    Abc_Obj_t * pObj, * pFanin;
-    int i, k, nCands, fLeavesOnly, RetValue;
-    assert( pCut->nLeaves > 0 );
-    // clear ref counters
-    memset( p->pRefs, 0, sizeof(int) * pCut->nLeaves );
-    // mark cut leaves
-    Abc_LutCutForEachLeaf( p->pNtk, pCut, pObj, i )
-    {
-        assert( pObj->fMarkA == 0 );
-        pObj->fMarkA = 1;
-        pObj->pCopy = (void *)i;
-    }
-    // ref leaves pointed from the internal nodes
-    nCands = 0;
-    Abc_LutCutForEachNode( p->pNtk, pCut, pObj, i )
-    {
-        fLeavesOnly = 1;
-        Abc_ObjForEachFanin( pObj, pFanin, k )
-            if ( pFanin->fMarkA )
-                p->pRefs[(int)pFanin->pCopy]++;
-            else
-                fLeavesOnly = 0;
-        if ( fLeavesOnly )
-            p->pCands[nCands++] = pObj->Id;
-    }
-    // look at the nodes that only point to the leaves
-    RetValue = 0;
-    for ( i = 0; i < nCands; i++ )
-    {
-        pObj = Abc_NtkObj( p->pNtk, p->pCands[i] );
-        Abc_ObjForEachFanin( pObj, pFanin, k )
-        {
-            assert( pFanin->fMarkA == 1 );
-            if ( p->pRefs[(int)pFanin->pCopy] > 1 )
-                break;
-        }
-        if ( k == Abc_ObjFaninNum(pObj) )
-        {
-            RetValue = 1;
-            break;
-        }
-    }
-    // unmark cut leaves
-    Abc_LutCutForEachLeaf( p->pNtk, pCut, pObj, i )
-        pObj->fMarkA = 0;
-    return RetValue;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if pDom is contained in pCut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Abc_LutNodeCutsOneDominance( Lut_Cut_t * pDom, Lut_Cut_t * pCut )
-{
-    int i, k;
-    for ( i = 0; i < (int)pDom->nLeaves; i++ )
-    {
-        for ( k = 0; k < (int)pCut->nLeaves; k++ )
-            if ( pDom->pLeaves[i] == pCut->pLeaves[k] )
-                break;
-        if ( k == (int)pCut->nLeaves ) // node i in pDom is not contained in pCut
-            return 0;
-    }
-    // every node in pDom is contained in pCut
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Check if the cut exists.]
-
-  Description [Returns 1 if the cut exists.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_LutNodeCutsOneFilter( Lut_Cut_t * pCuts, int nCuts, Lut_Cut_t * pCutNew )
-{
-    Lut_Cut_t * pCut;
-    int i, k;
-    assert( pCutNew->uSign[0] || pCutNew->uSign[1] );
-    // try to find the cut
-    for ( i = 0; i < nCuts; i++ )
-    {
-        pCut = pCuts + i;
-        if ( pCut->nLeaves == 0 )
-            continue;
-        if ( pCut->nLeaves == pCutNew->nLeaves )
-        {
-            if ( pCut->uSign[0] == pCutNew->uSign[0] && pCut->uSign[1] == pCutNew->uSign[1] )
-            {
-                for ( k = 0; k < (int)pCutNew->nLeaves; k++ )
-                    if ( pCut->pLeaves[k] != pCutNew->pLeaves[k] )
-                        break;
-                if ( k == (int)pCutNew->nLeaves )
-                    return 1;
-            }
-            continue;
-        }
-        if ( pCut->nLeaves < pCutNew->nLeaves )
-        {
-            // skip the non-contained cuts
-            if ( (pCut->uSign[0] & pCutNew->uSign[0]) != pCut->uSign[0] )
-                continue;
-            if ( (pCut->uSign[1] & pCutNew->uSign[1]) != pCut->uSign[1] )
-                continue;
-            // check containment seriously
-            if ( Abc_LutNodeCutsOneDominance( pCut, pCutNew ) )
-                return 1;
-            continue;
-        }
-        // check potential containment of other cut
-
-        // skip the non-contained cuts
-        if ( (pCut->uSign[0] & pCutNew->uSign[0]) != pCutNew->uSign[0] )
-            continue;
-        if ( (pCut->uSign[1] & pCutNew->uSign[1]) != pCutNew->uSign[1] )
-            continue;
-        // check containment seriously
-        if ( Abc_LutNodeCutsOneDominance( pCutNew, pCut ) )
-            pCut->nLeaves = 0; // removed
-    }
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints the given cut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_LutNodePrintCut( Lut_Man_t * p, Lut_Cut_t * pCut )
-{
-    Abc_Obj_t * pObj;
-    int i;
-    printf( "LEAVES:\n" );
-    Abc_LutCutForEachLeaf( p->pNtk, pCut, pObj, i )
-    {
-        Abc_ObjPrint( stdout, pObj );
-    }
-    printf( "NODES:\n" );
-    Abc_LutCutForEachNode( p->pNtk, pCut, pObj, i )
-    {
-        Abc_ObjPrint( stdout, pObj );
-        assert( Abc_ObjIsNode(pObj) );
-    }
-    printf( "\n" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Set the cut signature.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_LutNodeCutSignature( Lut_Cut_t * pCut )
-{
-    unsigned i;
-    pCut->uSign[0] = pCut->uSign[1] = 0;
-    for ( i = 0; i < pCut->nLeaves; i++ )
-    {
-        pCut->uSign[(pCut->pLeaves[i] & 32) > 0] |= (1 << (pCut->pLeaves[i] & 31));
-        if ( i != pCut->nLeaves - 1 )
-            assert( pCut->pLeaves[i] < pCut->pLeaves[i+1] );
-    }
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the set of all cuts.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_LutNodeCutsOne( Lut_Man_t * p, Lut_Cut_t * pCut, int Node )
-{
-    Lut_Cut_t * pCutNew;
-    Abc_Obj_t * pObj, * pFanin;
-    int i, k, j, nLeavesNew;
-
-    // check if the cut can stand adding one more internal node
-    if ( pCut->nNodes == LUT_SIZE_MAX )
-        return;
-
-    // if the node is a PI, quit
-    pObj = Abc_NtkObj( p->pNtk, Node );
-    if ( Abc_ObjIsCi(pObj) )
-        return;
-    assert( Abc_ObjIsNode(pObj) );
-    assert( Abc_ObjFaninNum(pObj) <= p->pPars->nLutSize );
-
-    // if the node is not in the MFFC, check the limit
-    if ( !Abc_NodeIsTravIdCurrent(pObj) )
-    {
-        if ( (int)pCut->nNodesDup == p->pPars->nLutsOver )
-            return;
-        assert( (int)pCut->nNodesDup < p->pPars->nLutsOver );
-    }
-
-    // check the possibility of adding this node using the signature
-    nLeavesNew = pCut->nLeaves - 1;
-    Abc_ObjForEachFanin( pObj, pFanin, i )
-    {
-        if ( (pCut->uSign[(pFanin->Id & 32) > 0] & (1 << (pFanin->Id & 31))) )
-            continue;
-        if ( ++nLeavesNew > p->pPars->nVarsMax )
-            return;
-    }
-
-    // initialize the set of leaves to the nodes in the cut
-    assert( p->nCuts < LUT_CUTS_MAX );
-    pCutNew = p->pCuts + p->nCuts;
-/*
-if ( p->pObj->Id == 31 && Node == 38 && pCut->pNodes[0] == 31 && pCut->pNodes[1] == 34 && pCut->pNodes[2] == 35 )//p->nCuts == 48 )
-{
-    int x = 0;
-    printf( "Start:\n" );
-    Abc_LutNodePrintCut( p, pCut );
-}
-*/
-    pCutNew->nLeaves = 0;
-    for ( i = 0; i < (int)pCut->nLeaves; i++ )
-        if ( pCut->pLeaves[i] != Node )
-            pCutNew->pLeaves[pCutNew->nLeaves++] = pCut->pLeaves[i];
-
-    // add new nodes
-    Abc_ObjForEachFanin( pObj, pFanin, i )
-    {
-        // find the place where this node belongs
-        for ( k = 0; k < (int)pCutNew->nLeaves; k++ )
-            if ( pCutNew->pLeaves[k] >= pFanin->Id )
-                break;
-        if ( k < (int)pCutNew->nLeaves && pCutNew->pLeaves[k] == pFanin->Id )
-            continue;
-        // check if there is room
-        if ( (int)pCutNew->nLeaves == p->pPars->nVarsMax )
-            return;
-        // move all the nodes
-        for ( j = pCutNew->nLeaves; j > k; j-- )
-            pCutNew->pLeaves[j] = pCutNew->pLeaves[j-1];
-        pCutNew->pLeaves[k] = pFanin->Id;
-        pCutNew->nLeaves++;
-        assert( pCutNew->nLeaves <= LUT_SIZE_MAX );
-    }
-    
-    // skip the contained cuts
-    Abc_LutNodeCutSignature( pCutNew );
-    if ( Abc_LutNodeCutsOneFilter( p->pCuts, p->nCuts, pCutNew ) )
-        return;
-
-    // update the set of internal nodes
-    assert( pCut->nNodes < LUT_SIZE_MAX );
-    memcpy( pCutNew->pNodes, pCut->pNodes, pCut->nNodes * sizeof(int) );
-    pCutNew->nNodes = pCut->nNodes;
-    pCutNew->pNodes[ pCutNew->nNodes++ ] = Node;
-
-    // add the marked node
-    pCutNew->nNodesDup = pCut->nNodesDup + !Abc_NodeIsTravIdCurrent(pObj);
-/*
-if ( p->pObj->Id == 31 && Node == 38 )//p->nCuts == 48 )
-{
-    int x = 0;
-    printf( "Finish:\n" );
-    Abc_LutNodePrintCut( p, pCutNew );
-}
-*/
-    // add the cut to storage
-    assert( p->nCuts < LUT_CUTS_MAX );
-    p->nCuts++;
-
-    assert( pCut->nNodes <= p->nMffc + pCutNew->nNodesDup );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the set of all cuts.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_LutNodeCuts( Lut_Man_t * p )
-{
-    Lut_Cut_t * pCut, * pCut2;
-    int i, k, Temp, nMffc, fChanges;
-
-    // mark the MFFC of the node with the current trav ID
-    nMffc = p->nMffc = Abc_NodeMffcLabel( p->pObj );
-    assert( nMffc > 0 );
-    if ( nMffc == 1 )
-        return 0;
-
-    // initialize the first cut
-    pCut = p->pCuts; p->nCuts = 1;
-    pCut->nNodes = 0; 
-    pCut->nNodesDup = 0;
-    pCut->nLeaves = 1;
-    pCut->pLeaves[0] = p->pObj->Id;
-    // assign the signature
-    Abc_LutNodeCutSignature( pCut );
-
-    // perform the cut computation
-    for ( i = 0; i < p->nCuts; i++ )
-    {
-        pCut = p->pCuts + i;
-        if ( pCut->nLeaves == 0 )
-            continue;
-        // try to expand the fanins of this cut
-        for ( k = 0; k < (int)pCut->nLeaves; k++ )
-        {
-            // create a new cut
-            Abc_LutNodeCutsOne( p, pCut, pCut->pLeaves[k] );
-            // quit if the number of cuts has exceeded the limit
-            if ( p->nCuts == LUT_CUTS_MAX )
-                break;
-        }
-        if ( p->nCuts == LUT_CUTS_MAX )
-            break;
-    }
-    if ( p->nCuts == LUT_CUTS_MAX ) 
-        p->nNodesOver++;
-
-    // record the impact of this node
-    if ( p->pPars->fSatur )
-        Abc_LutNodeRecordImpact( p );
-
-    // compress the cuts by removing empty ones, those with negative Weight, and decomposable ones
-    p->nEvals = 0;
-    for ( i = 0; i < p->nCuts; i++ )
-    {
-        pCut = p->pCuts + i;
-        if ( pCut->nLeaves < 2 )
-            continue;
-        // compute the number of LUTs neede to implement this cut
-        // V = N * (K-1) + 1  ~~~~~  N = Ceiling[(V-1)/(K-1)] = (V-1)/(K-1) + [(V-1)%(K-1) > 0]
-        pCut->nLuts = (pCut->nLeaves-1)/(p->pPars->nLutSize-1) + ( (pCut->nLeaves-1)%(p->pPars->nLutSize-1) > 0 ); 
-        pCut->Weight = (float)1.0 * (pCut->nNodes - pCut->nNodesDup) / pCut->nLuts; //p->pPars->nLutsMax;
-        if ( pCut->Weight <= 1.0 )
-            continue;
-        pCut->fHasDsd = Abc_LutNodeCutsCheckDsd( p, pCut );
-        if ( pCut->fHasDsd )
-            continue;
-        p->pEvals[p->nEvals++] = i;
-    }
-    if ( p->nEvals == 0 )
-        return 0;
-
-    // sort the cuts by Weight
-    do {
-        fChanges = 0;
-        for ( i = 0; i < p->nEvals - 1; i++ )
-        {
-            pCut = p->pCuts + p->pEvals[i];
-            pCut2 = p->pCuts + p->pEvals[i+1];
-            if ( pCut->Weight >= pCut2->Weight )
-                continue;
-            Temp = p->pEvals[i];
-            p->pEvals[i] = p->pEvals[i+1];
-            p->pEvals[i+1] = Temp;
-            fChanges = 1;
-        }
-    } while ( fChanges );
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the truth able of one cut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-unsigned * Abc_LutCutTruth_rec( Hop_Man_t * pMan, Hop_Obj_t * pObj, int nVars, Vec_Ptr_t * vTtNodes, int * iCount )
-{
-    unsigned * pTruth, * pTruth0, * pTruth1;
-    assert( !Hop_IsComplement(pObj) );
-    if ( pObj->pData )
-    {
-        assert( ((unsigned)pObj->pData) & 0xffff0000 );
-        return pObj->pData;
-    }
-    // get the plan for a new truth table
-    pTruth = Vec_PtrEntry( vTtNodes, (*iCount)++ );
-    if ( Hop_ObjIsConst1(pObj) )
-        Extra_TruthFill( pTruth, nVars );
-    else
-    {
-        assert( Hop_ObjIsAnd(pObj) );
-        // compute the truth tables of the fanins
-        pTruth0 = Abc_LutCutTruth_rec( pMan, Hop_ObjFanin0(pObj), nVars, vTtNodes, iCount );
-        pTruth1 = Abc_LutCutTruth_rec( pMan, Hop_ObjFanin1(pObj), nVars, vTtNodes, iCount );
-        // creat the truth table of the node
-        Extra_TruthAndPhase( pTruth, pTruth0, pTruth1, nVars, Hop_ObjFaninC0(pObj), Hop_ObjFaninC1(pObj) );
-    }
-    pObj->pData = pTruth;
-    return pTruth;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the truth able of one cut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-unsigned * Abc_LutCutTruth( Lut_Man_t * p, Lut_Cut_t * pCut )
-{
-    Hop_Man_t * pManHop = p->pNtk->pManFunc;
-    Hop_Obj_t * pObjHop;
-    Abc_Obj_t * pObj, * pFanin;
-    unsigned * pTruth;
-    int i, k, iCount = 0;
-//    Abc_LutNodePrintCut( p, pCut );
-
-    // initialize the leaves
-    Abc_LutCutForEachLeaf( p->pNtk, pCut, pObj, i )
-        pObj->pCopy = Vec_PtrEntry( p->vTtElems, i );
-
-    // construct truth table in the topological order
-    Abc_LutCutForEachNodeReverse( p->pNtk, pCut, pObj, i )
-    {
-        // get the local AIG
-        pObjHop = Hop_Regular(pObj->pData);
-        // clean the data field of the nodes in the AIG subgraph
-        Hop_ObjCleanData_rec( pObjHop );
-        // set the initial truth tables at the fanins
-        Abc_ObjForEachFanin( pObj, pFanin, k )
-        {
-            assert( ((unsigned)pFanin->pCopy) & 0xffff0000 );
-            Hop_ManPi( pManHop, k )->pData = pFanin->pCopy;
-        }
-        // compute the truth table of internal nodes
-        pTruth = Abc_LutCutTruth_rec( pManHop, pObjHop, pCut->nLeaves, p->vTtNodes, &iCount );
-        if ( Hop_IsComplement(pObj->pData) )
-            Extra_TruthNot( pTruth, pTruth, pCut->nLeaves );
-        // set the truth table at the node
-        pObj->pCopy = (Abc_Obj_t *)pTruth;
-    }
-
-    return pTruth;
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Prepares the mapping manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_LutIfManStart( Lut_Man_t * p )
-{
-    If_Par_t * pPars;
-    assert( p->pIfMan == NULL );
-    // set defaults
-    pPars = ALLOC( If_Par_t, 1 );
-    memset( pPars, 0, sizeof(If_Par_t) );
-    // user-controlable paramters
-    pPars->nLutSize    =  p->pPars->nLutSize;
-    pPars->nCutsMax    =  8;
-    pPars->nFlowIters  =  0; // 1
-    pPars->nAreaIters  =  0; // 1 
-    pPars->DelayTarget = -1;
-    pPars->fPreprocess =  0;
-    pPars->fArea       =  1;
-    pPars->fFancy      =  0;
-    pPars->fExpRed     =  0; //
-    pPars->fLatchPaths =  0;
-    pPars->fSeqMap     =  0;
-    pPars->fVerbose    =  0;
-    // internal parameters
-    pPars->fTruth      =  0;
-    pPars->fUsePerm    =  0; 
-    pPars->nLatches    =  0;
-    pPars->pLutLib     =  NULL; // Abc_FrameReadLibLut();
-    pPars->pTimesArr   =  NULL; 
-    pPars->pTimesArr   =  NULL;   
-    pPars->fUseBdds    =  0;
-    pPars->fUseSops    =  0;
-    pPars->fUseCnfs    =  0;
-    pPars->fUseMv      =  0;
-    // start the mapping manager and set its parameters
-    p->pIfMan = If_ManStart( pPars );
-    If_ManSetupSetAll( p->pIfMan, 1000 );
-    p->pIfMan->pPars->pTimesArr = ALLOC( float, 32 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Transforms the decomposition graph into the AIG.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-If_Obj_t * Abc_LutIfManMapPrimeInternal( If_Man_t * pIfMan, Kit_Graph_t * pGraph )
-{
-    Kit_Node_t * pNode;
-    If_Obj_t * pAnd0, * pAnd1;
-    int i;
-    // check for constant function
-    if ( Kit_GraphIsConst(pGraph) )
-        return If_ManConst1(pIfMan);
-    // check for a literal
-    if ( Kit_GraphIsVar(pGraph) )
-        return Kit_GraphVar(pGraph)->pFunc;
-    // build the AIG nodes corresponding to the AND gates of the graph
-    Kit_GraphForEachNode( pGraph, pNode, i )
-    {
-        pAnd0 = Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc; 
-        pAnd1 = Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc; 
-        pNode->pFunc = If_ManCreateAnd( pIfMan, 
-            If_Regular(pAnd0), If_IsComplement(pAnd0) ^ pNode->eEdge0.fCompl, 
-            If_Regular(pAnd1), If_IsComplement(pAnd1) ^ pNode->eEdge1.fCompl );
-    }
-    return pNode->pFunc;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Strashes one logic node using its SOP.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-If_Obj_t * Abc_LutIfManMapPrime( If_Man_t * pIfMan, If_Obj_t ** ppLeaves, Kit_Graph_t * pGraph )
-{
-    Kit_Node_t * pNode;
-    If_Obj_t * pRes;
-    int i;
-    // collect the fanins
-    Kit_GraphForEachLeaf( pGraph, pNode, i )
-        pNode->pFunc = ppLeaves[i];
-    // perform strashing
-    pRes = Abc_LutIfManMapPrimeInternal( pIfMan, pGraph );
-    return If_NotCond( pRes, Kit_GraphIsComplement(pGraph) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates the choice node for the given number.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-If_Obj_t * Abc_LutIfManChoiceOne( If_Man_t * pIfMan, If_Obj_t ** pNodes, int iNode, int nLeaves, int fXor )
-{
-    If_Obj_t * pPrev, * pAnd, * pOne, * pMany;
-    int v;
-    pPrev = NULL;
-    for ( v = 0; v < nLeaves; v++ )
-    {
-        if ( (iNode & (1 << v)) == 0 )
-            continue;
-        pOne  = pNodes[1 << v];
-        pMany = pNodes[iNode & ~(1 << v)];
-        if ( fXor )
-            pAnd = If_ManCreateXnor( pIfMan, If_Regular(pOne), pMany ); 
-        else
-            pAnd = If_ManCreateAnd( pIfMan, If_Regular(pOne), If_IsComplement(pOne), If_Regular(pMany), If_IsComplement(pMany) ); 
-        pAnd->pEquiv = pPrev;
-        pPrev = pAnd;
-    }
-    return pPrev;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates the choice node for the given number.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-If_Obj_t * Abc_LutIfManChoice( If_Man_t * pIfMan, If_Obj_t ** pLeaves, int nLeaves, int fXor )
-{
-    If_Obj_t ** pNodes, * pRes;
-    int v, m, nMints;
-    // allocate room for nodes
-    assert( nLeaves >= 2 );
-    nMints = (1 << nLeaves);
-    pNodes = ALLOC( If_Obj_t *, nMints );
-    // set elementary ones
-    pNodes[0] = NULL;
-    for ( v = 0; v < nLeaves; v++ )
-        pNodes[1<<v] = pLeaves[v];
-    // set triples and so on
-    for ( v = 2; v <= nLeaves; v++ )
-        for ( m = 0; m < nMints; m++ )
-            if ( Kit_WordCountOnes(m) == v )
-            {
-                pNodes[m] = Abc_LutIfManChoiceOne( pIfMan, pNodes, m, nLeaves, fXor );
-                if ( v > 2 )
-                    If_ManCreateChoice( pIfMan, pNodes[m] );
-            }
-    pRes = pNodes[nMints-1];
-    free( pNodes );
-    return pRes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates the choice node for the given number.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-If_Obj_t * Abc_LutIfManPart_rec( If_Man_t * pIfMan, If_Obj_t ** pLeaves, int nLeaves, int fXor )
-{
-    If_Obj_t * pObjNew1, * pObjNew2;
-    if ( nLeaves <= 5 )
-        return Abc_LutIfManChoice( pIfMan, pLeaves, nLeaves, fXor );
-    pObjNew1 = Abc_LutIfManPart_rec( pIfMan, pLeaves,               nLeaves / 2,             fXor );
-    pObjNew2 = Abc_LutIfManPart_rec( pIfMan, pLeaves + nLeaves / 2, nLeaves - (nLeaves / 2), fXor );
-    if ( fXor )
-        return If_ManCreateXnor( pIfMan, pObjNew1, pObjNew2 ); 
-    else
-        return If_ManCreateAnd( pIfMan, pObjNew1, 0, pObjNew2, 0 ); 
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prepares the mapping manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-If_Obj_t * Abc_LutIfManMap_New_rec( Lut_Man_t * p, Kit_DsdNtk_t * pNtk, int iLit )
-{
-    Kit_Graph_t * pGraph;
-    Kit_DsdObj_t * pObj;
-    If_Obj_t * pObjNew, * pFansNew[16];
-    unsigned i, iLitFanin, fCompl;
-
-    // remember the complement
-    fCompl = Kit_DsdLitIsCompl(iLit); 
-    iLit = Kit_DsdLitRegular(iLit); 
-    assert( !Kit_DsdLitIsCompl(iLit) );
-
-    // consider the case of simple gate
-    pObj = Kit_DsdNtkObj( pNtk, Kit_DsdLit2Var(iLit) );
-    if ( pObj == NULL )
-    {
-        pObjNew = If_ManCi( p->pIfMan, Kit_DsdLit2Var(iLit) );
-        return If_NotCond( pObjNew, fCompl );
-    }
-
-    // solve for the inputs
-    Kit_DsdObjForEachFanin( pNtk, pObj, iLitFanin, i )
-        pFansNew[i] = Abc_LutIfManMap_New_rec( p, pNtk, iLitFanin );
-
-    // generate choices for multi-input gate
-    if ( pObj->Type == KIT_DSD_AND || pObj->Type == KIT_DSD_XOR )
-    {
-        assert( pObj->nFans >= 2 );
-        if ( pObj->Type == KIT_DSD_XOR )
-        {
-            fCompl ^= ((pObj->nFans-1) & 1); // flip if the number of operations is odd
-            for ( i = 0; i < pObj->nFans; i++ )
-            {
-                fCompl ^= If_IsComplement(pFansNew[i]);
-                pFansNew[i] = If_Regular(pFansNew[i]);
-            }
-        }
-        pObjNew = Abc_LutIfManPart_rec( p->pIfMan, pFansNew, pObj->nFans, pObj->Type == KIT_DSD_XOR );
-        return If_NotCond( pObjNew, fCompl );
-    }
-    assert( pObj->Type == KIT_DSD_PRIME );
-
-    // derive the factored form
-    pGraph = Kit_TruthToGraph( Kit_DsdObjTruth(pObj), pObj->nFans, p->vCover );
-    // convert factored form into the AIG
-    pObjNew = Abc_LutIfManMapPrime( p->pIfMan, pFansNew, pGraph ); 
-    Kit_GraphFree( pGraph );
-    return If_NotCond( pObjNew, fCompl );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Find the best cofactoring variable.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_LutFindBestCofactoring( Lut_Man_t * p, Kit_DsdNtk_t * pNtk, unsigned * pTruth, int nVars )
-{
-    Kit_DsdNtk_t * pNtk0, * pNtk1;//, * pTemp;
-    unsigned * pCofs2[3] = { pNtk->pMem, pNtk->pMem + Kit_TruthWordNum(pNtk->nVars), pNtk->pMem + 2 * Kit_TruthWordNum(pNtk->nVars) };
-    int i, MaxBlock0, MaxBlock1, MaxBlockBest = 1000, VarBest = -1;
-    int fVerbose = 1;
-
-    if ( fVerbose )
-    {
-//        printf( "Function: " );
-//        Extra_PrintBinary( stdout, pTruth, (1 << nVars) ); 
-//        Extra_PrintHexadecimal( stdout, pTruth, nVars ); 
-        printf( "\n" );
-        printf( "\n" );
-        printf( "V =%2d: ", pNtk->nVars );
-        Kit_DsdPrint( stdout, pNtk );
-    }
-    for ( i = 0; i < nVars; i++ )
-    {
-        Kit_TruthCofactor0New( pCofs2[0], pTruth, nVars, i );
-        Kit_TruthCofactor1New( pCofs2[1], pTruth, nVars, i );
-        Kit_TruthXor( pCofs2[2], pCofs2[0], pCofs2[1], nVars ); 
-
-        pNtk0 = Kit_DsdDecompose( pCofs2[0], nVars );
-        MaxBlock0 = Kit_DsdNonDsdSizeMax( pNtk0 );
-//        pNtk0 = Kit_DsdExpand( pTemp = pNtk0 );
-//        Kit_DsdNtkFree( pTemp );
-        if ( fVerbose )
-        {
-            printf( "Variable %2d: Diff = %6d.\n", i, Kit_TruthCountOnes(pCofs2[2], nVars) );
-
-            printf( "Cof%d0: ", i );
-            Kit_DsdPrint( stdout, pNtk0 );
-        }
-
-        pNtk1 = Kit_DsdDecompose( pCofs2[1], nVars );
-        MaxBlock1 = Kit_DsdNonDsdSizeMax( pNtk1 );
-//        pNtk1 = Kit_DsdExpand( pTemp = pNtk1 );
-//        Kit_DsdNtkFree( pTemp );
-        if ( fVerbose )
-        {
-            printf( "Cof%d1: ", i );
-            Kit_DsdPrint( stdout, pNtk1 );
-        }
-
-        if ( fVerbose )
-        {
-            printf( "MaxBlock0 = %2d. MaxBlock1 = %2d. ", MaxBlock0, MaxBlock1 );
-            if ( MaxBlock0 < p->pPars->nLutSize && MaxBlock1 < p->pPars->nLutSize )
-                printf( "  feasible\n" );
-            else
-                printf( "infeasible\n" );
-        }
-
-        if ( MaxBlock0 < p->pPars->nLutSize && MaxBlock1 < p->pPars->nLutSize )
-        {
-            if ( MaxBlockBest > ABC_MAX(MaxBlock0, MaxBlock1) )
-            {
-                MaxBlockBest = ABC_MAX(MaxBlock0, MaxBlock1);
-                VarBest = i;
-            }
-        }
-
-        Kit_DsdNtkFree( pNtk0 );
-        Kit_DsdNtkFree( pNtk1 );
-    }
-    if ( fVerbose )
-    {
-        printf( "Best variable = %d.\n", VarBest ); 
-        printf( "\n" );
-    }
-    return VarBest;
-   
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prepares the mapping manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-If_Obj_t * Abc_LutIfManMap_rec( Lut_Man_t * p, Kit_DsdNtk_t * pNtk, int iLit, If_Obj_t * pResult )
-{
-    Kit_Graph_t * pGraph;
-    Kit_DsdObj_t * pObj;
-    If_Obj_t * pObjNew, * pFansNew[16];
-    unsigned i, iLitFanin, fCompl;
-
-    // remember the complement
-    fCompl = Kit_DsdLitIsCompl(iLit); 
-    iLit = Kit_DsdLitRegular(iLit); 
-    assert( !Kit_DsdLitIsCompl(iLit) );
-
-    // consider the case of simple gate
-    pObj = Kit_DsdNtkObj( pNtk, Kit_DsdLit2Var(iLit) );
-    if ( pObj == NULL )
-    {
-        pObjNew = If_ManCi( p->pIfMan, Kit_DsdLit2Var(iLit) );
-        return If_NotCond( pObjNew, fCompl );
-    }
-    if ( pObj->Type == KIT_DSD_AND )
-    {
-        assert( pObj->nFans == 2 );
-        pFansNew[0] = pResult? pResult : Abc_LutIfManMap_rec( p, pNtk, pObj->pFans[0], NULL );
-        pFansNew[1] = Abc_LutIfManMap_rec( p, pNtk, pObj->pFans[1], NULL );
-        if ( pFansNew[0] == NULL || pFansNew[1] == NULL )
-            return NULL;
-        pObjNew = If_ManCreateAnd( p->pIfMan, If_Regular(pFansNew[0]), If_IsComplement(pFansNew[0]), If_Regular(pFansNew[1]), If_IsComplement(pFansNew[1]) ); 
-        return If_NotCond( pObjNew, fCompl );
-    }
-    if ( pObj->Type == KIT_DSD_XOR )
-    {
-        assert( pObj->nFans == 2 );
-        pFansNew[0] = pResult? pResult : Abc_LutIfManMap_rec( p, pNtk, pObj->pFans[0], NULL );
-        pFansNew[1] = Abc_LutIfManMap_rec( p, pNtk, pObj->pFans[1], NULL );
-        if ( pFansNew[0] == NULL || pFansNew[1] == NULL )
-            return NULL;
-        fCompl ^= 1 ^ If_IsComplement(pFansNew[0]) ^ If_IsComplement(pFansNew[1]);
-        pObjNew = If_ManCreateXnor( p->pIfMan, If_Regular(pFansNew[0]), If_Regular(pFansNew[1]) );
-        return If_NotCond( pObjNew, fCompl );
-    }
-    assert( pObj->Type == KIT_DSD_PRIME );
-    p->nBlocks[pObj->nFans]++;
-
-    // solve for the inputs
-    Kit_DsdObjForEachFanin( pNtk, pObj, iLitFanin, i )
-    {
-        if ( i == 0 )
-            pFansNew[i] = pResult? pResult : Abc_LutIfManMap_rec( p, pNtk, iLitFanin, NULL );
-        else
-            pFansNew[i] = Abc_LutIfManMap_rec( p, pNtk, iLitFanin, NULL );
-        if ( pFansNew[i] == NULL )
-            return NULL;
-    }
-
-    // find best cofactoring variable
-//    if ( pObj->nFans > 3 )
-//        Kit_DsdCofactoring( Kit_DsdObjTruth(pObj), pObj->nFans, NULL, 4, 1 );
-    if ( !p->fCofactoring && p->pPars->nVarsShared > 0 && (int)pObj->nFans > p->pPars->nLutSize )
-//        return Abc_LutIfManMapMulti( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
-        Abc_LutIfManMapMulti( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
-
-
-    // derive the factored form
-    pGraph = Kit_TruthToGraph( Kit_DsdObjTruth(pObj), pObj->nFans, p->vCover );
-    if ( pGraph == NULL )
-        return NULL;
-    // convert factored form into the AIG
-    pObjNew = Abc_LutIfManMapPrime( p->pIfMan, pFansNew, pGraph ); 
-    Kit_GraphFree( pGraph );
-    return If_NotCond( pObjNew, fCompl );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prepares the mapping manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_LutCutUpdate( Lut_Man_t * p, Lut_Cut_t * pCut, Kit_DsdNtk_t * pNtk )
-{
-    extern Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vCover );
-    Kit_DsdObj_t * pRoot;
-    If_Obj_t * pDriver;
-    Abc_Obj_t * pLeaf, * pObjNew;
-    int nGain, i;
-
-    // check special cases
-    pRoot = Kit_DsdNtkRoot( pNtk );
-    if ( pRoot->Type == KIT_DSD_CONST1 )
-    {
-        pObjNew = Abc_NtkCreateNodeConst1( p->pNtk );
-        pObjNew = Abc_ObjNotCond( pObjNew, Kit_DsdLitIsCompl(pNtk->Root) );
-
-        // perform replacement
-        pObjNew->Level = p->pObj->Level;
-        Abc_ObjReplace( p->pObj, pObjNew );
-        Res_UpdateNetworkLevel( pObjNew, p->vLevels );
-        p->nGainTotal += pCut->nNodes - pCut->nNodesDup;
-        return 1;
-    }
-    if ( pRoot->Type == KIT_DSD_VAR )
-    {
-        pObjNew = Abc_NtkObj( p->pNtk, pCut->pLeaves[ Kit_DsdLit2Var(pRoot->pFans[0]) ] );
-        pObjNew = Abc_ObjNotCond( pObjNew, Kit_DsdLitIsCompl(pNtk->Root) ^ Kit_DsdLitIsCompl(pRoot->pFans[0]) );
-
-        // perform replacement
-        pObjNew->Level = p->pObj->Level;
-        Abc_ObjReplace( p->pObj, pObjNew );
-        Res_UpdateNetworkLevel( pObjNew, p->vLevels );
-        p->nGainTotal += pCut->nNodes - pCut->nNodesDup;
-        return 1;
-    }
-    assert( pRoot->Type == KIT_DSD_AND || pRoot->Type == KIT_DSD_XOR || pRoot->Type == KIT_DSD_PRIME );
-
-    // start the mapping manager
-    if ( p->pIfMan == NULL )
-        Abc_LutIfManStart( p );
-
-    // prepare the mapping manager
-    If_ManRestart( p->pIfMan );
-    // create the PI variables
-    for ( i = 0; i < p->pPars->nVarsMax; i++ )
-        If_ManCreateCi( p->pIfMan );
-    // set the arrival times
-    Abc_LutCutForEachLeaf( p->pNtk, pCut, pLeaf, i )
-        p->pIfMan->pPars->pTimesArr[i] = (float)pLeaf->Level;
-    // prepare the PI cuts
-    If_ManSetupCiCutSets( p->pIfMan );
-    // create the internal nodes
-//    pDriver = Abc_LutIfManMap_New_rec( p, pNtk, pNtk->Root );
-    pDriver = Abc_LutIfManMap_rec( p, pNtk, pNtk->Root, NULL );
-    if ( pDriver == NULL )
-        return 0;
-    // create the PO node
-    If_ManCreateCo( p->pIfMan, If_Regular(pDriver), 0 );
-
-    // perform mapping
-    p->pIfMan->pPars->fAreaOnly = 1;
-    If_ManPerformMappingComb( p->pIfMan );
-
-    // compute the gain in area
-    nGain = pCut->nNodes - pCut->nNodesDup - (int)p->pIfMan->AreaGlo;
-    if ( p->pPars->fVeryVerbose )
-        printf( "       Mffc = %2d. Mapped = %2d. Gain = %3d. Depth increase = %d.\n", 
-            pCut->nNodes - pCut->nNodesDup, (int)p->pIfMan->AreaGlo, nGain, (int)p->pIfMan->RequiredGlo - (int)p->pObj->Level );
-
-    // quit if there is no gain
-    if ( !(nGain > 0 || (p->pPars->fZeroCost && nGain == 0)) )
-        return 0;
-    // quit if depth increases too much
-    if ( (int)p->pIfMan->RequiredGlo - (int)p->pObj->Level > p->pPars->nGrowthLevel )
-        return 0;
-
-    // perform replacement
-    p->nGainTotal += nGain;
-    p->nChanges++;
-
-    // prepare the mapping manager
-    If_ManCleanNodeCopy( p->pIfMan );
-    If_ManCleanCutData( p->pIfMan );
-    // set the PIs of the cut
-    Abc_LutCutForEachLeaf( p->pNtk, pCut, pLeaf, i )
-        If_ObjSetCopy( If_ManCi(p->pIfMan, i), pLeaf );
-    // get the area of mapping
-    pObjNew = Abc_NodeFromIf_rec( p->pNtk, p->pIfMan, If_Regular(pDriver), p->vCover );
-    pObjNew->pData = Hop_NotCond( pObjNew->pData, If_IsComplement(pDriver) );
-
-    // perform replacement
-    pObjNew->Level = p->pObj->Level;
-    Abc_ObjReplace( p->pObj, pObjNew );
-    Res_UpdateNetworkLevel( pObjNew, p->vLevels );
-    return 1;
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Performs resynthesis for one node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_LutResynthesizeNode( Lut_Man_t * p )
-{
-    extern void Kit_DsdTest( unsigned * pTruth, int nVars );
-    extern int Kit_DsdEval( unsigned * pTruth, int nVars, int nLutSize );
-
-    Kit_DsdNtk_t * pDsdNtk;
-    Lut_Cut_t * pCut;
-    unsigned * pTruth;
-    void * pDsd = NULL;
-//    int Result, Gain;
-    int i, RetValue, clk;
-
-    // compute the cuts
-clk = clock();
-    if ( !Abc_LutNodeCuts( p ) )
-    {
-p->timeCuts += clock() - clk;
-        return 0;
-    }
-p->timeCuts += clock() - clk;
-
-    if ( p->pPars->fVeryVerbose )
-    printf( "Node %5d : Mffc size = %5d. Cuts = %5d.\n", p->pObj->Id, p->nMffc, p->nEvals );
-    // try the good cuts
-    p->nCutsTotal  += p->nCuts;
-    p->nCutsUseful += p->nEvals;
-    for ( i = 0; i < p->nEvals; i++ )
-    {
-        // get the cut
-        pCut = p->pCuts + p->pEvals[i];
-
-        // compute the truth table
-clk = clock();
-        pTruth = Abc_LutCutTruth( p, pCut );
-p->timeTruth += clock() - clk;
-
-
-/*
-        // evaluate the result of decomposition        
-        Result = Kit_DsdEval( pTruth, pCut->nLeaves, 3 );
-        // calculate expected gain
-        Gain = (Result < 0) ? -1 : pCut->nNodes - pCut->nNodesDup - Result;
-        if ( !(Gain < 0 || (Gain == 0 && p->pPars->fZeroCost)) )
-            continue;
-*/
-
-clk = clock();
-//        Kit_DsdTest( pTruth, pCut->nLeaves );
-        pDsdNtk = Kit_DsdDeriveNtk( pTruth, pCut->nLeaves, p->pPars->nLutSize );
-p->timeEval += clock() - clk;
-
-        if ( Kit_DsdNtkRoot(pDsdNtk)->nFans == 16 ) // skip 16-input non-DSD because ISOP will not work
-        {
-            Kit_DsdNtkFree( pDsdNtk );
-            continue;
-        }
-/*
-        // skip large non-DSD blocks
-        if ( Kit_DsdNonDsdSizeMax(pDsdNtk) > 7 )
-        {
-            Kit_DsdNtkFree( pDsdNtk );
-            continue;
-        }
-*/
-  
-/*        
-        if ( pCut->nLeaves > 6 && pCut->nLeaves < 12 && Kit_DsdNonDsdSizeMax(pDsdNtk) == pCut->nLeaves )
-        {
-//            Abc_NtkPrintMeasures( pTruth, pCut->nLeaves );
-//            Kit_DsdTestCofs( pDsdNtk, pTruth );
-
-//            Abc_NtkPrintOneDecomp( pTruth, pCut->nLeaves );
-            Abc_NtkPrintOneDec( pTruth, pCut->nLeaves );
-        }
-*/
-
-        if ( p->pPars->fVeryVerbose )
-        {
-//            Extra_PrintHexadecimal( stdout, pTruth, pCut->nLeaves ); printf( "\n" );
-//            printf( "    Cut %2d : L = %2d. S = %2d. Vol = %2d. Q = %d. N = %d. W = %4.2f. New = %2d. Gain = %2d.\n", 
-//                i, pCut->nLeaves, Extra_TruthSupportSize(pTruth, pCut->nLeaves), pCut->nNodes, pCut->nNodesDup, pCut->nLuts, pCut->Weight, Result, Gain );
-            printf( "  C%02d: L= %2d/%2d  V= %2d/%d  N= %d  W= %4.2f  ", 
-                i, pCut->nLeaves, Extra_TruthSupportSize(pTruth, pCut->nLeaves), pCut->nNodes, pCut->nNodesDup, pCut->nLuts, pCut->Weight );
-            Kit_DsdPrint( stdout, pDsdNtk );
-        }
-
-        // update the network
-clk = clock();
-        RetValue = Abc_LutCutUpdate( p, pCut, pDsdNtk );
-        Kit_DsdNtkFree( pDsdNtk );
-p->timeMap += clock() - clk;
-        if ( RetValue )
-            break;
-    }
-    return 1;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Performs resynthesis for one network.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_LutResynthesize( Abc_Ntk_t * pNtk, Lut_Par_t * pPars )
-{
-    ProgressBar * pProgress;
-    Lut_Man_t * p;
-    Abc_Obj_t * pObj;
-    double Delta;
-    int i, Iter, nNodes, nNodesPrev, clk = clock();
-    assert( Abc_NtkIsLogic(pNtk) );
-
-    // get the number of inputs
-    pPars->nLutSize = Abc_NtkGetFaninMax( pNtk );
-    pPars->nVarsMax = pPars->nLutsMax * (pPars->nLutSize - 1) + 1; // V = N * (K-1) + 1
-    if ( pPars->fVerbose )
-    {
-        printf( "Resynthesis for %d %d-LUTs with %d non-MFFC LUTs, %d crossbars, and %d-input cuts.\n",
-            pPars->nLutsMax, pPars->nLutSize, pPars->nLutsOver, pPars->nVarsShared, pPars->nVarsMax );
-    }
-    if ( pPars->nVarsMax > 16 )
-    {
-        printf( "Currently cannot handle resynthesis with more than %d inputs (reduce \"-N <num>\").\n", 16 );
-        return 1;
-    }
- 
-    // convert logic to AIGs
-    Abc_NtkToAig( pNtk );
-
-    // start the manager
-    p = Abc_LutManStart( pPars );
-    p->pNtk = pNtk;
-    p->nNodesTotal = Abc_NtkNodeNum(pNtk);
-    p->vLevels = Vec_VecStart( 3 * Abc_NtkLevel(pNtk) ); // computes levels of all nodes
-    if ( p->pPars->fSatur )
-        p->vVisited = Vec_VecStart( 0 );
-
-    // iterate over the network
-    nNodesPrev = p->nNodesTotal;
-    for ( Iter = 1; ; Iter++ )
-    {
-        // expand storage for changed nodes
-        if ( p->pPars->fSatur )
-            Vec_VecExpand( p->vVisited, Abc_NtkObjNumMax(pNtk) + 1 );
-
-        // consider all nodes
-        nNodes = Abc_NtkObjNumMax(pNtk);
-        if ( !pPars->fVeryVerbose )
-            pProgress = Extra_ProgressBarStart( stdout, nNodes );
-        Abc_NtkForEachNode( pNtk, pObj, i )
-        {
-            if ( i >= nNodes )
-                break;
-            if ( !pPars->fVeryVerbose )
-                Extra_ProgressBarUpdate( pProgress, i, NULL );
-            // skip the nodes that did not change
-            if ( p->pPars->fSatur && !Abc_LutNodeHasChanged(p, pObj->Id) )
-                continue;
-            // resynthesize
-            p->pObj = pObj;
-            Abc_LutResynthesizeNode( p );
-        }
-        if ( !pPars->fVeryVerbose )
-            Extra_ProgressBarStop( pProgress );
-
-        // check the increase
-        Delta = 100.00 * (nNodesPrev - Abc_NtkNodeNum(pNtk)) / p->nNodesTotal;
-        if ( Delta < 0.05 )
-            break;
-        nNodesPrev = Abc_NtkNodeNum(pNtk);
-        if ( !p->pPars->fSatur )
-            break;
-    }
-
-    if ( pPars->fVerbose )
-    {
-        printf( "N = %5d (%3d)  Cut = %5d (%4d)  Change = %5d  Gain = %5d  (%5.2f %%) Iter = %2d\n", 
-            p->nNodesTotal, p->nNodesOver, p->nCutsTotal, p->nCutsUseful, p->nChanges, p->nGainTotal, 100.0 * p->nGainTotal / p->nNodesTotal, Iter );
-        printf( "Non_DSD blocks: " );
-        for ( i = 3; i <= pPars->nVarsMax; i++ )
-            if ( p->nBlocks[i] )
-                printf( "%d=%d  ", i, p->nBlocks[i] );
-        printf( "\n" );
-        p->timeTotal = clock() - clk;
-        p->timeOther = p->timeTotal - p->timeCuts - p->timeTruth - p->timeEval - p->timeMap;
-        PRTP( "Cuts  ", p->timeCuts,  p->timeTotal );
-        PRTP( "Truth ", p->timeTruth, p->timeTotal );
-        PRTP( "Eval  ", p->timeEval,  p->timeTotal );
-        PRTP( "Map   ", p->timeMap,   p->timeTotal );
-        PRTP( "Other ", p->timeOther, p->timeTotal );
-        PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
-    }
-
-    Abc_LutManStop( p );
-    // check the resulting network
-    if ( !Abc_NtkCheck( pNtk ) )
-    {
-        printf( "Abc_LutResynthesize: The network check has failed.\n" );
-        return 0;
-    }
-    return 1;
-}
-
-
-
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Records variable order.]
-
-  Description [Increaments Order[x][y] by 1 if x should be above y in the DSD.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_LutCreateVarOrder( Kit_DsdNtk_t * pNtk, char pTable[][16] )
-{
-    Kit_DsdObj_t * pObj;
-    unsigned uSuppFanins, k;
-    int Above[16], Below[16];
-    int nAbove, nBelow, iFaninLit, i, x, y;
-    // iterate through the nodes
-    Kit_DsdNtkForEachObj( pNtk, pObj, i )
-    {
-        // collect fanin support of this node
-        nAbove = 0;
-        uSuppFanins = 0;
-        Kit_DsdObjForEachFanin( pNtk, pObj, iFaninLit, k )
-        {
-            if ( Kit_DsdLitIsLeaf( pNtk, iFaninLit ) )
-                Above[nAbove++] = Kit_DsdLit2Var(iFaninLit);
-            else
-                uSuppFanins |= Kit_DsdLitSupport( pNtk, iFaninLit );
-        }
-        // find the below variables
-        nBelow = 0;
-        for ( y = 0; y < 16; y++ )
-            if ( uSuppFanins & (1 << y) )
-                Below[nBelow++] = y;
-        // create all pairs
-        for ( x = 0; x < nAbove; x++ )
-            for ( y = 0; y < nBelow; y++ )
-                pTable[Above[x]][Below[y]]++;
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates commmon variable order.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_LutCreateCommonOrder( char pTable[][16], int pOrder[], int nLeaves )
-{
-    int Score[16] = {0};
-    int i, y, x;
-    // compute scores for each leaf
-    for ( i = 0; i < nLeaves; i++ )
-    {
-        for ( y = 0; y < nLeaves; y++ )
-            Score[i] += pTable[i][y];
-        for ( x = 0; x < nLeaves; x++ )
-            Score[i] -= pTable[x][i];
-    }
-/*
-    printf( "Scores: " );
-    for ( i = 0; i < nLeaves; i++ )
-        printf( "%d ", Score[i] );
-    printf( "\n" );
-*/
-    // sort the scores
-    Extra_BubbleSort( pOrder, Score, nLeaves, 0 );
-/*
-    printf( "Scores: " );
-    for ( i = 0; i < nLeaves; i++ )
-        printf( "%d ", Score[pOrder[i]] );
-    printf( "\n" );
-*/
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prepares the mapping manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-If_Obj_t * Abc_LutIfManMapMulti_rec( Lut_Man_t * p, Kit_DsdNtk_t ** ppNtks, int * piLits, int * piCofVar, int nCBars, If_Obj_t ** ppLeaves, int nLeaves, int * pOrder )
-{
-    Kit_DsdObj_t * pObj;
-    If_Obj_t * pObjsNew[4][8], * pResPrev;
-    unsigned uSupps[8], uSuppFanin;
-    int piLitsNew[8], pDecision[8] = {0};
-    int i, v, k, nSize = (1 << nCBars);
-
-    // find which of the variables is highest in the order
-
-    // go though non-trivial components
-    for ( i = 0; i < nSize; i++ )
-    {
-        if ( piLits[i] == -1 )
-            continue;
-        pObj = Kit_DsdNtkObj( ppNtks[i], Kit_DsdLit2Var(piLits[i]) );
-        uSuppFanin = pObj? Kit_DsdLitSupport( ppNtks[i], pObj->pFans[0] ) : 0;
-        uSupps[i] = Kit_DsdLitSupport( ppNtks[i], piLits[i] ) & ~uSuppFanin;
-    }
-    // find the variable that appears the highest in the order
-    for ( v = 0; v < nLeaves; v++ )
-    {
-        for ( i = 0; i < nSize; i++ )
-            if ( uSupps[i] & (1 << pOrder[v]) )
-                break;
-    }
-    assert( v < nLeaves );
-    // pull out all components that have this variable
-    for ( i = 0; i < nSize; i++ )
-        pDecision[i] = ( uSupps[i] & (1 << pOrder[v]) );
-
-
-    // iterate over the nodes
-    for ( i = 0; i < nSize; i++ )
-    {
-        pObj = Kit_DsdNtkObj( ppNtks[i], Kit_DsdLit2Var(piLits[i]) );
-        if ( pDecision[i] )
-            piLitsNew[i] = pObj->pFans[0];
-        else
-            piLitsNew[i] = piLits[i];
-    }
-
-    // call again
-    pResPrev = Abc_LutIfManMapMulti_rec( p, ppNtks, piLitsNew, piCofVar, nCBars, ppLeaves, nLeaves, pOrder );
-
-    // create new set of nodes
-    for ( i = 0; i < nSize; i++ )
-    {
-        if ( pDecision[i] )
-            pObjsNew[nCBars][i] = Abc_LutIfManMap_rec( p, ppNtks[i], piLits[i], pResPrev );
-        else
-            pObjsNew[nCBars][i] = pResPrev;
-    }
-
-    // create MUX using these outputs
-    for ( k = nCBars; k > 0; k-- )
-    {
-        nSize /= 2;
-        for ( i = 0; i < nSize; i++ )
-            pObjsNew[k-1][i] = If_ManCreateMnux( p->pIfMan, pObjsNew[k][2*i+0], pObjsNew[k][2*i+1], ppLeaves[piCofVar[k-1]] );
-    }
-    assert( nCBars == 1 && nSize == 1 );
-    return If_NotCond( pObjsNew[0][0], nCBars & 1 );  
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prepares the mapping manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-If_Obj_t * Abc_LutIfManMapMulti( Lut_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves )
-{
-    If_Obj_t * pResult;
-    Kit_DsdNtk_t * ppNtks[8] = {0}, * pTemp;
-    int piCofVar[4], pOrder[16] = {0}, pPrios[16], pFreqs[16] = {0}, piLits[16];
-    int i, k, nCBars, nSize, nMemSize;
-    unsigned * ppCofs[4][8], uSupport;
-    char pTable[16][16] = {0};
-    int fVerbose = 1;
-
-    // allocate storage for cofactors
-    nMemSize = Kit_TruthWordNum(nVars);
-    ppCofs[0][0] = ALLOC( unsigned, 32 * nMemSize );
-    nSize = 0;
-    for ( i = 0; i < 4; i++ )
-    for ( k = 0; k < 8; k++ )
-        ppCofs[i][k] = ppCofs[0][0] + nMemSize * nSize++;
-    assert( nSize == 32 );
-
-    // find the best cofactoring variables
-    nCBars = Kit_DsdCofactoring( pTruth, nVars, piCofVar, p->pPars->nVarsShared, 0 );
-
-    // copy the function
-    Kit_TruthCopy( ppCofs[0][0], pTruth, nVars );
-
-    // decompose w.r.t. these variables
-    for ( k = 0; k < nCBars; k++ )
-    {
-        nSize = (1 << k);
-        for ( i = 0; i < nSize; i++ )
-        {
-            Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] );
-            Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] );
-        }
-    }
-    nSize = (1 << nCBars);
-    // compute variable frequences
-    for ( i = 0; i < nSize; i++ )
-    {
-        uSupport = Kit_TruthSupport( ppCofs[nCBars][i], nVars );
-        for ( k = 0; k < nVars; k++ )
-            if ( uSupport & (1<<k) )
-                pFreqs[k]++;
-    }
-    // compute DSD networks
-    for ( i = 0; i < nSize; i++ )
-    {
-        ppNtks[i] = Kit_DsdDecompose( ppCofs[nCBars][i], nVars );
-        ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] );
-        Kit_DsdNtkFree( pTemp );
-        if ( fVerbose )
-        {
-            printf( "Cof%d%d: ", nCBars, i );
-            Kit_DsdPrint( stdout, ppNtks[i] );
-        }
-    }
-    free( ppCofs[0][0] );
-
-    // find common variable order
-    for ( i = 0; i < nSize; i++ )
-    {
-        Kit_DsdGetSupports( ppNtks[i] );
-        Abc_LutCreateVarOrder( ppNtks[i], pTable );
-    }
-    Abc_LutCreateCommonOrder( pTable, pOrder, nVars );
-
-    printf( "Common variable order: " );
-    for ( i = 0; i < nVars; i++ )
-        printf( "%c ", 'a' + pOrder[i] );
-    printf( "\n" );
-
-    // derive variable priority
-    for ( i = 0; i < 16; i++ )
-        pPrios[i] = 16;
-    for ( i = 0; i < nVars; i++ )
-        pPrios[pOrder[i]] = i;
-
-    // transform all networks according to the variable order
-    for ( i = 0; i < nSize; i++ )
-    {
-        ppNtks[i] = Kit_DsdShrink( pTemp = ppNtks[i], pPrios );
-        Kit_DsdNtkFree( pTemp );
-        Kit_DsdGetSupports( ppNtks[i] );
-        // undec nodes should be rotated in such a way that the first input has as many shared inputs as possible
-        Kit_DsdRotate( ppNtks[i], pFreqs );
-        // collect the roots
-        piLits[i] = ppNtks[i]->Root;
-    }
-/*
-    p->fCofactoring = 1;
-    pResult = Abc_LutIfManMapMulti_rec( p, ppNtks[nCBars], piLits, piCofVar, nCBars, ppLeaves, nVars, pOrder );
-    p->fCofactoring = 0;
-*/
-    // free the networks
-    for ( i = 0; i < 8; i++ )
-        if ( ppNtks[i] )
-            Kit_DsdNtkFree( ppNtks[i] );
-
-    return pResult;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index b8c4a6c0..074b8ae8 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -145,8 +145,8 @@ If_Man_t * Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
         Extra_ProgressBarUpdate( pProgress, i, "Initial" );
         // add the node to the mapper
         pNode->pCopy = (Abc_Obj_t *)If_ManCreateAnd( pIfMan, 
-            (If_Obj_t *)Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode), 
-            (If_Obj_t *)Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) );
+            If_NotCond( (If_Obj_t *)Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ), 
+            If_NotCond( (If_Obj_t *)Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) ) );
         // set up the choice node
         if ( Abc_AigNodeIsChoice( pNode ) )
         {
@@ -162,7 +162,7 @@ If_Man_t * Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
 
     // set the primary outputs without copying the phase
     Abc_NtkForEachCo( pNtk, pNode, i )
-        If_ManCreateCo( pIfMan, (If_Obj_t *)Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) );
+        If_ManCreateCo( pIfMan, If_NotCond( (If_Obj_t *)Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ) );
     return pIfMan;
 }
 
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 9bc51dbe..f6c73102 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -11,7 +11,6 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcDebug.c \
     src/base/abci/abcDress.c \
     src/base/abci/abcDsd.c \
-    src/base/abci/abcDsdRes.c \
     src/base/abci/abcEspresso.c \
     src/base/abci/abcExtract.c \
     src/base/abci/abcFpga.c \
diff --git a/src/base/io/io.c b/src/base/io/io.c
index e1d4de97..20caeb57 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -715,7 +715,7 @@ int IoCommandReadTruth( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fHex;
     int c;
 
-    fHex = 0;
+    fHex = 1;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "xh" ) ) != EOF )
     {
diff --git a/src/map/if/if.h b/src/map/if/if.h
index a5aa3356..706f8552 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -212,6 +212,11 @@ struct If_Obj_t_
     If_Cut_t           CutBest;       // the best cut selected 
 };
 
+static inline If_Obj_t * If_Regular( If_Obj_t * p )                          { return (If_Obj_t *)((unsigned long)(p) & ~01);  }
+static inline If_Obj_t * If_Not( If_Obj_t * p )                              { return (If_Obj_t *)((unsigned long)(p) ^  01);  }
+static inline If_Obj_t * If_NotCond( If_Obj_t * p, int c )                   { return (If_Obj_t *)((unsigned long)(p) ^ (c));  }
+static inline int        If_IsComplement( If_Obj_t * p )                     { return (int )(((unsigned long)p) & 01);         }
+
 static inline int        If_ManCiNum( If_Man_t * p )                         { return p->nObjs[IF_CI];               }
 static inline int        If_ManCoNum( If_Man_t * p )                         { return p->nObjs[IF_CO];               }
 static inline int        If_ManAndNum( If_Man_t * p )                        { return p->nObjs[IF_AND];              }
@@ -334,10 +339,10 @@ extern If_Man_t *      If_ManStart( If_Par_t * pPars );
 extern void            If_ManRestart( If_Man_t * p );
 extern void            If_ManStop( If_Man_t * p );
 extern If_Obj_t *      If_ManCreateCi( If_Man_t * p );
-extern If_Obj_t *      If_ManCreateCo( If_Man_t * p, If_Obj_t * pDriver, int fCompl0 );
-extern If_Obj_t *      If_ManCreateAnd( If_Man_t * p, If_Obj_t * pFan0, int fCompl0, If_Obj_t * pFan1, int fCompl1 );
-extern If_Obj_t *      If_ManCreateXnor( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1 );
-extern If_Obj_t *      If_ManCreateMnux( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1, If_Obj_t * pCtrl );
+extern If_Obj_t *      If_ManCreateCo( If_Man_t * p, If_Obj_t * pDriver );
+extern If_Obj_t *      If_ManCreateAnd( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1 );
+extern If_Obj_t *      If_ManCreateXor( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1 );
+extern If_Obj_t *      If_ManCreateMux( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1, If_Obj_t * pCtrl );
 extern void            If_ManCreateChoice( If_Man_t * p, If_Obj_t * pRepr );
 extern void            If_ManSetupCutTriv( If_Man_t * p, If_Cut_t * pCut, int ObjId );
 extern void            If_ManSetupCiCutSets( If_Man_t * p );
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index 923dd7d5..14267f8e 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -175,13 +175,13 @@ If_Obj_t * If_ManCreateCi( If_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-If_Obj_t * If_ManCreateCo( If_Man_t * p, If_Obj_t * pDriver, int fCompl0 )
+If_Obj_t * If_ManCreateCo( If_Man_t * p, If_Obj_t * pDriver )
 {
     If_Obj_t * pObj;
     pObj = If_ManSetupObj( p );
-    pObj->Type = IF_CO;
-    pObj->fCompl0 = fCompl0;
     Vec_PtrPush( p->vCos, pObj );
+    pObj->Type = IF_CO;
+    pObj->fCompl0 = If_IsComplement(pDriver); pDriver = If_Regular(pDriver);
     pObj->pFanin0 = pDriver; pDriver->nRefs++; 
     p->nObjs[IF_CO]++;
     return pObj;
@@ -198,17 +198,26 @@ If_Obj_t * If_ManCreateCo( If_Man_t * p, If_Obj_t * pDriver, int fCompl0 )
   SeeAlso     []
 
 ***********************************************************************/
-If_Obj_t * If_ManCreateAnd( If_Man_t * p, If_Obj_t * pFan0, int fCompl0, If_Obj_t * pFan1, int fCompl1 )
+If_Obj_t * If_ManCreateAnd( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1 )
 {
     If_Obj_t * pObj;
+    // perform constant propagation
+    if ( pFan0 == pFan1 )
+        return pFan0;
+    if ( pFan0 == If_Not(pFan1) )
+        return If_Not(p->pConst1);
+    if ( If_Regular(pFan0) == p->pConst1 )
+        return pFan0 == p->pConst1 ? pFan1 : If_Not(p->pConst1);
+    if ( If_Regular(pFan1) == p->pConst1 )
+        return pFan1 == p->pConst1 ? pFan0 : If_Not(p->pConst1);
     // get memory for the new object
     pObj = If_ManSetupObj( p );
     pObj->Type    = IF_AND;
-    pObj->fCompl0 = fCompl0;
-    pObj->fCompl1 = fCompl1;
+    pObj->fCompl0 = If_IsComplement(pFan0); pFan0 = If_Regular(pFan0);
+    pObj->fCompl1 = If_IsComplement(pFan1); pFan1 = If_Regular(pFan1);
     pObj->pFanin0 = pFan0; pFan0->nRefs++; pFan0->nVisits++; pFan0->nVisitsCopy++;
     pObj->pFanin1 = pFan1; pFan1->nRefs++; pFan1->nVisits++; pFan1->nVisitsCopy++;
-    pObj->fPhase  = (fCompl0 ^ pFan0->fPhase) & (fCompl1 ^ pFan1->fPhase);
+    pObj->fPhase  = (pObj->fCompl0 ^ pFan0->fPhase) & (pObj->fCompl1 ^ pFan1->fPhase);
     pObj->Level   = 1 + IF_MAX( pFan0->Level, pFan1->Level );
     if ( p->nLevelMax < (int)pObj->Level )
         p->nLevelMax = (int)pObj->Level;
@@ -227,12 +236,12 @@ If_Obj_t * If_ManCreateAnd( If_Man_t * p, If_Obj_t * pFan0, int fCompl0, If_Obj_
   SeeAlso     []
 
 ***********************************************************************/
-If_Obj_t * If_ManCreateXnor( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1 )
+If_Obj_t * If_ManCreateXor( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1 )
 {
     If_Obj_t * pRes1, * pRes2;
-    pRes1 = If_ManCreateAnd( p, pFan0, 0, pFan1, 1 );
-    pRes2 = If_ManCreateAnd( p, pFan0, 1, pFan1, 0 );
-    return If_ManCreateAnd( p, pRes1, 1, pRes2, 1 );
+    pRes1 = If_ManCreateAnd( p, If_Not(pFan0), pFan1 );
+    pRes2 = If_ManCreateAnd( p, pFan0, If_Not(pFan1) );
+    return If_Not( If_ManCreateAnd( p, If_Not(pRes1), If_Not(pRes2) ) );
 }
 
 /**Function*************************************************************
@@ -246,12 +255,12 @@ If_Obj_t * If_ManCreateXnor( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1 )
   SeeAlso     []
 
 ***********************************************************************/
-If_Obj_t * If_ManCreateMnux( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1, If_Obj_t * pCtrl )
+If_Obj_t * If_ManCreateMux( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1, If_Obj_t * pCtrl )
 {
     If_Obj_t * pRes1, * pRes2;
-    pRes1 = If_ManCreateAnd( p, pFan0, 0, pCtrl, 1 );
-    pRes2 = If_ManCreateAnd( p, pFan1, 0, pCtrl, 0 );
-    return If_ManCreateAnd( p, pRes1, 1, pRes2, 1 );
+    pRes1 = If_ManCreateAnd( p, pFan0, If_Not(pCtrl) );
+    pRes2 = If_ManCreateAnd( p, pFan1, pCtrl );
+    return If_Not( If_ManCreateAnd( p, If_Not(pRes1), If_Not(pRes2) ) );
 }
 
 /**Function*************************************************************
diff --git a/src/opt/kit/kit.h b/src/opt/kit/kit.h
index a0552b19..229b0bce 100644
--- a/src/opt/kit/kit.h
+++ b/src/opt/kit/kit.h
@@ -159,6 +159,7 @@ static inline unsigned        Kit_DsdLitSupport( Kit_DsdNtk_t * pNtk, int Lit )
 
 #define KIT_MIN(a,b)       (((a) < (b))? (a) : (b))
 #define KIT_MAX(a,b)       (((a) > (b))? (a) : (b))
+#define KIT_INFINITY       (100000000)
 
 #ifndef ALLOC
 #define ALLOC(type, num)     ((type *) malloc(sizeof(type) * (num)))
@@ -235,6 +236,10 @@ static inline int Kit_WordFindFirstBit( unsigned uWord )
             return i;
     return -1;
 }
+static inline int Kit_WordHasOneBit( unsigned uWord )
+{
+    return (uWord & (uWord - 1)) == 0;
+}
 static inline int Kit_WordCountOnes( unsigned uWord )
 {
     uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
@@ -250,6 +255,14 @@ static inline int Kit_TruthCountOnes( unsigned * pIn, int nVars )
         Counter += Kit_WordCountOnes(pIn[w]);
     return Counter;
 }
+static inline int Kit_TruthFindFirstBit( unsigned * pIn, int nVars )
+{
+    int w;
+    for ( w = 0; w < Kit_TruthWordNum(nVars); w++ )
+        if ( pIn[w] )
+            return Kit_WordFindFirstBit(pIn[w]);
+    return -1;
+}
 static inline int Kit_TruthIsEqual( unsigned * pIn0, unsigned * pIn1, int nVars )
 {
     int w;
@@ -433,7 +446,9 @@ extern DdNode *        Kit_TruthToBdd( DdManager * dd, unsigned * pTruth, int nV
 /*=== kitDsd.c ==========================================================*/
 extern Kit_DsdNtk_t *  Kit_DsdDeriveNtk( unsigned * pTruth, int nVars, int nLutSize );
 extern unsigned *      Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk );
+extern void            Kit_DsdTruth( Kit_DsdNtk_t * pNtk, unsigned * pTruthRes );
 extern void            Kit_DsdPrint( FILE * pFile, Kit_DsdNtk_t * pNtk );
+extern void            Kit_DsdPrintExpanded( Kit_DsdNtk_t * pNtk );
 extern Kit_DsdNtk_t *  Kit_DsdDecompose( unsigned * pTruth, int nVars );
 extern void            Kit_DsdNtkFree( Kit_DsdNtk_t * pNtk );
 extern int             Kit_DsdNonDsdSizeMax( Kit_DsdNtk_t * pNtk );
diff --git a/src/opt/kit/kitDsd.c b/src/opt/kit/kitDsd.c
index 8dd1b06f..8b6b6979 100644
--- a/src/opt/kit/kitDsd.c
+++ b/src/opt/kit/kitDsd.c
@@ -47,7 +47,7 @@ Kit_DsdMan_t * Kit_DsdManAlloc( int nVars )
     p->nVars = nVars;
     p->nWords = Kit_TruthWordNum( p->nVars );
     p->vTtElems = Vec_PtrAllocTruthTables( p->nVars );
-    p->vTtNodes = Vec_PtrAllocSimInfo( 64, p->nWords );
+    p->vTtNodes = Vec_PtrAllocSimInfo( 1024, p->nWords );
     return p;
 }
 
@@ -262,6 +262,25 @@ void Kit_DsdPrint( FILE * pFile, Kit_DsdNtk_t * pNtk )
 
 /**Function*************************************************************
 
+  Synopsis    [Print the DSD formula.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_DsdPrintExpanded( Kit_DsdNtk_t * pNtk )
+{
+    Kit_DsdNtk_t * pTemp;
+    pTemp = Kit_DsdExpand( pNtk );
+    Kit_DsdPrint( stdout, pNtk );
+    Kit_DsdNtkFree( pTemp );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Derives the truth table of the DSD node.]
 
   Description []
@@ -384,6 +403,26 @@ unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk )
     return pTruthRes;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Derives the truth table of the DSD network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_DsdTruth( Kit_DsdNtk_t * pNtk, unsigned * pTruthRes )
+{
+    Kit_DsdMan_t * p;
+    unsigned * pTruth;
+    p = Kit_DsdManAlloc( pNtk->nVars );
+    pTruth = Kit_DsdTruthCompute( p, pNtk );
+    Kit_TruthCopy( pTruthRes, pTruth, pNtk->nVars );
+    Kit_DsdManFree( p );
+}
 
 /**Function*************************************************************
 
@@ -551,29 +590,25 @@ void Kit_DsdExpandCollectXor_rec( Kit_DsdNtk_t * p, int iLit, int * piLitsNew, i
 int Kit_DsdExpandNode_rec( Kit_DsdNtk_t * pNew, Kit_DsdNtk_t * p, int iLit )
 {
     unsigned * pTruth, * pTruthNew;
-    unsigned i, fCompl, iLitFanin, piLitsNew[16], nLitsNew = 0;
+    unsigned i, iLitFanin, piLitsNew[16], nLitsNew = 0;
     Kit_DsdObj_t * pObj, * pObjNew;
 
-    // remember the complement
-    fCompl = Kit_DsdLitIsCompl(iLit); 
-    iLit = Kit_DsdLitRegular(iLit); 
-    assert( !Kit_DsdLitIsCompl(iLit) );
-
     // consider the case of simple gate
     pObj = Kit_DsdNtkObj( p, Kit_DsdLit2Var(iLit) );
     if ( pObj == NULL )
-        return Kit_DsdLitNotCond( iLit, fCompl );
+        return iLit;
     if ( pObj->Type == KIT_DSD_AND )
     {
-        Kit_DsdExpandCollectAnd_rec( p, iLit, piLitsNew, &nLitsNew );
+        Kit_DsdExpandCollectAnd_rec( p, Kit_DsdLitRegular(iLit), piLitsNew, &nLitsNew );
         pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_AND, nLitsNew );
         for ( i = 0; i < pObjNew->nFans; i++ )
             pObjNew->pFans[i] = Kit_DsdExpandNode_rec( pNew, p, piLitsNew[i] );
-        return Kit_DsdVar2Lit( pObjNew->Id, fCompl );
+        return Kit_DsdVar2Lit( pObjNew->Id, Kit_DsdLitIsCompl(iLit) );
     }
     if ( pObj->Type == KIT_DSD_XOR )
     {
-        Kit_DsdExpandCollectXor_rec( p, iLit, piLitsNew, &nLitsNew );
+        int fCompl = Kit_DsdLitIsCompl(iLit);
+        Kit_DsdExpandCollectXor_rec( p, Kit_DsdLitRegular(iLit), piLitsNew, &nLitsNew );
         pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_XOR, nLitsNew );
         for ( i = 0; i < pObjNew->nFans; i++ )
         {
@@ -602,7 +637,7 @@ int Kit_DsdExpandNode_rec( Kit_DsdNtk_t * pNew, Kit_DsdNtk_t * p, int iLit )
         }
     }
     // if the incoming phase is complemented, absorb it into the prime node
-    if ( fCompl )
+    if ( Kit_DsdLitIsCompl(iLit) )
         Kit_TruthNot( pTruthNew, pTruthNew, pObj->nFans );
     return Kit_DsdVar2Lit( pObjNew->Id, 0 );
 }
@@ -655,46 +690,48 @@ Kit_DsdNtk_t * Kit_DsdExpand( Kit_DsdNtk_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Kit_DsdCompSort( int pPrios[], unsigned uSupps[], int piLitsNew[], int nVars )
+void Kit_DsdCompSort( int pPrios[], unsigned uSupps[], unsigned char * piLits, int nVars, int piLitsRes[] )
 {
-    int nSuppSizes[16], Priority[16], pOrder[16], Temp[16];
-    int i, k, iVarBest, SuppMax, PrioMin;
+    int nSuppSizes[16], Priority[16], pOrder[16];
+    int i, k, iVarBest, SuppMax, PrioMax;
     // compute support sizes and priorities of the components
     for ( i = 0; i < nVars; i++ )
     {
-        Temp[i] = piLitsNew[i];
+        assert( uSupps[i] );
         pOrder[i] = i;
-        Priority[i] = 16;
-        nSuppSizes[i] = Kit_WordCountOnes(uSupps[i]);
+        Priority[i] = KIT_INFINITY;
         for ( k = 0; k < 16; k++ )
             if ( uSupps[i] & (1 << k) )
                 Priority[i] = KIT_MIN( Priority[i], pPrios[k] );
         assert( Priority[i] != 16 );
+        nSuppSizes[i] = Kit_WordCountOnes(uSupps[i]);
     }
-    // find the component by with largest size and smallest priority
+    // sort the components by pririty
+    Extra_BubbleSort( pOrder, Priority, nVars, 0 );
+    // find the component by with largest size and lowest priority
     iVarBest = -1;
-    SuppMax = 0;
-    PrioMin = 16;
+    SuppMax  = 0;
+    PrioMax  = 0;
     for ( i = 0; i < nVars; i++ )
     {
-        if ( SuppMax < nSuppSizes[i] || (SuppMax == nSuppSizes[i] && PrioMin > Priority[i]) )
+        if ( SuppMax < nSuppSizes[i] || (SuppMax == nSuppSizes[i] && PrioMax < Priority[i]) )
         {
-            SuppMax = nSuppSizes[i];
-            PrioMin = Priority[i];
+            SuppMax  = nSuppSizes[i];
+            PrioMax  = Priority[i];
             iVarBest = i;
         }
     }
-    // sort the components by pririty
-    Extra_BubbleSort( pOrder, Priority, nVars, 1 );
+    assert( iVarBest != -1 );
     // copy the resulting literals
     k = 0;
-    piLitsNew[k++] = piLitsNew[iVarBest];
+    piLitsRes[k++] = piLits[iVarBest];
     for ( i = 0; i < nVars; i++ )
     {
         if ( pOrder[i] == iVarBest )
             continue;
-        piLitsNew[k++] = piLitsNew[pOrder[i]];
+        piLitsRes[k++] = piLits[pOrder[i]];
     }
+    assert( k == nVars );
 }
 
 /**Function*************************************************************
@@ -713,76 +750,52 @@ int Kit_DsdShrink_rec( Kit_DsdNtk_t * pNew, Kit_DsdNtk_t * p, int iLit, int pPri
     Kit_DsdObj_t * pObj, * pObjNew;
     unsigned * pTruth, * pTruthNew;
     unsigned i, piLitsNew[16], uSupps[16];
-    int fCompl, iLitFanin, iLitNew;
-
-    // remember the complement
-    fCompl = Kit_DsdLitIsCompl(iLit); 
-    iLit = Kit_DsdLitRegular(iLit); 
-    assert( !Kit_DsdLitIsCompl(iLit) );
+    int iLitFanin, iLitNew;
 
     // consider the case of simple gate
     pObj = Kit_DsdNtkObj( p, Kit_DsdLit2Var(iLit) );
     if ( pObj == NULL )
-        return Kit_DsdLitNotCond( iLit, fCompl );
+        return iLit;
     if ( pObj->Type == KIT_DSD_AND )
     {
-        if ( pObj->nFans == 2 )
+        // get the supports
+        Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
+            uSupps[i] = Kit_DsdLitSupport( p, iLitFanin );
+        // put the largest component last
+        // sort other components in the decreasing order of priority of their vars
+        Kit_DsdCompSort( pPrios, uSupps, pObj->pFans, pObj->nFans, piLitsNew );
+        // construct the two-input node network
+        iLitNew = Kit_DsdShrink_rec( pNew, p, piLitsNew[0], pPrios );
+        for ( i = 1; i < pObj->nFans; i++ )
         {
             pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_AND, 2 );
-            pObjNew->pFans[0] = Kit_DsdShrink_rec( pNew, p, pObj->pFans[0], pPrios );
-            pObjNew->pFans[1] = Kit_DsdShrink_rec( pNew, p, pObj->pFans[1], pPrios );
-        }
-        else
-        {
-            // get the supports
-            Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
-            {
-                piLitsNew[i] = iLitFanin;
-                uSupps[i] = Kit_DsdLitSupport( p, iLitFanin );
-            }
-            // put the largest component first
-            // sort other components in the increasing order of the highest variable
-            Kit_DsdCompSort( pPrios, uSupps, piLitsNew, pObj->nFans );
-            iLitNew = Kit_DsdShrink_rec( pNew, p, piLitsNew[0], pPrios );
-            for ( i = 1; i < pObj->nFans; i++ )
-            {
-                pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_AND, 2 );
-                pObjNew->pFans[0] = iLitNew;
-                pObjNew->pFans[1] = Kit_DsdShrink_rec( pNew, p, piLitsNew[i], pPrios );
-                iLitNew = Kit_DsdVar2Lit( pObjNew->Id, 0 );
-            }
+            pObjNew->pFans[0] = Kit_DsdShrink_rec( pNew, p, piLitsNew[i], pPrios );
+            pObjNew->pFans[1] = iLitNew;
+            iLitNew = Kit_DsdVar2Lit( pObjNew->Id, 0 );
         }
-        return Kit_DsdVar2Lit( pObjNew->Id, fCompl );
+        return Kit_DsdVar2Lit( pObjNew->Id, Kit_DsdLitIsCompl(iLit) );
     }
     if ( pObj->Type == KIT_DSD_XOR )
     {
-        if ( pObj->nFans == 2 )
+        // get the supports
+        Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
         {
-            pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_XOR, 2 );
-            pObjNew->pFans[0] = Kit_DsdShrink_rec( pNew, p, pObj->pFans[0], pPrios );
-            pObjNew->pFans[1] = Kit_DsdShrink_rec( pNew, p, pObj->pFans[1], pPrios );
+            assert( !Kit_DsdLitIsCompl(iLitFanin) );
+            uSupps[i] = Kit_DsdLitSupport( p, iLitFanin );
         }
-        else
+        // put the largest component last
+        // sort other components in the decreasing order of priority of their vars
+        Kit_DsdCompSort( pPrios, uSupps, pObj->pFans, pObj->nFans, piLitsNew );
+        // construct the two-input node network
+        iLitNew = Kit_DsdShrink_rec( pNew, p, piLitsNew[0], pPrios );
+        for ( i = 1; i < pObj->nFans; i++ )
         {
-            // get the supports
-            Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
-            {
-                piLitsNew[i] = iLitFanin;
-                uSupps[i] = Kit_DsdLitSupport( p, iLitFanin );
-            }
-            // put the largest component first
-            // sort other components in the increasing order of the highest variable
-            Kit_DsdCompSort( pPrios, uSupps, piLitsNew, pObj->nFans );
-            iLitNew = Kit_DsdShrink_rec( pNew, p, piLitsNew[0], pPrios );
-            for ( i = 1; i < pObj->nFans; i++ )
-            {
-                pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_XOR, 2 );
-                pObjNew->pFans[0] = iLitNew;
-                pObjNew->pFans[1] = Kit_DsdShrink_rec( pNew, p, piLitsNew[i], pPrios );
-                iLitNew = Kit_DsdVar2Lit( pObjNew->Id, 0 );
-            }
+            pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_XOR, 2 );
+            pObjNew->pFans[0] = Kit_DsdShrink_rec( pNew, p, piLitsNew[i], pPrios );
+            pObjNew->pFans[1] = iLitNew;
+            iLitNew = Kit_DsdVar2Lit( pObjNew->Id, 0 );
         }
-        return Kit_DsdVar2Lit( pObjNew->Id, fCompl );
+        return Kit_DsdVar2Lit( pObjNew->Id, Kit_DsdLitIsCompl(iLit) );
     }
     assert( pObj->Type == KIT_DSD_PRIME );
 
@@ -804,7 +817,7 @@ int Kit_DsdShrink_rec( Kit_DsdNtk_t * pNew, Kit_DsdNtk_t * p, int iLit, int pPri
         }
     }
     // if the incoming phase is complemented, absorb it into the prime node
-    if ( fCompl )
+    if ( Kit_DsdLitIsCompl(iLit) )
         Kit_TruthNot( pTruthNew, pTruthNew, pObj->nFans );
     return Kit_DsdVar2Lit( pObjNew->Id, 0 );
 }
@@ -877,22 +890,26 @@ void Kit_DsdRotate( Kit_DsdNtk_t * p, int pFreqs[] )
             Weights[k] = 0;
             for ( v = 0; v < 16; v++ )
                 if ( uSuppFanin & (1 << v) )
-                    Weights[k] += pFreqs[v];
+                    Weights[k] += pFreqs[v] - 1;
         }
         // find the most frequent fanin
-        WeightMax = FaninMax = 0;
+        WeightMax = 0; 
+        FaninMax = -1;
         for ( k = 0; k < pObj->nFans; k++ )
             if ( WeightMax < Weights[k] )
             {
                 WeightMax = Weights[k];
                 FaninMax = k;
             }
-        assert( k < pObj->nFans );
+        // no need to reorder if there are no frequent fanins
+        if ( FaninMax == -1 )
+            continue;
         // move the fanins number k to the first place
         nSwaps = 0;
         pIn = Kit_DsdObjTruth(pObj);
-        pOut = p->pSupps;
-        for ( v = k-1; v >= 0; v-- )
+        pOut = p->pMem;
+//        for ( v = FaninMax; v < ((int)pObj->nFans)-1; v++ )
+        for ( v = FaninMax-1; v >= 0; v-- )
         {
             // swap the fanins
             Temp = pObj->pFans[v];
@@ -903,8 +920,8 @@ void Kit_DsdRotate( Kit_DsdNtk_t * p, int pFreqs[] )
             pTemp = pIn; pIn = pOut; pOut = pTemp;
             nSwaps++;
         }
-        if ( nSwaps & 1)
-            Kit_TruthCopy( pIn, pOut, pObj->nFans );
+        if ( nSwaps & 1 )
+            Kit_TruthCopy( pOut, pIn, pObj->nFans );
     }    
 }
 
@@ -919,19 +936,53 @@ void Kit_DsdRotate( Kit_DsdNtk_t * p, int pFreqs[] )
   SeeAlso     []
 
 ***********************************************************************/
-void Kit_DsdGetSupports( Kit_DsdNtk_t * p )
+unsigned Kit_DsdGetSupports_rec( Kit_DsdNtk_t * p, int iLit )
 {
     Kit_DsdObj_t * pObj;
     unsigned uSupport, k;
-    int iFaninLit, i;
+    int iFaninLit;
+    pObj = Kit_DsdNtkObj( p, Kit_DsdLit2Var(iLit) );
+    if ( pObj == NULL )
+        return Kit_DsdLitSupport( p, iLit );
+    uSupport = 0;
+    Kit_DsdObjForEachFanin( p, pObj, iFaninLit, k )
+        uSupport |= Kit_DsdGetSupports_rec( p, iFaninLit );
+    p->pSupps[pObj->Id - p->nVars] = uSupport;
+    assert( uSupport <= 0xFFFF );
+    return uSupport;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compute the support.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_DsdGetSupports( Kit_DsdNtk_t * p )
+{
+    Kit_DsdObj_t * pRoot;
+    assert( p->pSupps == NULL );
     p->pSupps = ALLOC( unsigned, p->nNodes );
-    Kit_DsdNtkForEachObj( p, pObj, i )
+    // consider simple special cases
+    pRoot = Kit_DsdNtkRoot(p);
+    if ( pRoot->Type == KIT_DSD_CONST1 )
     {
-        uSupport = 0;
-        Kit_DsdObjForEachFanin( p, pObj, iFaninLit, k )
-            uSupport |= Kit_DsdLitSupport( p, iFaninLit );
-        p->pSupps[pObj->Id - p->nVars] = uSupport;
-    }    
+        assert( p->nNodes == 1 );
+        p->pSupps[0] = 0;
+    }
+    if ( pRoot->Type == KIT_DSD_VAR )
+    {
+        assert( p->nNodes == 1 );
+        p->pSupps[0] = Kit_DsdLitSupport( p, pRoot->pFans[0] );
+    }
+    else
+        Kit_DsdGetSupports_rec( p, p->Root );
+    assert( p->pSupps[0] <= 0xFFFF );
 }
 
 /**Function*************************************************************
@@ -1772,6 +1823,251 @@ int Kit_DsdCofactoring( unsigned * pTruth, int nVars, int * pCofVars, int nLimit
     return nStep;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Canonical decomposition into completely DSD-structure.]
+
+  Description [Returns the number of cofactoring steps. Also returns
+  the cofactoring variables in pVars.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_DsdPrintCofactors( unsigned * pTruth, int nVars, int nCofLevel, int fVerbose )
+{
+    Kit_DsdNtk_t * ppNtks[32] = {0}, * pTemp;
+    unsigned * ppCofs[5][16];
+    int piCofVar[5];
+    int nPrimeSizeMax, nPrimeSizeCur, nSuppSizeMax;
+    int i, k, v1, v2, v3, v4, s, nSteps, nSize, nMemSize;
+    assert( nCofLevel < 5 );
+
+    // print the function
+    ppNtks[0] = Kit_DsdDecompose( pTruth, nVars );
+    ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] );
+    Kit_DsdNtkFree( pTemp );
+    if ( fVerbose )
+        Kit_DsdPrint( stdout, ppNtks[0] );
+    Kit_DsdNtkFree( ppNtks[0] );
+
+    // allocate storage for cofactors
+    nMemSize = Kit_TruthWordNum(nVars);
+    ppCofs[0][0] = ALLOC( unsigned, 80 * nMemSize );
+    nSize = 0;
+    for ( i = 0; i <  5; i++ )
+    for ( k = 0; k < 16; k++ )
+        ppCofs[i][k] = ppCofs[0][0] + nMemSize * nSize++;
+    assert( nSize == 80 );
+
+    // copy the function
+    Kit_TruthCopy( ppCofs[0][0], pTruth, nVars );
+
+    if ( nCofLevel == 1 )
+    for ( v1 = 0; v1 < nVars; v1++ )
+    {
+        nSteps = 0;
+        piCofVar[nSteps++] = v1;
+
+        printf( "    Variables { " );
+        for ( i = 0; i < nSteps; i++ )
+            printf( "%c ", 'a' + piCofVar[i] );
+        printf( "}\n" );
+
+        // single cofactors
+        for ( s = 1; s <= nSteps; s++ )
+        {
+            for ( k = 0; k < s; k++ )
+            {
+                nSize = (1 << k);
+                for ( i = 0; i < nSize; i++ )
+                {
+                    Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] );
+                    Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] );
+                }
+            }
+        }
+        // compute DSD networks
+        nSize = (1 << nSteps);
+        nPrimeSizeMax = 0;
+        nSuppSizeMax = 0;
+        for ( i = 0; i < nSize; i++ )
+        {
+            ppNtks[i] = Kit_DsdDecompose( ppCofs[nSteps][i], nVars );
+            ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] );
+            Kit_DsdNtkFree( pTemp );
+            if ( fVerbose )
+            {
+                printf( "Cof%d%d: ", nSteps, i );
+                Kit_DsdPrint( stdout, ppNtks[i] );
+            }
+            // compute the largest non-decomp block
+            nPrimeSizeCur  = Kit_DsdNonDsdSizeMax(ppNtks[i]);
+            nPrimeSizeMax  = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur );
+            Kit_DsdNtkFree( ppNtks[i] );
+            nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nSteps][i], nVars );
+        }
+        printf( "Max = %2d. Supps = %2d.\n", nPrimeSizeMax, nSuppSizeMax );
+    }
+
+    if ( nCofLevel == 2 )
+    for ( v1 = 0; v1 < nVars; v1++ )
+    for ( v2 = v1+1; v2 < nVars; v2++ )
+    {
+        nSteps = 0;
+        piCofVar[nSteps++] = v1;
+        piCofVar[nSteps++] = v2;
+
+        printf( "    Variables { " );
+        for ( i = 0; i < nSteps; i++ )
+            printf( "%c ", 'a' + piCofVar[i] );
+        printf( "}\n" );
+
+        // single cofactors
+        for ( s = 1; s <= nSteps; s++ )
+        {
+            for ( k = 0; k < s; k++ )
+            {
+                nSize = (1 << k);
+                for ( i = 0; i < nSize; i++ )
+                {
+                    Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] );
+                    Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] );
+                }
+            }
+        }
+        // compute DSD networks
+        nSize = (1 << nSteps);
+        nPrimeSizeMax = 0;
+        nSuppSizeMax = 0;
+        for ( i = 0; i < nSize; i++ )
+        {
+            ppNtks[i] = Kit_DsdDecompose( ppCofs[nSteps][i], nVars );
+            ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] );
+            Kit_DsdNtkFree( pTemp );
+            if ( fVerbose )
+            {
+                printf( "Cof%d%d: ", nSteps, i );
+                Kit_DsdPrint( stdout, ppNtks[i] );
+            }
+            // compute the largest non-decomp block
+            nPrimeSizeCur  = Kit_DsdNonDsdSizeMax(ppNtks[i]);
+            nPrimeSizeMax  = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur );
+            Kit_DsdNtkFree( ppNtks[i] );
+            nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nSteps][i], nVars );
+        }
+        printf( "Max = %2d. Supps = %2d.\n", nPrimeSizeMax, nSuppSizeMax );
+    }
+
+    if ( nCofLevel == 3 )
+    for ( v1 = 0; v1 < nVars; v1++ )
+    for ( v2 = v1+1; v2 < nVars; v2++ )
+    for ( v3 = v2+1; v3 < nVars; v3++ )
+    {
+        nSteps = 0;
+        piCofVar[nSteps++] = v1;
+        piCofVar[nSteps++] = v2;
+        piCofVar[nSteps++] = v3;
+
+        printf( "    Variables { " );
+        for ( i = 0; i < nSteps; i++ )
+            printf( "%c ", 'a' + piCofVar[i] );
+        printf( "}\n" );
+
+        // single cofactors
+        for ( s = 1; s <= nSteps; s++ )
+        {
+            for ( k = 0; k < s; k++ )
+            {
+                nSize = (1 << k);
+                for ( i = 0; i < nSize; i++ )
+                {
+                    Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] );
+                    Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] );
+                }
+            }
+        }
+        // compute DSD networks
+        nSize = (1 << nSteps);
+        nPrimeSizeMax = 0;
+        nSuppSizeMax = 0;
+        for ( i = 0; i < nSize; i++ )
+        {
+            ppNtks[i] = Kit_DsdDecompose( ppCofs[nSteps][i], nVars );
+            ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] );
+            Kit_DsdNtkFree( pTemp );
+            if ( fVerbose )
+            {
+                printf( "Cof%d%d: ", nSteps, i );
+                Kit_DsdPrint( stdout, ppNtks[i] );
+            }
+            // compute the largest non-decomp block
+            nPrimeSizeCur  = Kit_DsdNonDsdSizeMax(ppNtks[i]);
+            nPrimeSizeMax  = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur );
+            Kit_DsdNtkFree( ppNtks[i] );
+            nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nSteps][i], nVars );
+        }
+        printf( "Max = %2d. Supps = %2d.\n", nPrimeSizeMax, nSuppSizeMax );
+    }
+
+    if ( nCofLevel == 4 )
+    for ( v1 = 0; v1 < nVars; v1++ )
+    for ( v2 = v1+1; v2 < nVars; v2++ )
+    for ( v3 = v2+1; v3 < nVars; v3++ )
+    for ( v4 = v3+1; v4 < nVars; v4++ )
+    {
+        nSteps = 0;
+        piCofVar[nSteps++] = v1;
+        piCofVar[nSteps++] = v2;
+        piCofVar[nSteps++] = v3;
+        piCofVar[nSteps++] = v4;
+
+        printf( "    Variables { " );
+        for ( i = 0; i < nSteps; i++ )
+            printf( "%c ", 'a' + piCofVar[i] );
+        printf( "}\n" );
+
+        // single cofactors
+        for ( s = 1; s <= nSteps; s++ )
+        {
+            for ( k = 0; k < s; k++ )
+            {
+                nSize = (1 << k);
+                for ( i = 0; i < nSize; i++ )
+                {
+                    Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] );
+                    Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] );
+                }
+            }
+        }
+        // compute DSD networks
+        nSize = (1 << nSteps);
+        nPrimeSizeMax = 0;
+        nSuppSizeMax = 0;
+        for ( i = 0; i < nSize; i++ )
+        {
+            ppNtks[i] = Kit_DsdDecompose( ppCofs[nSteps][i], nVars );
+            ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] );
+            Kit_DsdNtkFree( pTemp );
+            if ( fVerbose )
+            {
+                printf( "Cof%d%d: ", nSteps, i );
+                Kit_DsdPrint( stdout, ppNtks[i] );
+            }
+            // compute the largest non-decomp block
+            nPrimeSizeCur  = Kit_DsdNonDsdSizeMax(ppNtks[i]);
+            nPrimeSizeMax  = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur );
+            Kit_DsdNtkFree( ppNtks[i] );
+            nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nSteps][i], nVars );
+        }
+        printf( "Max = %2d. Supps = %2d.\n", nPrimeSizeMax, nSuppSizeMax );
+    }
+
+
+    free( ppCofs[0][0] );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/lpk/lpk.h b/src/opt/lpk/lpk.h
new file mode 100644
index 00000000..092b43e1
--- /dev/null
+++ b/src/opt/lpk/lpk.h
@@ -0,0 +1,82 @@
+/**CFile****************************************************************
+
+  FileName    [lpk.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Fast Boolean matching for LUT structures.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: lpk.h,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __LPK_H__
+#define __LPK_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif 
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Lpk_Par_t_ Lpk_Par_t;
+struct Lpk_Par_t_
+{
+    // user-controlled parameters
+    int               nLutsMax;      // (N) the maximum number of LUTs in the structure
+    int               nLutsOver;     // (Q) the maximum number of LUTs not in the MFFC
+    int               nVarsShared;   // (S) the maximum number of shared variables (crossbars)
+    int               nGrowthLevel;  // (L) the maximum increase in the node level after resynthesis
+    int               fSatur;        // iterate till saturation
+    int               fZeroCost;     // accept zero-cost replacements
+    int               fVerbose;      // the verbosiness flag
+    int               fVeryVerbose;  // additional verbose info printout
+    // internal parameters
+    int               nLutSize;      // (K) the LUT size (determined by the input network)
+    int               nVarsMax;      // (V) the largest number of variables: V = N * (K-1) + 1
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                           ITERATORS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== lpkCore.c ========================================================*/
+extern int     Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars );
+
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/opt/lpk/lpkCore.c b/src/opt/lpk/lpkCore.c
new file mode 100644
index 00000000..cbd971e3
--- /dev/null
+++ b/src/opt/lpk/lpkCore.c
@@ -0,0 +1,280 @@
+/**CFile****************************************************************
+
+  FileName    [lpkCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Fast Boolean matching for LUT structures.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: lpkCore.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "lpkInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if at least one entry has changed.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Lpk_NodeHasChanged( Lpk_Man_t * p, int iNode )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pTemp;
+    int i;
+    vNodes = Vec_VecEntry( p->vVisited, iNode );
+    if ( Vec_PtrSize(vNodes) == 0 )
+        return 1;
+    Vec_PtrForEachEntry( vNodes, pTemp, i )
+    {
+        // check if the node has changed
+        pTemp = Abc_NtkObj( p->pNtk, (int)pTemp );
+        if ( pTemp == NULL )
+            return 1;
+        // check if the number of fanouts has changed
+//        if ( Abc_ObjFanoutNum(pTemp) != (int)Vec_PtrEntry(vNodes, i+1) )
+//            return 1;
+        i++;
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs resynthesis for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Lpk_ResynthesizeNode( Lpk_Man_t * p )
+{
+    Kit_DsdNtk_t * pDsdNtk;
+    Lpk_Cut_t * pCut;
+    unsigned * pTruth;
+    void * pDsd = NULL;
+    int i, RetValue, clk;
+
+    Lpk_Cut_t * pCutMax;
+
+    // compute the cuts
+clk = clock();
+    if ( !Lpk_NodeCuts( p ) )
+    {
+p->timeCuts += clock() - clk;
+        return 0;
+    }
+p->timeCuts += clock() - clk;
+
+    // find the max volume cut
+    pCutMax = NULL;
+    for ( i = 0; i < p->nEvals; i++ )
+    {
+        pCut = p->pCuts + p->pEvals[i];
+        if ( pCutMax == NULL || pCutMax->nNodes < pCut->nNodes )
+            pCutMax = pCut;
+    }
+    assert( pCutMax != NULL );
+    
+
+    if ( p->pPars->fVeryVerbose )
+    printf( "Node %5d : Mffc size = %5d. Cuts = %5d.\n", p->pObj->Id, p->nMffc, p->nEvals );
+    // try the good cuts
+    p->nCutsTotal  += p->nCuts;
+    p->nCutsUseful += p->nEvals;
+    for ( i = 0; i < p->nEvals; i++ )
+    {
+        // get the cut
+        pCut = p->pCuts + p->pEvals[i];
+
+        if ( pCut != pCutMax )
+            continue;
+
+        // compute the truth table
+clk = clock();
+        pTruth = Lpk_CutTruth( p, pCut );
+p->timeTruth += clock() - clk;
+
+clk = clock();
+        pDsdNtk = Kit_DsdDeriveNtk( pTruth, pCut->nLeaves, p->pPars->nLutSize );
+p->timeEval += clock() - clk;
+
+        if ( Kit_DsdNtkRoot(pDsdNtk)->nFans == 16 ) // skip 16-input non-DSD because ISOP will not work
+        {
+            Kit_DsdNtkFree( pDsdNtk );
+            continue;
+        }
+
+        if ( p->pPars->fVeryVerbose )
+        {
+            printf( "  C%02d: L= %2d/%2d  V= %2d/%d  N= %d  W= %4.2f  ", 
+                i, pCut->nLeaves, Extra_TruthSupportSize(pTruth, pCut->nLeaves), pCut->nNodes, pCut->nNodesDup, pCut->nLuts, pCut->Weight );
+            Kit_DsdPrint( stdout, pDsdNtk );
+        }
+
+        // update the network
+clk = clock();
+        RetValue = Lpk_CutExplore( p, pCut, pDsdNtk );
+        Kit_DsdNtkFree( pDsdNtk );
+p->timeMap += clock() - clk;
+        if ( RetValue )
+            break;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs resynthesis for one network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
+{
+    ProgressBar * pProgress;
+    Lpk_Man_t * p;
+    Abc_Obj_t * pObj;
+    double Delta;
+    int i, Iter, nNodes, nNodesPrev, clk = clock();
+    assert( Abc_NtkIsLogic(pNtk) );
+
+    // get the number of inputs
+    pPars->nLutSize = Abc_NtkGetFaninMax( pNtk );
+    // adjust the number of crossbars based on LUT size
+    if ( pPars->nVarsShared > pPars->nLutSize - 2 )
+        pPars->nVarsShared = pPars->nLutSize - 2;
+    // get the max number of LUTs tried
+    pPars->nVarsMax = pPars->nLutsMax * (pPars->nLutSize - 1) + 1; // V = N * (K-1) + 1
+    while ( pPars->nVarsMax > 16 )
+    {
+        pPars->nLutsMax--;
+        pPars->nVarsMax = pPars->nLutsMax * (pPars->nLutSize - 1) + 1;
+
+    }
+    if ( pPars->fVerbose )
+    {
+        printf( "Resynthesis for %d %d-LUTs with %d non-MFFC LUTs, %d crossbars, and %d-input cuts.\n",
+            pPars->nLutsMax, pPars->nLutSize, pPars->nLutsOver, pPars->nVarsShared, pPars->nVarsMax );
+    }
+ 
+    // convert logic to AIGs
+    Abc_NtkToAig( pNtk );
+
+    // start the manager
+    p = Lpk_ManStart( pPars );
+    p->pNtk = pNtk;
+    p->nNodesTotal = Abc_NtkNodeNum(pNtk);
+    p->vLevels = Vec_VecStart( 3 * Abc_NtkLevel(pNtk) ); // computes levels of all nodes
+    if ( p->pPars->fSatur )
+        p->vVisited = Vec_VecStart( 0 );
+
+    // iterate over the network
+    nNodesPrev = p->nNodesTotal;
+    for ( Iter = 1; ; Iter++ )
+    {
+        // expand storage for changed nodes
+        if ( p->pPars->fSatur )
+            Vec_VecExpand( p->vVisited, Abc_NtkObjNumMax(pNtk) + 1 );
+
+        // consider all nodes
+        nNodes = Abc_NtkObjNumMax(pNtk);
+        if ( !pPars->fVeryVerbose )
+            pProgress = Extra_ProgressBarStart( stdout, nNodes );
+        Abc_NtkForEachNode( pNtk, pObj, i )
+        {
+            // skip all except the final node
+//            if ( !Abc_ObjIsCo(Abc_ObjFanout0(pObj)) )
+//                continue;
+
+            if ( i >= nNodes )
+                break;
+            if ( !pPars->fVeryVerbose )
+                Extra_ProgressBarUpdate( pProgress, i, NULL );
+            // skip the nodes that did not change
+            if ( p->pPars->fSatur && !Lpk_NodeHasChanged(p, pObj->Id) )
+                continue;
+            // resynthesize
+            p->pObj = pObj;
+            Lpk_ResynthesizeNode( p );
+
+            if ( p->nChanges == 3 )
+                break;
+        }
+        if ( !pPars->fVeryVerbose )
+            Extra_ProgressBarStop( pProgress );
+
+        // check the increase
+        Delta = 100.00 * (nNodesPrev - Abc_NtkNodeNum(pNtk)) / p->nNodesTotal;
+        if ( Delta < 0.05 )
+            break;
+        nNodesPrev = Abc_NtkNodeNum(pNtk);
+        if ( !p->pPars->fSatur )
+            break;
+
+        break;
+    }
+
+    if ( pPars->fVerbose )
+    {
+        printf( "N = %5d (%3d)  Cut = %5d (%4d)  Change = %5d  Gain = %5d  (%5.2f %%) Iter = %2d\n", 
+            p->nNodesTotal, p->nNodesOver, p->nCutsTotal, p->nCutsUseful, p->nChanges, p->nGainTotal, 100.0 * p->nGainTotal / p->nNodesTotal, Iter );
+        printf( "Non_DSD blocks: " );
+        for ( i = 3; i <= pPars->nVarsMax; i++ )
+            if ( p->nBlocks[i] )
+                printf( "%d=%d  ", i, p->nBlocks[i] );
+        printf( "\n" );
+        p->timeTotal = clock() - clk;
+        p->timeOther = p->timeTotal - p->timeCuts - p->timeTruth - p->timeEval - p->timeMap;
+        PRTP( "Cuts  ", p->timeCuts,  p->timeTotal );
+        PRTP( "Truth ", p->timeTruth, p->timeTotal );
+        PRTP( "Eval  ", p->timeEval,  p->timeTotal );
+        PRTP( "Map   ", p->timeMap,   p->timeTotal );
+        PRTP( "Other ", p->timeOther, p->timeTotal );
+        PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
+    }
+
+    Lpk_ManStop( p );
+    // check the resulting network
+    if ( !Abc_NtkCheck( pNtk ) )
+    {
+        printf( "Lpk_Resynthesize: The network check has failed.\n" );
+        return 0;
+    }
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/lpk/lpkCut.c b/src/opt/lpk/lpkCut.c
new file mode 100644
index 00000000..251ec829
--- /dev/null
+++ b/src/opt/lpk/lpkCut.c
@@ -0,0 +1,584 @@
+/**CFile****************************************************************
+
+  FileName    [lpkCut.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Fast Boolean matching for LUT structures.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: lpkCut.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "lpkInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the truth able of one cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Lpk_CutTruth_rec( Hop_Man_t * pMan, Hop_Obj_t * pObj, int nVars, Vec_Ptr_t * vTtNodes, int * iCount )
+{
+    unsigned * pTruth, * pTruth0, * pTruth1;
+    assert( !Hop_IsComplement(pObj) );
+    if ( pObj->pData )
+    {
+        assert( ((unsigned)pObj->pData) & 0xffff0000 );
+        return pObj->pData;
+    }
+    // get the plan for a new truth table
+    pTruth = Vec_PtrEntry( vTtNodes, (*iCount)++ );
+    if ( Hop_ObjIsConst1(pObj) )
+        Extra_TruthFill( pTruth, nVars );
+    else
+    {
+        assert( Hop_ObjIsAnd(pObj) );
+        // compute the truth tables of the fanins
+        pTruth0 = Lpk_CutTruth_rec( pMan, Hop_ObjFanin0(pObj), nVars, vTtNodes, iCount );
+        pTruth1 = Lpk_CutTruth_rec( pMan, Hop_ObjFanin1(pObj), nVars, vTtNodes, iCount );
+        // creat the truth table of the node
+        Extra_TruthAndPhase( pTruth, pTruth0, pTruth1, nVars, Hop_ObjFaninC0(pObj), Hop_ObjFaninC1(pObj) );
+    }
+    pObj->pData = pTruth;
+    return pTruth;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the truth able of one cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut )
+{
+    Hop_Man_t * pManHop = p->pNtk->pManFunc;
+    Hop_Obj_t * pObjHop;
+    Abc_Obj_t * pObj, * pFanin;
+    unsigned * pTruth;
+    int i, k, iCount = 0;
+//    Lpk_NodePrintCut( p, pCut );
+
+    // initialize the leaves
+    Lpk_CutForEachLeaf( p->pNtk, pCut, pObj, i )
+        pObj->pCopy = Vec_PtrEntry( p->vTtElems, i );
+
+    // construct truth table in the topological order
+    Lpk_CutForEachNodeReverse( p->pNtk, pCut, pObj, i )
+    {
+        // get the local AIG
+        pObjHop = Hop_Regular(pObj->pData);
+        // clean the data field of the nodes in the AIG subgraph
+        Hop_ObjCleanData_rec( pObjHop );
+        // set the initial truth tables at the fanins
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+        {
+            assert( ((unsigned)pFanin->pCopy) & 0xffff0000 );
+            Hop_ManPi( pManHop, k )->pData = pFanin->pCopy;
+        }
+        // compute the truth table of internal nodes
+        pTruth = Lpk_CutTruth_rec( pManHop, pObjHop, pCut->nLeaves, p->vTtNodes, &iCount );
+        if ( Hop_IsComplement(pObj->pData) )
+            Extra_TruthNot( pTruth, pTruth, pCut->nLeaves );
+        // set the truth table at the node
+        pObj->pCopy = (Abc_Obj_t *)pTruth;
+    }
+
+    return pTruth;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if at least one entry has changed.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Lpk_NodeRecordImpact( Lpk_Man_t * p )
+{
+    Lpk_Cut_t * pCut;
+    Vec_Ptr_t * vNodes = Vec_VecEntry( p->vVisited, p->pObj->Id );
+    Abc_Obj_t * pNode;
+    int i, k;
+    // collect the nodes that impact the given node
+    Vec_PtrClear( vNodes );
+    for ( i = 0; i < p->nCuts; i++ )
+    {
+        pCut = p->pCuts + i;
+        for ( k = 0; k < (int)pCut->nLeaves; k++ )
+        {
+            pNode = Abc_NtkObj( p->pNtk, pCut->pLeaves[k] );
+            if ( pNode->fMarkC )
+                continue;
+            pNode->fMarkC = 1;
+            Vec_PtrPush( vNodes, (void *)pNode->Id );
+            Vec_PtrPush( vNodes, (void *)Abc_ObjFanoutNum(pNode) );
+        }
+    }
+    // clear the marks
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+    {
+        pNode = Abc_NtkObj( p->pNtk, (int)pNode );
+        pNode->fMarkC = 0;
+        i++;
+    }
+//printf( "%d ", Vec_PtrSize(vNodes) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the cut has structural DSD.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Lpk_NodeCutsCheckDsd( Lpk_Man_t * p, Lpk_Cut_t * pCut )
+{
+    Abc_Obj_t * pObj, * pFanin;
+    int i, k, nCands, fLeavesOnly, RetValue;
+    assert( pCut->nLeaves > 0 );
+    // clear ref counters
+    memset( p->pRefs, 0, sizeof(int) * pCut->nLeaves );
+    // mark cut leaves
+    Lpk_CutForEachLeaf( p->pNtk, pCut, pObj, i )
+    {
+        assert( pObj->fMarkA == 0 );
+        pObj->fMarkA = 1;
+        pObj->pCopy = (void *)i;
+    }
+    // ref leaves pointed from the internal nodes
+    nCands = 0;
+    Lpk_CutForEachNode( p->pNtk, pCut, pObj, i )
+    {
+        fLeavesOnly = 1;
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+            if ( pFanin->fMarkA )
+                p->pRefs[(int)pFanin->pCopy]++;
+            else
+                fLeavesOnly = 0;
+        if ( fLeavesOnly )
+            p->pCands[nCands++] = pObj->Id;
+    }
+    // look at the nodes that only point to the leaves
+    RetValue = 0;
+    for ( i = 0; i < nCands; i++ )
+    {
+        pObj = Abc_NtkObj( p->pNtk, p->pCands[i] );
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+        {
+            assert( pFanin->fMarkA == 1 );
+            if ( p->pRefs[(int)pFanin->pCopy] > 1 )
+                break;
+        }
+        if ( k == Abc_ObjFaninNum(pObj) )
+        {
+            RetValue = 1;
+            break;
+        }
+    }
+    // unmark cut leaves
+    Lpk_CutForEachLeaf( p->pNtk, pCut, pObj, i )
+        pObj->fMarkA = 0;
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if pDom is contained in pCut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Lpk_NodeCutsOneDominance( Lpk_Cut_t * pDom, Lpk_Cut_t * pCut )
+{
+    int i, k;
+    for ( i = 0; i < (int)pDom->nLeaves; i++ )
+    {
+        for ( k = 0; k < (int)pCut->nLeaves; k++ )
+            if ( pDom->pLeaves[i] == pCut->pLeaves[k] )
+                break;
+        if ( k == (int)pCut->nLeaves ) // node i in pDom is not contained in pCut
+            return 0;
+    }
+    // every node in pDom is contained in pCut
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Check if the cut exists.]
+
+  Description [Returns 1 if the cut exists.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Lpk_NodeCutsOneFilter( Lpk_Cut_t * pCuts, int nCuts, Lpk_Cut_t * pCutNew )
+{
+    Lpk_Cut_t * pCut;
+    int i, k;
+    assert( pCutNew->uSign[0] || pCutNew->uSign[1] );
+    // try to find the cut
+    for ( i = 0; i < nCuts; i++ )
+    {
+        pCut = pCuts + i;
+        if ( pCut->nLeaves == 0 )
+            continue;
+        if ( pCut->nLeaves == pCutNew->nLeaves )
+        {
+            if ( pCut->uSign[0] == pCutNew->uSign[0] && pCut->uSign[1] == pCutNew->uSign[1] )
+            {
+                for ( k = 0; k < (int)pCutNew->nLeaves; k++ )
+                    if ( pCut->pLeaves[k] != pCutNew->pLeaves[k] )
+                        break;
+                if ( k == (int)pCutNew->nLeaves )
+                    return 1;
+            }
+            continue;
+        }
+        if ( pCut->nLeaves < pCutNew->nLeaves )
+        {
+            // skip the non-contained cuts
+            if ( (pCut->uSign[0] & pCutNew->uSign[0]) != pCut->uSign[0] )
+                continue;
+            if ( (pCut->uSign[1] & pCutNew->uSign[1]) != pCut->uSign[1] )
+                continue;
+            // check containment seriously
+            if ( Lpk_NodeCutsOneDominance( pCut, pCutNew ) )
+                return 1;
+            continue;
+        }
+        // check potential containment of other cut
+
+        // skip the non-contained cuts
+        if ( (pCut->uSign[0] & pCutNew->uSign[0]) != pCutNew->uSign[0] )
+            continue;
+        if ( (pCut->uSign[1] & pCutNew->uSign[1]) != pCutNew->uSign[1] )
+            continue;
+        // check containment seriously
+        if ( Lpk_NodeCutsOneDominance( pCutNew, pCut ) )
+            pCut->nLeaves = 0; // removed
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the given cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Lpk_NodePrintCut( Lpk_Man_t * p, Lpk_Cut_t * pCut, int fLeavesOnly )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    if ( !fLeavesOnly )
+        printf( "LEAVES:\n" );
+    Lpk_CutForEachLeaf( p->pNtk, pCut, pObj, i )
+        printf( "%d,", pObj->Id );
+    if ( !fLeavesOnly )
+    {
+        printf( "\nNODES:\n" );
+        Lpk_CutForEachNode( p->pNtk, pCut, pObj, i )
+        {
+            printf( "%d,", pObj->Id );
+            assert( Abc_ObjIsNode(pObj) );
+        }
+        printf( "\n" );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Set the cut signature.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Lpk_NodeCutSignature( Lpk_Cut_t * pCut )
+{
+    unsigned i;
+    pCut->uSign[0] = pCut->uSign[1] = 0;
+    for ( i = 0; i < pCut->nLeaves; i++ )
+    {
+        pCut->uSign[(pCut->pLeaves[i] & 32) > 0] |= (1 << (pCut->pLeaves[i] & 31));
+        if ( i != pCut->nLeaves - 1 )
+            assert( pCut->pLeaves[i] < pCut->pLeaves[i+1] );
+    }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the set of all cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Lpk_NodeCutsOne( Lpk_Man_t * p, Lpk_Cut_t * pCut, int Node )
+{
+    Lpk_Cut_t * pCutNew;
+    Abc_Obj_t * pObj, * pFanin;
+    int i, k, j, nLeavesNew;
+/*
+    printf( "Exploring cut " );
+    Lpk_NodePrintCut( p, pCut, 1 );
+    printf( "with node %d\n", Node );
+*/
+    // check if the cut can stand adding one more internal node
+    if ( pCut->nNodes == LPK_SIZE_MAX )
+        return;
+
+    // if the node is a PI, quit
+    pObj = Abc_NtkObj( p->pNtk, Node );
+    if ( Abc_ObjIsCi(pObj) )
+        return;
+    assert( Abc_ObjIsNode(pObj) );
+    assert( Abc_ObjFaninNum(pObj) <= p->pPars->nLutSize );
+
+    // if the node is not in the MFFC, check the limit
+    if ( !Abc_NodeIsTravIdCurrent(pObj) )
+    {
+        if ( (int)pCut->nNodesDup == p->pPars->nLutsOver )
+            return;
+        assert( (int)pCut->nNodesDup < p->pPars->nLutsOver );
+    }
+
+    // check the possibility of adding this node using the signature
+    nLeavesNew = pCut->nLeaves - 1;
+    Abc_ObjForEachFanin( pObj, pFanin, i )
+    {
+        if ( (pCut->uSign[(pFanin->Id & 32) > 0] & (1 << (pFanin->Id & 31))) )
+            continue;
+        if ( ++nLeavesNew > p->pPars->nVarsMax )
+            return;
+    }
+
+    // initialize the set of leaves to the nodes in the cut
+    assert( p->nCuts < LPK_CUTS_MAX );
+    pCutNew = p->pCuts + p->nCuts;
+/*
+if ( p->pObj->Id == 31 && Node == 38 && pCut->pNodes[0] == 31 && pCut->pNodes[1] == 34 && pCut->pNodes[2] == 35 )//p->nCuts == 48 )
+{
+    int x = 0;
+    printf( "Start:\n" );
+    Lpk_NodePrintCut( p, pCut );
+}
+*/
+    pCutNew->nLeaves = 0;
+    for ( i = 0; i < (int)pCut->nLeaves; i++ )
+        if ( pCut->pLeaves[i] != Node )
+            pCutNew->pLeaves[pCutNew->nLeaves++] = pCut->pLeaves[i];
+
+    // add new nodes
+    Abc_ObjForEachFanin( pObj, pFanin, i )
+    {
+        // find the place where this node belongs
+        for ( k = 0; k < (int)pCutNew->nLeaves; k++ )
+            if ( pCutNew->pLeaves[k] >= pFanin->Id )
+                break;
+        if ( k < (int)pCutNew->nLeaves && pCutNew->pLeaves[k] == pFanin->Id )
+            continue;
+        // check if there is room
+        if ( (int)pCutNew->nLeaves == p->pPars->nVarsMax )
+            return;
+        // move all the nodes
+        for ( j = pCutNew->nLeaves; j > k; j-- )
+            pCutNew->pLeaves[j] = pCutNew->pLeaves[j-1];
+        pCutNew->pLeaves[k] = pFanin->Id;
+        pCutNew->nLeaves++;
+        assert( pCutNew->nLeaves <= LPK_SIZE_MAX );
+
+    }
+/*
+    printf( "   Trying cut: " );
+    Lpk_NodePrintCut( p, pCutNew, 1 );
+    printf( "\n" );
+*/
+    // skip the contained cuts
+    Lpk_NodeCutSignature( pCutNew );
+    if ( Lpk_NodeCutsOneFilter( p->pCuts, p->nCuts, pCutNew ) )
+        return;
+
+
+    // update the set of internal nodes
+    assert( pCut->nNodes < LPK_SIZE_MAX );
+    memcpy( pCutNew->pNodes, pCut->pNodes, pCut->nNodes * sizeof(int) );
+    pCutNew->nNodes = pCut->nNodes;
+    pCutNew->pNodes[ pCutNew->nNodes++ ] = Node;
+
+    // add the marked node
+    pCutNew->nNodesDup = pCut->nNodesDup + !Abc_NodeIsTravIdCurrent(pObj);
+/*
+if ( p->pObj->Id == 31 && Node == 38 )//p->nCuts == 48 )
+{
+    int x = 0;
+    printf( "Finish:\n" );
+    Lpk_NodePrintCut( p, pCutNew );
+}
+*/
+    // add the cut to storage
+    assert( p->nCuts < LPK_CUTS_MAX );
+    p->nCuts++;
+
+    assert( pCut->nNodes <= p->nMffc + pCutNew->nNodesDup );
+/*
+    printf( "      Creating cut: " );
+    Lpk_NodePrintCut( p, pCutNew, 1 );
+    printf( "\n" );
+*/
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the set of all cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Lpk_NodeCuts( Lpk_Man_t * p )
+{
+    Lpk_Cut_t * pCut, * pCut2;
+    int i, k, Temp, nMffc, fChanges;
+
+    // mark the MFFC of the node with the current trav ID
+    nMffc = p->nMffc = Abc_NodeMffcLabel( p->pObj );
+    assert( nMffc > 0 );
+    if ( nMffc == 1 )
+        return 0;
+
+    // initialize the first cut
+    pCut = p->pCuts; p->nCuts = 1;
+    pCut->nNodes = 0; 
+    pCut->nNodesDup = 0;
+    pCut->nLeaves = 1;
+    pCut->pLeaves[0] = p->pObj->Id;
+    // assign the signature
+    Lpk_NodeCutSignature( pCut );
+
+    // perform the cut computation
+    for ( i = 0; i < p->nCuts; i++ )
+    {
+        pCut = p->pCuts + i;
+        if ( pCut->nLeaves == 0 )
+            continue;
+        // try to expand the fanins of this cut
+        for ( k = 0; k < (int)pCut->nLeaves; k++ )
+        {
+            // create a new cut
+            Lpk_NodeCutsOne( p, pCut, pCut->pLeaves[k] );
+            // quit if the number of cuts has exceeded the limit
+            if ( p->nCuts == LPK_CUTS_MAX )
+                break;
+        }
+        if ( p->nCuts == LPK_CUTS_MAX )
+            break;
+    }
+    if ( p->nCuts == LPK_CUTS_MAX ) 
+        p->nNodesOver++;
+
+    // record the impact of this node
+    if ( p->pPars->fSatur )
+        Lpk_NodeRecordImpact( p );
+
+    // compress the cuts by removing empty ones, those with negative Weight, and decomposable ones
+    p->nEvals = 0;
+    for ( i = 0; i < p->nCuts; i++ )
+    {
+        pCut = p->pCuts + i;
+        if ( pCut->nLeaves < 2 )
+            continue;
+        // compute the number of LUTs neede to implement this cut
+        // V = N * (K-1) + 1  ~~~~~  N = Ceiling[(V-1)/(K-1)] = (V-1)/(K-1) + [(V-1)%(K-1) > 0]
+        pCut->nLuts = (pCut->nLeaves-1)/(p->pPars->nLutSize-1) + ( (pCut->nLeaves-1)%(p->pPars->nLutSize-1) > 0 ); 
+        pCut->Weight = (float)1.0 * (pCut->nNodes - pCut->nNodesDup) / pCut->nLuts; //p->pPars->nLutsMax;
+        if ( pCut->Weight <= 1.0 )
+            continue;
+        pCut->fHasDsd = Lpk_NodeCutsCheckDsd( p, pCut );
+        if ( pCut->fHasDsd )
+            continue;
+        p->pEvals[p->nEvals++] = i;
+    }
+    if ( p->nEvals == 0 )
+        return 0;
+
+    // sort the cuts by Weight
+    do {
+        fChanges = 0;
+        for ( i = 0; i < p->nEvals - 1; i++ )
+        {
+            pCut = p->pCuts + p->pEvals[i];
+            pCut2 = p->pCuts + p->pEvals[i+1];
+            if ( pCut->Weight >= pCut2->Weight )
+                continue;
+            Temp = p->pEvals[i];
+            p->pEvals[i] = p->pEvals[i+1];
+            p->pEvals[i+1] = Temp;
+            fChanges = 1;
+        }
+    } while ( fChanges );
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/lpk/lpkInt.h b/src/opt/lpk/lpkInt.h
new file mode 100644
index 00000000..fe442302
--- /dev/null
+++ b/src/opt/lpk/lpkInt.h
@@ -0,0 +1,161 @@
+/**CFile****************************************************************
+
+  FileName    [lpkInt.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Fast Boolean matching for LUT structures.]
+
+  Synopsis    [Internal declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: lpkInt.h,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __LPK_INT_H__
+#define __LPK_INT_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif 
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "abc.h"
+#include "kit.h"
+#include "if.h"
+#include "lpk.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+#define LPK_SIZE_MAX             24     // the largest size of the function
+#define LPK_CUTS_MAX            512     // the largest number of cuts considered
+
+typedef struct Lpk_Man_t_ Lpk_Man_t;
+typedef struct Lpk_Cut_t_ Lpk_Cut_t;
+
+struct Lpk_Cut_t_
+{
+    unsigned     nLeaves       : 6;     // (L) the number of leaves
+    unsigned     nNodes        : 6;     // (M) the number of nodes
+    unsigned     nNodesDup     : 6;     // (Q) nodes outside of MFFC
+    unsigned     nLuts         : 6;     // (N) the number of LUTs to try
+    unsigned     unused        : 6;     // unused
+    unsigned     fHasDsd       : 1;     // set to 1 if the cut has structural DSD (and so cannot be used)
+    unsigned     fMark         : 1;     // multipurpose mark
+    unsigned     uSign[2];              // the signature
+    float        Weight;                // the weight of the cut: (M - Q)/N(V)   (the larger the better)
+    int          Gain;                  // the gain achieved using this cut
+    int          pLeaves[LPK_SIZE_MAX]; // the leaves of the cut
+    int          pNodes[LPK_SIZE_MAX];  // the nodes of the cut
+};
+
+struct Lpk_Man_t_
+{
+    // parameters
+    Lpk_Par_t *  pPars;                 // the set of parameters
+    // current representation
+    Abc_Ntk_t *  pNtk;                  // the network
+    Abc_Obj_t *  pObj;                  // the node to resynthesize 
+    // cut representation
+    int          nMffc;                 // the size of MFFC of the node
+    int          nCuts;                 // the total number of cuts    
+    int          nCutsMax;              // the largest possible number of cuts
+    int          nEvals;                // the number of good cuts
+    Lpk_Cut_t    pCuts[LPK_CUTS_MAX];   // the storage for cuts
+    int          pEvals[LPK_CUTS_MAX];  // the good cuts
+    // visited nodes 
+    Vec_Vec_t *  vVisited;
+    // mapping manager
+    If_Man_t *   pIfMan;
+    Vec_Int_t *  vCover; 
+    Vec_Vec_t *  vLevels;
+    // temporary variables
+    int          fCofactoring;          // working in the cofactoring mode
+    int          fCalledOnce;           // limits the depth of MUX cofactoring
+    int          pRefs[LPK_SIZE_MAX];   // fanin reference counters 
+    int          pCands[LPK_SIZE_MAX];  // internal nodes pointing only to the leaves
+    // truth table representation
+    Vec_Ptr_t *  vTtElems;              // elementary truth tables
+    Vec_Ptr_t *  vTtNodes;              // storage for temporary truth tables of the nodes 
+    // variable sets
+    Vec_Int_t *  vSets[8];
+    // statistics
+    int          nNodesTotal;           // total number of nodes
+    int          nNodesOver;            // nodes with cuts over the limit 
+    int          nCutsTotal;            // total number of cuts
+    int          nCutsUseful;           // useful cuts 
+    int          nGainTotal;            // the gain in LUTs
+    int          nChanges;              // the number of changed nodes
+    // counter of non-DSD blocks
+    int          nBlocks[17];
+    // rutime
+    int          timeCuts;
+    int          timeTruth;
+    int          timeEval;
+    int          timeMap;
+    int          timeOther;
+    int          timeTotal;
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                           ITERATORS                              ///
+////////////////////////////////////////////////////////////////////////
+
+#define Lpk_CutForEachLeaf( pNtk, pCut, pObj, i )                                        \
+    for ( i = 0; (i < (int)(pCut)->nLeaves) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pLeaves[i])), 1); i++ )
+#define Lpk_CutForEachNode( pNtk, pCut, pObj, i )                                        \
+    for ( i = 0; (i < (int)(pCut)->nNodes) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pNodes[i])), 1); i++ )
+#define Lpk_CutForEachNodeReverse( pNtk, pCut, pObj, i )                                 \
+    for ( i = (int)(pCut)->nNodes - 1; (i >= 0) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pNodes[i])), 1); i-- )
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== lpkCut.c =========================================================*/
+extern unsigned *     Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut );
+extern int            Lpk_NodeCuts( Lpk_Man_t * p );
+/*=== lpkMap.c =========================================================*/
+extern Lpk_Man_t *    Lpk_ManStart( Lpk_Par_t * pPars );
+extern void           Lpk_ManStop( Lpk_Man_t * p );
+/*=== lpkMap.c =========================================================*/
+extern int            Lpk_CutExplore( Lpk_Man_t * p, Lpk_Cut_t * pCut, Kit_DsdNtk_t * pNtk );
+extern If_Obj_t *     Lpk_MapPrime( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves );
+extern If_Obj_t *     Lpk_MapTree_rec( Lpk_Man_t * p, Kit_DsdNtk_t * pNtk, If_Obj_t ** ppLeaves, int iLit, If_Obj_t * pResult );
+/*=== lpkMulti.c =======================================================*/
+extern If_Obj_t *     Lpk_MapTreeMulti( Lpk_Man_t * p, unsigned * pTruth, int nLeaves, If_Obj_t ** ppLeaves );
+/*=== lpkMux.c =========================================================*/
+extern If_Obj_t *     Lpk_MapTreeMux_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves );
+extern If_Obj_t *     Lpk_MapSuppRedDec_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves );
+/*=== lpkSets.c =========================================================*/
+extern unsigned       Lpk_MapSuppRedDecSelect( Lpk_Man_t * p, unsigned * pTruth, int nVars, int * piVar, int * piVarReused );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/opt/lpk/lpkMan.c b/src/opt/lpk/lpkMan.c
new file mode 100644
index 00000000..da8b0e3a
--- /dev/null
+++ b/src/opt/lpk/lpkMan.c
@@ -0,0 +1,96 @@
+/**CFile****************************************************************
+
+  FileName    [lpkMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Fast Boolean matching for LUT structures.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: lpkMan.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "lpkInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars )
+{
+    Lpk_Man_t * p;
+    int i;
+    assert( pPars->nLutsMax <= 16 );
+    assert( pPars->nVarsMax > 0 );
+    p = ALLOC( Lpk_Man_t, 1 );
+    memset( p, 0, sizeof(Lpk_Man_t) );
+    p->pPars = pPars;
+    p->nCutsMax = LPK_CUTS_MAX;
+    p->vTtElems = Vec_PtrAllocTruthTables( pPars->nVarsMax );
+    p->vTtNodes = Vec_PtrAllocSimInfo( 256, Abc_TruthWordNum(pPars->nVarsMax) );
+    p->vCover = Vec_IntAlloc( 1 << 12 );
+    for ( i = 0; i < 8; i++ )
+        p->vSets[i] = Vec_IntAlloc(100);
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Lpk_ManStop( Lpk_Man_t * p )
+{
+    int i;
+    for ( i = 0; i < 8; i++ )
+        Vec_IntFree(p->vSets[i]);
+    if ( p->pIfMan )
+    {
+        void * pPars = p->pIfMan->pPars;
+        If_ManStop( p->pIfMan );
+        free( pPars );
+    }
+    if ( p->vLevels )
+        Vec_VecFree( p->vLevels );
+    if ( p->vVisited )
+        Vec_VecFree( p->vVisited );
+    Vec_IntFree( p->vCover );
+    Vec_PtrFree( p->vTtElems );
+    Vec_PtrFree( p->vTtNodes );
+    free( p );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/lpk/lpkMap.c b/src/opt/lpk/lpkMap.c
new file mode 100644
index 00000000..c647fdf7
--- /dev/null
+++ b/src/opt/lpk/lpkMap.c
@@ -0,0 +1,349 @@
+/**CFile****************************************************************
+
+  FileName    [lpkMap.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Fast Boolean matching for LUT structures.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: lpkMap.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "lpkInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+extern void Res_UpdateNetworkLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the mapping manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Lpk_IfManStart( Lpk_Man_t * p )
+{
+    If_Par_t * pPars;
+    assert( p->pIfMan == NULL );
+    // set defaults
+    pPars = ALLOC( If_Par_t, 1 );
+    memset( pPars, 0, sizeof(If_Par_t) );
+    // user-controlable paramters
+    pPars->nLutSize    =  p->pPars->nLutSize;
+    pPars->nCutsMax    = 16;
+    pPars->nFlowIters  =  0; // 1
+    pPars->nAreaIters  =  0; // 1 
+    pPars->DelayTarget = -1;
+    pPars->fPreprocess =  0;
+    pPars->fArea       =  1;
+    pPars->fFancy      =  0;
+    pPars->fExpRed     =  0; //
+    pPars->fLatchPaths =  0;
+    pPars->fSeqMap     =  0;
+    pPars->fVerbose    =  0;
+    // internal parameters
+    pPars->fTruth      =  0;
+    pPars->fUsePerm    =  0; 
+    pPars->nLatches    =  0;
+    pPars->pLutLib     =  NULL; // Abc_FrameReadLibLut();
+    pPars->pTimesArr   =  NULL; 
+    pPars->pTimesArr   =  NULL;   
+    pPars->fUseBdds    =  0;
+    pPars->fUseSops    =  0;
+    pPars->fUseCnfs    =  0;
+    pPars->fUseMv      =  0;
+    // start the mapping manager and set its parameters
+    p->pIfMan = If_ManStart( pPars );
+    If_ManSetupSetAll( p->pIfMan, 1000 );
+    p->pIfMan->pPars->pTimesArr = ALLOC( float, 32 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms the decomposition graph into the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+If_Obj_t * Lpk_MapPrimeInternal( If_Man_t * pIfMan, Kit_Graph_t * pGraph )
+{
+    Kit_Node_t * pNode;
+    If_Obj_t * pAnd0, * pAnd1;
+    int i;
+    // check for constant function
+    if ( Kit_GraphIsConst(pGraph) )
+        return If_ManConst1(pIfMan);
+    // check for a literal
+    if ( Kit_GraphIsVar(pGraph) )
+        return Kit_GraphVar(pGraph)->pFunc;
+    // build the AIG nodes corresponding to the AND gates of the graph
+    Kit_GraphForEachNode( pGraph, pNode, i )
+    {
+        pAnd0 = Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc; 
+        pAnd1 = Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc; 
+        pNode->pFunc = If_ManCreateAnd( pIfMan, 
+            If_NotCond( If_Regular(pAnd0), If_IsComplement(pAnd0) ^ pNode->eEdge0.fCompl ), 
+            If_NotCond( If_Regular(pAnd1), If_IsComplement(pAnd1) ^ pNode->eEdge1.fCompl ) );
+    }
+    return pNode->pFunc;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Strashes one logic node using its SOP.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+If_Obj_t * Lpk_MapPrime( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves )
+{
+    Kit_Graph_t * pGraph;
+    Kit_Node_t * pNode;
+    If_Obj_t * pRes;
+    int i;
+    // derive the factored form
+    pGraph = Kit_TruthToGraph( pTruth, nVars, p->vCover );
+    if ( pGraph == NULL )
+        return NULL;
+    // collect the fanins
+    Kit_GraphForEachLeaf( pGraph, pNode, i )
+        pNode->pFunc = ppLeaves[i];
+    // perform strashing
+    pRes = Lpk_MapPrimeInternal( p->pIfMan, pGraph );
+    pRes = If_NotCond( pRes, Kit_GraphIsComplement(pGraph) );
+    Kit_GraphFree( pGraph );
+    return pRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the mapping manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Lpk_CutExplore( Lpk_Man_t * p, Lpk_Cut_t * pCut, Kit_DsdNtk_t * pNtk )
+{
+    extern Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vCover );
+    Kit_DsdObj_t * pRoot;
+    If_Obj_t * pDriver, * ppLeaves[16];
+    Abc_Obj_t * pLeaf, * pObjNew;
+    int nGain, i;
+//    int nOldShared;
+
+    // check special cases
+    pRoot = Kit_DsdNtkRoot( pNtk );
+    if ( pRoot->Type == KIT_DSD_CONST1 )
+    {
+        if ( Kit_DsdLitIsCompl(pNtk->Root) )
+            pObjNew = Abc_NtkCreateNodeConst0( p->pNtk );
+        else
+            pObjNew = Abc_NtkCreateNodeConst1( p->pNtk );
+
+        // perform replacement
+        pObjNew->Level = p->pObj->Level;
+        Abc_ObjReplace( p->pObj, pObjNew );
+        Res_UpdateNetworkLevel( pObjNew, p->vLevels );
+        p->nGainTotal += pCut->nNodes - pCut->nNodesDup;
+        return 1;
+    }
+    if ( pRoot->Type == KIT_DSD_VAR )
+    {
+        pObjNew = Abc_NtkObj( p->pNtk, pCut->pLeaves[ Kit_DsdLit2Var(pRoot->pFans[0]) ] );
+        if ( Kit_DsdLitIsCompl(pNtk->Root) ^ Kit_DsdLitIsCompl(pRoot->pFans[0]) )
+            pObjNew = Abc_NtkCreateNodeInv( p->pNtk, pObjNew );
+
+        // perform replacement
+        pObjNew->Level = p->pObj->Level;
+        Abc_ObjReplace( p->pObj, pObjNew );
+        Res_UpdateNetworkLevel( pObjNew, p->vLevels );
+        p->nGainTotal += pCut->nNodes - pCut->nNodesDup;
+        return 1;
+    }
+    assert( pRoot->Type == KIT_DSD_AND || pRoot->Type == KIT_DSD_XOR || pRoot->Type == KIT_DSD_PRIME );
+
+    // start the mapping manager
+    if ( p->pIfMan == NULL )
+        Lpk_IfManStart( p );
+
+    // prepare the mapping manager
+    If_ManRestart( p->pIfMan );
+    // create the PI variables
+    for ( i = 0; i < p->pPars->nVarsMax; i++ )
+        ppLeaves[i] = If_ManCreateCi( p->pIfMan );
+    // set the arrival times
+    Lpk_CutForEachLeaf( p->pNtk, pCut, pLeaf, i )
+        p->pIfMan->pPars->pTimesArr[i] = (float)pLeaf->Level;
+    // prepare the PI cuts
+    If_ManSetupCiCutSets( p->pIfMan );
+    // create the internal nodes
+    p->fCalledOnce = 0;
+    pDriver = Lpk_MapTree_rec( p, pNtk, ppLeaves, pNtk->Root, NULL );
+    if ( pDriver == NULL )
+        return 0;
+    // create the PO node
+    If_ManCreateCo( p->pIfMan, If_Regular(pDriver) );
+
+    // perform mapping
+    p->pIfMan->pPars->fAreaOnly = 1;
+    If_ManPerformMappingComb( p->pIfMan );
+
+    // compute the gain in area
+    nGain = pCut->nNodes - pCut->nNodesDup - (int)p->pIfMan->AreaGlo;
+    if ( p->pPars->fVeryVerbose )
+        printf( "       Mffc = %2d. Mapped = %2d. Gain = %3d. Depth increase = %d.\n", 
+            pCut->nNodes - pCut->nNodesDup, (int)p->pIfMan->AreaGlo, nGain, (int)p->pIfMan->RequiredGlo - (int)p->pObj->Level );
+
+    // quit if there is no gain
+    if ( !(nGain > 0 || (p->pPars->fZeroCost && nGain == 0)) )
+        return 0;
+
+    // quit if depth increases too much
+    if ( (int)p->pIfMan->RequiredGlo - (int)p->pObj->Level > p->pPars->nGrowthLevel )
+        return 0;
+
+    // perform replacement
+    p->nGainTotal += nGain;
+    p->nChanges++;
+
+    // prepare the mapping manager
+    If_ManCleanNodeCopy( p->pIfMan );
+    If_ManCleanCutData( p->pIfMan );
+    // set the PIs of the cut
+    Lpk_CutForEachLeaf( p->pNtk, pCut, pLeaf, i )
+        If_ObjSetCopy( If_ManCi(p->pIfMan, i), pLeaf );
+    // get the area of mapping
+    pObjNew = Abc_NodeFromIf_rec( p->pNtk, p->pIfMan, If_Regular(pDriver), p->vCover );
+    pObjNew->pData = Hop_NotCond( pObjNew->pData, If_IsComplement(pDriver) );
+
+    // perform replacement
+    pObjNew->Level = p->pObj->Level;
+    Abc_ObjReplace( p->pObj, pObjNew );
+    Res_UpdateNetworkLevel( pObjNew, p->vLevels );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the mapping manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+If_Obj_t * Lpk_MapTree_rec( Lpk_Man_t * p, Kit_DsdNtk_t * pNtk, If_Obj_t ** ppLeaves, int iLit, If_Obj_t * pResult )
+{
+    Kit_DsdObj_t * pObj;
+    If_Obj_t * pObjNew, * pFansNew[16];
+    unsigned i, iLitFanin;
+
+    assert( iLit >= 0 );
+
+    // consider the case of a gate
+    pObj = Kit_DsdNtkObj( pNtk, Kit_DsdLit2Var(iLit) );
+    if ( pObj == NULL )
+    {
+        pObjNew = ppLeaves[Kit_DsdLit2Var(iLit)];
+        return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) );
+    }
+    if ( pObj->Type == KIT_DSD_CONST1 )
+    {
+        return If_NotCond( If_ManConst1(p->pIfMan), Kit_DsdLitIsCompl(iLit) );
+    }
+    if ( pObj->Type == KIT_DSD_VAR )
+    {
+        pObjNew = ppLeaves[Kit_DsdLit2Var(pObj->pFans[0])];
+        return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) ^ Kit_DsdLitIsCompl(pObj->pFans[0]) );
+    }
+    if ( pObj->Type == KIT_DSD_AND )
+    {
+        assert( pObj->nFans == 2 );
+        pFansNew[0] = Lpk_MapTree_rec( p, pNtk, ppLeaves, pObj->pFans[0], NULL );
+        pFansNew[1] = pResult? pResult : Lpk_MapTree_rec( p, pNtk, ppLeaves, pObj->pFans[1], NULL );
+        if ( pFansNew[0] == NULL || pFansNew[1] == NULL )
+            return NULL;
+        pObjNew = If_ManCreateAnd( p->pIfMan, pFansNew[0], pFansNew[1] ); 
+        return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) );
+    }
+    if ( pObj->Type == KIT_DSD_XOR )
+    {
+        int fCompl = Kit_DsdLitIsCompl(iLit);
+        assert( pObj->nFans == 2 );
+        pFansNew[0] = Lpk_MapTree_rec( p, pNtk, ppLeaves, pObj->pFans[0], NULL );
+        pFansNew[1] = pResult? pResult : Lpk_MapTree_rec( p, pNtk, ppLeaves, pObj->pFans[1], NULL );
+        if ( pFansNew[0] == NULL || pFansNew[1] == NULL )
+            return NULL;
+        fCompl ^= If_IsComplement(pFansNew[0]) ^ If_IsComplement(pFansNew[1]);
+        pObjNew = If_ManCreateXor( p->pIfMan, If_Regular(pFansNew[0]), If_Regular(pFansNew[1]) );
+        return If_NotCond( pObjNew, fCompl );
+    }
+    assert( pObj->Type == KIT_DSD_PRIME );
+    p->nBlocks[pObj->nFans]++;
+
+    // solve for the inputs
+    Kit_DsdObjForEachFanin( pNtk, pObj, iLitFanin, i )
+    {
+        if ( i == 0 )
+            pFansNew[i] = pResult? pResult : Lpk_MapTree_rec( p, pNtk, ppLeaves, iLitFanin, NULL );
+        else
+            pFansNew[i] = Lpk_MapTree_rec( p, pNtk, ppLeaves, iLitFanin, NULL );
+        if ( pFansNew[i] == NULL )
+            return NULL;
+    }
+/*
+    if ( !p->fCofactoring && p->pPars->nVarsShared > 0 && (int)pObj->nFans > p->pPars->nLutSize )
+    {
+        pObjNew = Lpk_MapTreeMulti( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
+        return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) );
+    }
+*/
+
+    // find best cofactoring variable
+    if ( pObj->nFans > 3 && !p->fCalledOnce )
+//        pObjNew = Lpk_MapTreeMux_rec( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
+        pObjNew = Lpk_MapSuppRedDec_rec( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
+    else
+        pObjNew = Lpk_MapPrime( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
+    return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/lpk/lpkMulti.c b/src/opt/lpk/lpkMulti.c
new file mode 100644
index 00000000..82cf3578
--- /dev/null
+++ b/src/opt/lpk/lpkMulti.c
@@ -0,0 +1,495 @@
+/**CFile****************************************************************
+
+  FileName    [lpkMulti.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Fast Boolean matching for LUT structures.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: lpkMulti.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "lpkInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Records variable order.]
+
+  Description [Increaments Order[x][y] by 1 if x should be above y in the DSD.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Lpk_CreateVarOrder( Kit_DsdNtk_t * pNtk, char pTable[][16] )
+{
+    Kit_DsdObj_t * pObj;
+    unsigned uSuppFanins, k;
+    int Above[16], Below[16];
+    int nAbove, nBelow, iFaninLit, i, x, y;
+    // iterate through the nodes
+    Kit_DsdNtkForEachObj( pNtk, pObj, i )
+    {
+        // collect fanin support of this node
+        nAbove = 0;
+        uSuppFanins = 0;
+        Kit_DsdObjForEachFanin( pNtk, pObj, iFaninLit, k )
+        {
+            if ( Kit_DsdLitIsLeaf( pNtk, iFaninLit ) )
+                Above[nAbove++] = Kit_DsdLit2Var(iFaninLit);
+            else
+                uSuppFanins |= Kit_DsdLitSupport( pNtk, iFaninLit );
+        }
+        // find the below variables
+        nBelow = 0;
+        for ( y = 0; y < 16; y++ )
+            if ( uSuppFanins & (1 << y) )
+                Below[nBelow++] = y;
+        // create all pairs
+        for ( x = 0; x < nAbove; x++ )
+            for ( y = 0; y < nBelow; y++ )
+                pTable[Above[x]][Below[y]]++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates commmon variable order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Lpk_CreateCommonOrder( char pTable[][16], int piCofVar[], int nCBars, int pPrios[], int nVars, int fVerbose )
+{
+    int Score[16] = {0}, pPres[16];
+    int i, y, x, iVarBest, ScoreMax, PrioCount;
+
+    // mark the present variables
+    for ( i = 0; i < nVars; i++ )
+        pPres[i] = 1;
+    // remove cofactored variables
+    for ( i = 0; i < nCBars; i++ )
+        pPres[piCofVar[i]] = 0;
+
+    // compute scores for each leaf
+    for ( i = 0; i < nVars; i++ )
+    {
+        if ( pPres[i] == 0 )
+            continue;
+        for ( y = 0; y < nVars; y++ )
+            Score[i] += pTable[i][y];
+        for ( x = 0; x < nVars; x++ )
+            Score[i] -= pTable[x][i];
+    }
+
+    // print the scores
+    if ( fVerbose )
+    {
+        printf( "Scores: " );
+        for ( i = 0; i < nVars; i++ )
+            printf( "%c=%d ", 'a'+i, Score[i] );
+        printf( "   " );
+        printf( "Prios: " );
+    }
+
+    // derive variable priority
+    // variables with equal score receive the same priority
+    for ( i = 0; i < nVars; i++ )
+        pPrios[i] = 16;
+
+    // iterate until variables remain
+    for ( PrioCount = 1; ; PrioCount++ )
+    {
+        // find the present variable with the highest score
+        iVarBest = -1;
+        ScoreMax = -100000;
+        for ( i = 0; i < nVars; i++ )
+        {
+            if ( pPres[i] == 0 )
+                continue;
+            if ( ScoreMax < Score[i] )
+            {
+                ScoreMax = Score[i];
+                iVarBest = i;
+            }
+        }
+        if ( iVarBest == -1 )
+            break;
+        // give the next priority to all vars having this score
+        if ( fVerbose )
+            printf( "%d=", PrioCount );
+        for ( i = 0; i < nVars; i++ )
+        {
+            if ( pPres[i] == 0 )
+                continue;
+            if ( Score[i] == ScoreMax )
+            {
+                pPrios[i] = PrioCount;
+                pPres[i] = 0;
+                if ( fVerbose )
+                    printf( "%c", 'a'+i );
+            }
+        }
+        if ( fVerbose )
+            printf( " " );
+    }
+    if ( fVerbose )
+        printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds components with the highest priority.]
+
+  Description [Returns the number of components selected.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Lpk_FindHighest( Kit_DsdNtk_t ** ppNtks, int * piLits, int nSize, int * pPrio, int * pDecision )
+{
+    Kit_DsdObj_t * pObj;
+    unsigned uSupps[8], uSuppFanin, uSuppTotal, uSuppLarge;
+    int i, pTriv[8], PrioMin, iVarMax, nComps, fOneNonTriv;
+
+    // find individual support and total support 
+    uSuppTotal = 0;
+    for ( i = 0; i < nSize; i++ )
+    {
+        pTriv[i] = 1;
+        if ( piLits[i] < 0 ) 
+            uSupps[i] = 0;
+        else if ( Kit_DsdLitIsLeaf(ppNtks[i], piLits[i]) )
+            uSupps[i] = Kit_DsdLitSupport( ppNtks[i], piLits[i] );
+        else
+        {
+            pObj = Kit_DsdNtkObj( ppNtks[i], Kit_DsdLit2Var(piLits[i]) );
+            if ( pObj->Type == KIT_DSD_PRIME )
+            {
+                pTriv[i] = 0;
+                uSuppFanin = Kit_DsdLitSupport( ppNtks[i], pObj->pFans[0] );
+            }
+            else
+            {
+                assert( pObj->nFans == 2 );
+                if ( !Kit_DsdLitIsLeaf(ppNtks[i], pObj->pFans[0]) )
+                    pTriv[i] = 0;
+                uSuppFanin = Kit_DsdLitSupport( ppNtks[i], pObj->pFans[1] );
+            }
+            uSupps[i] = Kit_DsdLitSupport( ppNtks[i], piLits[i] ) & ~uSuppFanin;
+        }
+        assert( uSupps[i] <= 0xFFFF );
+        uSuppTotal |= uSupps[i];
+    }
+    if ( uSuppTotal == 0 )
+        return 0;
+
+    // find one support variable with the highest priority
+    PrioMin = ABC_INFINITY;
+    iVarMax = -1;
+    for ( i = 0; i < 16; i++ )
+        if ( uSuppTotal & (1 << i) )
+            if ( PrioMin > pPrio[i] )
+            {
+                PrioMin = pPrio[i];
+                iVarMax = i;
+            }
+    assert( iVarMax != -1 );
+
+    // select components, which have this variable
+    nComps = 0;
+    fOneNonTriv = 0;
+    uSuppLarge = 0;
+    for ( i = 0; i < nSize; i++ )
+        if ( uSupps[i] & (1<<iVarMax) )
+        {
+            if ( pTriv[i] || !fOneNonTriv )
+            {
+                if ( !pTriv[i] )
+                {
+                    uSuppLarge = uSupps[i];
+                    fOneNonTriv = 1;
+                }
+                pDecision[i] = 1;
+                nComps++;
+            }
+            else
+                pDecision[i] = 0;
+        }
+        else
+            pDecision[i] = 0;
+
+    // add other non-trivial not-taken components whose support is contained in the current large component support
+    if ( fOneNonTriv )
+        for ( i = 0; i < nSize; i++ )
+            if ( !pTriv[i] && pDecision[i] == 0 && (uSupps[i] & ~uSuppLarge) == 0 )
+            {
+                pDecision[i] = 1;
+                nComps++;
+            }
+
+    return nComps;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the mapping manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+If_Obj_t * Lpk_MapTreeMulti_rec( Lpk_Man_t * p, Kit_DsdNtk_t ** ppNtks, int * piLits, int * piCofVar, int nCBars, If_Obj_t ** ppLeaves, int nLeaves, int * pPrio )
+{
+    Kit_DsdObj_t * pObj;
+    If_Obj_t * pObjsNew[4][8], * pResPrev;
+    int piLitsNew[8], pDecision[8];
+    int i, k, nComps, nSize;
+
+    // find which of the variables is highest in the order
+    nSize = (1 << nCBars);
+    nComps = Lpk_FindHighest( ppNtks, piLits, nSize, pPrio, pDecision );
+    if ( nComps == 0 )
+        return If_Not( If_ManConst1(p->pIfMan) );
+
+    // iterate over the nodes
+    if ( p->pPars->fVeryVerbose )
+        printf( "Decision: " );
+    for ( i = 0; i < nSize; i++ )
+    {
+        if ( pDecision[i] )
+        {
+            if ( p->pPars->fVeryVerbose )
+                printf( "%d ", i );
+            assert( piLits[i] >= 0 );
+            pObj = Kit_DsdNtkObj( ppNtks[i], Kit_DsdLit2Var(piLits[i]) );
+            if ( pObj == NULL )
+                piLitsNew[i] = -2;
+            else if ( pObj->Type == KIT_DSD_PRIME )
+                piLitsNew[i] = pObj->pFans[0];
+            else
+                piLitsNew[i] = pObj->pFans[1];
+        }
+        else
+            piLitsNew[i] = piLits[i];
+    }
+    if ( p->pPars->fVeryVerbose )
+        printf( "\n" );
+
+    // call again
+    pResPrev = Lpk_MapTreeMulti_rec( p, ppNtks, piLitsNew, piCofVar, nCBars, ppLeaves, nLeaves, pPrio );
+
+    // create new set of nodes
+    for ( i = 0; i < nSize; i++ )
+    {
+        if ( pDecision[i] )
+            pObjsNew[nCBars][i] = Lpk_MapTree_rec( p, ppNtks[i], ppLeaves, piLits[i], pResPrev );
+        else if ( piLits[i] == -1 )
+            pObjsNew[nCBars][i] = If_ManConst1(p->pIfMan);
+        else if ( piLits[i] == -2 )
+            pObjsNew[nCBars][i] = If_Not( If_ManConst1(p->pIfMan) );
+        else
+            pObjsNew[nCBars][i] = pResPrev;
+    }
+
+    // create MUX using these outputs
+    for ( k = nCBars; k > 0; k-- )
+    {
+        nSize /= 2;
+        for ( i = 0; i < nSize; i++ )
+            pObjsNew[k-1][i] = If_ManCreateMux( p->pIfMan, pObjsNew[k][2*i+0], pObjsNew[k][2*i+1], ppLeaves[piCofVar[k-1]] );
+    }
+    assert( nSize == 1 );
+    return pObjsNew[0][0];  
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the mapping manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+If_Obj_t * Lpk_MapTreeMulti( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves )
+{
+    static Counter = 0;
+    If_Obj_t * pResult;
+    Kit_DsdNtk_t * ppNtks[8] = {0}, * pTemp;
+    Kit_DsdObj_t * pRoot;
+    int piCofVar[4], pPrios[16], pFreqs[16] = {0}, piLits[16];
+    int i, k, nCBars, nSize, nMemSize;
+    unsigned * ppCofs[4][8], uSupport;
+    char pTable[16][16] = {0};
+    int fVerbose = p->pPars->fVeryVerbose;
+
+    Counter++;
+//    printf( "Run %d.\n", Counter );
+
+    // allocate storage for cofactors
+    nMemSize = Kit_TruthWordNum(nVars);
+    ppCofs[0][0] = ALLOC( unsigned, 32 * nMemSize );
+    nSize = 0;
+    for ( i = 0; i < 4; i++ )
+    for ( k = 0; k < 8; k++ )
+        ppCofs[i][k] = ppCofs[0][0] + nMemSize * nSize++;
+    assert( nSize == 32 );
+
+    // find the best cofactoring variables
+    nCBars = Kit_DsdCofactoring( pTruth, nVars, piCofVar, p->pPars->nVarsShared, 0 );
+//    nCBars = 2;
+//    piCofVar[0] = 0;
+//    piCofVar[1] = 1;
+
+
+    // copy the function
+    Kit_TruthCopy( ppCofs[0][0], pTruth, nVars );
+
+    // decompose w.r.t. these variables
+    for ( k = 0; k < nCBars; k++ )
+    {
+        nSize = (1 << k);
+        for ( i = 0; i < nSize; i++ )
+        {
+            Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] );
+            Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] );
+        }
+    }
+    nSize = (1 << nCBars);
+    // compute DSD networks
+    for ( i = 0; i < nSize; i++ )
+    {
+        ppNtks[i] = Kit_DsdDecompose( ppCofs[nCBars][i], nVars );
+        ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] );
+        Kit_DsdNtkFree( pTemp );
+        if ( fVerbose )
+        {
+            printf( "Cof%d%d: ", nCBars, i );
+            Kit_DsdPrint( stdout, ppNtks[i] );
+        }
+    }
+
+    // compute variable frequences
+    for ( i = 0; i < nSize; i++ )
+    {
+        uSupport = Kit_TruthSupport( ppCofs[nCBars][i], nVars );
+        for ( k = 0; k < nVars; k++ )
+            if ( uSupport & (1<<k) )
+                pFreqs[k]++;
+    }
+
+    // find common variable order
+    for ( i = 0; i < nSize; i++ )
+    {
+        Kit_DsdGetSupports( ppNtks[i] );
+        Lpk_CreateVarOrder( ppNtks[i], pTable );
+    }
+    Lpk_CreateCommonOrder( pTable, piCofVar, nCBars, pPrios, nVars, fVerbose );
+    // update priorities with frequences
+    for ( i = 0; i < nVars; i++ )
+        pPrios[i] = pPrios[i] * 256 + (16 - pFreqs[i]) * 16 + i;
+
+    if ( fVerbose )
+        printf( "After restructuring with priority:\n" );
+
+    if ( Counter == 1 )
+    {
+        int x = 0;
+    }
+    // transform all networks according to the variable order
+    for ( i = 0; i < nSize; i++ )
+    {
+        ppNtks[i] = Kit_DsdShrink( pTemp = ppNtks[i], pPrios );
+        Kit_DsdNtkFree( pTemp );
+        Kit_DsdGetSupports( ppNtks[i] );
+        assert( ppNtks[i]->pSupps[0] <= 0xFFFF );
+        // undec nodes should be rotated in such a way that the first input has as many shared inputs as possible
+        Kit_DsdRotate( ppNtks[i], pFreqs );
+        // print the resulting networks
+        if ( fVerbose )
+        {
+            printf( "Cof%d%d: ", nCBars, i );
+            Kit_DsdPrint( stdout, ppNtks[i] );
+        }
+    }
+ 
+    for ( i = 0; i < nSize; i++ )
+    {
+        // collect the roots
+        pRoot = Kit_DsdNtkRoot(ppNtks[i]);
+        if ( pRoot->Type == KIT_DSD_CONST1 )
+            piLits[i] = Kit_DsdLitIsCompl(ppNtks[i]->Root)? -2: -1;
+        else if ( pRoot->Type == KIT_DSD_VAR )
+            piLits[i] = Kit_DsdLitNotCond( pRoot->pFans[0], Kit_DsdLitIsCompl(ppNtks[i]->Root) );
+        else
+            piLits[i] = ppNtks[i]->Root;
+    }
+
+
+    // recursively construct AIG for mapping
+    p->fCofactoring = 1;
+    pResult = Lpk_MapTreeMulti_rec( p, ppNtks, piLits, piCofVar, nCBars, ppLeaves, nVars, pPrios );
+    p->fCofactoring = 0;
+
+    if ( fVerbose )
+        printf( "\n" );
+
+    // verify the transformations
+    nSize = (1 << nCBars);
+    for ( i = 0; i < nSize; i++ )
+        Kit_DsdTruth( ppNtks[i], ppCofs[nCBars][i] );
+    // mux the truth tables
+    for ( k = nCBars-1; k >= 0; k-- )
+    {
+        nSize = (1 << k);
+        for ( i = 0; i < nSize; i++ )
+            Kit_TruthMuxVar( ppCofs[k][i], ppCofs[k+1][2*i+0], ppCofs[k+1][2*i+1], nVars, piCofVar[k] );
+    }
+    if ( !Extra_TruthIsEqual( pTruth, ppCofs[0][0], nVars ) )
+        printf( "Verification failed.\n" );
+
+
+    // free the networks
+    for ( i = 0; i < 8; i++ )
+        if ( ppNtks[i] )
+            Kit_DsdNtkFree( ppNtks[i] );
+    free( ppCofs[0][0] );
+
+    return pResult;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/lpk/lpkMux.c b/src/opt/lpk/lpkMux.c
new file mode 100644
index 00000000..d9e013f0
--- /dev/null
+++ b/src/opt/lpk/lpkMux.c
@@ -0,0 +1,257 @@
+/**CFile****************************************************************
+
+  FileName    [lpkMux.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Fast Boolean matching for LUT structures.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: lpkMux.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "lpkInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Find the best cofactoring variable.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Lpk_MapTreeBestVar( Lpk_Man_t * p, unsigned * pTruth, int nVars )
+{
+//    Kit_DsdNtk_t * ppNtks[2], * pTemp;
+    unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 );
+    unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 );
+    int i, iBestVar, nSuppSizeCur0, nSuppSizeCur1, nSuppSizeCur, nSuppSizeMin;
+//    int nPrimeSizeCur0, nPrimeSizeCur1, nPrimeSizeCur, nPrimeSizeMin;
+
+    // iterate through variables
+    iBestVar = -1;
+    nSuppSizeMin = ABC_INFINITY;
+//    nPrimeSizeMin = ABC_INFINITY;
+    for ( i = 0; i < nVars; i++ )
+    {
+        // cofactor the functiona and get support sizes
+        Kit_TruthCofactor0New( pCof0, pTruth, nVars, i );
+        Kit_TruthCofactor1New( pCof1, pTruth, nVars, i );
+        nSuppSizeCur0 = Kit_TruthSupportSize( pCof0, nVars );
+        nSuppSizeCur1 = Kit_TruthSupportSize( pCof1, nVars );
+        nSuppSizeCur  = nSuppSizeCur0 + nSuppSizeCur1;
+/*
+        // check the size of the largest prime components
+        ppNtks[0] = Kit_DsdDecompose( pCof0, nVars );
+        ppNtks[1] = Kit_DsdDecompose( pCof1, nVars );
+        // compute the largest non-decomp block
+        nPrimeSizeCur0 = Kit_DsdNonDsdSizeMax(ppNtks[0]);
+        nPrimeSizeCur1 = Kit_DsdNonDsdSizeMax(ppNtks[1]);
+        nPrimeSizeCur  = KIT_MAX( nPrimeSizeCur0, nPrimeSizeCur1 );
+
+        printf( "Evaluating variable %c:\n", 'a'+i );
+//        Kit_DsdPrintExpanded( ppNtks[0] );
+//        Kit_DsdPrintExpanded( ppNtks[1] );
+
+        ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] );
+        Kit_DsdNtkFree( pTemp );
+
+        ppNtks[1] = Kit_DsdExpand( pTemp = ppNtks[1] );
+        Kit_DsdNtkFree( pTemp );
+
+        Kit_DsdPrint( stdout, ppNtks[0] );
+        Kit_DsdPrint( stdout, ppNtks[1] );
+
+//        Lpk_DsdEvalSets( p, ppNtks[0], ppNtks[1] );
+
+        // free the networks
+        Kit_DsdNtkFree( ppNtks[0] );
+        Kit_DsdNtkFree( ppNtks[1] );
+*/
+        // compare this variable with other variables
+        if ( nSuppSizeMin > nSuppSizeCur ) //|| (nSuppSizeMin == nSuppSizeCur && nPrimeSizeMin > nPrimeSizeCur ) )
+        {
+            nSuppSizeMin = nSuppSizeCur;
+//            nPrimeSizeMin = nPrimeSizeCur;
+            iBestVar = i;
+        }
+    }
+    printf( "\n" );
+    assert( iBestVar != -1 );
+    return iBestVar;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Maps the function by the best cofactoring.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+If_Obj_t * Lpk_MapTreeMux_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves )
+{
+    If_Obj_t * pObj0, * pObj1;
+    Kit_DsdNtk_t * ppNtks[2];
+    unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 );
+    unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 );
+    int iBestVar;
+    assert( nVars > 3 );
+    p->fCalledOnce = 1;
+
+    // cofactor w.r.t. the best variable
+    iBestVar = Lpk_MapTreeBestVar( p, pTruth, nVars );
+    Kit_TruthCofactor0New( pCof0, pTruth, nVars, iBestVar );
+    Kit_TruthCofactor1New( pCof1, pTruth, nVars, iBestVar );
+    // decompose the functions
+    ppNtks[0] = Kit_DsdDecompose( pCof0, nVars );
+    ppNtks[1] = Kit_DsdDecompose( pCof1, nVars );
+    if ( p->pPars->fVeryVerbose )
+    {
+        printf( "Cofactoring w.r.t. var %c (%d -> %d+%d supp vars):\n", 
+            'a'+iBestVar, nVars, Kit_TruthSupportSize(pCof0, nVars), Kit_TruthSupportSize(pCof1, nVars) );
+        Kit_DsdPrintExpanded( ppNtks[0] );
+        Kit_DsdPrintExpanded( ppNtks[1] );
+    }
+    // map the DSD structures
+    pObj0 = Lpk_MapTree_rec( p, ppNtks[0], ppLeaves, ppNtks[0]->Root, NULL );
+    pObj1 = Lpk_MapTree_rec( p, ppNtks[1], ppLeaves, ppNtks[1]->Root, NULL );
+    Kit_DsdNtkFree( ppNtks[0] );
+    Kit_DsdNtkFree( ppNtks[1] );
+    return If_ManCreateMux( p->pIfMan, pObj0, pObj1, ppLeaves[iBestVar] );
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Implements support-reducing decomposition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+If_Obj_t * Lpk_MapSuppRedDec_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves )
+{
+    Kit_DsdNtk_t * pNtkDec, * pNtkComp;
+    If_Obj_t * pObjNew;
+    unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes,  0 );
+    unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes,  1 );
+    unsigned * pDec0 = Vec_PtrEntry( p->vTtNodes,  2 );
+    unsigned * pDec1 = Vec_PtrEntry( p->vTtNodes,  3 );
+    unsigned * pDec  = Vec_PtrEntry( p->vTtNodes,  4 );
+    unsigned * pCo00 = Vec_PtrEntry( p->vTtNodes,  5 );
+    unsigned * pCo01 = Vec_PtrEntry( p->vTtNodes,  6 );
+    unsigned * pCo10 = Vec_PtrEntry( p->vTtNodes,  7 );
+    unsigned * pCo11 = Vec_PtrEntry( p->vTtNodes,  8 );
+    unsigned * pCo0  = Vec_PtrEntry( p->vTtNodes,  9 );
+    unsigned * pCo1  = Vec_PtrEntry( p->vTtNodes, 10 );
+    unsigned * pCo   = Vec_PtrEntry( p->vTtNodes, 11 );
+    int TrueMint0, TrueMint1;
+    int uSubsets, uSubset0, uSubset1, iVar, iVarReused, i;
+
+    // determine if supp-red decomposition exists
+    uSubsets = Lpk_MapSuppRedDecSelect( p, pTruth, nVars, &iVar, &iVarReused );
+    if ( uSubsets == 0 )
+        return NULL;
+
+    // get the bound sets
+    uSubset0 = uSubsets & 0xFFFF;
+    uSubset1 = uSubsets >> 16;
+    // get the cofactors
+    Kit_TruthCofactor0New( pCof0, pTruth, nVars, iVar );
+    Kit_TruthCofactor1New( pCof1, pTruth, nVars, iVar );
+    // find any true assignments of the cofactors
+    TrueMint0 = Kit_TruthFindFirstBit( pCof0, nVars );
+    TrueMint1 = Kit_TruthFindFirstBit( pCof1, nVars );
+    assert( TrueMint0 >= 0 && TrueMint1 >= 0 );
+    // cofactor the cofactors according to these minterms
+    Kit_TruthCopy( pDec0, pCof0, nVars );
+    Kit_TruthCopy( pDec1, pCof1, nVars );
+    for ( i = 0; i < nVars; i++ )
+        if ( !(uSubset0 & (1 << i)) )
+        {
+            if ( TrueMint0 & (1 << i) )
+                Kit_TruthCofactor1( pDec0, nVars, i );
+            else
+                Kit_TruthCofactor0( pDec0, nVars, i );
+        }
+    for ( i = 0; i < nVars; i++ )
+        if ( !(uSubset1 & (1 << i)) )
+        {
+            if ( TrueMint1 & (1 << i) )
+                Kit_TruthCofactor1( pDec1, nVars, i );
+            else
+                Kit_TruthCofactor0( pDec1, nVars, i );
+        }
+    // get the decomposed function
+    Kit_TruthMuxVar( pDec, pDec0, pDec1, nVars, iVar );
+
+    // derive the remainders
+    Kit_TruthAndPhase( pCo00, pCof0, pDec0, nVars, 0, 1 );
+    Kit_TruthAndPhase( pCo01, pCof0, pDec0, nVars, 0, 0 );
+    Kit_TruthAndPhase( pCo10, pCof1, pDec1, nVars, 0, 1 );
+    Kit_TruthAndPhase( pCo11, pCof1, pDec1, nVars, 0, 0 );
+    // quantify bound set variables
+    for ( i = 0; i < nVars; i++ )
+        if ( uSubset0 & (1 << i) )
+        {
+            Kit_TruthExist( pCo00, nVars, i );
+            Kit_TruthExist( pCo01, nVars, i );
+        }
+    for ( i = 0; i < nVars; i++ )
+        if ( uSubset1 & (1 << i) )
+        {
+            Kit_TruthExist( pCo10, nVars, i );
+            Kit_TruthExist( pCo11, nVars, i );
+        }
+    // derive the functions by composing them with the new variable (iVarReused)
+    Kit_TruthMuxVar( pCo0, pCo00, pCo01, nVars, iVarReused );
+    Kit_TruthMuxVar( pCo1, pCo10, pCo11, nVars, iVarReused );
+    // derive the composition function
+    Kit_TruthMuxVar( pCo , pCo0 , pCo1 , nVars, iVar );
+
+    // process the decomposed function
+    pNtkDec = Kit_DsdDecompose( pDec, nVars );
+    Kit_DsdPrint( stdout, pNtkDec );
+    ppLeaves[iVarReused] = Lpk_MapTree_rec( p, pNtkDec, ppLeaves, pNtkDec->Root, NULL );
+    Kit_DsdNtkFree( pNtkDec );
+
+    // process the composition function 
+    pNtkComp = Kit_DsdDecompose( pCo, nVars );
+    Kit_DsdPrint( stdout, pNtkComp );
+    pObjNew = Lpk_MapTree_rec( p, pNtkComp, ppLeaves, pNtkComp->Root, NULL );
+    Kit_DsdNtkFree( pNtkComp );
+    return pObjNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/lpk/lpkSets.c b/src/opt/lpk/lpkSets.c
new file mode 100644
index 00000000..721705cb
--- /dev/null
+++ b/src/opt/lpk/lpkSets.c
@@ -0,0 +1,399 @@
+/**CFile****************************************************************
+
+  FileName    [lpkSets.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Fast Boolean matching for LUT structures.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: lpkSets.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "lpkInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Lpk_Set_t_ Lpk_Set_t;
+struct Lpk_Set_t_
+{
+    char         iVar;        // the cofactoring variable
+    char         Over;        // the overlap in supports
+    char         SRed;        // the support reduction
+    char         Size;        // the size of the boundset
+    unsigned     uSubset0;    // the first subset (with removed)
+    unsigned     uSubset1;    // the second subset (with removed)
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively computes decomposable subsets.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned Lpk_ComputeSets_rec( Kit_DsdNtk_t * p, int iLit, Vec_Int_t * vSets )
+{
+    unsigned i, iLitFanin, uSupport, uSuppCur;
+    Kit_DsdObj_t * pObj;
+    // consider the case of simple gate
+    pObj = Kit_DsdNtkObj( p, Kit_DsdLit2Var(iLit) );
+    if ( pObj == NULL )
+        return (1 << Kit_DsdLit2Var(iLit));
+    if ( pObj->Type == KIT_DSD_AND || pObj->Type == KIT_DSD_XOR )
+    {
+        unsigned uSupps[16], Limit, s;
+        uSupport = 0;
+        Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
+        {
+            uSupps[i] = Lpk_ComputeSets_rec( p, iLitFanin, vSets );
+            uSupport |= uSupps[i];
+        }
+        // create all subsets, except empty and full
+        Limit = (1 << pObj->nFans) - 1;
+        for ( s = 1; s < Limit; s++ )
+        {
+            uSuppCur = 0;
+            for ( i = 0; i < pObj->nFans; i++ )
+                if ( s & (1 << i) )
+                    uSuppCur |= uSupps[i];
+            Vec_IntPush( vSets, uSuppCur );
+        }
+        return uSupport;
+    }
+    assert( pObj->Type == KIT_DSD_PRIME );
+    // get the cumulative support of all fanins
+    uSupport = 0;
+    Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i )
+    {
+        uSuppCur  = Lpk_ComputeSets_rec( p, iLitFanin, vSets );
+        uSupport |= uSuppCur;
+        Vec_IntPush( vSets, uSuppCur );
+    }
+    return uSupport;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the set of subsets of decomposable variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned Lpk_ComputeSets( Kit_DsdNtk_t * p, Vec_Int_t * vSets )
+{
+    unsigned uSupport, Entry, i;
+    assert( p->nVars <= 16 );
+    Vec_IntClear( vSets );
+    Vec_IntPush( vSets, 0 );
+    if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_CONST1 )
+        return 0;
+    if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_VAR )
+    {
+        uSupport = ( 1 << Kit_DsdLit2Var(Kit_DsdNtkRoot(p)->pFans[0]) );
+        Vec_IntPush( vSets, uSupport );
+        return uSupport;
+    }
+    uSupport = Lpk_ComputeSets_rec( p, p->Root, vSets );
+    assert( (uSupport & 0xFFFF0000) == 0 );
+    Vec_IntPush( vSets, uSupport );
+    // set the remaining variables
+    Vec_IntForEachEntry( vSets, Entry, i )
+        Vec_IntWriteEntry( vSets, i, Entry | ((uSupport & ~Entry) << 16) );
+    return uSupport;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the sets of subsets.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Lpk_PrintSetOne( int uSupport )
+{
+    unsigned k;
+    for ( k = 0; k < 16; k++ )
+        if ( uSupport & (1<<k) )
+            printf( "%c", 'a'+k );
+    printf( " " );
+}
+/**Function*************************************************************
+
+  Synopsis    [Prints the sets of subsets.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Lpk_PrintSets( Vec_Int_t * vSets )
+{
+    unsigned uSupport, i;
+    printf( "Subsets(%d): ", Vec_IntSize(vSets) );
+    Vec_IntForEachEntry( vSets, uSupport, i )
+        Lpk_PrintSetOne( uSupport );
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes maximal support reducing bound-sets.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Lpk_ComposeSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1, int nVars, int iCofVar,
+    Lpk_Set_t * pStore, int * pSize, int nSizeLimit )
+{
+    static int nTravId = 0;            // the number of the times this is visited
+    static int TravId[1<<16] = {0};    // last visited
+    static char SRed[1<<16];           // best support reduction
+    static char Over[1<<16];           // best overlaps
+    static unsigned Parents[1<<16];    // best set of parents
+    static unsigned short Used[1<<16]; // storage for used subsets
+    int nSuppSize, nSuppOver, nSuppRed, nUsed, nMinOver, i, k, s;
+    unsigned Entry, Entry0, Entry1;
+    unsigned uSupp, uSupp0, uSupp1, uSuppTotal;
+    Lpk_Set_t * pEntry;
+
+    if ( nTravId == (1 << 30) )
+        memset( TravId, 0, sizeof(int) * (1 << 16) );
+
+    // collect support reducing subsets
+    nUsed = 0;
+    nTravId++;
+    uSuppTotal = Kit_BitMask(nVars) & ~(1<<iCofVar);
+    Vec_IntForEachEntry( vSets0, Entry0, i )
+    Vec_IntForEachEntry( vSets1, Entry1, k )
+    {
+        uSupp0 = (Entry0 & 0xFFFF);
+        uSupp1 = (Entry1 & 0xFFFF);
+        // skip trivial
+        if ( uSupp0 == 0 || uSupp1 == 0 || (uSupp0 | uSupp1) == uSuppTotal )
+            continue;
+        if ( Kit_WordHasOneBit(uSupp0) && Kit_WordHasOneBit(uSupp1) )
+            continue;
+        // get the entry
+        Entry = Entry0 | Entry1;
+        uSupp = Entry & 0xFFFF;
+        // set the bound set size
+        nSuppSize = Kit_WordCountOnes( uSupp );
+        // get the number of overlapping vars
+        nSuppOver = Kit_WordCountOnes( Entry & (Entry >> 16) );
+        // get the support reduction
+        nSuppRed  = nSuppSize - 1 - nSuppOver;
+        // only consider support-reducing subsets
+        if ( nSuppRed <= 0 )
+            continue;
+        // check if this support is already used
+        if ( TravId[uSupp] < nTravId )
+        {
+            Used[nUsed++] = uSupp;
+
+            TravId[uSupp] = nTravId;
+            SRed[uSupp] = nSuppRed;
+            Over[uSupp] = nSuppOver;
+            Parents[uSupp] = (k << 16) | i;
+        }
+        else if ( TravId[uSupp] == nTravId && SRed[uSupp] < nSuppRed )
+        {
+            TravId[uSupp] = nTravId;
+            SRed[uSupp] = nSuppRed;
+            Over[uSupp] = nSuppOver;
+            Parents[uSupp] = (k << 16) | i;
+        }
+    }
+
+    // check if there are non-overlapping
+    nMinOver = 1000;
+    for ( s = 0; s < nUsed; s++ )
+        if ( nMinOver > Over[Used[s]] )
+            nMinOver = Over[Used[s]];
+
+
+    // collect the accumulated ones
+    for ( s = 0; s < nUsed; s++ )
+        if ( Over[Used[s]] == nMinOver )
+        {
+            // save the entry
+            if ( *pSize == nSizeLimit )
+                return;
+            pEntry = pStore + (*pSize)++;
+
+            i = Parents[Used[s]] & 0xFFFF;
+            k = Parents[Used[s]] >> 16;
+
+            pEntry->uSubset0 = Vec_IntEntry(vSets0, i);
+            pEntry->uSubset1 = Vec_IntEntry(vSets1, k);
+            Entry  = pEntry->uSubset0 | pEntry->uSubset1;
+
+            // record the cofactoring variable
+            pEntry->iVar = iCofVar;
+            // set the bound set size
+            pEntry->Size = Kit_WordCountOnes( Entry & 0xFFFF );
+            // get the number of overlapping vars
+            pEntry->Over = Kit_WordCountOnes( Entry & (Entry >> 16) );
+            // get the support reduction
+            pEntry->SRed  = pEntry->Size - 1 - pEntry->Over;
+            assert( pEntry->SRed > 0 );
+        }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints one set.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Lpk_MapSuppPrintSet( Lpk_Set_t * pSet, int i )
+{
+    unsigned Entry;
+    Entry = pSet->uSubset0 | pSet->uSubset1;
+    printf( "%2d : ", i );
+    printf( "Var = %c  ",  'a' + pSet->iVar );
+    printf( "Size = %2d  ", pSet->Size );
+    printf( "Over = %2d  ", pSet->Over );
+    printf( "SRed = %2d  ", pSet->SRed );
+    Lpk_PrintSetOne( Entry );
+    printf( "              " );
+    Lpk_PrintSetOne( Entry >> 16 );
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Evaluates the cofactors.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned Lpk_MapSuppRedDecSelect( Lpk_Man_t * p, unsigned * pTruth, int nVars, int * piVar, int * piVarReused )
+{
+    static int nStoreSize = 256;
+    static Lpk_Set_t pStore[256], * pSet, * pSetBest;
+    Kit_DsdNtk_t * ppNtks[2], * pTemp;
+    Vec_Int_t * vSets0 = p->vSets[0];
+    Vec_Int_t * vSets1 = p->vSets[1];
+    unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 );
+    unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 );
+    int nSets, i, SizeMax;
+    unsigned Entry;
+
+    // collect decomposable subsets for each pair of cofactors
+    nSets = 0;
+    for ( i = 0; i < nVars; i++ )
+    {
+        printf( "Evaluating variable %c:\n", 'a'+i );
+        // evaluate the cofactor pair
+        Kit_TruthCofactor0New( pCof0, pTruth, nVars, i );
+        Kit_TruthCofactor1New( pCof1, pTruth, nVars, i );
+        // decompose and expand
+        ppNtks[0] = Kit_DsdDecompose( pCof0, nVars );
+        ppNtks[1] = Kit_DsdDecompose( pCof1, nVars );
+        ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] );      Kit_DsdNtkFree( pTemp );
+        ppNtks[1] = Kit_DsdExpand( pTemp = ppNtks[1] );      Kit_DsdNtkFree( pTemp );
+        Kit_DsdPrint( stdout, ppNtks[0] );
+        Kit_DsdPrint( stdout, ppNtks[1] );
+        // compute subsets
+        Lpk_ComputeSets( ppNtks[0], vSets0 );
+        Lpk_ComputeSets( ppNtks[1], vSets1 );
+        // print subsets
+        Lpk_PrintSets( vSets0 );
+        Lpk_PrintSets( vSets1 );
+        // free the networks
+        Kit_DsdNtkFree( ppNtks[0] );
+        Kit_DsdNtkFree( ppNtks[1] );
+        // evaluate the pair
+        Lpk_ComposeSets( vSets0, vSets1, nVars, i, pStore, &nSets, nStoreSize );
+    }
+
+    // print the results
+    printf( "\n" );
+    for ( i = 0; i < nSets; i++ )
+        Lpk_MapSuppPrintSet( pStore + i, i );
+
+    // choose the best subset
+    SizeMax = 0;
+    pSetBest = NULL;
+    for ( i = 0; i < nSets; i++ )
+    {
+        pSet = pStore + i;
+        if ( pSet->Size > p->pPars->nLutSize - 1 )
+            continue;
+        if ( SizeMax < pSet->Size )
+        {
+            pSetBest = pSet;
+            SizeMax = pSet->Size;
+        }
+    }
+    if ( pSetBest == NULL )
+    {
+        printf( "Could not select a subset.\n" );
+        return 0;
+    }
+    else
+    {
+        printf( "Selected the following subset:\n" );
+        Lpk_MapSuppPrintSet( pSetBest, pSetBest - pStore );
+    }
+
+    // prepare the return result
+    // get the remaining variables
+    Entry = ((pSetBest->uSubset0 >> 16) | (pSetBest->uSubset1 >> 16));
+    // get the variables to be removed
+    Entry = Kit_BitMask(nVars) & ~(1<<pSetBest->iVar) & ~Entry;
+    // make sure there are some - otherwise it is not supp-red
+    assert( Entry );
+    // remember the first such variable
+    *piVarReused = Kit_WordFindFirstBit( Entry );
+    *piVar = pSetBest->iVar;
+    return (pSetBest->uSubset1 << 16) | (pSetBest->uSubset0 & 0xFFFF);
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/lpk/lpk_.c b/src/opt/lpk/lpk_.c
new file mode 100644
index 00000000..d8555e08
--- /dev/null
+++ b/src/opt/lpk/lpk_.c
@@ -0,0 +1,48 @@
+/**CFile****************************************************************
+
+  FileName    [lpk_.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Fast Boolean matching for LUT structures.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: lpk_.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "lpkInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/lpk/module.make b/src/opt/lpk/module.make
new file mode 100644
index 00000000..9e7bbc7c
--- /dev/null
+++ b/src/opt/lpk/module.make
@@ -0,0 +1,7 @@
+SRC +=    src/aig/lpk/lpkCore.c \
+    src/aig/lpk/lpkCut.c \
+    src/aig/lpk/lpkMan.c \
+    src/aig/lpk/lpkMap.c \
+    src/aig/lpk/lpkMulti.c \
+    src/aig/lpk/lpkMux.c \
+    src/aig/lpk/lpkSets.c