Changes to LUT mappers.

9 files changed, 398 insertions, 36 deletions

diff --git a/abclib.dsp b/abclib.dsp
index e1e89830..d2b7d737 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -2343,6 +2343,10 @@ SOURCE=.\src\map\if\ifReduce.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\map\if\ifSat.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\map\if\ifSelect.c
 # End Source File
 # Begin Source File
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 6db36aa0..b8e41dc0 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -974,6 +974,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
     {
 //        extern void Dau_DsdTest();
 //        Dau_DsdTest();
+//        extern void If_ManSatTest();
+//        If_ManSatTest();
     }
 
     if ( Sdm_ManCanRead() )
@@ -2274,7 +2276,12 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
 //        Extra_PrintBinary( stdout, pTruth, 1 << Abc_ObjFaninNum(pObj) );
 //        Abc_Print( -1, "\n" );
         if ( fPrintDec )//&&Abc_ObjFaninNum(pObj) <= 6 )
+        {
+            word * pTruthW = (word *)pTruth;
+            if ( Abc_ObjFaninNum(pObj) < 6 )
+                pTruthW[0] = Abc_Tt6Stretch( pTruthW[0], Abc_ObjFaninNum(pObj) );
             Dau_DecTrySets( (word *)pTruth, Abc_ObjFaninNum(pObj), 1 );
+        }
         if ( fProfile )
             Kit_TruthPrintProfile( pTruth, Abc_ObjFaninNum(pObj) );
         else if ( fCofactor )
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 41d30da4..13828701 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -55,7 +55,7 @@ ABC_NAMESPACE_HEADER_START
 // the largest possible user cut cost
 #define IF_COST_MAX          8191 // ((1<<13)-1)
 
-#define IF_BIG_CHAR 120
+#define IF_BIG_CHAR ((char)120)
 
 // object types
 typedef enum { 
@@ -233,7 +233,8 @@ struct If_Man_t_
     int                nCuts5, nCuts5a;
     If_DsdMan_t *      pIfDsdMan;
     Vec_Mem_t *        vTtMem;        // truth table memory and hash table
-    Vec_Int_t *        vDsds;         // mapping of truth table into DSD
+    Vec_Int_t *        vTtDsds;       // mapping of truth table into DSD
+    Vec_Str_t *        vTtPerms;      // mapping of truth table into permutations
     int                nBestCutSmall[2];
 
     // timing manager
@@ -520,7 +521,7 @@ extern void            If_DsdManDump( If_DsdMan_t * p );
 extern void            If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int fVerbose );
 extern void            If_DsdManFree( If_DsdMan_t * p );
 extern int             If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char * pPerm, char * pLutStruct );
-extern int             If_DsdManCheckDec( If_DsdMan_t * pIfMan, int iDsd );
+extern int             If_DsdManCheckDec( If_DsdMan_t * p, int iDsd );
 /*=== ifLib.c =============================================================*/
 extern If_LibLut_t *   If_LibLutRead( char * FileName );
 extern If_LibLut_t *   If_LibLutDup( If_LibLut_t * p );
diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c
index 5c3fecc9..e6c2dfac 100644
--- a/src/map/if/ifDsd.c
+++ b/src/map/if/ifDsd.c
@@ -505,9 +505,10 @@ int If_DsdObjFindOrAdd( If_DsdMan_t * p, int Type, int * pLits, int nLits, word
     unsigned * pSpot = If_DsdObjHashLookup( p, Type, pLits, nLits, truthId );
     if ( *pSpot )
         return *pSpot;
-    if ( truthId >= 0 && truthId == Vec_MemEntryNum(p->vTtMem)-1 )
+    if ( truthId >= 0 && truthId == Vec_PtrSize(p->vTtDecs) )
     {
         Vec_Int_t * vSets = Dau_DecFindSets( pTruth, nLits );
+        assert( truthId == Vec_MemEntryNum(p->vTtMem)-1 );
         Vec_PtrPush( p->vTtDecs, vSets );
 //        Dau_DecPrintSets( vSets, nLits );
     }
@@ -533,7 +534,8 @@ void If_DsdManComputeTruth_rec( If_DsdMan_t * p, int iDsd, word * pRes, unsigned
     If_DsdObj_t * pObj = If_DsdVecObj( p->vObjs, Abc_Lit2Var(iDsd) );
     if ( If_DsdObjType(pObj) == IF_DSD_VAR )
     {
-        int iPermLit = (int)pPermLits[(*pnSupp)++];
+        int iPermLit = pPermLits ? (int)pPermLits[*pnSupp] : Abc_Var2Lit(*pnSupp, 0);
+        (*pnSupp)++;
         assert( (*pnSupp) <= p->nVars );
         Abc_TtCopy( pRes, p->pTtElems[Abc_Lit2Var(iPermLit)], p->nWords, fCompl ^ Abc_LitIsCompl(iPermLit) );
         return;
@@ -589,7 +591,8 @@ word * If_DsdManComputeTruth( If_DsdMan_t * p, int iDsd, unsigned char * pPermLi
         Abc_TtConst1( pRes, p->nWords );
     else if ( pObj->Type == IF_DSD_VAR )
     {
-        int iPermLit = (int)pPermLits[nSupp++];
+        int iPermLit = pPermLits ? (int)pPermLits[nSupp] : Abc_Var2Lit(nSupp, 0);
+        nSupp++;
         Abc_TtCopy( pRes, p->pTtElems[Abc_Lit2Var(iPermLit)], p->nWords, Abc_LitIsCompl(iDsd) ^ Abc_LitIsCompl(iPermLit) );
     }
     else
@@ -923,7 +926,7 @@ void If_DsdManGetSuppSizes( If_DsdMan_t * p, If_DsdObj_t * pObj, int * pSSizes )
         pSSizes[i] = If_DsdObjSuppSize(pFanin);    
 }
 // checks if there is a way to package some fanins 
-int If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize )
+int If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fVerbose )
 {
     int i[6], LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR];
     int nFans = If_DsdObjFaninNum(pObj);
@@ -953,12 +956,49 @@ int If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int
             continue;
         return (1 << i[0]) | (1 << i[1]) | (1 << i[2]);
     }
+    if ( pObj->nFans == 4 )
+        return 0;
+    for ( i[0] = 0;      i[0] < nFans; i[0]++ )
+    for ( i[1] = i[0]+1; i[1] < nFans; i[1]++ )
+    for ( i[2] = i[1]+1; i[2] < nFans; i[2]++ )
+    for ( i[3] = i[2]+1; i[3] < nFans; i[3]++ )
+    {
+        SizeIn = pSSizes[i[0]] + pSSizes[i[1]] + pSSizes[i[2]] + pSSizes[i[3]];
+        SizeOut = pObj->nSupp - SizeIn;
+        if ( SizeIn > LutSize || SizeOut > LimitOut )
+            continue;
+        return (1 << i[0]) | (1 << i[1]) | (1 << i[2]) | (1 << i[3]);
+    }
     return 0;
 }
 // checks if there is a way to package some fanins 
-int If_DsdManCheckPrime( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize )
+int If_DsdManCheckMux( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fVerbose )
+{
+    int LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR];
+    assert( If_DsdObjFaninNum(pObj) == 3 );
+    assert( If_DsdObjSuppSize(pObj) > LutSize );
+    If_DsdManGetSuppSizes( p, pObj, pSSizes );
+    LimitOut = LutSize - (nSuppAll - If_DsdObjSuppSize(pObj) + 1);
+    assert( LimitOut < LutSize );
+    // first input
+    SizeIn = pSSizes[0] + pSSizes[1];
+    SizeOut = pSSizes[2];
+    if ( SizeIn <= LutSize && SizeOut <= LimitOut )
+    {
+        return 1;
+    }
+    // second input
+    SizeIn = pSSizes[0] + pSSizes[2];
+    SizeOut = pSSizes[1];
+    if ( SizeIn <= LutSize && SizeOut <= LimitOut )
+    {
+        return 1;
+    }
+    return 0;
+}
+// checks if there is a way to package some fanins 
+int If_DsdManCheckPrime( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fVerbose )
 {
-    int fVerbose = 0;
     int i, v, set, LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR];
     int truthId = If_DsdObjTruthId( p, pObj );
     int nFans = If_DsdObjFaninNum(pObj);
