Adding support for a different bit-blasting of a multiplier and squarer.

abclib.dsp

@@ -4323,6 +4323,10 @@ SOURCE=.\src\aig\gia\giaRex.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\gia\giaSatLut.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\gia\giaSatMap.c
 # End Source File
 # Begin Source File

src/aig/gia/giaSatLut.c

+/**CFile****************************************************************
+
+  FileName    [giaSatLut.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Scalable AIG package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: giaSatLut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+#include "sat/bsat/satStore.h"
+#include "misc/vec/vecWec.h"
+#include "misc/util/utilNam.h"
+#include "map/scl/sclCon.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Sbl_Man_t_ Sbl_Man_t;
+struct Sbl_Man_t_
+{
+    sat_solver *     pSat;       // SAT solver
+    Vec_Int_t *      vCardVars;  // candinality variables
+    int              LogN;       // max vars
+    int              FirstVar;   // first variable to be used
+    int              LitShift;   // shift in terms of literals (2*Gia_ManCiNum(pGia)+2)
+    int              nInputs;    // the number of inputs
+    // mapping 
+    Vec_Wec_t *      vMapping;   // current mapping
+    // window
+    Gia_Man_t *      pGia;
+    Vec_Int_t *      vLeaves;    // leaf nodes
+    Vec_Int_t *      vNodes;     // internal nodes
+    Vec_Int_t *      vRoots;     // driver nodes (a subset of vNodes)
+    Vec_Int_t *      vRootVars;  // driver nodes (as SAT variables)
+    // cuts
+    Vec_Wrd_t *      vCutsI;     // input bit patterns
+    Vec_Wrd_t *      vCutsN;     // node bit patterns
+    Vec_Int_t *      vCutsNum;   // cut counts for each obj
+    Vec_Int_t *      vCutsStart; // starting cuts for each obj
+    Vec_Int_t *      vCutsObj;   // object to which this cut belongs
+    Vec_Wrd_t *      vTempI;     // temporary cuts
+    Vec_Wrd_t *      vTempN;     // temporary cuts
+    Vec_Int_t *      vSolCuts;   // cuts belonging to solution
+    Vec_Int_t *      vSolCuts2;  // cuts belonging to solution
+    // temporary
+    Vec_Int_t *      vLits;      // literals
+    Vec_Int_t *      vAssump;    // literals
+    Vec_Int_t *      vPolar;     // variables polarity
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Wec_t * Sbl_ManToMapping( Gia_Man_t * p )
+{
+    Vec_Wec_t * vMapping = Vec_WecStart( Gia_ManObjNum(p) );
+    int Obj, Fanin, k;
+    Gia_ManForEachLut( p, Obj )
+        Gia_LutForEachFanin( p, Obj, Fanin, k )
+            Vec_WecPush( vMapping, Obj, Fanin );
+    return vMapping;
+}
+Vec_Int_t * Sbl_ManFromMapping( Gia_Man_t * p, Vec_Wec_t * vMap )
+{
+    Vec_Int_t * vMapping, * vVec; int i, k, Obj;
+    vMapping = Vec_IntAlloc( Gia_ManObjNum(p) + Vec_WecSizeSize(vMap) + 2*Vec_WecSizeUsed(vMap) );
+    Vec_IntFill( vMapping, Gia_ManObjNum(p), 0 );
+    Vec_WecForEachLevel( vMap, vVec, i )
+        if ( Vec_IntSize(vVec) > 0 )
+        {
+            Vec_IntWriteEntry( vMapping, i, Vec_IntSize(vMapping) );
+            Vec_IntPush( vMapping, Vec_IntSize(vVec) );
+            Vec_IntForEachEntry( vVec, Obj, k )
+                Vec_IntPush( vMapping, Obj );
+            Vec_IntPush( vMapping, i );
+        }
+    assert( Vec_IntSize(vMapping) < 16 || Vec_IntSize(vMapping) == Vec_IntCap(vMapping) );
+    return vMapping;
+}
+void Sbl_ManUpdateMapping( Sbl_Man_t * p )
+{
+    Vec_Int_t * vObj;
+    int i, c, b, iObj; 
+    word CutI, CutN;
+    assert( Vec_IntSize(p->vSolCuts2) < Vec_IntSize(p->vSolCuts) );
+    Vec_IntForEachEntry( p->vNodes, iObj, i )
+        Vec_IntClear( Vec_WecEntry(p->vMapping, iObj) );
+    Vec_IntForEachEntry( p->vSolCuts2, c, i )
+    {
+        CutI = Vec_WrdEntry( p->vCutsI, c );
+        CutN = Vec_WrdEntry( p->vCutsN, c );
+        iObj = Vec_IntEntry( p->vCutsObj, c );
+        iObj = Vec_IntEntry( p->vNodes, iObj );
+        vObj = Vec_WecEntry( p->vMapping, iObj );
+        assert( Vec_IntSize(vObj) == 0 );
+        for ( b = 0; b < 64; b++ )
+            if ( (CutI >> b) & 1 )
+                Vec_IntPush( vObj, Vec_IntEntry(p->vLeaves, b) );
+        for ( b = 0; b < 64; b++ )
+            if ( (CutN >> b) & 1 )
+                Vec_IntPush( vObj, Vec_IntEntry(p->vNodes, b) );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static int Sbl_ManPrintCut( word CutI, word CutN, int nInputs )
+{
+    int b, Count = 0; 
+    printf( "{ " );
+    for ( b = 0; b < 64; b++ )
+        if ( (CutI >> b) & 1 )
+            printf( "i%d ", b + 1 ), Count++;
+    printf( " " );
+    for ( b = 0; b < 64; b++ )
+        if ( (CutN >> b) & 1 )
+            printf( "n%d ", nInputs + b + 1 ), Count++;
+    printf( "};\n" );
+    return Count;
+}
+static int Sbl_ManFindAndPrintCut( Sbl_Man_t * p, int c )
+{
+    return Sbl_ManPrintCut( Vec_WrdEntry(p->vCutsI, c), Vec_WrdEntry(p->vCutsN, c), Vec_IntSize(p->vLeaves) );
+}
+static inline int Sbl_CutIsFeasible( word CutI, word CutN )
+{
+    int Count = (CutI != 0) + (CutN != 0);
+    CutI = CutI & (CutI-1);  CutN = CutN & (CutN-1);  Count += (CutI != 0) + (CutN != 0);
+    CutI = CutI & (CutI-1);  CutN = CutN & (CutN-1);  Count += (CutI != 0) + (CutN != 0);
+    CutI = CutI & (CutI-1);  CutN = CutN & (CutN-1);  Count += (CutI != 0) + (CutN != 0);  
+    CutI = CutI & (CutI-1);  CutN = CutN & (CutN-1);  Count += (CutI != 0) + (CutN != 0);
+    return Count <= 4;
+}
+static inline int Sbl_CutPushUncontained( Vec_Wrd_t * vCutsI, Vec_Wrd_t * vCutsN, word CutI, word CutN )
+{
+    int i, k = 0;
+    assert( vCutsI->nSize == vCutsN->nSize );
+    for ( i = 0; i < vCutsI->nSize; i++ )
+        if ( (vCutsI->pArray[i] & CutI) == vCutsI->pArray[i] && (vCutsN->pArray[i] & CutN) == vCutsN->pArray[i]  )
+            return 1;
+    for ( i = 0; i < vCutsI->nSize; i++ )
+        if ( (vCutsI->pArray[i] & CutI) != CutI || (vCutsN->pArray[i] & CutN) != CutN )
+        {
+            Vec_WrdWriteEntry( vCutsI, k, vCutsI->pArray[i] );
+            Vec_WrdWriteEntry( vCutsN, k, vCutsN->pArray[i] );
+            k++;
+        }
+    Vec_WrdShrink( vCutsI, k );
+    Vec_WrdShrink( vCutsN, k );
+    Vec_WrdPush( vCutsI, CutI );
+    Vec_WrdPush( vCutsN, CutN );
+    return 0;
+}
+static inline void Sbl_ManComputeCutsOne( Sbl_Man_t * p, int Fan0, int Fan1, int Obj )
+{
+    word * pCutsI = Vec_WrdArray(p->vCutsI);
+    word * pCutsN = Vec_WrdArray(p->vCutsN);
+    int Start0 = Vec_IntEntry( p->vCutsStart, Fan0 );
+    int Start1 = Vec_IntEntry( p->vCutsStart, Fan1 );
+    int Limit0 = Start0 + Vec_IntEntry( p->vCutsNum, Fan0 );
+    int Limit1 = Start1 + Vec_IntEntry( p->vCutsNum, Fan1 );
+    int i, k;
+    Vec_WrdClear( p->vTempI );
+    Vec_WrdClear( p->vTempN );
+    for ( i = Start0; i < Limit0; i++ )
+        for ( k = Start1; k < Limit1; k++ )
+            if ( Sbl_CutIsFeasible(pCutsI[i] | pCutsI[k], pCutsN[i] | pCutsN[k]) )
+                Sbl_CutPushUncontained( p->vTempI, p->vTempN, pCutsI[i] | pCutsI[k], pCutsN[i] | pCutsN[k] );
+    Vec_IntPush( p->vCutsStart, Vec_WrdSize(p->vCutsI) );
+    Vec_IntPush( p->vCutsNum, Vec_WrdSize(p->vTempI) + 1 );
+    Vec_WrdAppend( p->vCutsI, p->vTempI );
+    Vec_WrdAppend( p->vCutsN, p->vTempN );
+    Vec_WrdPush( p->vCutsI, 0 );
+    Vec_WrdPush( p->vCutsN, (((word)1) << Obj) );
+    for ( i = 0; i <= Vec_WrdSize(p->vTempI); i++ )
+        Vec_IntPush( p->vCutsObj, Obj );
+}
+static inline int Sbl_ManFindCut( Sbl_Man_t * p, int Obj, word CutI, word CutN )
+{
+    word * pCutsI = Vec_WrdArray(p->vCutsI);
+    word * pCutsN = Vec_WrdArray(p->vCutsN);
+    int Start0 = Vec_IntEntry( p->vCutsStart, Obj );
+    int Limit0 = Start0 + Vec_IntEntry( p->vCutsNum, Obj );
+    int i;
+//    printf( "Looking for:\n" );
+//    Sbl_ManPrintCut( CutI, CutN, p->nInputs );
+//    printf( "\n" );
+    for ( i = Start0; i < Limit0; i++ )
+    {
+//        Sbl_ManPrintCut( pCutsI[i], pCutsN[i], p->nInputs );
+        if ( pCutsI[i] == CutI && pCutsN[i] == CutN )
+            return i;
+    }
+    return -1;
+}
+int Sbl_ManComputeCuts( Sbl_Man_t * p )
+{
+    Gia_Obj_t * pObj, * pFanin; 
+    int i, k, Index, nObjs = Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vNodes);
+    assert( Vec_IntSize(p->vLeaves) <= 64 && Vec_IntSize(p->vNodes) <= 64 );
+    // assign leaf cuts
+    Vec_IntClear( p->vCutsStart );
+    Vec_IntClear( p->vCutsObj );
+    Vec_IntClear( p->vCutsNum );
+    Vec_WrdClear( p->vCutsI );
+    Vec_WrdClear( p->vCutsN );
+    Gia_ManForEachObjVec( p->vLeaves, p->pGia, pObj, i )
+    {
+        Vec_IntPush( p->vCutsStart, Vec_WrdSize(p->vCutsI) );
+        Vec_IntPush( p->vCutsObj, -1 );
+        Vec_IntPush( p->vCutsNum, 1 );
+        Vec_WrdPush( p->vCutsI, (((word)1) << i) );
+        Vec_WrdPush( p->vCutsN, 0 );
+        pObj->Value = i;
+    }
+    // assign internal cuts
+    Gia_ManForEachObjVec( p->vNodes, p->pGia, pObj, i )
+    {
+        assert( Gia_ObjIsAnd(pObj) );
+        assert( ~Gia_ObjFanin0(pObj)->Value );
+        assert( ~Gia_ObjFanin1(pObj)->Value );
+        Sbl_ManComputeCutsOne( p, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value, i );
+        pObj->Value = Vec_IntSize(p->vLeaves) + i;
+    }
+    assert( Vec_IntSize(p->vCutsStart) == nObjs );
+    assert( Vec_IntSize(p->vCutsNum)   == nObjs );
+    assert( Vec_WrdSize(p->vCutsI)     == Vec_WrdSize(p->vCutsN) );
+    assert( Vec_WrdSize(p->vCutsI)     == Vec_IntSize(p->vCutsObj) );
+    // check that roots are mapped nodes
+    Vec_IntClear( p->vRootVars );
+    Gia_ManForEachObjVec( p->vRoots, p->pGia, pObj, i )
+    {
+        int Obj = Gia_ObjId(p->pGia, pObj);
+        if ( Gia_ObjIsCi(pObj) )
+            continue;
+        assert( Gia_ObjIsLut(p->pGia, Obj) );
+        assert( ~pObj->Value );
+        Vec_IntPush( p->vRootVars, pObj->Value - Vec_IntSize(p->vLeaves) );
+    }
+    // create current solution
+    Vec_IntClear( p->vPolar );
+    Vec_IntClear( p->vSolCuts );
+    Gia_ManForEachObjVec( p->vNodes, p->pGia, pObj, i )
+    {
+        word CutI = 0, CutN = 0;
+        int Obj = Gia_ObjId(p->pGia, pObj);
+        if ( !Gia_ObjIsLut(p->pGia, Obj) )
+            continue;
+        assert( (int)pObj->Value == Vec_IntSize(p->vLeaves) + i );
+        // add node
+        Vec_IntPush( p->vPolar, i );
+        Vec_IntPush( p->vSolCuts, i );
+        // add its cut
+        Gia_LutForEachFaninObj( p->pGia, Obj, pFanin, k )
+        {
+            assert( (int)pFanin->Value < Vec_IntSize(p->vLeaves) || Gia_ObjIsLut(p->pGia, Gia_ObjId(p->pGia, pFanin)) );
+            assert( ~pFanin->Value );
+            if ( (int)pFanin->Value < Vec_IntSize(p->vLeaves) )
+                CutI |= ((word)1 << pFanin->Value);
+            else
+                CutN |= ((word)1 << (pFanin->Value - Vec_IntSize(p->vLeaves)));
+        }
+        // find the new cut
+        Index = Sbl_ManFindCut( p, Vec_IntSize(p->vLeaves) + i, CutI, CutN );
+        assert( Index >= 0 );
+        Vec_IntPush( p->vPolar, p->FirstVar+Index );
+    }
+    // clean value
+    Gia_ManForEachObjVec( p->vLeaves, p->pGia, pObj, i )
+        pObj->Value = ~0;
+    Gia_ManForEachObjVec( p->vNodes, p->pGia, pObj, i )
+        pObj->Value = ~0;
+    return Vec_WrdSize(p->vCutsI);
+}
+int Sbl_ManCreateCnf( Sbl_Man_t * p )
+{
+    int i, k, c, pLits[2], value;
+    word * pCutsN = Vec_WrdArray(p->vCutsN);
+    assert( p->FirstVar == sat_solver_nvars(p->pSat) );
+    sat_solver_setnvars( p->pSat, sat_solver_nvars(p->pSat) + Vec_WrdSize(p->vCutsI) );
+    //printf( "\n" );
+    for ( i = 0; i < Vec_IntSize(p->vNodes); i++ )
+    {
+        int Start0 = Vec_IntEntry( p->vCutsStart, Vec_IntSize(p->vLeaves) + i );
+        int Limit0 = Start0 + Vec_IntEntry( p->vCutsNum, Vec_IntSize(p->vLeaves) + i ) - 1;
+        // add main clause
+        Vec_IntClear( p->vLits );
+        Vec_IntPush( p->vLits, Abc_Var2Lit(i, 1) );
+        //printf( "Node %d implies cuts: ", i );
+        for ( k = Start0; k < Limit0; k++ )
+        {
+            Vec_IntPush( p->vLits, Abc_Var2Lit(p->FirstVar+k, 0) );
+            //printf( "%d ", p->FirstVar+k );
+        }
+        //printf( "\n" );
+        value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits)  );
+        assert( value );
+        // binary clauses
+        for ( k = Start0; k < Limit0; k++ )
+        {
+            word Cut = pCutsN[k];
+            //printf( "Cut %d implies root node %d.\n", p->FirstVar+k, i );
+            // root clause
+            pLits[0] = Abc_Var2Lit( p->FirstVar+k, 1 );
+            pLits[1] = Abc_Var2Lit( i, 0 );
+            value = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+            assert( value );
+            // fanin clauses
+            for ( c = 0; c < 64 && Cut; c++, Cut >>= 1 )
+            {
+                if ( (Cut & 1) == 0 )
+                    continue;
+                //printf( "Cut %d implies fanin %d.\n", p->FirstVar+k, c );
+                pLits[1] = Abc_Var2Lit( c, 0 );
+                value = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+                assert( value );
+            }
+        }
+    }
+    sat_solver_set_polarity( p->pSat, Vec_IntArray(p->vPolar), Vec_IntSize(p->vPolar) );
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Sbl_Man_t * Sbl_ManAlloc( Gia_Man_t * pGia, int LogN )
+{
+    Sbl_Man_t * p = ABC_CALLOC( Sbl_Man_t, 1 );
+    extern sat_solver * Sbm_AddCardinSolver( int LogN, Vec_Int_t ** pvVars );
+    p->pSat = Sbm_AddCardinSolver( LogN, &p->vCardVars );
+    p->LogN = LogN;
+    p->FirstVar  = sat_solver_nvars( p->pSat );
+    // window
+    p->pGia       = pGia;
+    p->vLeaves    = Vec_IntAlloc( 64 );
+    p->vNodes     = Vec_IntAlloc( 64 );
+    p->vRoots     = Vec_IntAlloc( 64 );
+    p->vRootVars  = Vec_IntAlloc( 64 );
+    // cuts
+    p->vCutsI     = Vec_WrdAlloc( 1000 );     // input bit patterns
+    p->vCutsN     = Vec_WrdAlloc( 1000 );     // node bit patterns
+    p->vCutsNum   = Vec_IntAlloc( 64 );       // cut counts for each obj
+    p->vCutsStart = Vec_IntAlloc( 64 );       // starting cuts for each obj
+    p->vCutsObj   = Vec_IntAlloc( 1000 );
+    p->vSolCuts   = Vec_IntAlloc( 64 );
+    p->vSolCuts2  = Vec_IntAlloc( 64 );
+    p->vTempI     = Vec_WrdAlloc( 32 ); 
+    p->vTempN     = Vec_WrdAlloc( 32 ); 
+    // internal
+    p->vLits      = Vec_IntAlloc( 64 );
+    p->vAssump    = Vec_IntAlloc( 64 );
+    p->vPolar     = Vec_IntAlloc( 1000 );
+    // other
+    Gia_ManFillValue( pGia );
+    p->vMapping   = Sbl_ManToMapping( pGia );
+    return p;
+}
+
+void Sbl_ManStop( Sbl_Man_t * p )
+{
+    sat_solver_delete( p->pSat );
+    Vec_IntFree( p->vCardVars );
+    Vec_WecFree( p->vMapping );
+    // internal
+    Vec_IntFree( p->vLeaves );
+    Vec_IntFree( p->vNodes );
+    Vec_IntFree( p->vRoots );
+    Vec_IntFree( p->vRootVars );
+    // cuts
+    Vec_WrdFree( p->vCutsI );
+    Vec_WrdFree( p->vCutsN );
+    Vec_IntFree( p->vCutsNum );
+    Vec_IntFree( p->vCutsStart );
+    Vec_IntFree( p->vCutsObj );
+    Vec_IntFree( p->vSolCuts );
+    Vec_IntFree( p->vSolCuts2 );
+    Vec_WrdFree( p->vTempI );
+    Vec_WrdFree( p->vTempN );
+    // temporary
+    Vec_IntFree( p->vLits );
+    Vec_IntFree( p->vAssump );
+    Vec_IntFree( p->vPolar );
+    // other
+    ABC_FREE( p );
+}
+
+void Sbl_ManWindow( Sbl_Man_t * p )
+{
+    int i, ObjId;
+    // collect leaves
+    Vec_IntClear( p->vLeaves );
+    Gia_ManForEachCiId( p->pGia, ObjId, i )
+        Vec_IntPush( p->vLeaves, ObjId );
+    // collect internal
+    Vec_IntClear( p->vNodes );
+    Gia_ManForEachAndId( p->pGia, ObjId )
+        Vec_IntPush( p->vNodes, ObjId );
+    // collect roots
+    Vec_IntClear( p->vRoots );
+    Gia_ManForEachCoDriverId( p->pGia, ObjId, i )
+        Vec_IntPush( p->vRoots, ObjId );
+}
+
+int Sbl_ManTestSat( Gia_Man_t * pGia, int fVerbose )
+{
+    abctime clk = Abc_Clock(), clk2;
+    int i, LogN = 6, nVars = 1 << LogN, status, Root;
+    Sbl_Man_t * p = Sbl_ManAlloc( pGia, LogN );
+    int fKeepTrying = 1;
+    int StartSol;
+
+    // derive window
+    Sbl_ManWindow( p );
+    // derive cuts
+    Sbl_ManComputeCuts( p );
+    // derive SAT instance
+    Sbl_ManCreateCnf( p );
+
+    if ( fVerbose )
+    Vec_IntPrint( p->vSolCuts );
+
+    if ( fVerbose )
+    printf( "All clauses = %d.  Multi clauses = %d.  Binary clauses = %d.  Other clauses = %d.\n\n", 
+        sat_solver_nclauses(p->pSat), Vec_IntSize(p->vNodes), Vec_WrdSize(p->vCutsI) - Vec_IntSize(p->vNodes), 
+        sat_solver_nclauses(p->pSat) - Vec_WrdSize(p->vCutsI) );
+
+    // create assumptions
+    // cardinality
+    Vec_IntClear( p->vAssump );
+    Vec_IntPush( p->vAssump, -1 );
+    // unused variables
+    for ( i = Vec_IntSize(p->vNodes); i < nVars; i++ )
+        Vec_IntPush( p->vAssump, Abc_Var2Lit(i, 1) );
+    // root variables
+    Vec_IntForEachEntry( p->vRootVars, Root, i )
+        Vec_IntPush( p->vAssump, Abc_Var2Lit(Root, 0) );
+//    Vec_IntPrint( p->vAssump );
+
+    StartSol = Vec_IntSize(p->vSolCuts) + 1;
+//    StartSol = 30;
+    while ( fKeepTrying && StartSol-fKeepTrying > 0 )
+    {
+        if ( fVerbose )
+            printf( "Trying to find mapping with %d gates.\n", StartSol-fKeepTrying );
+    //    for ( i = Vec_IntSize(p->vSolCuts)-5; i < nVars; i++ )
+    //        Vec_IntPush( p->vAssump, Abc_Var2Lit(Vec_IntEntry(p->vCardVars, i), 1) );
+        Vec_IntWriteEntry( p->vAssump, 0, Abc_Var2Lit(Vec_IntEntry(p->vCardVars, StartSol-fKeepTrying), 1) );
+        // solve the problem
+        clk2 = Abc_Clock();
+        status = sat_solver_solve( p->pSat, Vec_IntArray(p->vAssump), Vec_IntLimit(p->vAssump), 0, 0, 0, 0 );
+        if ( status == l_True )
+        {
+            int Count = 0, LitCount = 0;
+            if ( fVerbose )
+            {
+                printf( "Inputs = %d.  ANDs = %d.  Total = %d. All vars = %d.\n", 
+                    Vec_IntSize(p->vLeaves), Vec_IntSize(p->vNodes), 
+                    Vec_IntSize(p->vLeaves)+Vec_IntSize(p->vNodes), nVars );
+                for ( i = 0; i < Vec_IntSize(p->vNodes); i++ )
+                    printf( "%d", sat_solver_var_value(p->pSat, i) );
+                printf( "\n" );
+                for ( i = 0; i < Vec_IntSize(p->vNodes); i++ )
+                    if ( sat_solver_var_value(p->pSat, i) )
+                    {
+                        printf( "%d=%d ", i, sat_solver_var_value(p->pSat, i) );
+                        Count++;
+                    }
+                printf( "Count = %d\n", Count );
+            }
+//            for ( i = p->FirstVar; i < sat_solver_nvars(p->pSat); i++ )
+//                printf( "%d", sat_solver_var_value(p->pSat, i) );
+//            printf( "\n" );
+            Count = 1;
+            Vec_IntClear( p->vSolCuts2 );
+            for ( i = p->FirstVar; i < sat_solver_nvars(p->pSat); i++ )
+                if ( sat_solver_var_value(p->pSat, i) )
+                {
+                    if ( fVerbose )
+                        printf( "Cut %3d : ", Count++ );
+                    if ( fVerbose )
+                        LitCount += Sbl_ManFindAndPrintCut( p, i-p->FirstVar );
+                    Vec_IntPush( p->vSolCuts2, i-p->FirstVar );
+                }
+            if ( fVerbose )
+                printf( "LitCount = %d.\n", LitCount );
+        }
+        fKeepTrying = status == l_True ? fKeepTrying + 1 : 0;
+        if ( fVerbose )
+        {
+            if ( status == l_False )
+                printf( "UNSAT " );
+            else if ( status == l_True )
+                printf( "SAT   " );
+            else 
+                printf( "UNDEC " );
+            Abc_PrintTime( 1, "Time", Abc_Clock() - clk2 );
+            Abc_PrintTime( 1, "Total time", Abc_Clock() - clk );
+            printf( "\n" );
+        }
+    }
+
+    // update solution
+    Sbl_ManUpdateMapping( p );
+
+    Vec_IntFreeP( &pGia->vMapping );
+    pGia->vMapping = Sbl_ManFromMapping( pGia, p->vMapping );
+
+    Sbl_ManStop( p );
+    return 1;
+}
+
+void Gia_ManLutSat( Gia_Man_t * p, int nNumber, int nConfl, int fVerbose )
+{
+    Sbl_ManTestSat( p, fVerbose );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+

src/aig/gia/giaSatMap.c

@@ -84,7 +84,7 @@ struct Sbm_Man_t_
 ***********************************************************************/
 int Sbm_ManCheckSol( Sbm_Man_t * p, Vec_Int_t * vSol )
 {
-    int K = Vec_IntSize(vSol) - 1;
+    //int K = Vec_IntSize(vSol) - 1;
     int i, j, Lit, Cut;
     int RetValue = 1;
     Vec_Int_t * vCut;

src/aig/gia/module.make

@@ -54,6 +54,7 @@ SRC +=    src/aig/gia/giaAig.c \
     src/aig/gia/giaResub.c \
     src/aig/gia/giaRetime.c \
     src/aig/gia/giaRex.c \
+    src/aig/gia/giaSatLut.c \
     src/aig/gia/giaSatMap.c \
     src/aig/gia/giaScl.c \
     src/aig/gia/giaScript.c \

src/base/abci/abc.c

@@ -418,6 +418,7 @@ static int Abc_CommandAbc9Mf                 ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9Nf                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Of                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Pack               ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9SatLut             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Unmap              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Struct             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Trace              ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -1042,6 +1043,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&nf",           Abc_CommandAbc9Nf,           0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&of",           Abc_CommandAbc9Of,           0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&pack",         Abc_CommandAbc9Pack,         0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&satlut",       Abc_CommandAbc9SatLut,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&unmap",        Abc_CommandAbc9Unmap,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&struct",       Abc_CommandAbc9Struct,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&trace",        Abc_CommandAbc9Trace,        0 );
@@ -34817,6 +34819,83 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9SatLut( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern void Gia_ManLutSat( Gia_Man_t * p, int nNumber, int nConfl, int fVerbose );
+    int c, nNumber = 32, nConfl = 0, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "NCvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-N\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nNumber = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nNumber < 2 )
+            {
+                Abc_Print( -1, "Illigal number of AIG nodes.\n" );
+                goto usage;
+            }
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-C\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nConfl = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Empty GIA network.\n" );
+        return 1;
+    }
+    if ( !Gia_ManHasMapping(pAbc->pGia) )
+    {
+        Abc_Print( -1, "Current AIG has no mapping. Run \"&if\".\n" );
+        return 1;
+    }
+    if ( Gia_ManLutSizeMax(pAbc->pGia) > 4 )
+        Abc_Print( 0, "Current AIG has mapping into %d-LUTs.\n", Gia_ManLutSizeMax(pAbc->pGia) );
+    Gia_ManLutSat( pAbc->pGia, nNumber, nConfl, fVerbose );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &satlut [-NC num] [-vh]\n" );
+    Abc_Print( -2, "\t           performs SAT-based remapping of the 4-LUT network\n" );
+    Abc_Print( -2, "\t-N num   : the limit on the number of AIG nodes in the window [default = %d]\n", nNumber );
+    Abc_Print( -2, "\t-C num   : the limit on the number of conflicts [default = %d]\n", nNumber );
+    Abc_Print( -2, "\t-v       : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h       : prints the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9Unmap( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern void Gia_ManTestStruct( Gia_Man_t * p );