Version abc70831

15 files changed, 1464 insertions, 91 deletions

diff --git a/abc.dsp b/abc.dsp
index c4f6e05f..a38cb10f 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -1542,6 +1542,22 @@ SOURCE=.\src\opt\lpk\lpk.h
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\opt\lpk\lpkAbcCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\lpk\lpkAbcDsd.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\lpk\lpkAbcFun.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\lpk\lpkAbcMux.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\opt\lpk\lpkCore.c
 # End Source File
 # Begin Source File
diff --git a/src/aig/kit/kit.h b/src/aig/kit/kit.h
index 2f7bbef4..c08bead2 100644
--- a/src/aig/kit/kit.h
+++ b/src/aig/kit/kit.h
@@ -143,6 +143,7 @@ static inline int             Kit_DsdLitRegular( int Lit )           { return Li
  
 static inline unsigned        Kit_DsdObjOffset( int nFans )          { return (nFans >> 2) + ((nFans & 3) > 0);                    }
 static inline unsigned *      Kit_DsdObjTruth( Kit_DsdObj_t * pObj ) { return pObj->Type == KIT_DSD_PRIME ? (unsigned *)pObj->pFans + pObj->Offset: NULL; }
+static inline int             Kit_DsdNtkObjNum( Kit_DsdNtk_t * pNtk ){ return pNtk->nVars + pNtk->nNodes; }
 static inline Kit_DsdObj_t *  Kit_DsdNtkObj( Kit_DsdNtk_t * pNtk, int Id )      { assert( Id >= 0 && Id < pNtk->nVars + pNtk->nNodes ); return Id < pNtk->nVars ? NULL : pNtk->pNodes[Id - pNtk->nVars]; }
 static inline Kit_DsdObj_t *  Kit_DsdNtkRoot( Kit_DsdNtk_t * pNtk )             { return Kit_DsdNtkObj( pNtk, Kit_DsdLit2Var(pNtk->Root) );                      }
 static inline int             Kit_DsdLitIsLeaf( Kit_DsdNtk_t * pNtk, int Lit )   { int Id = Kit_DsdLit2Var(Lit); assert( Id >= 0 && Id < pNtk->nVars + pNtk->nNodes ); return Id < pNtk->nVars; }
@@ -429,6 +430,25 @@ static inline void Kit_TruthMux( unsigned * pOut, unsigned * pIn0, unsigned * pI
     for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
         pOut[w] = (pIn0[w] & ~pCtrl[w]) | (pIn1[w] & pCtrl[w]);
 }
+static inline void Kit_TruthIthVar( unsigned * pTruth, int nVars, int iVar )
+{
+    unsigned Masks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
+    int k, nWords = (nVars <= 5 ? 1 : (1 << (nVars - 5)));
+    if ( iVar < 5 )
+    {
+        for ( k = 0; k < nWords; k++ )
+            pTruth[k] = Masks[iVar];
+    }
+    else
+    {
+        for ( k = 0; k < nWords; k++ )
+            if ( k & (1 << (iVar-5)) )
+                pTruth[k] = ~(unsigned)0;
+            else
+                pTruth[k] = 0;
+    }
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                           ITERATORS                              ///
@@ -453,12 +473,13 @@ extern DdNode *        Kit_SopToBdd( DdManager * dd, Kit_Sop_t * cSop, int nVars
 extern DdNode *        Kit_GraphToBdd( DdManager * dd, Kit_Graph_t * pGraph );
 extern DdNode *        Kit_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars, int fMSBonTop );
 /*=== kitDsd.c ==========================================================*/
-extern Kit_DsdMan_t *  Kit_DsdManAlloc( int nVars );
+extern Kit_DsdMan_t *  Kit_DsdManAlloc( int nVars, int nNodes );
 extern void            Kit_DsdManFree( Kit_DsdMan_t * p );
 extern Kit_DsdNtk_t *  Kit_DsdDeriveNtk( unsigned * pTruth, int nVars, int nLutSize );
 extern unsigned *      Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp );
 extern void            Kit_DsdTruth( Kit_DsdNtk_t * pNtk, unsigned * pTruthRes );
 extern void            Kit_DsdTruthPartial( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned * pTruthRes, unsigned uSupp );
+extern void            Kit_DsdTruthPartialTwo( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp, int iVar, unsigned * pTruthCo, unsigned * pTruthDec );
 extern void            Kit_DsdPrint( FILE * pFile, Kit_DsdNtk_t * pNtk );
 extern void            Kit_DsdPrintExpanded( Kit_DsdNtk_t * pNtk );
 extern void            Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
diff --git a/src/aig/kit/kitDsd.c b/src/aig/kit/kitDsd.c
index 06377cba..354ab6ef 100644
--- a/src/aig/kit/kitDsd.c
+++ b/src/aig/kit/kitDsd.c
@@ -39,7 +39,7 @@
   SeeAlso     []
 
 ***********************************************************************/
-Kit_DsdMan_t * Kit_DsdManAlloc( int nVars )
+Kit_DsdMan_t * Kit_DsdManAlloc( int nVars, int nNodes )
 {
     Kit_DsdMan_t * p;
     p = ALLOC( Kit_DsdMan_t, 1 );
@@ -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( 1024, p->nWords );
+    p->vTtNodes = Vec_PtrAllocSimInfo( nNodes, p->nWords );
     return p;
 }
 
@@ -472,11 +472,40 @@ unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned
   SeeAlso     []
 
 ***********************************************************************/
+void Kit_DsdTruthComputeTwo( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp, int iVar )
+{
+    unsigned * pTruthRes;
+    int i;
+    // if support is specified, request that supports are available
+    if ( uSupp )
+        Kit_DsdGetSupports( pNtk );
+    // assign elementary truth tables
+    assert( pNtk->nVars <= p->nVars );
+    for ( i = 0; i < (int)pNtk->nVars; i++ )
+        Kit_TruthCopy( Vec_PtrEntry(p->vTtNodes, i), Vec_PtrEntry(p->vTtElems, i), p->nVars );
+    // compute truth table for each node
+    pTruthRes = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(pNtk->Root), uSupp );
+    // complement the truth table if needed
+    if ( Kit_DsdLitIsCompl(pNtk->Root) )
+        Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars );
+}
+
+/**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 );
+    p = Kit_DsdManAlloc( pNtk->nVars, Kit_DsdNtkObjNum(pNtk) );
     pTruth = Kit_DsdTruthCompute( p, pNtk, 0 );
     Kit_TruthCopy( pTruthRes, pTruth, pNtk->nVars );
     Kit_DsdManFree( p );
@@ -501,6 +530,29 @@ void Kit_DsdTruthPartial( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned * pTru
 
 /**Function*************************************************************
 
+  Synopsis    [Derives the truth table of the DSD network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Kit_DsdTruthPartialTwo( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp, int iVar, unsigned * pTruthCo, unsigned * pTruthDec )
+{
+    unsigned * pTruth;
+    Kit_DsdObj_t * pRoot;
+    Kit_DsdTruthComputeTwo( p, pNtk, uSupp, iVar );
+    pRoot = Kit_DsdNtkRoot( pNtk );
+    pTruth = Vec_PtrEntry( p->vTtNodes, 2*pRoot->Id+0 );
+    Kit_TruthCopy( pTruthCo, pTruth, p->nVars );
+    pTruth = Vec_PtrEntry( p->vTtNodes, 2*pRoot->Id+1 );
+    Kit_TruthCopy( pTruthDec, pTruth, p->nVars );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Counts the number of blocks of the given number of inputs.]
 
   Description []
@@ -1620,7 +1672,7 @@ int Kit_DsdEval( unsigned * pTruth, int nVars, int nLutSize )
 //    printf( "Eval = %d.\n", Result );
 
     // recompute the truth table
-    p = Kit_DsdManAlloc( nVars );
+    p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk) );
     pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 );
     if ( !Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
         printf( "Verification failed.\n" );
@@ -1645,7 +1697,7 @@ void Kit_DsdVerify( Kit_DsdNtk_t * pNtk, unsigned * pTruth, int nVars )
 {
     Kit_DsdMan_t * p;
     unsigned * pTruthC;
-    p = Kit_DsdManAlloc( nVars );
+    p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk) );
     pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 );
     if ( !Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
         printf( "Verification failed.\n" );
@@ -1687,7 +1739,7 @@ void Kit_DsdTest( unsigned * pTruth, int nVars )
 //        Kit_DsdTestCofs( pNtk, pTruth );
 
     // recompute the truth table
-    p = Kit_DsdManAlloc( nVars );
+    p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk) );
     pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 );
 //    Extra_PrintBinary( stdout, pTruth, 1 << nVars ); printf( "\n" );
 //    Extra_PrintBinary( stdout, pTruthC, 1 << nVars ); printf( "\n" );
@@ -1757,7 +1809,7 @@ void Kit_DsdPrecompute4Vars()
             printf( "\n" );
 */
 