@@ -967,10 +1007,10 @@ if ( fVerbose )
 printf( "\n" );
 if ( fVerbose )
 Dau_DecPrintSets( vSets, nFans );
-    assert( pObj->nFans > 2 );
+    assert( If_DsdObjFaninNum(pObj) > 2 );
     assert( If_DsdObjSuppSize(pObj) > LutSize );
     If_DsdManGetSuppSizes( p, pObj, pSSizes );
-    LimitOut = LutSize - (nSuppAll - pObj->nSupp + 1);
+    LimitOut = LutSize - (nSuppAll - If_DsdObjSuppSize(pObj) + 1);
     assert( LimitOut < LutSize );
     Vec_IntForEachEntry( vSets, set, i )
     {
@@ -996,9 +1036,8 @@ Dau_DecPrintSets( vSets, nFans );
     }
     return 0;
 }
-int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize )
+int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fVerbose )
 {
-    int fVerbose = 0;
     If_DsdObj_t * pObj, * pTemp; int i, Mask;
     pObj = If_DsdVecObj( p->vObjs, Abc_Lit2Var(iDsd) );
     if ( fVerbose )
@@ -1022,7 +1061,7 @@ int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize )
     If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i )
         if ( (If_DsdObjType(pTemp) == IF_DSD_AND || If_DsdObjType(pTemp) == IF_DSD_XOR) && If_DsdObjFaninNum(pTemp) > 2 && If_DsdObjSuppSize(pTemp) > LutSize )
         {
-            if ( (Mask = If_DsdManCheckAndXor(p, pTemp, If_DsdObjSuppSize(pObj), LutSize)) )
+            if ( (Mask = If_DsdManCheckAndXor(p, pTemp, If_DsdObjSuppSize(pObj), LutSize, fVerbose)) )
             {
                 if ( fVerbose )
                 printf( "    " );
@@ -1034,9 +1073,23 @@ int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize )
             }
         }
     If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i )
-        if ( If_DsdObjType(pTemp) == IF_DSD_PRIME )
+        if ( If_DsdObjType(pTemp) == IF_DSD_MUX && If_DsdObjSuppSize(pTemp) > LutSize )
+        {
+            if ( (Mask = If_DsdManCheckMux(p, pTemp, If_DsdObjSuppSize(pObj), LutSize, fVerbose)) )
+            {
+                if ( fVerbose )
+                printf( "    " );
+                if ( fVerbose )
+                Abc_TtPrintBinary( (word *)&Mask, 4 ); 
+                if ( fVerbose )
+                printf( "    Using multi-input MUX node\n" );
+                return 1;
+            }
+        }
+    If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i )
+        if ( If_DsdObjType(pTemp) == IF_DSD_PRIME && If_DsdObjSuppSize(pTemp) > LutSize )
         {
-            if ( (Mask = If_DsdManCheckPrime(p, pTemp, If_DsdObjSuppSize(pObj), LutSize)) )
+            if ( (Mask = If_DsdManCheckPrime(p, pTemp, If_DsdObjSuppSize(pObj), LutSize, fVerbose)) )
             {
                 if ( fVerbose )
                 printf( "    " );
@@ -1049,6 +1102,8 @@ int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize )
         }
     if ( fVerbose )
     printf( "    UNDEC\n" );
+
+//    If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), NULL, 1 );
     return 0;
 }
 int If_DsdManCheckXYZ( If_DsdMan_t * p, int iDsd, int LutSize ) 
