Adding command 'exact' developed by Mathias Soeken to implement Knuth's exact synthesis algorithm.

4 files changed, 649 insertions, 0 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 78afb412..2d63af2d 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -642,6 +642,8 @@ extern ABC_DLL int                Abc_NtkLevelReverse( Abc_Ntk_t * pNtk );
 extern ABC_DLL int                Abc_NtkIsAcyclic( Abc_Ntk_t * pNtk );
 extern ABC_DLL int                Abc_NtkIsAcyclicWithBoxes( Abc_Ntk_t * pNtk );
 extern ABC_DLL Vec_Ptr_t *        Abc_AigGetLevelizedOrder( Abc_Ntk_t * pNtk, int fCollectCis );
+/*=== abcExact.c ==========================================================*/
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int fVerbose );
 /*=== abcFanio.c ==========================================================*/
 extern ABC_DLL void               Abc_ObjAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin );
 extern ABC_DLL void               Abc_ObjDeleteFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index e883c8fc..bc411998 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -135,6 +135,7 @@ static int Abc_CommandCascade                ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandExtract                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandVarMin                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDetect                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandExact                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandLogic                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandComb                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -773,6 +774,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Synthesis",    "extract",       Abc_CommandExtract,          1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "varmin",        Abc_CommandVarMin,           0 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "detect",        Abc_CommandDetect,           0 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "exact",         Abc_CommandExact,            1 );
 
     Cmd_CommandAdd( pAbc, "Various",      "logic",         Abc_CommandLogic,            1 );
     Cmd_CommandAdd( pAbc, "Various",      "comb",          Abc_CommandComb,             1 );