-        p = Kit_DsdManAlloc( 4 );
+        p = Kit_DsdManAlloc( 4, Kit_DsdNtkObjNum(pNtk) );
         pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 );
         if ( !Extra_TruthIsEqual( &uTruth, pTruthC, 4 ) )
             printf( "Verification failed.\n" );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 3902830d..f740ee18 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -5160,7 +5160,7 @@ usage:
   Description []
                
   SideEffects []
-
+ 
   SeeAlso     []
 
 ***********************************************************************/
@@ -11278,6 +11278,11 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Only works for structrally hashed networks.\n" );
         return 1;
     }
+    if ( !Abc_NtkLatchNum(pNtk) )
+    {
+        fprintf( pErr, "Only works for sequential networks.\n" );
+        return 1;
+    }
     // modify the current network
     pNtkRes = Abc_NtkDarLatchSweep( pNtk, fLatchSweep, fVerbose );
     if ( pNtkRes == NULL )
@@ -11367,6 +11372,11 @@ int Abc_CommandCycle( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Only works for strashed networks or logic SOP networks.\n" );
         return 1;
     }
+    if ( !Abc_NtkLatchNum(pNtk) )
+    {
+        fprintf( pErr, "Only works for sequential networks.\n" );
+        return 1;
+    }
 
     if ( Abc_NtkIsStrash(pNtk) )
         Abc_NtkCycleInitState( pNtk, nFrames, fVerbose );
@@ -11457,7 +11467,11 @@ int Abc_CommandXsim( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Only works for strashed networks.\n" );
         return 1;
     }
-
+    if ( !Abc_NtkLatchNum(pNtk) )
+    {
+        fprintf( pErr, "Only works for sequential networks.\n" );
+        return 1;
+    }
     Abc_NtkXValueSimulate( pNtk, nFrames, fXInputs, fXState, fVerbose );
     return 0;
 
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 40a52ce8..f8f7d20e 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -834,8 +834,8 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer
     // conver to the manager
     pMan = Abc_NtkToDar( pNtk, 0 );
     // derive CNF
-//    pCnf = Cnf_Derive( pMan, 0 );
-    pCnf = Cnf_DeriveSimple( pMan, 0 );
+    pCnf = Cnf_Derive( pMan, 0 );
+//    pCnf = Cnf_DeriveSimple( pMan, 0 );
     // convert into the SAT solver
     pSat = Cnf_DataWriteIntoSolver( pCnf );
     vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan );
diff --git a/src/base/abci/abcPart.c b/src/base/abci/abcPart.c
index f0989b23..23e9d28d 100644
--- a/src/base/abci/abcPart.c
+++ b/src/base/abci/abcPart.c
@@ -366,7 +366,7 @@ timeFind += clock() - clk2;
             Vec_PtrPush( vPartsAll, vPart );
             Vec_PtrPush( vPartSuppsAll, vPartSupp );
 
-            Vec_PtrPush( vPartSuppsChar, Abc_NtkSuppCharStart(vOne, Abc_NtkPiNum(pNtk)) );
+            Vec_PtrPush( vPartSuppsChar, Abc_NtkSuppCharStart(vOne, Abc_NtkCiNum(pNtk)) );
         }
         else
         {
@@ -380,7 +380,7 @@ timeFind += clock() - clk2;
             // reinsert new support
             Vec_PtrWriteEntry( vPartSuppsAll, iPart, vPartSupp );
 
-            Abc_NtkSuppCharAdd( Vec_PtrEntry(vPartSuppsChar, iPart), vOne, Abc_NtkPiNum(pNtk) );
+            Abc_NtkSuppCharAdd( Vec_PtrEntry(vPartSuppsChar, iPart), vOne, Abc_NtkCiNum(pNtk) );
         }
     }
 
@@ -801,7 +801,7 @@ Abc_Ntk_t * Abc_NtkFraigPartitioned( Abc_Ntk_t * pNtk, void * pParams )
     // perform partitioning
     assert( Abc_NtkIsStrash(pNtk) );
 //    vParts = Abc_NtkPartitionNaive( pNtk, 20 );
-    vParts = Abc_NtkPartitionSmart( pNtk, 0, 1 );
+    vParts = Abc_NtkPartitionSmart( pNtk, 0, 0 );
 
     Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "unset progressbar" );
 