@@ -1058,6 +1113,22 @@ int If_DsdManCheckXYZ( If_DsdMan_t * p, int iDsd, int LutSize )
 
 /**Function*************************************************************
 
+  Synopsis    [Checks existence of decomposition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_DsdManCheckDec( If_DsdMan_t * p, int iDsd )
+{
+    return If_DsdVecObjMark( p->vObjs, Abc_Lit2Var(iDsd) );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Add the function to the DSD manager.]
 
   Description []
@@ -1075,10 +1146,10 @@ int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char
     assert( nLeaves <= DAU_MAX_VAR );
     Abc_TtCopy( pCopy, pTruth, p->nWords, 0 );
     nSizeNonDec = Dau_DsdDecompose( pCopy, nLeaves, 0, 0, pDsd );
-    if ( !strcmp(pDsd, "(![(!e!d)c]!(b!a))") )
-    {
+//    if ( !strcmp(pDsd, "(![(!e!d)c]!(b!a))") )
+//    {
 //        int x = 0;
-    }
+//    }
     if ( nSizeNonDec > 0 )
         Abc_TtStretch6( pCopy, nSizeNonDec, p->nVars );
     memset( pPerm, 0xFF, nLeaves );
@@ -1096,19 +1167,36 @@ int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char
         If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), pPerm, 1 );
         printf( "\n" );
     }
-    If_DsdVecObjIncRef( p->vObjs, Abc_Lit2Var(iDsd) );
-    if ( pLutStruct )
+    if ( pLutStruct && If_DsdVecObjRef(p->vObjs, Abc_Lit2Var(iDsd)) )
     {
         int LutSize = (int)(pLutStruct[0] - '0');
-        assert( pLutStruct[2] == 0 );
-        if ( If_DsdManCheckXY( p, iDsd, LutSize ) )
+        assert( pLutStruct[2] == 0 ); // XY
+        if ( !If_DsdManCheckXY( p, iDsd, LutSize, 0 ) )
             If_DsdVecObjSetMark( p->vObjs, Abc_Lit2Var(iDsd) );
     }
+    If_DsdVecObjIncRef( p->vObjs, Abc_Lit2Var(iDsd) );
     return iDsd;
 }
-int If_DsdManCheckDec( If_DsdMan_t * p, int iDsd )
+
+/**Function*************************************************************
+
+  Synopsis    [Checks existence of decomposition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_DsdManTest()
 {
-    return If_DsdVecObjMark( p->vObjs, Abc_Lit2Var(iDsd) );
+    Vec_Int_t * vSets;
+    word t = 0x5277;
+    t = Abc_Tt6Stretch( t, 4 );
+//    word t = 0xD9D900D900D900001010001000100000;
+    vSets = Dau_DecFindSets( &t, 6 );
+    Vec_IntFree( vSets );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index ae7552b3..5025429e 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -86,9 +86,12 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
     if ( pPars->fUseDsd )
     {
         p->pIfDsdMan = If_DsdManAlloc( pPars->nLutSize );
-        p->vDsds = Vec_IntAlloc( 1000 );
-        Vec_IntPush( p->vDsds, 0 );
-        Vec_IntPush( p->vDsds, 2 );
+        p->vTtDsds = Vec_IntAlloc( 1000 );
+        Vec_IntPush( p->vTtDsds, 0 );
+        Vec_IntPush( p->vTtDsds, 2 );
+        p->vTtPerms = Vec_StrAlloc( 10000 );
+        Vec_StrFill( p->vTtPerms, 2 * p->pPars->nLutSize, IF_BIG_CHAR );
+        Vec_StrWriteEntry( p->vTtPerms, p->pPars->nLutSize, 0 );
     }
     // create the constant node
     p->pConst1   = If_ManSetupObj( p );
@@ -173,7 +176,8 @@ void If_ManStop( If_Man_t * p )
     Vec_PtrFreeP( &p->vObjsRev );
     Vec_PtrFreeP( &p->vLatchOrder );
     Vec_IntFreeP( &p->vLags );
-    Vec_IntFreeP( &p->vDsds );
+    Vec_IntFreeP( &p->vTtDsds );
+    Vec_StrFreeP( &p->vTtPerms );
     Vec_MemHashFree( p->vTtMem );
     Vec_MemFreeP( &p->vTtMem );
     Mem_FixedStop( p->pMemObj, 0 );
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index 34e83139..c719215f 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -140,7 +140,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
 {
     If_Set_t * pCutSet;
     If_Cut_t * pCut0, * pCut1, * pCut;
-    int i, k;
+    int i, k, v;
     assert( p->pPars->fSeqMap || !If_ObjIsAnd(pObj->pFanin0) || pObj->pFanin0->pCutSet->nCuts > 0 );
     assert( p->pPars->fSeqMap || !If_ObjIsAnd(pObj->pFanin1) || pObj->pFanin1->pCutSet->nCuts > 0 );
 
@@ -254,20 +254,32 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
             if ( p->pPars->fUseDsd )
             {
                 int truthId = Abc_Lit2Var(pCut->iCutFunc);
-                if ( Vec_IntSize(p->vDsds) <= truthId || Vec_IntEntry(p->vDsds, truthId) == -1 )
+                if ( Vec_IntSize(p->vTtDsds) <= truthId || Vec_IntEntry(p->vTtDsds, truthId) == -1 )
                 {
                     pCut->iCutDsd = If_DsdManCompute( p->pIfDsdMan, If_CutTruthW(p, pCut), pCut->nLeaves, (unsigned char *)pCut->pPerm, p->pPars->pLutStruct );
-                    while ( Vec_IntSize(p->vDsds) <= truthId )
-                        Vec_IntPush( p->vDsds, -1 );
-                    Vec_IntWriteEntry( p->vDsds, truthId, Abc_LitNotCond(pCut->iCutDsd, Abc_LitIsCompl(pCut->iCutFunc)) );
+//                    printf( "%d(%d) ", pCut->iCutDsd, If_DsdManCheckDec( p->pIfDsdMan, pCut->iCutDsd ) );
+                    while ( Vec_IntSize(p->vTtDsds) <= truthId )
+                    {
+                        Vec_IntPush( p->vTtDsds, -1 );
+                        for ( v = 0; v < p->pPars->nLutSize; v++ )
+                            Vec_StrPush( p->vTtPerms, IF_BIG_CHAR );
+                    }
+                    Vec_IntWriteEntry( p->vTtDsds, truthId, Abc_LitNotCond(pCut->iCutDsd, Abc_LitIsCompl(pCut->iCutFunc)) );
+                    for ( v = 0; v < (int)pCut->nLeaves; v++ )
+                        Vec_StrWriteEntry( p->vTtPerms, truthId * p->pPars->nLutSize + v, (char)pCut->pPerm[v] );
                 }
                 else
-                    pCut->iCutDsd = Abc_LitNotCond( Vec_IntEntry(p->vDsds, truthId), Abc_LitIsCompl(pCut->iCutFunc) );
+                {
+                    pCut->iCutDsd = Abc_LitNotCond( Vec_IntEntry(p->vTtDsds, truthId), Abc_LitIsCompl(pCut->iCutFunc) );
+                    for ( v = 0; v < (int)pCut->nLeaves; v++ )
+                        pCut->pPerm[v] = (unsigned char)Vec_StrEntry( p->vTtPerms, truthId * p->pPars->nLutSize + v );
+                }
                 if ( p->pPars->pLutStruct )
                 {
                     int Value = If_DsdManCheckDec( p->pIfDsdMan, pCut->iCutDsd );
                     if ( Value != (int)pCut->fUseless )
-                        printf( "Difference\n" );
+                    {
+                    }
                 }
             }
         }
diff --git a/src/map/if/ifSat.c b/src/map/if/ifSat.c
new file mode 100644
index 00000000..0afe7ea5
--- /dev/null
+++ b/src/map/if/ifSat.c
@@ -0,0 +1,199 @@
+/**CFile****************************************************************
+
+  FileName    [ifSat.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [FPGA mapping based on priority cuts.]
+
+  Synopsis    [SAT-based evaluation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - November 21, 2006.]
+
+  Revision    [$Id: ifSat.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "if.h"
+#include "sat/bsat/satSolver.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+ 
+/**Function*************************************************************
+
+  Synopsis    [Builds SAT instance for the given structure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+sat_solver * If_ManSatBuildXY( int nLutSize )
+{
+    int nMintsL = (1 << nLutSize);
+    int nMintsF = (1 << (2 * nLutSize - 1));
+    int nVars   = 2 * nMintsL + nMintsF;
+    int iVarP0  = 0;           // LUT0 parameters (total nMintsL)
+    int iVarP1  = nMintsL;     // LUT1 parameters (total nMintsL)
+    int m,iVarM = 2 * nMintsL; // MUX vars        (total nMintsF)
+    sat_solver * p = sat_solver_new();
+    sat_solver_setnvars( p, nVars );
+    for ( m = 0; m < nMintsF; m++ )
+        sat_solver_add_mux( p, iVarP0 + m % nMintsL, iVarP1 + 2 * (m / nMintsL) + 1, iVarP1 + 2 * (m / nMintsL), iVarM + m );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns config string for the given truth table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_ManSatCheckXY( sat_solver * p, int nLutSize, word * pTruth, int nVars, unsigned uSet, word * pTBound, word * pTFree, Vec_Int_t * vLits )
+{
+    int iBSet, nBSet = 0;
+    int iSSet, nSSet = 0;
+    int iFSet, nFSet = 0;
+    int nMintsL = (1 << nLutSize);
+    int nMintsF = (1 << (2 * nLutSize - 1));
+    int v, Value, m, mNew, nMintsFNew, nMintsLNew;
+    // collect variable sets
+    Dau_DecSortSet( uSet, nVars, &nBSet, &nSSet, &nFSet );
+    assert( nBSet + nSSet + nFSet == nVars );
+    // check variable bounds
+    assert( nSSet + nBSet <= nLutSize );
+    assert( nLutSize + nSSet + nFSet <= 2*nLutSize - 1 );
+    nMintsFNew = (1 << (nLutSize + nSSet + nFSet));
+    // remap minterms
+    Vec_IntFill( vLits, nMintsF, -1 );
+    for ( m = 0; m < (1 << nVars); m++ )
+    {
+        mNew = iBSet = iSSet = iFSet = 0;
+        for ( v = 0; v < nVars; v++ )
+        {
+            Value = ((uSet >> (v << 1)) & 3);
+            if ( Value == 0 ) // FS
+            {
+                if ( ((m >> v) & 1) )
+                    mNew |= 1 << (nLutSize + nSSet + iFSet);
+                iFSet++;
+            }
+            else if ( Value == 1 ) // BS
+            {
+                if ( ((m >> v) & 1) )
+                    mNew |= 1 << (nSSet + iBSet);
+                iBSet++;
+            }
+            else if ( Value == 3 ) // SS
+            {
+                if ( ((m >> v) & 1) )
+                {
+                    mNew |= 1 << iSSet;
+                    mNew |= 1 << (nLutSize + iSSet);
+                }
+                iSSet++;
+            }
+            else assert( Value == 0 );
+        }
+        assert( iBSet == nBSet && iFSet == nFSet );
+        assert( Vec_IntEntry(vLits, mNew) == -1 );
+        Vec_IntWriteEntry( vLits, mNew, Abc_TtGetBit(pTruth, m) );
+    }
+    // find assumptions
+    v = 0;
+    Vec_IntForEachEntry( vLits, Value, m )
+    {
+        printf( "%d", (Value >= 0) ? Value : 2 );
+        if ( Value >= 0 )
+            Vec_IntWriteEntry( vLits, v++, Abc_Var2Lit(2 * nMintsL + m, !Value) );
+    }
+    Vec_IntShrink( vLits, v );
+    printf( " %d\n", Vec_IntSize(vLits) );
+    // run SAT solver
+    Value = sat_solver_solve( p, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
+    if ( Value != l_True )
+        return 0;
+    // collect config
+    assert( nSSet + nBSet <= nLutSize );
+    *pTBound = 0;
+    nMintsLNew = (1 << (nSSet + nBSet));
+    for ( m = 0; m < nMintsLNew; m++ )
+        if ( sat_solver_var_value(p, m) )
+            Abc_TtSetBit( pTBound, m );
+    *pTBound = Abc_Tt6Stretch( *pTBound, nSSet + nBSet );
+    // collect configs
+    assert( nSSet + nFSet + 1 <= nLutSize );
+    *pTFree = 0;
+    nMintsLNew = (1 << (nSSet + nFSet + 1));
+    for ( m = 0; m < nMintsLNew; m++ )
+        if ( sat_solver_var_value(p, nMintsL+m) )
+            Abc_TtSetBit( pTFree, m );
+    *pTFree = Abc_Tt6Stretch( *pTFree, nSSet + nFSet + 1 );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Test procedure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_ManSatTest()
+{
+    int nVars = 6;
+    int nLutSize = 4;
+    sat_solver * p = If_ManSatBuildXY( nLutSize );
+//    char * pDsd = "(abcdefg)";
+//    char * pDsd = "([a!bc]d!e)";
+    char * pDsd = "0123456789ABCDEF{abcdef}";
+    word * pTruth = Dau_DsdToTruth( pDsd, nVars );
+    word uBound, uFree;
+    Vec_Int_t * vLits = Vec_IntAlloc( 100 );
+//    unsigned uSet = (1 << 0) | (1 << 2) | (1 << 4) | (1 << 6);
+//    unsigned uSet = (3 << 0) | (1 << 2) | (1 << 8) | (1 << 4);
+    unsigned uSet = (1 << 0) | (3 << 2) | (1 << 4) | (1 << 6);
+    int RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
+    assert( RetValue );
+    
+//    Abc_TtPrintBinary( pTruth, nVars );
+//    Abc_TtPrintBinary( &uBound, nLutSize );
+//    Abc_TtPrintBinary( &uFree, nLutSize );
+
+    Dau_DsdPrintFromTruth( pTruth, nVars );
+    Dau_DsdPrintFromTruth( &uBound, nLutSize );
+    Dau_DsdPrintFromTruth( &uFree, nLutSize );
+    sat_solver_delete(p);
+    Vec_IntFree( vLits );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/dau/dau.h b/src/opt/dau/dau.h
index 2e56899b..051abb7d 100644
--- a/src/opt/dau/dau.h
+++ b/src/opt/dau/dau.h
@@ -99,6 +99,7 @@ extern char *        Dau_DsdMerge( char * pDsd0i, int * pPerm0, char * pDsd1i, i
 
 /*=== dauNonDsd.c  ==========================================================*/
 extern Vec_Int_t *   Dau_DecFindSets( word * pInit, int nVars );