@@ -7274,6 +7276,61 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    int c, fVerbose = 0, nVars;
+    word pTruth[1];
+    Abc_Ntk_t * pNtkRes;
+
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( argc != globalUtilOptind + 1 )
+    {
+        goto usage;
+    }
+
+    nVars = Abc_TtReadHex( pTruth, argv[globalUtilOptind] );
+    pNtkRes = Abc_NtkFindExact( pTruth, nVars, 1, fVerbose );
+    assert( pNtkRes != NULL );
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    Abc_FrameClearVerifStatus( pAbc );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: exact [-vh] <truth>\n" );
+    Abc_Print( -2, "\t           finds optimum networks using SAT-based exact synthesis\n" );
+    Abc_Print( -2, "\t-v       : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h       : print the command usage\n");
+    Abc_Print( -2, "\t\n" );
+    Abc_Print( -2, "\t           This command was contributed by Mathias Soeken from EPFL in July 2016.\n" );
+    Abc_Print( -2, "\t           The author can be contacted as mathias.soeken at epfl.ch\n" );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandLogic( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk, * pNtkRes;
diff --git a/src/base/abci/abcExact.c b/src/base/abci/abcExact.c
new file mode 100644
index 00000000..68d9ebab
--- /dev/null
+++ b/src/base/abci/abcExact.c
@@ -0,0 +1,589 @@
+/**CFile****************************************************************
+
+  FileName    [abcExact.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Find minimum size networks with a SAT solver.]
+
+  Author      [Mathias Soeken]
+
+  Affiliation [EPFL]
+
+  Date        [Ver. 1.0. Started - July 15, 2016.]
+
+  Revision    [$Id: abcFanio.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+/* This implementation is based on Exercises 477 and 478 in
+ * Donald E. Knuth TAOCP Fascicle 6 (Satisfiability) Section 7.2.2.2
+ */
+
+#include "base/abc/abc.h"
+
+#include "misc/util/utilTruth.h"
+#include "misc/vec/vecInt.h"
+#include "misc/vec/vecPtr.h"
+#include "sat/bsat/satSolver.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Ses_Man_t_ Ses_Man_t;
+struct Ses_Man_t_
+{
+    sat_solver * pSat;          /* SAT solver */
+
+    word *       pSpec;         /* specification */
+    int          bSpecInv;      /* remembers whether spec was inverted for normalization */
+    int          nSpecVars;     /* number of variables in specification */
+    int          nSpecFunc;     /* number of functions to synthesize */
+    int          nRows;         /* number of rows in the specification (without 0) */
+    int          fVerbose;      /* be verbose */
+    int          fVeryVerbose;  /* be very verbose */
+
+    int          nGates;        /* number of gates */
+
+    int          nSimVars;      /* number of simulation vars x(i, t) */
+    int          nOutputVars;   /* number of output variables g(h, i) */
+    int          nGateVars;     /* number of gate variables f(i, p, q) */
+    int          nSelectVars;   /* number of select variables s(i, j, k ) */
+
+    int          nOutputOffset; /* offset where output variables start */
+    int          nGateOffset;   /* offset where gate variables start */
+    int          nSelectOffset; /* offset where select variables start */
+
+    abctime      timeSat;       /* SAT runtime */
+    abctime      timeSatSat;    /* SAT runtime (sat instance) */
+    abctime      timeSatUnsat;  /* SAT runtime (unsat instance) */
+    abctime      timeTotal;     /* all runtime */
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+static inline Ses_Man_t * Ses_ManAlloc( word * pTruth, int nVars, int nFunc, int fVerbose )
+{
+    int h;
+
+    Ses_Man_t * p = ABC_CALLOC( Ses_Man_t, 1 );
+    p->pSat       = NULL;
+    p->bSpecInv   = 0;
+    for ( h = 0; h < nFunc; ++h )
+        if ( pTruth[h] & 1 )
+        {
+            pTruth[h] = ~pTruth[h];
+            p->bSpecInv |= ( 1 << h );
+        }
+    p->pSpec        = pTruth;
+    p->nSpecVars    = nVars;
+    p->nSpecFunc    = nFunc;
+    p->nRows        = ( 1 << nVars ) - 1;
+    p->fVerbose     = fVerbose;
+    p->fVeryVerbose = 0;
+
+    return p;
+}
+
+static inline void Ses_ManClean( Ses_Man_t * pSes )
+{
+    int h;
+    for ( h = 0; h < pSes->nSpecFunc; ++h )
+        if ( ( pSes->bSpecInv >> h ) & 1 )
+            pSes->pSpec[h] = ~( pSes->pSpec[h] );
+
+    if ( pSes->pSat )
+        sat_solver_delete( pSes->pSat );
+    
+    ABC_FREE( pSes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Access variables based on indexes.]
+
+***********************************************************************/
+static inline int Ses_ManSimVar( Ses_Man_t * pSes, int i, int t )
+{
+    assert( i < pSes->nGates );
+    assert( t < pSes->nRows );
+
+    return pSes->nRows * i + t;
+}
+
+static inline int Ses_ManOutputVar( Ses_Man_t * pSes, int h, int i )
+{
+    assert( h < pSes->nSpecFunc );
+    assert( i < pSes->nGates );
+
+    return pSes->nOutputOffset + pSes->nGates * h + i;
+}
+
+static inline int Ses_ManGateVar( Ses_Man_t * pSes, int i, int p, int q )
+{
+    assert( i < pSes->nGates );
+    assert( p < 2 );
+    assert( q < 2 );
+    assert( p > 0 || q > 0 );
+
+    return pSes->nGateOffset + i * 3 + ( p << 1 ) + q - 1;
+}
+
+static inline int Ses_ManSelectVar( Ses_Man_t * pSes, int i, int j, int k )
+{
+    int a;
+    int offset;
+
+    assert( i < pSes->nGates );
+    assert( k < pSes->nSpecVars + i );
+    assert( j < k );
+
+    offset = pSes->nSelectOffset;
+    for ( a = pSes->nSpecVars; a < pSes->nSpecVars + i; ++a )
+        offset += a * ( a - 1 ) / 2;
+
+    return offset + ( -j * ( 1 + j - 2 * ( pSes->nSpecVars + i ) ) ) / 2 + ( k - j - 1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Setup variables to find network with nGates gates.]
+
+***********************************************************************/
+static void Ses_ManCreateVars( Ses_Man_t * pSes, int nGates )
+{
+    int i;
+
+    if ( pSes->fVerbose )
+    {
+        printf( "create variables for network with %d functions over %d variables and %d gates\n", pSes->nSpecFunc, pSes->nSpecVars, nGates );
+    }
+
+    pSes->nGates      = nGates;
+    pSes->nSimVars    = nGates * pSes->nRows;
+    pSes->nOutputVars = pSes->nSpecFunc * nGates;
+    pSes->nGateVars   = nGates * 3;
+    pSes->nSelectVars = 0;
+    for ( i = pSes->nSpecVars; i < pSes->nSpecVars + nGates; ++i )
+        pSes->nSelectVars += ( i * ( i - 1 ) ) / 2;
+
+    pSes->nOutputOffset = pSes->nSimVars;
+    pSes->nGateOffset   = pSes->nSimVars + pSes->nOutputVars;
+    pSes->nSelectOffset = pSes->nSimVars + pSes->nOutputVars + pSes->nGateVars;
+
+    if ( pSes->pSat )
+        sat_solver_delete( pSes->pSat );
+    pSes->pSat = sat_solver_new();
+    sat_solver_setnvars( pSes->pSat, pSes->nSimVars + pSes->nOutputVars + pSes->nGateVars + pSes->nSelectVars );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Create clauses.]
+
+***********************************************************************/
+static inline void Ses_ManCreateMainClause( Ses_Man_t * pSes, int t, int i, int j, int k, int a, int b, int c )
+{
+    int pLits[5], ctr = 0, value;
+
+    pLits[ctr++] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 );
+    pLits[ctr++] = Abc_Var2Lit( Ses_ManSimVar( pSes, i, t ), a );
+
+    if ( j < pSes->nSpecVars )
+    {
+        if ( ( ( s_Truths6[j] >> ( t + 1 ) ) & 1 ) != b ) /* 1 in clause, we can omit the clause */
+            return;
+    }
+    else
+        pLits[ctr++] = Abc_Var2Lit( Ses_ManSimVar( pSes, j - pSes->nSpecVars, t ), b );
+
+    if ( k < pSes->nSpecVars )
+    {
+        if ( ( ( s_Truths6[k] >> ( t + 1 ) ) & 1 ) != c ) /* 1 in clause, we can omit the clause */
+            return;
+    }
+    else
+        pLits[ctr++] = Abc_Var2Lit( Ses_ManSimVar( pSes, k - pSes->nSpecVars, t ), c );
+
+    if ( b > 0 || c > 0 )
+        pLits[ctr++] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, b, c ), 1 - a );
+
+    value = sat_solver_addclause( pSes->pSat, pLits, pLits + ctr );
+    assert( value );
+}
+
+static void Ses_ManCreateClauses( Ses_Man_t * pSes )
+{
+    extern int Extra_TruthVarsSymm( unsigned * pTruth, int nVars, int iVar0, int iVar1 );
+
+    int h, i, j, k, t, ii, jj, kk, p, q;
+    int pLits[2];
+    Vec_Int_t * vLits;
+
+    for ( t = 0; t < pSes->nRows; ++t )
+        for ( i = 0; i < pSes->nGates; ++i )
+        {
+            /* main clauses */
+            for ( j = 0; j < pSes->nSpecVars + i; ++j )
+                for ( k = j + 1; k < pSes->nSpecVars + i; ++k )
+                {
+                    Ses_ManCreateMainClause( pSes, t, i, j, k, 0, 0, 1 );
+                    Ses_ManCreateMainClause( pSes, t, i, j, k, 0, 1, 0 );
+                    Ses_ManCreateMainClause( pSes, t, i, j, k, 0, 1, 1 );
+                    Ses_ManCreateMainClause( pSes, t, i, j, k, 1, 0, 0 );
+                    Ses_ManCreateMainClause( pSes, t, i, j, k, 1, 0, 1 );
+                    Ses_ManCreateMainClause( pSes, t, i, j, k, 1, 1, 0 );
+                    Ses_ManCreateMainClause( pSes, t, i, j, k, 1, 1, 1 );
+                }
+
+            /* output clauses */
+            for ( h = 0; h < pSes->nSpecFunc; ++h )
+            {
+                pLits[0] = Abc_Var2Lit( Ses_ManOutputVar( pSes, h, i ), 1 );
+                pLits[1] = Abc_Var2Lit( Ses_ManSimVar( pSes, i, t ), 1 - (int)( ( pSes->pSpec[h] >> ( t + 1 ) ) & 1 ) );
+                assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 2 ) );
+            }
+        }
+
+    /* some output is selected */
+    for ( h = 0; h < pSes->nSpecFunc; ++h )
+    {
+        vLits = Vec_IntAlloc( pSes->nGates );
+        for ( i = 0; i < pSes->nGates; ++i )
+            Vec_IntPush( vLits, Abc_Var2Lit( Ses_ManOutputVar( pSes, h, i ), 0 ) );
+        assert( sat_solver_addclause( pSes->pSat, Vec_IntArray( vLits ), Vec_IntLimit( vLits ) ) );
+        Vec_IntFree( vLits );
+    }
+
+    /* each gate has two operands */
+    for ( i = 0; i < pSes->nGates; ++i )
+    {
+        vLits = Vec_IntAlloc( ( ( pSes->nSpecVars + i ) * ( pSes->nSpecVars + i - 1 ) ) / 2 );
+        for ( j = 0; j < pSes->nSpecVars + i; ++j )
+            for ( k = j + 1; k < pSes->nSpecVars + i; ++k )
+                Vec_IntPush( vLits, Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 0 ) );
+        assert( sat_solver_addclause( pSes->pSat, Vec_IntArray( vLits ), Vec_IntLimit( vLits ) ) );
+        Vec_IntFree( vLits );
+    }
+
+    /* EXTRA clauses: use gate i at least once */
+    for ( i = 0; i < pSes->nGates; ++i )
+    {
+        vLits = Vec_IntAlloc( 0 );
+        for ( h = 0; h < pSes->nSpecFunc; ++h )
+            Vec_IntPush( vLits, Abc_Var2Lit( Ses_ManOutputVar( pSes, h, i ), 0 ) );
+        for ( ii = i + 1; ii < pSes->nGates; ++ii )
+        {
+            for ( j = 0; j < pSes->nSpecVars + i; ++j )
+                Vec_IntPush( vLits, Abc_Var2Lit( Ses_ManSelectVar( pSes, ii, j, pSes->nSpecVars + i ), 0 ) );
+            for ( j = pSes->nSpecVars + i + 1; j < pSes->nSpecVars + ii; ++j )
+                Vec_IntPush( vLits, Abc_Var2Lit( Ses_ManSelectVar( pSes, ii, pSes->nSpecVars + i, j ), 0 ) );
+        }
+        assert( sat_solver_addclause( pSes->pSat, Vec_IntArray( vLits ), Vec_IntLimit( vLits ) ) );
+        Vec_IntFree( vLits );
+    }
+
+    /* EXTRA clauses: co-lexicographic order */
+    for ( i = 0; i < pSes->nGates - 1; ++i )
+    {
+        for ( k = 2; k < pSes->nSpecVars + i; ++k )
+        {
+            for ( j = 1; j < k; ++j )
+                for ( jj = 0; jj < j; ++jj )
+                {
+                    pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 );
+                    pLits[1] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i + 1, jj, k ), 1 );
+                }
+
+            for ( j = 0; j < k; ++j )
+                for ( kk = 1; kk < k; ++kk )
+                    for ( jj = 0; jj < kk; ++jj )
+                    {
+                        pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 );
+                        pLits[1] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i + 1, jj, kk ), 1 );
+                    }
+        }
+    }
+
+    /* EXTRA clauses: symmetric variables */
+    if ( pSes->nSpecFunc == 1 ) /* only check if there is one output function */
+        for ( q = 1; q < pSes->nSpecVars; ++q )
+            for ( p = 0; p < q; ++p )
+                if ( Extra_TruthVarsSymm( (unsigned*)pSes->pSpec, pSes->nSpecVars, p, q ) )
+                {
+                    if ( pSes->fVeryVerbose )
+                        printf( "variables %d and %d are symmetric\n", p, q );
+                    for ( i = 0; i < pSes->nGates; ++i )
+                        for ( j = 0; j < q; ++j )
+                        {
+                            if ( j == p ) continue;
+
+                            vLits = Vec_IntAlloc( 0 );
+                            Vec_IntPush( vLits, Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, q ), 1 ) );
+                            for ( ii = 0; ii < i; ++ii )
+                                for ( kk = 1; kk < pSes->nSpecVars + ii; ++kk )
+                                    for ( jj = 0; jj < kk; ++jj )
+                                        if ( jj == p || kk == p )
+                                            Vec_IntPush( vLits, Abc_Var2Lit( Ses_ManSelectVar( pSes, ii, jj, kk ), 0 ) );
+                            assert( sat_solver_addclause( pSes->pSat, Vec_IntArray( vLits ), Vec_IntLimit( vLits ) ) );
+                            Vec_IntFree( vLits );
+                        }
+                }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Solve.]
+
+***********************************************************************/
+static inline int Ses_ManSolve( Ses_Man_t * pSes )
+{
+    int status;
+    abctime timeStart, timeDelta;
+
+    // if ( pSes->fVerbose )
+    // {
+    //     printf( "solve SAT instance with %d clauses and %d variables\n", sat_solver_nclauses( pSes->pSat ), sat_solver_nvars( pSes->pSat ) );
+    // }
+
+    timeStart = Abc_Clock();
+    status = sat_solver_solve( pSes->pSat, NULL, NULL, 0, 0, 0, 0 );
+    timeDelta = Abc_Clock() - timeStart;
+
+    pSes->timeSat += timeDelta;
+
+    if ( status == l_True )
+    {
+        pSes->timeSatSat += timeDelta;
+        return 1;
+    }
+    else if ( status == l_False )
+    {
+        pSes->timeSatUnsat += timeDelta;
+        return 0;
+    }
+    else
+    {
+        if ( pSes->fVerbose )
+        {
+            printf( "undefined\n" );
+        }
+        return 0;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Extract solution.]
+
+***********************************************************************/
+static Abc_Ntk_t * Ses_ManExtractSolution( Ses_Man_t * pSes )
+{
+    int h, i, j, k;
+    Abc_Ntk_t * pNtk;
+    Abc_Obj_t * pObj;
+    Vec_Ptr_t * pGates, * vNames;
+    char pGateTruth[5];
+    char * pSopCover;
+
+    pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
+    pNtk->pName = Extra_UtilStrsav( "exact" );
+    pGates = Vec_PtrAlloc( pSes->nSpecVars + pSes->nGates );
+    pGateTruth[3] = '0';
+    pGateTruth[4] = '\0';
+    vNames = Abc_NodeGetFakeNames( pSes->nSpecVars + pSes->nSpecFunc );
+
+    /* primary inputs */
+    Vec_PtrPush( pNtk->vObjs, NULL );
+    for ( i = 0; i < pSes->nSpecVars; ++i )
+    {
+        pObj = Abc_NtkCreatePi( pNtk );
+        Abc_ObjAssignName( pObj, (char*)Vec_PtrEntry( vNames, i ), NULL );
+        Vec_PtrPush( pGates, pObj );
+    }
+
+    /* gates */
+    for ( i = 0; i < pSes->nGates; ++i )
+    {
+        pGateTruth[2] = '0' + sat_solver_var_value( pSes->pSat, Ses_ManGateVar( pSes, i, 0, 1 ) );
+        pGateTruth[1] = '0' + sat_solver_var_value( pSes->pSat, Ses_ManGateVar( pSes, i, 1, 0 ) );
+        pGateTruth[0] = '0' + sat_solver_var_value( pSes->pSat, Ses_ManGateVar( pSes, i, 1, 1 ) );
+
+        if ( pSes->fVeryVerbose )
+        {
+            printf( "gate %d has truth table %s", pSes->nSpecVars + i, pGateTruth );
+        }
+
+        pSopCover = Abc_SopFromTruthBin( pGateTruth );
+        pObj = Abc_NtkCreateNode( pNtk );
+        pObj->pData = Abc_SopRegister( (Mem_Flex_t*)pNtk->pManFunc, pSopCover );
+        Vec_PtrPush( pGates, pObj );
+        ABC_FREE( pSopCover );
+
+        for ( k = 0; k < pSes->nSpecVars + i; ++k )
+            for ( j = 0; j < k; ++j )
+                if ( sat_solver_var_value( pSes->pSat, Ses_ManSelectVar( pSes, i, j, k ) ) )
+                {
+                    if ( pSes->fVeryVerbose )
+                        printf( " with children %d and %d\n", j, k );
+                    Abc_ObjAddFanin( pObj, (Abc_Obj_t *)Vec_PtrEntry( pGates, j ) );
+                    Abc_ObjAddFanin( pObj, (Abc_Obj_t *)Vec_PtrEntry( pGates, k ) );
+                    break;
+                }
+    }
+
+    /* outputs */
+    for ( h = 0; h < pSes->nSpecFunc; ++h )
+    {
+        pObj = Abc_NtkCreatePo( pNtk );
+        Abc_ObjAssignName( pObj, (char*)Vec_PtrEntry( vNames, pSes->nSpecVars + h ), NULL );
+        for ( i = 0; i < pSes->nGates; ++i )
+        {
+            if ( sat_solver_var_value( pSes->pSat, Ses_ManOutputVar( pSes, h, i ) ) )
+            {
+                /* if output has been inverted, we need to add an inverter */
+                if ( ( pSes->bSpecInv >> h ) & 1 )
+                    Abc_ObjAddFanin( pObj, Abc_NtkCreateNodeInv( pNtk, (Abc_Obj_t *)Vec_PtrEntry( pGates, pSes->nSpecVars + i ) ) );
+                else
+                    Abc_ObjAddFanin( pObj, (Abc_Obj_t *)Vec_PtrEntry( pGates, pSes->nSpecVars + i ) );
+            }
+        }
+    }
+    Abc_NodeFreeNames( vNames );
+
+    Vec_PtrFree( pGates );
+
+    if ( !Abc_NtkCheck( pNtk ) )
+        printf( "Ses_ManExtractSolution(): Network check has failed.\n" );
+
+
+    return pNtk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Synthesis algorithm.]
+
+***********************************************************************/
+static Abc_Ntk_t * Ses_ManFindMinimumSize( Ses_Man_t * pSes )
+{
+    int nGates = 0;
+    abctime timeStart;
+    Abc_Ntk_t * pNtk;
+
+    timeStart = Abc_Clock();
+
+    while ( true )
+    {
+        ++nGates;
+        Ses_ManCreateVars( pSes, nGates );
+        Ses_ManCreateClauses( pSes );
+        if ( Ses_ManSolve( pSes ) )
+        {
+            pNtk = Ses_ManExtractSolution( pSes );
+            pSes->timeTotal = Abc_Clock() - timeStart;
+            return pNtk;
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Debug.]
+
+***********************************************************************/
+static void Ses_ManPrintRuntime( Ses_Man_t * pSes )
+{
+    printf( "Runtime breakdown:\n" );
+    ABC_PRTP( "Sat   ", pSes->timeSat,      pSes->timeTotal );
+    ABC_PRTP( " Sat  ", pSes->timeSatSat,   pSes->timeTotal );
+    ABC_PRTP( " Unsat", pSes->timeSatUnsat, pSes->timeTotal );
+    ABC_PRTP( "ALL   ", pSes->timeTotal,    pSes->timeTotal );
+}
+
+static inline void Ses_ManPrintVars( Ses_Man_t * pSes )
+{
+    int h, i, j, k, p, q, t;
+
+    for ( i = 0; i < pSes->nGates; ++i )
+        for ( t = 0; t < pSes->nRows; ++t )
+            printf( "x(%d, %d) : %d\n", i, t, Ses_ManSimVar( pSes, i, t ) );
+
+    for ( h = 0; h < pSes->nSpecFunc; ++h )
+        for ( i = 0; i < pSes->nGates; ++i )
+            printf( "h(%d, %d) : %d\n", h, i, Ses_ManOutputVar( pSes, h, i ) );
+
+    for ( i = 0; i < pSes->nGates; ++i )
+        for ( p = 0; p <= 1; ++p )
+            for ( q = 0; q <= 1; ++ q)
+            {
+                if ( p == 0 && q == 0 ) { continue; }
+                printf( "f(%d, %d, %d) : %d\n", i, p, q, Ses_ManGateVar( pSes, i, p, q ) );
+            }
+
+    for ( i = 0; i < pSes->nGates; ++i )
+        for ( j = 0; j < pSes->nSpecVars + i; ++j )
+            for ( k = j + 1; k < pSes->nSpecVars + i; ++k )
+                printf( "s(%d, %d, %d) : %d\n", i, j, k, Ses_ManSelectVar( pSes, i, j, k ) );
+
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Find minimum size networks with a SAT solver.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int fVerbose )
+{
+    int i, j;
+    Ses_Man_t * pSes;
+    Abc_Ntk_t * pNtk;
+
+    /* some checks */
+    assert( nVars >= 2 && nVars <= 6 );
+
+    if ( fVerbose )
+    {
+        printf( "find optimum circuit for %d %d-variable functions:\n", nFunc, nVars );
+        for ( i = 0; i < nFunc; ++i )
+        {
+            printf( "  func %d: ", i + 1 );
+            for ( j = 0; j < ( 1 << nVars ); ++j )
+                printf( "%lu", ( pTruth[i] >> j ) & 1 );
+            printf( "\n" );
+        }
+    }
+
+    pSes = Ses_ManAlloc( pTruth, nVars, nFunc, fVerbose );
+    pNtk = Ses_ManFindMinimumSize( pSes );
+
+    if ( fVerbose )
+        Ses_ManPrintRuntime( pSes );
+
+    /* cleanup */
+    Ses_ManClean( pSes );
+
+    return pNtk;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index a3c343ee..492fc62a 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -16,6 +16,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcDress.c \
     src/base/abci/abcDress2.c \
     src/base/abci/abcDsd.c \
+    src/base/abci/abcExact.c \
     src/base/abci/abcExtract.c \
     src/base/abci/abcFraig.c \
     src/base/abci/abcFx.c \