diff --git a/src/opt/lpk/lpkAbcCore.c b/src/opt/lpk/lpkAbcCore.c
new file mode 100644
index 00000000..53b2668d
--- /dev/null
+++ b/src/opt/lpk/lpkAbcCore.c
@@ -0,0 +1,158 @@
+/**CFile****************************************************************
+
+  FileName    [lpkAbcCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Fast Boolean matching for LUT structures.]
+
+  Synopsis    [The new core procedure.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: lpkAbcCore.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "lpkInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Implements the function.]
+
+  Description [Returns the node implementing this function.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Lpk_FunImplement( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Lpk_Fun_t * p )
+{
+    Abc_Obj_t * pObjNew;
+    int i;
+    pObjNew = Abc_NtkCreateNode( pNtk );
+    for ( i = 0; i < (int)p->nVars; i++ )
+        Abc_ObjAddFanin( pObjNew, Vec_PtrEntry(vLeaves, p->pFanins[i]) );
+    Abc_ObjLevelNew( pObjNew );
+    // create the logic function
+    {
+        extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
+        // allocate memory for the ISOP
+        Vec_Int_t * vCover = Vec_IntAlloc( 0 );
+        // transform truth table into the decomposition tree
+        Kit_Graph_t * pGraph = Kit_TruthToGraph( Lpk_FunTruth(p, 0), p->nVars, vCover );
+        // derive the AIG for the decomposition tree
+        pObjNew->pData = Kit_GraphToHop( pNtk->pManFunc, pGraph );
+        Kit_GraphFree( pGraph );
+        Vec_IntFree( vCover );
+    }
+    return pObjNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Implements the function.]
+
+  Description [Returns the node implementing this function.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Lpk_LptImplement( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, int nLeavesOld )
+{
+    Lpk_Fun_t * pFun;
+    Abc_Obj_t * pRes;
+    int i;
+    for ( i = Vec_PtrSize(vLeaves) - 1; i >= nLeavesOld; i-- )
+    {
+        pFun = Vec_PtrEntry( vLeaves, i );
+        pRes = Lpk_FunImplement( pNtk, vLeaves, pFun );
+        Vec_PtrWriteEntry( vLeaves, i, pRes );
+        Lpk_FunFree( pFun );
+    }
+    return pRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Decomposes the function using recursive MUX decomposition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Lpk_LpkDecompose_rec( Lpk_Fun_t * p )
+{
+    Lpk_Fun_t * p2;
+    int VarPol;
+    assert( p->nAreaLim > 0 );
+    if ( p->nVars <= p->nLutK )
+        return 1;
+    // check if decomposition exists
+    VarPol = Lpk_FunAnalizeMux( p );
+    if ( VarPol == -1 )
+        return 0;
+    // split and call recursively
+    p2 = Lpk_FunSplitMux( p, VarPol );
+    if ( !Lpk_LpkDecompose_rec( p2 ) )
+        return 0;
+    return Lpk_LpkDecompose_rec( p );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Decomposes the function using recursive MUX decomposition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Lpk_LpkDecompose( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, unsigned * pTruth, int nLutK, int AreaLim, int DelayLim )
+{
+    Lpk_Fun_t * p;
+    Abc_Obj_t * pObjNew = NULL;
+    int i, nLeaves;
+    // create the starting function
+    nLeaves = Vec_PtrSize( vLeaves );
+    p = Lpk_FunCreate( pNtk, vLeaves, pTruth, nLutK, AreaLim, DelayLim );
+    Lpk_FunSuppMinimize( p );
+    // decompose the function 
+    if ( Lpk_LpkDecompose_rec(p) )
+        pObjNew = Lpk_LptImplement( pNtk, vLeaves, nLeaves );
+    else
+    {
+        for ( i = Vec_PtrSize(vLeaves) - 1; i >= nLeaves; i-- )
+            Lpk_FunFree( Vec_PtrEntry(vLeaves, i) );
+    }
+    Vec_PtrShrink( vLeaves, nLeaves );
+    return pObjNew;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/lpk/lpkAbcDsd.c b/src/opt/lpk/lpkAbcDsd.c
new file mode 100644
index 00000000..893844e0
--- /dev/null
+++ b/src/opt/lpk/lpkAbcDsd.c
@@ -0,0 +1,395 @@
+/**CFile****************************************************************
+
+  FileName    [lpkAbcDsd.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: lpkAbcDsd.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "lpkInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the variable whose cofs have min sum of supp sizes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Lpk_FunComputeMinSuppSizeVar( Lpk_Fun_t * p, unsigned ** ppTruths, int nTruths, unsigned ** ppCofs )
+{
+    int i, Var, VarBest, nSuppSize0, nSuppSize1, nSuppTotalMin, nSuppTotalCur, nSuppMaxMin, nSuppMaxCur;
+    VarBest = -1;
+    Lpk_SuppForEachVar( p->uSupp, Var )
+    {
+        nSuppMaxCur = 0;
+        nSuppTotalCur = 0;
+        for ( i = 0; i < nTruths; i++ )
+        {
+            Kit_TruthCofactor0New( ppCofs[2*i+0], ppTruths[i], p->nVars, Var );
+            Kit_TruthCofactor1New( ppCofs[2*i+1], ppTruths[i], p->nVars, Var );
+            nSuppSize0 = Kit_TruthSupportSize( ppCofs[2*i+0], p->nVars );
+            nSuppSize1 = Kit_TruthSupportSize( ppCofs[2*i+1], p->nVars );
+            nSuppMaxCur = ABC_MAX( nSuppMaxCur, nSuppSize0 );
+            nSuppMaxCur = ABC_MAX( nSuppMaxCur, nSuppSize1 );
+            nSuppTotalCur += nSuppSize0 + nSuppSize1;
+        }
+        if ( VarBest == -1 || nSuppTotalMin > nSuppTotalCur ||
+             (nSuppTotalMin == nSuppTotalCur && nSuppMaxMin > nSuppMaxCur) )
+        {
+            VarBest = Var;
+            nSuppMaxMin = nSuppMaxCur;
+            nSuppTotalMin = nSuppTotalCur;
+        }
+    }
+    // recompute cofactors for the best var
+    for ( i = 0; i < nTruths; i++ )
+    {
+        Kit_TruthCofactor0New( ppCofs[2*i+0], ppTruths[i], p->nVars, VarBest );
+        Kit_TruthCofactor1New( ppCofs[2*i+1], ppTruths[i], p->nVars, VarBest );
+    }
+    return VarBest;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively computes decomposable subsets.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned Lpk_ComputeBoundSets_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_ComputeBoundSets_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_ComputeBoundSets_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     []
+
+***********************************************************************/
+Vec_Int_t * Lpk_ComputeBoundSets( Kit_DsdNtk_t * p, int nSizeMax )
+{
+    Vec_Int_t * vSets;
+    unsigned uSupport, Entry;
+    int Number, i;
+    assert( p->nVars <= 16 );
+    vSets = Vec_IntAlloc( 100 );
+    Vec_IntPush( vSets, 0 );
+    if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_CONST1 )
+        return vSets;
+    if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_VAR )
+    {
+        uSupport = ( 1 << Kit_DsdLit2Var(Kit_DsdNtkRoot(p)->pFans[0]) );
+        Vec_IntPush( vSets, uSupport );
+        return vSets;
+    }
+    uSupport = Lpk_ComputeBoundSets_rec( p, p->Root, vSets );
+    assert( (uSupport & 0xFFFF0000) == 0 );
+    Vec_IntPush( vSets, uSupport );
+    // set the remaining variables
+    Vec_IntForEachEntry( vSets, Number, i )
+    {
+        Entry = Number;
+        Vec_IntWriteEntry( vSets, i, Entry | ((uSupport & ~Entry) << 16) );
+    }
+    return vSets;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Merges two bound sets.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Lpk_MergeBoundSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1 )
+{
+    Vec_Int_t * vSets;
+    int Entry0, Entry1, Entry;
+    int i, k;
+    vSets = Vec_IntAlloc( 100 );
+    Vec_IntForEachEntry( vSets0, Entry0, i )
+    Vec_IntForEachEntry( vSets1, Entry1, k )
+    {
+        Entry = Entry0 | Entry1;
+        if ( (Entry & (Entry >> 16)) )
+            continue;
+        Vec_IntPush( vSets, Entry );
+    }
+    return vSets;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates truth tables for cofactors.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Lpk_FunAllocTruthTables( Lpk_Fun_t * p, int nCofDepth, unsigned * ppTruths[5][16] )
+{
+    int i;
+    assert( nCofDepth <= 4 );
+    ppTruths[0][0] = Lpk_FunTruth( p, 0 );
+    if ( nCofDepth >= 1 )
+    {
+        ppTruths[1][0] = Lpk_FunTruth( p, 1 );
+        ppTruths[1][1] = Lpk_FunTruth( p, 2 );
+    }
+    if ( nCofDepth >= 2 )
+    {
+        ppTruths[2][0] = ALLOC( unsigned, Kit_TruthWordNum(p->nVars) * 4 );
+        for ( i = 1; i < 4; i++ )
+            ppTruths[2][i] = ppTruths[2][0] + Kit_TruthWordNum(p->nVars) * i;
+    }
+    if ( nCofDepth >= 3 )
+    {
+        ppTruths[3][0] = ALLOC( unsigned, Kit_TruthWordNum(p->nVars) * 8 );
+        for ( i = 1; i < 8; i++ )
+            ppTruths[3][i] = ppTruths[3][0] + Kit_TruthWordNum(p->nVars) * i;
+    }
+    if ( nCofDepth >= 4 )
+    {
+        ppTruths[4][0] = ALLOC( unsigned, Kit_TruthWordNum(p->nVars) * 16 );
+        for ( i = 1; i < 16; i++ )
+            ppTruths[4][i] = ppTruths[4][0] + Kit_TruthWordNum(p->nVars) * i;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates truth tables for cofactors.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Lpk_FunFreeTruthTables( Lpk_Fun_t * p, int nCofDepth, unsigned * ppTruths[5][16] )
+{
+    if ( nCofDepth >= 2 )
+        free( ppTruths[2][0] );
+    if ( nCofDepth >= 3 )
+        free( ppTruths[3][0] );
+    if ( nCofDepth >= 4 )
+        free( ppTruths[4][0] );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs DSD-based decomposition of the function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Lpk_Res_t * Lpk_FunAnalizeDsd( Lpk_Fun_t * p, int nCofDepth )
+{
+    static Lpk_Res_t Res, * pRes = &Res;
+    unsigned * ppTruths[5][16];
+    Vec_Int_t * pvBSets[4][8];
+    Kit_DsdNtk_t * pNtkDec, * pTemp;
+    unsigned uBoundSet;
+    int i, k, nVarsBS, nVarsRem, Delay, Area;
+    Lpk_FunAllocTruthTables( p, nCofDepth, ppTruths );
+    // find the best cofactors
+    memset( pRes, 0, sizeof(Lpk_Res_t) );
+    pRes->nCofVars = nCofDepth;
+    for ( i = 0; i < nCofDepth; i++ )
+        pRes->pCofVars[i] = Lpk_FunComputeMinSuppSizeVar( p, ppTruths[i], 1<<i, ppTruths[i+1] );
+    // derive decomposed networks
+    for ( i = 0; i < (1<<nCofDepth); i++ )
+    {
+        pNtkDec = Kit_DsdDecompose( ppTruths[nCofDepth][i], p->nVars );
+        pNtkDec = Kit_DsdExpand( pTemp = pNtkDec );      Kit_DsdNtkFree( pTemp );
+        pvBSets[nCofDepth][i] = Lpk_ComputeBoundSets( pNtkDec, p->nLutK - nCofDepth );
+        Kit_DsdNtkFree( pNtkDec );
+    }
+    // derive the set of feasible boundsets
+    for ( i = nCofDepth - 1; i >= 0; i-- )
+        for ( k = 0; k < (1<<i); k++ )
+            pvBSets[i][k] = Lpk_MergeBoundSets( pvBSets[i+1][2*k+0], pvBSets[i+1][2*k+1] );
+    // compare the resulting boundsets
+    Vec_IntForEachEntry( pvBSets[0][0], uBoundSet, i )
+    {
+        if ( uBoundSet == 0 )
+            continue;
+        assert( (uBoundSet & (uBoundSet >> 16)) == 0 );
+        nVarsBS = Kit_WordCountOnes( uBoundSet & 0xFFFF );
+        nVarsRem = p->nVars - nVarsBS + nCofDepth + 1;
+        Delay = 1 + Lpk_SuppDelay( uBoundSet & 0xFFFF, p->pDelays );
+        Area = 1 + Lpk_LutNumLuts( nVarsRem, p->nLutK );
+        if ( Delay > (int)p->nDelayLim || Area > (int)p->nAreaLim )
+            continue;
+        if ( uBoundSet == 0 || pRes->DelayEst > Delay || pRes->DelayEst == Delay && pRes->nSuppSizeL > nVarsRem )
+        {
+            pRes->nBSVars = nVarsBS;
+            pRes->BSVars = uBoundSet;
+            pRes->nSuppSizeS = nVarsBS;
+            pRes->nSuppSizeL = nVarsRem;
+            pRes->DelayEst = Delay;
+            pRes->AreaEst = Area;
+        }
+    }
+    // free cofactor storage
+    Lpk_FunFreeTruthTables( p, nCofDepth, ppTruths );
+    return pRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Splits the function into two subfunctions using DSD.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Lpk_Fun_t * Lpk_FunSplitDsd( Lpk_Fun_t * p, char * pCofVars, int nCofVars, unsigned uBoundSet )
+{
+    Kit_DsdMan_t * pDsdMan;
+    Kit_DsdNtk_t * pNtkDec, * pTemp;
+    unsigned * pTruth  = Lpk_FunTruth( p, 0 );
+    unsigned * pTruth0 = Lpk_FunTruth( p, 1 );
+    unsigned * pTruth1 = Lpk_FunTruth( p, 2 );
+    Lpk_Fun_t * pNew;
+    unsigned * ppTruths[5][16];
+    char pBSVars[5];
+    int i, k, nVars, nCofs;
+    // get the bound set variables
+    nVars = Lpk_SuppToVars( uBoundSet, pBSVars );
+    // compute the cofactors
+    Lpk_FunAllocTruthTables( p, nCofVars, ppTruths );
+    for ( i = 0; i < nCofVars; i++ )
+        for ( k = 0; k < (1<<i); k++ )
+        {
+            Kit_TruthCofactor0New( ppTruths[i+1][2*k+0], ppTruths[i][k], p->nVars, pCofVars[i] );
+            Kit_TruthCofactor1New( ppTruths[i+1][2*k+1], ppTruths[i][k], p->nVars, pCofVars[i] );
+        }
+    // decompose each cofactor w.r.t. the bound set
+    nCofs = (1<<nCofVars);
+    pDsdMan = Kit_DsdManAlloc( p->nVars, p->nVars * 4 );
+    for ( k = 0; k < nCofs; k++ )
+    {
+        pNtkDec = Kit_DsdDecompose( ppTruths[nCofVars][k], p->nVars );
+        pNtkDec = Kit_DsdExpand( pTemp = pNtkDec );      Kit_DsdNtkFree( pTemp );
+        Kit_DsdTruthPartialTwo( pDsdMan, pNtkDec, uBoundSet, pBSVars[0], ppTruths[nCofVars+1][k], ppTruths[nCofVars+1][nCofs+k] );
+        Kit_DsdNtkFree( pNtkDec );
+    }
+    Kit_DsdManFree( pDsdMan );
+    // compute the composition function
+    for ( i = nCofVars - 1; i >= 1; i-- )
+        for ( k = 0; k < (1<<i); k++ )
+            Kit_TruthMuxVar( ppTruths[i][k], ppTruths[i+1][2*k+0], ppTruths[i+1][2*k+1], nVars, pCofVars[i] );
+    // now the composition/decomposition functions are in pTruth0/pTruth1
+
+    // derive the new component
+    pNew = Lpk_FunDup( p, pTruth1 );
+    // update the old component
+    Kit_TruthCopy( pTruth, pTruth0, p->nVars );
+    p->uSupp = Kit_TruthSupport( pTruth0, p->nVars );
+    p->pFanins[pBSVars[0]] = pNew->Id;
+    p->pDelays[pBSVars[0]] = Lpk_SuppDelay( pNew->uSupp, pNew->pDelays );
+    // support minimize both
+    Lpk_FunSuppMinimize( p );
+    Lpk_FunSuppMinimize( pNew );
+    // update delay and area requirements
+    pNew->nDelayLim = p->nDelayLim - 1;
+    pNew->nAreaLim = 1;
+    p->nAreaLim = p->nAreaLim - 1;
+
+    // free cofactor storage
+    Lpk_FunFreeTruthTables( p, nCofVars, ppTruths );
+    return pNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/lpk/lpkAbcFun.c b/src/opt/lpk/lpkAbcFun.c
new file mode 100644
index 00000000..f7d2f402
--- /dev/null
+++ b/src/opt/lpk/lpkAbcFun.c
@@ -0,0 +1,204 @@
+/**CFile****************************************************************
+
+  FileName    [lpkAbcFun.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Fast Boolean matching for LUT structures.]
+
+  Synopsis    [Procedures working on decomposed functions.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: lpkAbcFun.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "lpkInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates the function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Lpk_Fun_t * Lpk_FunAlloc( int nVars )
+{
+    Lpk_Fun_t * p;
+    p = (Lpk_Fun_t *)malloc( sizeof(Lpk_Fun_t) + sizeof(unsigned) * Kit_TruthWordNum(nVars) * 3 );
+    memset( p, 0, sizeof(Lpk_Fun_t) );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes the function]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Lpk_FunFree( Lpk_Fun_t * p )
+{
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the starting function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Lpk_Fun_t * Lpk_FunCreate( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, unsigned * pTruth, int nLutK, int AreaLim, int DelayLim )
+{
+    Lpk_Fun_t * p;
+    Abc_Obj_t * pNode;
+    int i;
+    p = Lpk_FunAlloc( Vec_PtrSize(vLeaves) );
+    p->Id = Vec_PtrSize(vLeaves);
+    p->vNodes = vLeaves;
+    p->nVars = Vec_PtrSize(vLeaves);
+    p->nLutK = nLutK;
+    p->nAreaLim = AreaLim;
+    p->nDelayLim = DelayLim;
+    p->uSupp = Kit_TruthSupport( pTruth, p->nVars );
+    Kit_TruthCopy( Lpk_FunTruth(p,0), pTruth, p->nVars );
+    Vec_PtrForEachEntry( vLeaves, pNode, i )
+    {
+        p->pFanins[i] = i;
+        p->pDelays[i] = pNode->Level;
+    }
+    Vec_PtrPush( p->vNodes, p );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the new function with the given truth table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Lpk_Fun_t * Lpk_FunDup( Lpk_Fun_t * p, unsigned * pTruth )
+{
+    Lpk_Fun_t * pNew;
+    pNew = Lpk_FunAlloc( p->nVars );
+    pNew->Id = Vec_PtrSize(p->vNodes);
+    pNew->vNodes = p->vNodes;
+    pNew->nVars = p->nVars;
+    pNew->nLutK = p->nLutK;
+    pNew->nAreaLim = p->nAreaLim;
+    pNew->nDelayLim = p->nDelayLim;
+    pNew->uSupp = Kit_TruthSupport( pTruth, p->nVars );
+    Kit_TruthCopy( Lpk_FunTruth(pNew,0), pTruth, p->nVars );
+    memcpy( pNew->pFanins, p->pFanins, 16 );
+    memcpy( pNew->pDelays, p->pDelays, 16 );
+    Vec_PtrPush( p->vNodes, pNew );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Minimizes support of the function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Lpk_FunSuppMinimize( Lpk_Fun_t * p )
+{
+    int j, k, nVarsNew;
+    // compress the truth table
+    if ( p->uSupp == Kit_BitMask(p->nVars) )
+        return;
+    // minimize support
+    nVarsNew = Kit_WordCountOnes(p->uSupp);
+    Kit_TruthShrink( Lpk_FunTruth(p, 1), Lpk_FunTruth(p, 0), nVarsNew, p->nVars, p->uSupp, 1 );
+    for ( j = k = 0; j < (int)p->nVars; j++ )
+        if ( p->uSupp & (1 << j) )
+        {
+            p->pFanins[k] = p->pFanins[j];
+            p->pDelays[k] = p->pDelays[j];
+            k++;
+        }
+    assert( k == nVarsNew );
+    p->nVars = k;
+    p->uSupp = Kit_BitMask(p->nVars);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Get the delay of the bound set.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Lpk_SuppDelay( unsigned uSupp, char * pDelays )
+{
+    int Delay, Var;
+    Delay = 0;
+    Lpk_SuppForEachVar( uSupp, Var )
+        Delay = ABC_MAX( Delay, pDelays[Var] );
+    return Delay + 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts support into variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Lpk_SuppToVars( unsigned uBoundSet, char * pVars )
+{
+    int i, nVars = 0;
+    Lpk_SuppForEachVar( uBoundSet, i )
+        pVars[nVars++] = i;
+    return nVars;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/lpk/lpkAbcMux.c b/src/opt/lpk/lpkAbcMux.c
new file mode 100644
index 00000000..1525a7e0
--- /dev/null
+++ b/src/opt/lpk/lpkAbcMux.c
@@ -0,0 +1,254 @@
+/**CFile****************************************************************
+
+  FileName    [lpkAbcMux.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Fast Boolean matching for LUT structures.]
+
+  Synopsis    [Iterative MUX decomposition.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: lpkAbcMux.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "lpkInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Computes cofactors w.r.t. the given var.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Lpk_FunComputeCofs( Lpk_Fun_t * p, int iVar )
+{
+    unsigned * pTruth  = Lpk_FunTruth( p, 0 );
+    unsigned * pTruth0 = Lpk_FunTruth( p, 1 );
+    unsigned * pTruth1 = Lpk_FunTruth( p, 2 );
+    Kit_TruthCofactor0New( pTruth0, pTruth, p->nVars, iVar );
+    Kit_TruthCofactor1New( pTruth1, pTruth, p->nVars, iVar );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes cofactors w.r.t. each variable.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Lpk_FunComputeCofSupps( Lpk_Fun_t * p, unsigned * puSupps )
+{
+    unsigned * pTruth  = Lpk_FunTruth( p, 0 );
+    unsigned * pTruth0 = Lpk_FunTruth( p, 1 );
+    unsigned * pTruth1 = Lpk_FunTruth( p, 2 );
+    int Var;
+    Lpk_SuppForEachVar( p->uSupp, Var )
+    {
+        Lpk_FunComputeCofs( p, Var );
+        puSupps[2*Var+0] = Kit_TruthSupport( pTruth0, p->nVars );
+        puSupps[2*Var+1] = Kit_TruthSupport( pTruth1, p->nVars );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks the possibility of MUX decomposition.]
+
+  Description [Returns the best variable to use for MUX decomposition.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Lpk_FunAnalizeMux( Lpk_Fun_t * p )
+{
+    unsigned puSupps[32] = {0};
+    int nSuppSize0, nSuppSize1, Delay, Delay0, Delay1, DelayA, DelayB;
+    int Var, Area, Polarity, VarBest, AreaBest, PolarityBest, nSuppSizeBest;
+
+    if ( p->nVars > p->nAreaLim * (p->nLutK - 1) + 1 )
+        return -1;
+    // get cofactor supports for each variable
+    Lpk_FunComputeCofSupps( p, puSupps );
+    // derive the delay and area of each MUX-decomposition
+    VarBest = -1;
+    Lpk_SuppForEachVar( p->uSupp, Var )
+    {
+        nSuppSize0 = Kit_WordCountOnes(puSupps[2*Var+0]);
+        nSuppSize1 = Kit_WordCountOnes(puSupps[2*Var+1]);
+        if ( nSuppSize0 <= (int)p->nLutK - 2 && nSuppSize1 <= (int)p->nLutK - 2 )
+        {
+            // include cof var into 0-block
+            DelayA = Lpk_SuppDelay( puSupps[2*Var+0] | (1<<Var), p->pDelays );
+            DelayB = Lpk_SuppDelay( puSupps[2*Var+1]           , p->pDelays );
+            Delay0 = ABC_MAX( DelayA, DelayB + 1 );
+            // include cof var into 1-block
+            DelayA = Lpk_SuppDelay( puSupps[2*Var+1] | (1<<Var), p->pDelays );
+            DelayB = Lpk_SuppDelay( puSupps[2*Var+0]           , p->pDelays );
+            Delay1 = ABC_MAX( DelayA, DelayB + 1 );
+            // get the best delay
+            Delay = ABC_MIN( Delay0, Delay1 );
+            Area = 2;
+            Polarity = (int)(Delay1 == Delay);
+        }
+        else if ( nSuppSize0 <= (int)p->nLutK - 2 )
+        {
+            DelayA = Lpk_SuppDelay( puSupps[2*Var+0] | (1<<Var), p->pDelays );
+            DelayB = Lpk_SuppDelay( puSupps[2*Var+1]           , p->pDelays );
+            Delay = ABC_MAX( DelayA, DelayB + 1 );
+            Area = 1 + Lpk_LutNumLuts( nSuppSize1, p->nLutK );
+            Polarity = 0;
+        }
+        else if ( nSuppSize0 <= (int)p->nLutK )
+        {
+            DelayA = Lpk_SuppDelay( puSupps[2*Var+1] | (1<<Var), p->pDelays );
+            DelayB = Lpk_SuppDelay( puSupps[2*Var+0]           , p->pDelays );
+            Delay = ABC_MAX( DelayA, DelayB + 1 );
+            Area = 1 + Lpk_LutNumLuts( nSuppSize1+2, p->nLutK );
+            Polarity = 1;
+        }
+        else if ( nSuppSize1 <= (int)p->nLutK - 2 )
+        {
+            DelayA = Lpk_SuppDelay( puSupps[2*Var+1] | (1<<Var), p->pDelays );
+            DelayB = Lpk_SuppDelay( puSupps[2*Var+0]           , p->pDelays );
+            Delay = ABC_MAX( DelayA, DelayB + 1 );
+            Area = 1 + Lpk_LutNumLuts( nSuppSize0, p->nLutK );
+            Polarity = 1;
+        }
+        else if ( nSuppSize1 <= (int)p->nLutK )
+        {
+            DelayA = Lpk_SuppDelay( puSupps[2*Var+0] | (1<<Var), p->pDelays );
+            DelayB = Lpk_SuppDelay( puSupps[2*Var+1]           , p->pDelays );
+            Delay = ABC_MAX( DelayA, DelayB + 1 );
+            Area = 1 + Lpk_LutNumLuts( nSuppSize0+2, p->nLutK );
+            Polarity = 0;
+        }
+        else
+        {
+            // include cof var into 0-block
+            DelayA = Lpk_SuppDelay( puSupps[2*Var+0] | (1<<Var), p->pDelays );
+            DelayB = Lpk_SuppDelay( puSupps[2*Var+1]           , p->pDelays );
+            Delay0 = ABC_MAX( DelayA, DelayB + 1 );
+            // include cof var into 1-block
+            DelayA = Lpk_SuppDelay( puSupps[2*Var+1] | (1<<Var), p->pDelays );
+            DelayB = Lpk_SuppDelay( puSupps[2*Var+0]           , p->pDelays );
+            Delay1 = ABC_MAX( DelayA, DelayB + 1 );
+            // get the best delay
+            Delay = ABC_MIN( Delay0, Delay1 );
+            if ( Delay == Delay0 )
+                Area = Lpk_LutNumLuts( nSuppSize0+2, p->nLutK ) + Lpk_LutNumLuts( nSuppSize1, p->nLutK );
+            else
+                Area = Lpk_LutNumLuts( nSuppSize1+2, p->nLutK ) + Lpk_LutNumLuts( nSuppSize0, p->nLutK );
+            Polarity = (int)(Delay1 == Delay);
+        }
+        // find the best variable
+        if ( Delay > (int)p->nDelayLim )
+            continue;
+        if ( Area > (int)p->nAreaLim )
+            continue;
+        if ( VarBest == -1 || AreaBest > Area || (AreaBest == Area && nSuppSizeBest > nSuppSize0+nSuppSize1) )
+        {
+            VarBest = Var;
+            AreaBest = Area;
+            PolarityBest = Polarity;
+            nSuppSizeBest = nSuppSize0+nSuppSize1;
+        }
+    }
+    return (VarBest == -1)? -1 : (2*VarBest + Polarity);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms the function decomposed by the MUX decomposition.]
+
+  Description [Returns the best variable to use for MUX decomposition.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Lpk_Fun_t * Lpk_FunSplitMux( Lpk_Fun_t * p, int VarPol )
+{
+    Lpk_Fun_t * pNew;
+    unsigned * pTruth  = Lpk_FunTruth( p, 0 );
+    unsigned * pTruth0 = Lpk_FunTruth( p, 1 );
+    unsigned * pTruth1 = Lpk_FunTruth( p, 2 );
+    int Var = VarPol / 2;
+    int Pol = VarPol % 2;
+    int iVarVac;
+    assert( VarPol >= 0 && VarPol < 2 * (int)p->nVars );
+    assert( p->nAreaLim >= 2 );
+    Lpk_FunComputeCofs( p, Var );
+    if ( Pol == 0 )
+    {
+        // derive the new component
+        pNew = Lpk_FunDup( p, pTruth1 );
+        // update the old component
+        p->uSupp = Kit_TruthSupport( pTruth0, p->nVars );
+        iVarVac = Kit_WordFindFirstBit( ~(p->uSupp | (1 << Var)) );
+        assert( iVarVac < (int)p->nVars );
+        Kit_TruthIthVar( pTruth, p->nVars, iVarVac );
+        // update the truth table
+        Kit_TruthMux( pTruth, pTruth0, pTruth1, pTruth, p->nVars );
+        p->pFanins[iVarVac] = pNew->Id;
+        p->pDelays[iVarVac] = Lpk_SuppDelay( pNew->uSupp, pNew->pDelays );
+        // support minimize both
+        Lpk_FunSuppMinimize( p );
+        Lpk_FunSuppMinimize( pNew );
+        // update delay and area requirements
+        pNew->nDelayLim = p->nDelayLim - 1;
+        if ( p->nVars <= p->nLutK )
+        {
+            pNew->nAreaLim = p->nAreaLim - 1;
+            p->nAreaLim = 1;
+        }
+        else if ( pNew->nVars <= pNew->nLutK )
+        {
+            pNew->nAreaLim = 1;
+            p->nAreaLim = p->nAreaLim - 1;
+        }
+        else if ( p->nVars < pNew->nVars )
+        {
+            pNew->nAreaLim = p->nAreaLim / 2 + p->nAreaLim % 2;
+            p->nAreaLim = p->nAreaLim / 2 - p->nAreaLim % 2;
+        }
+        else // if ( pNew->nVars < p->nVars )
+        {
+            pNew->nAreaLim = p->nAreaLim / 2 - p->nAreaLim % 2;
+            p->nAreaLim = p->nAreaLim / 2 + p->nAreaLim % 2;
+        }
+    }
+    return p;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/lpk/lpkCore.c b/src/opt/lpk/lpkCore.c
index a1da45b5..2158f8f7 100644
--- a/src/opt/lpk/lpkCore.c
+++ b/src/opt/lpk/lpkCore.c
@@ -258,11 +258,6 @@ p->timeCuts += clock() - clk;
         if ( p->pPars->fFirst && i == 1 )
             break;
 
-        if ( p->pObj->Id == 8835 )
-        {
-            int x = 0;
-        }
-
         // compute the truth table
 clk = clock();
         pTruth = Lpk_CutTruth( p, pCut );
@@ -312,6 +307,91 @@ p->timeEval += clock() - clk;
 
 /**Function*************************************************************
 
+  Synopsis    [Performs resynthesis for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Lpk_ResynthesizeNodeNew( Lpk_Man_t * p )
+{
+    static int Count = 0;
+    Vec_Ptr_t * vLeaves;
+    Abc_Obj_t * pObjNew;
+    Lpk_Cut_t * pCut;
+    unsigned * pTruth;
+    void * pDsd = NULL;
+    int i, k, clk;
+
+    // compute the cuts
+clk = clock();
+    if ( !Lpk_NodeCuts( 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 );
+    vLeaves = Vec_PtrAlloc( 32 );
+    // 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 ( p->pPars->fFirst && i == 1 )
+            break;
+
+        // collect nodes into the array
+        Vec_PtrClear( vLeaves );
+        for ( k = 0; k < (int)pCut->nLeaves; k++ )
+            Vec_PtrPush( vLeaves, Abc_NtkObj(p->pNtk, pCut->pLeaves[i]) );
+
+        // compute the truth table
+clk = clock();
+        pTruth = Lpk_CutTruth( p, pCut );
+p->timeTruth += clock() - clk;
+
+        if ( p->pPars->fVeryVerbose )
+        {
+//            char * pFileName;
+            int nSuppSize;
+            Kit_DsdNtk_t * pDsdNtk;
+            nSuppSize = Extra_TruthSupportSize(pTruth, pCut->nLeaves);
+            printf( "  C%02d: L= %2d/%2d  V= %2d/%d  N= %d  W= %4.2f  ", 
+                i, pCut->nLeaves, nSuppSize, pCut->nNodes, pCut->nNodesDup, pCut->nLuts, pCut->Weight );
+
+            pDsdNtk = Kit_DsdDecompose( pTruth, pCut->nLeaves ); 
+//        Kit_DsdVerify( pDsdNtk, pTruth, pCut->nLeaves ); 
+            Kit_DsdPrint( stdout, pDsdNtk );
+            Kit_DsdNtkFree( pDsdNtk );
+//            Kit_DsdPrintFromTruth( pTruth, pCut->nLeaves );
+//            pFileName = Kit_TruthDumpToFile( pTruth, pCut->nLeaves, Count++ );
+//            printf( "Saved truth table in file \"%s\".\n", pFileName );
+        }
+
+        // update the network
+clk = clock();
+        pObjNew = Lpk_LpkDecompose( p->pNtk, vLeaves, pTruth, p->pPars->nLutSize,
+            (int)pCut->nNodes - (int)pCut->nNodesDup - 1, Abc_ObjRequiredLevel(p->pObj) );
+p->timeEval += clock() - clk;
+
+        // perform replacement
+        if ( pObjNew )
+            Abc_NtkUpdate( p->pObj, pObjNew, p->vLevels );
+    }
+    Vec_PtrFree( vLeaves );
+    return 1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Performs resynthesis for one network.]
 
   Description []
diff --git a/src/opt/lpk/lpkCut.c b/src/opt/lpk/lpkCut.c
index 27a0317c..d0908a6a 100644
--- a/src/opt/lpk/lpkCut.c
+++ b/src/opt/lpk/lpkCut.c
@@ -410,14 +410,6 @@ void Lpk_NodeCutsOne( Lpk_Man_t * p, Lpk_Cut_t * pCut, int Node )
     // 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 )
@@ -443,47 +435,30 @@ if ( p->pObj->Id == 31 && Node == 38 && pCut->pNodes[0] == 31 && pCut->pNodes[1]
         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 );
-}
-*/
+    pCutNew->nNodesDup = pCut->nNodesDup;
+    // check if the node is already there
+    for ( i = 0; i < (int)pCutNew->nNodes; i++ )
+        if ( pCutNew->pNodes[i] == Node )
+            break;
+    if ( i == (int)pCutNew->nNodes ) // new node
+    {
+        pCutNew->pNodes[ pCutNew->nNodes++ ] = Node;
+        pCutNew->nNodesDup += !Abc_NodeIsTravIdCurrent(pObj);
+    }
+    // the number of nodes does not exceed MFFC plus duplications
+    assert( pCutNew->nNodes <= p->nMffc + pCutNew->nNodesDup );
     // 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" );
-*/
-
-//    if ( !(pCut->nNodes <= p->nMffc + pCutNew->nNodesDup) )
-//        printf( "Assertion in line 477 failed.\n" );
 }
 
 /**Function*************************************************************
@@ -527,13 +502,6 @@ int Lpk_NodeCuts( Lpk_Man_t * p )
         // try to expand the fanins of this cut
         for ( k = 0; k < (int)pCut->nLeaves; k++ )
         {
-
-            if ( p->pObj->Id == 28 && i == 273 && k == 13 )
-            {
-                Abc_Obj_t * pFanin = Abc_NtkObj(p->pNtk, pCut->pLeaves[k]);
-                int s = 0;
-            }
-
             // create a new cut
             Lpk_NodeCutsOne( p, pCut, pCut->pLeaves[k] );
             // quit if the number of cuts has exceeded the limit
@@ -559,7 +527,7 @@ int Lpk_NodeCuts( Lpk_Man_t * p )
             continue;
         // compute the minimum number of LUTs needed 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->nLuts = Lpk_LutNumLuts( pCut->nLeaves, p->pPars->nLutSize ); 
         pCut->Weight = (float)1.0 * (pCut->nNodes - pCut->nNodesDup) / pCut->nLuts; //p->pPars->nLutsMax;
         if ( pCut->Weight <= 1.001 )
             continue;
diff --git a/src/opt/lpk/lpkInt.h b/src/opt/lpk/lpkInt.h
index 683e7b92..d04032ef 100644
--- a/src/opt/lpk/lpkInt.h
+++ b/src/opt/lpk/lpkInt.h
@@ -117,6 +117,47 @@ struct Lpk_Man_t_
     int          timeTotal;
 };
 
+
+// preliminary decomposition result
+typedef struct Lpk_Res_t_ Lpk_Res_t;
+struct Lpk_Res_t_
+{
+    int           nBSVars;
+    unsigned      BSVars;
+    int           nCofVars;
+    char          pCofVars[4];
+    int           nSuppSizeS;
+    int           nSuppSizeL;
+    int           DelayEst;
+    int           AreaEst;
+};
+
+// function to be decomposed
+typedef struct Lpk_Fun_t_ Lpk_Fun_t;
+struct Lpk_Fun_t_
+{
+    Vec_Ptr_t *   vNodes;           // the array of all functions
+    unsigned int  Id         :  5;  // the ID of this node
+    unsigned int  nVars      :  5;  // the number of variables
+    unsigned int  nLutK      :  4;  // the number of LUT inputs
+    unsigned int  nAreaLim   :  8;  // the area limit (the largest allowed)
+    unsigned int  nDelayLim  : 10;  // the delay limit (the largest allowed)
+    char          pFanins[16];      // the fanins of this function
+    char          pDelays[16];      // the delays of the inputs
+    unsigned      uSupp;            // the support of this component
+    unsigned      pTruth[0];        // the truth table (contains room for three truth tables)    
+};
+
+#define Lpk_SuppForEachVar( Supp, Var )\
+    for ( Var = 0; Var < 16; Var++ )\
+        if ( !(Supp & (1<<Var)) ) {} else
+
+static inline int Lpk_LutNumVars( int nLutsLim, int nLutK )  { return  nLutsLim * (nLutK - 1) + 1;                                            }
+static inline int Lpk_LutNumLuts( int nVarsMax, int nLutK )  { return (nVarsMax - 1) / (nLutK - 1) + (int)((nVarsMax - 1) % (nLutK - 1) > 0); }
+    
+static inline unsigned * Lpk_FunTruth( Lpk_Fun_t * p, int Num )  { assert( Num < 3 ); return p->pTruth + Kit_TruthWordNum(p->nVars) * Num; }
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -136,6 +177,24 @@ struct Lpk_Man_t_
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/*=== lpkAbcCore.c ============================================================*/
+extern Abc_Obj_t *    Lpk_LpkDecompose( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, unsigned * pTruth, int nLutK, int AreaLim, int DelayLim );
+/*=== lpkAbcFun.c ============================================================*/
+extern Lpk_Fun_t *    Lpk_FunAlloc( int nVars );
+extern void           Lpk_FunFree( Lpk_Fun_t * p );
+extern Lpk_Fun_t *    Lpk_FunCreate( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, unsigned * pTruth, int nLutK, int AreaLim, int DelayLim );
+extern Lpk_Fun_t *    Lpk_FunDup( Lpk_Fun_t * p, unsigned * pTruth );
+extern void           Lpk_FunSuppMinimize( Lpk_Fun_t * p );
+extern int            Lpk_SuppDelay( unsigned uSupp, char * pDelays );
+extern int            Lpk_SuppToVars( unsigned uBoundSet, char * pVars );
+/*=== lpkAbcDsd.c ============================================================*/
+extern Lpk_Res_t *    Lpk_FunAnalizeDsd( Lpk_Fun_t * p, int nCofDepth );
+extern Lpk_Fun_t *    Lpk_FunSplitDsd( Lpk_Fun_t * p, char * pCofVars, int nCofVars, unsigned uBoundSet );
+/*=== lpkAbcMux.c ============================================================*/
+extern int            Lpk_FunAnalizeMux( Lpk_Fun_t * p );
+extern Lpk_Fun_t *    Lpk_FunSplitMux( Lpk_Fun_t * p, int VarPol );
+
+
 /*=== lpkCut.c =========================================================*/
 extern unsigned *     Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut );
 extern int            Lpk_NodeCuts( Lpk_Man_t * p );
diff --git a/src/opt/lpk/lpkMan.c b/src/opt/lpk/lpkMan.c
index c11a0a33..5be198d7 100644
--- a/src/opt/lpk/lpkMan.c
+++ b/src/opt/lpk/lpkMan.c
@@ -54,7 +54,7 @@ Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars )
     p->vCover = Vec_IntAlloc( 1 << 12 );
     for ( i = 0; i < 8; i++ )
         p->vSets[i] = Vec_IntAlloc(100);
-    p->pDsdMan = Kit_DsdManAlloc( pPars->nVarsMax );
+    p->pDsdMan = Kit_DsdManAlloc( pPars->nVarsMax, 64 );
     return p;
 }
 
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 512c5751..19ff6f8b 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -27,6 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "satSolver.h"
 
 //#define SAT_USE_SYSTEM_MEMORY_MANAGEMENT
+#define WATCHFLAG  1
 
 //=================================================================================================
 // Debug:
@@ -90,9 +91,11 @@ static inline void  clause_setactivity(clause* c, float a) { *((float*)&c->lits[
 //=================================================================================================
 // Encode literals in clause pointers:
 
-static clause* clause_from_lit (lit l)     { return (clause*)((unsigned long)l + (unsigned long)l + 1);  }
 static bool    clause_is_lit   (clause* c) { return ((unsigned long)c & 1);                              }
+static clause* clause_from_lit (lit l)     { return (clause*)((unsigned long)l + (unsigned long)l + 1);  }
 static lit     clause_read_lit (clause* c) { return (lit)((unsigned long)c >> 1);                        }
+static clause* clause_from_lit2(lit l)     { return (clause*)(unsigned long)l;                           }
+static lit     clause_read_lit2(clause* c) { return (lit)(unsigned long)c;                               }
 
 //=================================================================================================
 // Simple helpers:
@@ -108,6 +111,15 @@ static inline void    vecp_remove(vecp* v, void* e)
     for (; j < vecp_size(v)-1; j++) ws[j] = ws[j+1];
     vecp_resize(v,vecp_size(v)-1);
 }
+static inline void    vecp_remove2(vecp* v, void* e)
+{
+    void** ws = vecp_begin(v);
+    int    j  = 0;
+    for (; ws[j] != e  ; j++);
+    assert(j < vecp_size(v));
+    for (; j < vecp_size(v)-2; j++) ws[j] = ws[j+2];
+    vecp_resize(v,vecp_size(v)-2);
+}
 
 //=================================================================================================
 // Variable order functions:
@@ -304,8 +316,26 @@ static clause* clause_new(sat_solver* s, lit* begin, lit* end, int learnt)
     //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)c);
     //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)c);
 
-    vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)(size > 2 ? c : clause_from_lit(begin[1])));
-    vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)(size > 2 ? c : clause_from_lit(begin[0])));
+    if ( WATCHFLAG )
+    {
+        if ( size == 2 )
+        {
+            vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)clause_from_lit(begin[1]));
+            vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)clause_from_lit(begin[0]));
+        }
+        else
+        {
+            vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)c);
+            vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)clause_from_lit2(begin[1]));
+            vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)c);
+            vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)clause_from_lit2(begin[0]));
+        }
+    }
+    else
+    {
+        vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)(size > 2 ? c : clause_from_lit(begin[1])));
+        vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)(size > 2 ? c : clause_from_lit(begin[0])));
+    }
 
     return c;
 }