+extern void          Dau_DecSortSet( unsigned set, int nVars, int * pnUnique, int * pnShared, int * pnFree );
 extern void          Dau_DecPrintSets( Vec_Int_t * vSets, int nVars );
 extern void          Dau_DecPrintSet( unsigned set, int nVars, int fNewLine );
 
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index 0d46b86b..345bbd28 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -368,6 +368,52 @@ static inline int sat_solver_add_xor( sat_solver * pSat, int iVarA, int iVarB, i
     assert( Cid );
     return 4;
 }
+static inline int sat_solver_add_mux( sat_solver * pSat, int iVarC, int iVarT, int iVarE, int iVarZ )
+{
+    lit Lits[3];
+    int Cid;
+    assert( iVarC >= 0 && iVarT >= 0 && iVarE >= 0 && iVarZ >= 0 );
+
+    Lits[0] = toLitCond( iVarC, 1 );
+    Lits[1] = toLitCond( iVarT, 1 );
+    Lits[2] = toLitCond( iVarZ, 0 );
+    Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
+    assert( Cid );
+
+    Lits[0] = toLitCond( iVarC, 1 );
+    Lits[1] = toLitCond( iVarT, 0 );
+    Lits[2] = toLitCond( iVarZ, 1 );
+    Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
+    assert( Cid );
+
+    Lits[0] = toLitCond( iVarC, 0 );
+    Lits[1] = toLitCond( iVarE, 1 );
+    Lits[2] = toLitCond( iVarZ, 0 );
+    Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
+    assert( Cid );
+
+    Lits[0] = toLitCond( iVarC, 0 );
+    Lits[1] = toLitCond( iVarE, 0 );
+    Lits[2] = toLitCond( iVarZ, 1 );
+    Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
+    assert( Cid );
+
+    if ( iVarT == iVarE )
+        return 4;
+
+    Lits[0] = toLitCond( iVarT, 0 );
+    Lits[1] = toLitCond( iVarE, 0 );
+    Lits[2] = toLitCond( iVarZ, 1 );
+    Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
+    assert( Cid );
+
+    Lits[0] = toLitCond( iVarT, 1 );
+    Lits[1] = toLitCond( iVarE, 1 );
+    Lits[2] = toLitCond( iVarZ, 0 );
+    Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
+    assert( Cid );
+    return 6;
+}
 static inline int sat_solver_add_xor_and( sat_solver * pSat, int iVarF, int iVarA, int iVarB, int iVarC )
 {
     // F = (a (+) b) * c