@@ -321,8 +351,24 @@ static void clause_remove(sat_solver* s, clause* c)
     //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)c);
 
     assert(lits[0] < s->size*2);
-    vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1])));
-    vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0])));
+    if ( WATCHFLAG )
+    {
+        if ( clause_size(c) == 2 )
+        {
+            vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)clause_from_lit(lits[1]));
+            vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)clause_from_lit(lits[0]));
+        }
+        else
+        {
+            vecp_remove2(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)c);
+            vecp_remove2(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)c);
+        }
+    }
+    else
+    {
+        vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1])));
+        vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0])));
+    }
 
     if (clause_learnt(c)){
         s->stats.learnts--;
@@ -703,6 +749,31 @@ static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt)
 }
 
 
+void sat_solver_check(sat_solver* s)
+{
+    int j, k;
+    lit Lit, First, *lits;
+    vecp* ws;
+    clause **begin, **end, **i;
+    for ( j = 0; j < s->size; j++ )
+    for ( k = 0; k < 2; k++ )
+    {
+        Lit = toLitCond( j, k );
+        ws = sat_solver_read_wlist(s,Lit);
+        begin = (clause**)vecp_begin(ws);
+        end   = begin + vecp_size(ws);
+        for (i = begin; i < end; i++)
+        {
+            if (clause_is_lit(*i))
+                continue;
+            lits = clause_begin(*i);
+            First = clause_read_lit2(*(i+1));
+            assert( First == lits[0] || First == lits[1] );
+            i++;
+        }
+    }
+}
+
 clause* sat_solver_propagate(sat_solver* s)
 {
     lbool*  values = s->assigns;
@@ -716,15 +787,19 @@ clause* sat_solver_propagate(sat_solver* s)
         clause **begin = (clause**)vecp_begin(ws);
         clause **end   = begin + vecp_size(ws);
         clause **i, **j;
+//        sat_solver_check(s);
 
         s->stats.propagations++;
         s->simpdb_props--;
-
+ 
         //printf("checking lit %d: "L_LIT"\n", veci_size(ws), L_lit(p));
-        for (i = j = begin; i < end; ){
-            if (clause_is_lit(*i)){
+        for (i = j = begin; i < end; i++)
+        {
+            if (clause_is_lit(*i))
+            {
                 *j++ = *i;
-                if (!enqueue(s,clause_read_lit(*i),clause_from_lit(p))){
+                if (!enqueue(s,clause_read_lit(*i),clause_from_lit(p)))
+                {
                     confl = s->binary;
                     (clause_begin(confl))[1] = lit_neg(p);
                     (clause_begin(confl))[0] = clause_read_lit(*i++);
@@ -733,13 +808,27 @@ clause* sat_solver_propagate(sat_solver* s)
                     while (i < end)
                         *j++ = *i++;
                 }
-            }else{
-                lit false_lit;
+            }
+            else
+            {
+                lit false_lit, first;
                 lbool sig;
 
+                if ( WATCHFLAG )
+                {
+                    first = clause_read_lit2(*(i+1));
+                    sig = !lit_sign(first); sig += sig - 1;
+                    if (values[lit_var(first)] == sig)
+                    {
+                        *j++ = *i++;
+                        *j++ = *i;
+                        continue;
+                    }
+                }
+
                 lits = clause_begin(*i);
 
-                // Make sure the false literal is data[1]:
+                // Make sure the false literal is in data[1]:
                 false_lit = lit_neg(p);
                 if (lits[0] == false_lit){
                     lits[0] = lits[1];
@@ -748,35 +837,95 @@ clause* sat_solver_propagate(sat_solver* s)
                 assert(lits[1] == false_lit);
                 //printf("checking clause: "); printlits(lits, lits+clause_size(*i)); printf("\n");
 
-                // If 0th watch is true, then clause is already satisfied.
-                sig = !lit_sign(lits[0]); sig += sig - 1;
-                if (values[lit_var(lits[0])] == sig){
-                    *j++ = *i;
-                }else{
+                if ( WATCHFLAG )
+                {
+/*
+                    // If 0th watch is true, then clause is already satisfied.
+                    sig = !lit_sign(lits[0]); sig += sig - 1;
+                    if (values[lit_var(lits[0])] == sig)
+                    {
+                        *j++ = *i++;
+                        *j++ = *i;
+                        continue;
+                    }
+                    else
+*/
+                    {
                     // Look for new watch:
                     lit* stop = lits + clause_size(*i);
                     lit* k;
-                    for (k = lits + 2; k < stop; k++){
+//                    assert( lits[0] == first );
+                    for (k = lits + 2; k < stop; k++)
+                    {
                         lbool sig = lit_sign(*k); sig += sig - 1;
-                        if (values[lit_var(*k)] != sig){
+                        if (values[lit_var(*k)] != sig)
+                        {
                             lits[1] = *k;
                             *k = false_lit;
-                            vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i);
-                            goto next; }
+//                            vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i);
+                            vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i++);
+                            vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),clause_from_lit2(lits[0]));
+                            break; 
+                        }
                     }
+                    if ( k < stop )
+                        continue;
 
                     *j++ = *i;
                     // Clause is unit under assignment:
-                    if (!enqueue(s,lits[0], *i)){
+                    if (!enqueue(s,lits[0], *i))
+                    {
                         confl = *i++;
+                        *j++ = clause_from_lit2(lits[0]); i++; //
                         // Copy the remaining watches:
                         while (i < end)
                             *j++ = *i++;
                     }
+                    else
+                    {
+                        *j++ = clause_from_lit2(lits[0]); i++; //
+                    }
+                    }
+                }
+                else
+                {
+                    // If 0th watch is true, then clause is already satisfied.
+                    sig = !lit_sign(lits[0]); sig += sig - 1;
+                    if (values[lit_var(lits[0])] == sig)
+                    {
+                        *j++ = *i;
+                    }
+                    else
+                    {
+                        // Look for new watch:
+                        lit* stop = lits + clause_size(*i);
+                        lit* k;
+                        for (k = lits + 2; k < stop; k++)
+                        {
+                            lbool sig = lit_sign(*k); sig += sig - 1;
+                            if (values[lit_var(*k)] != sig)
+                            {
+                                lits[1] = *k;
+                                *k = false_lit;
+                                vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i);
+                                break; 
+                            }
+                        }
+                        if ( k < stop )
+                            continue;
+
+                        *j++ = *i;
+                        // Clause is unit under assignment:
+                        if (!enqueue(s,lits[0], *i))
+                        {
+                            confl = *i++;
+                            // Copy the remaining watches:
+                            while (i < end)
+                                *j++ = *i++;
+                        }
+                    }
                 }
             }
-        next:
-            i++;
         }
 
         s->stats.inspects += j - (clause**)vecp_begin(ws);
@@ -795,7 +944,7 @@ void sat_solver_reducedb(sat_solver* s)
     double   extra_lim = s->cla_inc / vecp_size(&s->learnts); // Remove any clause below this activity
     clause** learnts = (clause**)vecp_begin(&s->learnts);
     clause** reasons = s->reasons;
-
+//printf( "Trying to reduce DB\n" );
     sat_solver_sort(vecp_begin(&s->learnts), vecp_size(&s->learnts), &clause_cmp);
 
     for (i = j = 0; i < vecp_size(&s->learnts) / 2; i++){
@@ -888,8 +1037,10 @@ static lbool sat_solver_search(sat_solver* s, sint64 nof_conflicts, sint64 nof_l
             }
 
             if (sat_solver_dlevel(s) == 0 && !s->fSkipSimplify)
+            {
                 // Simplify the set of problem clauses:
                 sat_solver_simplify(s);
+            }
 
             if (nof_learnts >= 0 && vecp_size(&s->learnts) - s->qtail >= nof_learnts)
                 // Reduce the set of learnt clauses:
@@ -1120,6 +1271,7 @@ bool sat_solver_simplify(sat_solver* s)
 
     if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0)
         return true;
+//printf( "Trying to simplify\n" );
 
     reasons = s->reasons;
     for (type = 0; type < 2; type++){