Several updates to exact synthesis.

2 files changed, 458 insertions, 75 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 74598b4b..244255da 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -7284,12 +7284,15 @@ usage:
 ***********************************************************************/
 int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    int c, nMaxDepth = -1, fVerbose = 0, nVars;
-    word pTruth[1];
+    extern Gia_Man_t * Gia_ManFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrivalTimes, int fVerbose );
+
+    int c, nMaxDepth = -1, fMakeAIG = 0, fTest = 0, fVerbose = 0, nVars = 0, nVarsTmp, nFunc = 0;
+    word pTruth[64];
     Abc_Ntk_t * pNtkRes;
+    Gia_Man_t * pGiaRes;
 
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Dvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Datvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -7304,6 +7307,12 @@ int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nMaxDepth < 0 )
                 goto usage;
             break;
+        case 'a':
+            fMakeAIG ^= 1;
+            break;
+        case 't':
+            fTest ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -7314,23 +7323,64 @@ int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv )
         }
     }
 
-    if ( argc != globalUtilOptind + 1 )
+    if ( fTest )
     {
+        extern void Abc_ExactTest();
+
+        printf( "run test suite, ignore all other settings\n" );
+        Abc_ExactTest( fVerbose );
+        return 0;
+    }
+
+    if ( argc == globalUtilOptind )
         goto usage;
+
+    memset( pTruth, 0, 64 );
+    while ( globalUtilOptind < argc )
+    {
+        if ( nFunc == 16 )
+        {
+            Abc_Print( -1, "Too many functions (at most 16 supported).\n" );
+            goto usage;
+        }
+        nVarsTmp = Abc_TtReadHex( &pTruth[nFunc << 2], argv[globalUtilOptind++] );
+        nFunc++;
+        if ( nVars == 0 )
+            nVars = nVarsTmp;
+        else if ( nVars > 8 )
+        {
+            Abc_Print( -1, "Only 8-variable functions are supported.\n" );
+            goto usage;
+        }
+        else if ( nVars != nVarsTmp )
+        {
+            Abc_Print( -1, "All functions need to have the same size.\n" );
+            goto usage;
+        }
     }
 
-    nVars = Abc_TtReadHex( pTruth, argv[globalUtilOptind] );
-    pNtkRes = Abc_NtkFindExact( pTruth, nVars, 1, nMaxDepth, fVerbose );
-    assert( pNtkRes != NULL );
-    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
-    Abc_FrameClearVerifStatus( pAbc );
+    if ( fMakeAIG )
+    {
+        pGiaRes = Gia_ManFindExact( pTruth, nVars, nFunc, nMaxDepth, NULL, fVerbose );
+        assert( pGiaRes != NULL );
+        Abc_FrameUpdateGia( pAbc, pGiaRes );
+    }
+    else
+    {
+        pNtkRes = Abc_NtkFindExact( pTruth, nVars, nFunc, nMaxDepth, NULL, 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 for hex truth table <truth>\n" );
-    Abc_Print( -2, "\t-D <num> : constrain maximum depth\n" );
-    Abc_Print( -2, "\t-v       : toggle verbose printout [default = %s]\n", fVerbose ? "yes": "no" );
+    Abc_Print( -2, "usage: exact [-D <num>] [-atvh] <truth1> <truth2> ...\n" );
+    Abc_Print( -2, "\t           finds optimum networks using SAT-based exact synthesis for hex truth tables <truth1> <truth2> ...\n" );
+    Abc_Print( -2, "\t-D <num> : constrain maximum depth (if too low, algorithm may not terminate)\n" );
+    Abc_Print( -2, "\t-a       : create AIG [default = %s]\n", fMakeAIG ? "yes" : "no" );
+    Abc_Print( -2, "\t-t       : run test suite\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" );
diff --git a/src/base/abci/abcExact.c b/src/base/abci/abcExact.c
index c721992b..1bb7973a 100644
--- a/src/base/abci/abcExact.c
+++ b/src/base/abci/abcExact.c
@@ -24,9 +24,11 @@
 
 #include "base/abc/abc.h"
 
+#include "aig/gia/gia.h"
 #include "misc/util/utilTruth.h"
 #include "misc/vec/vecInt.h"
 #include "misc/vec/vecPtr.h"
+#include "proof/cec/cec.h"
 #include "sat/bsat/satSolver.h"
 
 ABC_NAMESPACE_IMPL_START
@@ -36,6 +38,17 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+static word s_Truths8[32] = {
+    ABC_CONST(0xAAAAAAAAAAAAAAAA), ABC_CONST(0xAAAAAAAAAAAAAAAA), ABC_CONST(0xAAAAAAAAAAAAAAAA), ABC_CONST(0xAAAAAAAAAAAAAAAA),
+    ABC_CONST(0xCCCCCCCCCCCCCCCC), ABC_CONST(0xCCCCCCCCCCCCCCCC), ABC_CONST(0xCCCCCCCCCCCCCCCC), ABC_CONST(0xCCCCCCCCCCCCCCCC),
+    ABC_CONST(0xF0F0F0F0F0F0F0F0), ABC_CONST(0xF0F0F0F0F0F0F0F0), ABC_CONST(0xF0F0F0F0F0F0F0F0), ABC_CONST(0xF0F0F0F0F0F0F0F0),
+    ABC_CONST(0xFF00FF00FF00FF00), ABC_CONST(0xFF00FF00FF00FF00), ABC_CONST(0xFF00FF00FF00FF00), ABC_CONST(0xFF00FF00FF00FF00),
+    ABC_CONST(0xFFFF0000FFFF0000), ABC_CONST(0xFFFF0000FFFF0000), ABC_CONST(0xFFFF0000FFFF0000), ABC_CONST(0xFFFF0000FFFF0000),
+    ABC_CONST(0xFFFFFFFF00000000), ABC_CONST(0xFFFFFFFF00000000), ABC_CONST(0xFFFFFFFF00000000), ABC_CONST(0xFFFFFFFF00000000),
+    ABC_CONST(0x0000000000000000), ABC_CONST(0xFFFFFFFFFFFFFFFF), ABC_CONST(0x0000000000000000), ABC_CONST(0xFFFFFFFFFFFFFFFF),
+    ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0xFFFFFFFFFFFFFFFF), ABC_CONST(0xFFFFFFFFFFFFFFFF)
+};
+
 typedef struct Ses_Man_t_ Ses_Man_t;
 struct Ses_Man_t_
 {
@@ -47,6 +60,11 @@ struct Ses_Man_t_
     int          nSpecFunc;     /* number of functions to synthesize */
     int          nRows;         /* number of rows in the specification (without 0) */
     int          nMaxDepth;     /* maximum depth (-1 if depth is not constrained) */
+    int *        pArrivalTimes; /* arrival times of inputs (NULL if arrival times are ignored) */
+    int          nArrivalDelta; /* delta to the original arrival times (arrival times are normalized to have 0 as minimum element) */
+    int          nArrivalMax;   /* maximum normalized arrival time */
+    int          nBTLimit;      /* conflict limit */
+    int          fMakeAIG;      /* create AIG instead of general network */
     int          fVerbose;      /* be verbose */
     int          fVeryVerbose;  /* be very verbose */
 
@@ -73,36 +91,73 @@ struct Ses_Man_t_
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline Ses_Man_t * Ses_ManAlloc( word * pTruth, int nVars, int nFunc, int nMaxDepth, int fVerbose )
+int NormalizeArrivalTimes( int * pArrivalTimes, int nVars, int * maxNormalized )
 {
-    int h;
+    int * p = pArrivalTimes, * pEnd = pArrivalTimes + nVars;
+    int delta = *p;
+
+    while ( ++p < pEnd )
+        if ( *p < delta )
+            delta = *p;
+
+    *maxNormalized = 0;
+    p = pArrivalTimes;
+    while ( p < pEnd )
+    {
+        *p -= delta;
+        if ( *p > *maxNormalized )
+            *maxNormalized = *p;
+        ++p;
+    }
+
+    *maxNormalized += 1;
+
+    return delta;
+}
+
+static inline Ses_Man_t * Ses_ManAlloc( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrivalTimes, int fMakeAIG, int fVerbose )
+{
+    int h, i;
 
     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 )
+        if ( pTruth[h << 2] & 1 )
         {
-            pTruth[h] = ~pTruth[h];
+            for ( i = 0; i < 4; ++i )
+                pTruth[(h << 2) + i] = ~pTruth[(h << 2) + i];
             p->bSpecInv |= ( 1 << h );
         }
-    p->pSpec        = pTruth;
-    p->nSpecVars    = nVars;
-    p->nSpecFunc    = nFunc;
-    p->nRows        = ( 1 << nVars ) - 1;
-    p->nMaxDepth    = nMaxDepth;
-    p->fVerbose     = fVerbose;
-    p->fVeryVerbose = 0;
+    p->pSpec         = pTruth;
+    p->nSpecVars     = nVars;
+    p->nSpecFunc     = nFunc;
+    p->nRows         = ( 1 << nVars ) - 1;
+    p->nMaxDepth     = nMaxDepth;
+    p->pArrivalTimes = nMaxDepth >= 0 ? pArrivalTimes : NULL;
+    if ( p->pArrivalTimes )
+        p->nArrivalDelta = NormalizeArrivalTimes( p->pArrivalTimes, nVars, &p->nArrivalMax );
+    else
+        p->nArrivalDelta = p->nArrivalMax = 0;
+    p->fMakeAIG      = fMakeAIG;
+    p->nBTLimit      = nMaxDepth >= 0 ? 50000 : 0;
+    p->fVerbose      = fVerbose;
+    p->fVeryVerbose  = 0;
 
     return p;
 }
 
 static inline void Ses_ManClean( Ses_Man_t * pSes )
 {
-    int h;
+    int h, i;
     for ( h = 0; h < pSes->nSpecFunc; ++h )
         if ( ( pSes->bSpecInv >> h ) & 1 )
-            pSes->pSpec[h] = ~( pSes->pSpec[h] );
+            for ( i = 0; i < 4; ++i )
+                pSes->pSpec[(h << 2) + i] = ~( pSes->pSpec[(h << 2) + i] );
+
+    if ( pSes->pArrivalTimes )
+        for ( i = 0; i < pSes->nSpecVars; ++i )
+            pSes->pArrivalTimes[i] += pSes->nArrivalDelta;
 
     if ( pSes->pSat )
         sat_solver_delete( pSes->pSat );
@@ -160,9 +215,9 @@ static inline int Ses_ManSelectVar( Ses_Man_t * pSes, int i, int j, int k )
 static inline int Ses_ManDepthVar( Ses_Man_t * pSes, int i, int j )
 {
     assert( i < pSes->nGates );
-    assert( j <= i );
+    assert( j <= pSes->nArrivalMax + i );
 
-    return pSes->nDepthOffset + ( ( i * ( i + 1 ) ) / 2 ) + j;
+    return pSes->nDepthOffset + i * pSes->nArrivalMax + ( ( i * ( i + 1 ) ) / 2 ) + j;
 }
 
 /**Function*************************************************************
@@ -186,7 +241,7 @@ static void Ses_ManCreateVars( Ses_Man_t * pSes, int nGates )
     pSes->nSelectVars = 0;
     for ( i = pSes->nSpecVars; i < pSes->nSpecVars + nGates; ++i )
         pSes->nSelectVars += ( i * ( i - 1 ) ) / 2;
-    pSes->nDepthVars = pSes->nMaxDepth > 0 ? ( nGates * ( nGates + 1 ) ) / 2 : 0;
+    pSes->nDepthVars = pSes->nMaxDepth > 0 ? nGates * pSes->nArrivalMax + ( nGates * ( nGates + 1 ) ) / 2 : 0;
 
     pSes->nOutputOffset = pSes->nSimVars;
     pSes->nGateOffset   = pSes->nSimVars + pSes->nOutputVars;
@@ -213,7 +268,7 @@ static inline void Ses_ManCreateMainClause( Ses_Man_t * pSes, int t, int i, int
 
     if ( j < pSes->nSpecVars )
     {
-        if ( ( ( s_Truths6[j] >> ( t + 1 ) ) & 1 ) != b ) /* 1 in clause, we can omit the clause */
+        if ( Abc_TtGetBit( s_Truths8 + ( j << 2 ), t + 1 ) != b ) /* 1 in clause, we can omit the clause */
             return;
     }
     else
@@ -221,7 +276,7 @@ static inline void Ses_ManCreateMainClause( Ses_Man_t * pSes, int t, int i, int
 
     if ( k < pSes->nSpecVars )
     {
-        if ( ( ( s_Truths6[k] >> ( t + 1 ) ) & 1 ) != c ) /* 1 in clause, we can omit the clause */
+        if ( Abc_TtGetBit( s_Truths8 + ( k << 2 ), t + 1 ) != c ) /* 1 in clause, we can omit the clause */
             return;
     }
     else
@@ -238,7 +293,7 @@ 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 h, i, j, k, t, ii, jj, kk, p, q, d;
     int pLits[3];
     Vec_Int_t * vLits;
 
@@ -262,7 +317,7 @@ static void Ses_ManCreateClauses( Ses_Man_t * pSes )
             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 ) );
+                pLits[1] = Abc_Var2Lit( Ses_ManSimVar( pSes, i, t ), 1 - Abc_TtGetBit( &pSes->pSpec[h << 2], t + 1 ) );
                 assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 2 ) );
             }
         }
@@ -288,6 +343,29 @@ static void Ses_ManCreateClauses( Ses_Man_t * pSes )
         Vec_IntFree( vLits );
     }
 
+    /* only AIG */
+    if ( pSes->fMakeAIG )
+    {
+        for ( i = 0; i < pSes->nGates; ++i )
+        {
+            /* not 2 ones */
+            pLits[0] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 0, 1 ), 1 );
+            pLits[1] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 0 ), 1 );
+            pLits[2] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 1 ), 0 );
+            assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 3 ) );
+
+            pLits[0] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 0, 1 ), 1 );
+            pLits[1] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 0 ), 0 );
+            pLits[2] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 1 ), 1 );
+            assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 3 ) );
+
+            pLits[0] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 0, 1 ), 0 );
+            pLits[1] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 0 ), 1 );
+            pLits[2] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 1 ), 1 );
+            assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 3 ) );
+        }
+    }
+
     /* EXTRA clauses: use gate i at least once */
     for ( i = 0; i < pSes->nGates; ++i )
     {
@@ -331,7 +409,7 @@ static void Ses_ManCreateClauses( Ses_Man_t * pSes )
     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 ( Extra_TruthVarsSymm( (unsigned*)( &pSes->pSpec[h << 2] ), pSes->nSpecVars, p, q ) )
                 {
                     if ( pSes->fVeryVerbose )
                         printf( "variables %d and %d are symmetric\n", p, q );
@@ -357,11 +435,12 @@ static void Ses_ManCreateClauses( Ses_Man_t * pSes )
     {
         for ( i = 0; i < pSes->nGates; ++i )
         {
+            /* propagate depths from children */
             for ( k = 1; k < i; ++k )
                 for ( j = 0; j < k; ++j )
                 {
                     pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, pSes->nSpecVars + j, pSes->nSpecVars + k ), 1 );
-                    for ( jj = 0; jj <= j; ++jj )
+                    for ( jj = 0; jj <= pSes->nArrivalMax + j; ++jj )
                     {
                         pLits[1] = Abc_Var2Lit( Ses_ManDepthVar( pSes, j, jj ), 1 );
                         pLits[2] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, jj + 1 ), 0 );
@@ -373,7 +452,7 @@ static void Ses_ManCreateClauses( Ses_Man_t * pSes )
                 for ( j = 0; j < pSes->nSpecVars + k; ++j )
                 {
                     pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, pSes->nSpecVars + k ), 1 );
-                    for ( kk = 0; kk <= k; ++kk )
+                    for ( kk = 0; kk <= pSes->nArrivalMax + k; ++kk )
                     {
                         pLits[1] = Abc_Var2Lit( Ses_ManDepthVar( pSes, k, kk ), 1 );
                         pLits[2] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, kk + 1 ), 0 );
@@ -381,17 +460,38 @@ static void Ses_ManCreateClauses( Ses_Man_t * pSes )
                     }
                 }
 
-            pLits[0] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, 0 ), 0 );
-            assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 1 ) );
+            /* propagate depths from arrival times at PIs */
+            if ( pSes->pArrivalTimes )
+            {
+                for ( k = 1; k < pSes->nSpecVars + i; ++k )
+                    for ( j = 0; j < ( ( k < pSes->nSpecVars ) ? k : pSes->nSpecVars ); ++j )
+                    {
+                        d = pSes->pArrivalTimes[j];
+                        if ( k < pSes->nSpecVars && pSes->pArrivalTimes[k] > d )
+                            d = pSes->pArrivalTimes[k];
+
+                        pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 );
+                        pLits[1] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, d + 1 ), 0 );
+                        assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 2 ) );
+                    }
+            }
+            else
+            {
+                /* arrival times are 0 */
+                pLits[0] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, 0 ), 0 );
+                assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 1 ) );
+            }
 
-            for ( j = 1; j <= i; ++j )
+            /* reverse order encoding of depth variables */
+            for ( j = 1; j <= pSes->nArrivalMax + i; ++j )
             {
                 pLits[0] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, j ), 1 );
                 pLits[1] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, j - 1 ), 0 );
                 assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 2 ) );
             }
 
-            if ( pSes->nMaxDepth < i )
+            /* constrain maximum depth */
+            if ( pSes->nMaxDepth < pSes->nArrivalMax + i )
                 for ( h = 0; h < pSes->nSpecFunc; ++h )
                 {
                     pLits[0] = Abc_Var2Lit( Ses_ManOutputVar( pSes, h, i ), 1 );
@@ -412,13 +512,13 @@ 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 ) );
-    // }
+    if ( pSes->fVeryVerbose )
+    {
+        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 );
+    status = sat_solver_solve( pSes->pSat, NULL, NULL, pSes->nBTLimit, 0, 0, 0 );
     timeDelta = Abc_Clock() - timeStart;
 
     pSes->timeSat += timeDelta;
@@ -437,9 +537,9 @@ static inline int Ses_ManSolve( Ses_Man_t * pSes )
     {
         if ( pSes->fVerbose )
         {
-            printf( "undefined\n" );
+            printf( "resource limit reached\n" );
         }
-        return 0;
+        return 2;
     }
 }
 
@@ -448,7 +548,7 @@ static inline int Ses_ManSolve( Ses_Man_t * pSes )
   Synopsis    [Extract solution.]
 
 ***********************************************************************/
-static Abc_Ntk_t * Ses_ManExtractSolution( Ses_Man_t * pSes )
+static Abc_Ntk_t * Ses_ManExtractNtk( Ses_Man_t * pSes )
 {
     int h, i, j, k;
     Abc_Ntk_t * pNtk;
@@ -507,7 +607,7 @@ static Abc_Ntk_t * Ses_ManExtractSolution( Ses_Man_t * pSes )
             if ( pSes->nMaxDepth > 0 )
             {
                 printf( " and depth vector " );
-                for ( j = 0; j <= i; ++j )
+                for ( j = 0; j <= pSes->nArrivalMax + i; ++j )
                     printf( "%d", sat_solver_var_value( pSes->pSat, Ses_ManDepthVar( pSes, i, j ) ) );
             }
             printf( "\n" );
@@ -551,6 +651,88 @@ static Abc_Ntk_t * Ses_ManExtractSolution( Ses_Man_t * pSes )
     return pNtk;
 }
 
+static Gia_Man_t * Ses_ManExtractGia( Ses_Man_t * pSes )
+{
+    int h, i, j, k;
+    Gia_Man_t * pGia;
+    Vec_Int_t * pGates;
+    Vec_Ptr_t * vNames;
+    int nObj, nChild1, nChild2, fChild1Comp, fChild2Comp;
+
+    pGia = Gia_ManStart( pSes->nSpecVars + pSes->nGates + pSes->nSpecFunc + 1 );
+    pGia->nConstrs = 0;
+    pGia->pName = Extra_UtilStrsav( "exact" );
+
+    pGates = Vec_IntAlloc( pSes->nSpecVars + pSes->nGates );
+    vNames = Abc_NodeGetFakeNames( pSes->nSpecVars + pSes->nSpecFunc );
+
+    /* primary inputs */
+    pGia->vNamesIn = Vec_PtrStart( pSes->nSpecVars );
+    for ( i = 0; i < pSes->nSpecVars; ++i )
+    {
+        nObj = Gia_ManAppendCi( pGia );
+        Vec_IntPush( pGates, nObj );
+        Vec_PtrSetEntry( pGia->vNamesIn, i, Extra_UtilStrsav( Vec_PtrEntry( vNames, i ) ) );
+    }
+
+    /* gates */
+    for ( i = 0; i < pSes->nGates; ++i )
+    {
+        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 ) ) )
+                {
+                    nChild1 = Vec_IntEntry( pGates, j );
+                    nChild2 = Vec_IntEntry( pGates, k );
+                    fChild1Comp = fChild2Comp = 0;
+
+                    if ( sat_solver_var_value( pSes->pSat, Ses_ManGateVar( pSes, i, 0, 1 ) ) )
+                    {
+                        nChild1 = Abc_LitNot( nChild1 );
+                        fChild1Comp = 1;
+                    }
+                    if ( sat_solver_var_value( pSes->pSat, Ses_ManGateVar( pSes, i, 1, 0 ) ) )
+                    {
+                        nChild2 = Abc_LitNot( nChild2 );
+                        fChild2Comp = 1;
+                    }
+                    nObj = Gia_ManAppendAnd( pGia, nChild1, nChild2 );
+                    if ( fChild1Comp && fChild2Comp )
+                    {
+                        assert( sat_solver_var_value( pSes->pSat, Ses_ManGateVar( pSes, i, 1, 1 ) ) );
+                        nObj = Abc_LitNot( nObj );
+                    }
+
+                    Vec_IntPush( pGates, nObj );
+
+                    break;
+                }
+    }
+
+    /* outputs */
+    pGia->vNamesOut = Vec_PtrStart( pSes->nSpecFunc );
+    for ( h = 0; h < pSes->nSpecFunc; ++h )
+    {
+        for ( i = 0; i < pSes->nGates; ++i )
+        {
+            if ( sat_solver_var_value( pSes->pSat, Ses_ManOutputVar( pSes, h, i ) ) )
+            {
+                nObj = Vec_IntEntry( pGates, pSes->nSpecVars + i );
+                /* if output has been inverted, we need to add an inverter */
+                if ( ( pSes->bSpecInv >> h ) & 1 )
+                    nObj = Abc_LitNot( nObj );
+                Gia_ManAppendCo( pGia, nObj );
+                Vec_PtrSetEntry( pGia->vNamesOut, h, Extra_UtilStrsav( Vec_PtrEntry( vNames, pSes->nSpecVars + h ) ) );
+            }
+        }
+    }
+    Abc_NodeFreeNames( vNames );
+
+    Vec_IntFree( pGates );
+
+    return pGia;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Debug.]
@@ -565,6 +747,19 @@ static void Ses_ManPrintRuntime( Ses_Man_t * pSes )
     ABC_PRTP( "ALL   ", pSes->timeTotal,    pSes->timeTotal );
 }
 
+static inline void Ses_ManPrintFuncs( Ses_Man_t * pSes )
+{
+    int h;
+
+    printf( "find optimum circuit for %d %d-variable functions:\n", pSes->nSpecFunc, pSes->nSpecVars );
+    for ( h = 0; h < pSes->nSpecFunc; ++h )
+    {
+        printf( "  func %d: ", h + 1 );
+        Abc_TtPrintHexRev( stdout, &pSes->pSpec[h >> 2], pSes->nSpecVars );
+        printf( "\n" );
+    }
+}
+
 static inline void Ses_ManPrintVars( Ses_Man_t * pSes )
 {
     int h, i, j, k, p, q, t;
@@ -602,63 +797,92 @@ static inline void Ses_ManPrintVars( Ses_Man_t * pSes )
   Synopsis    [Synthesis algorithm.]
 
 ***********************************************************************/
-static Abc_Ntk_t * Ses_ManFindMinimumSize( Ses_Man_t * pSes )
+static int Ses_ManFindMinimumSize( Ses_Man_t * pSes )
 {
     int nGates = 0;
-    abctime timeStart;
-    Abc_Ntk_t * pNtk;
-
-    timeStart = Abc_Clock();
 
     while ( true )
     {
         ++nGates;
+
+        /* give up if number of gates is impossible for given depth */
+        if ( pSes->nMaxDepth != -1 && nGates >= ( 1 << pSes->nMaxDepth ) )
+            return 0;
+
         Ses_ManCreateVars( pSes, nGates );
         Ses_ManCreateClauses( pSes );
 
-        if ( Ses_ManSolve( pSes ) )
+        switch ( Ses_ManSolve( pSes ) )
         {
-            pNtk = Ses_ManExtractSolution( pSes );
-            pSes->timeTotal = Abc_Clock() - timeStart;
-            return pNtk;
+        case 1: return 1; /* SAT */
+        case 2: return 0; /* resource limit */
         }
     }
+
+    return 0;
 }
 
 /**Function*************************************************************
 
   Synopsis    [Find minimum size networks with a SAT solver.]
 
-  Description []
+  Description [If nMaxDepth is -1, then depth constraints are ignored.
+               If nMaxDepth is not -1, one can set pArrivalTimes which should have the length of nVars.
+               One can ignore pArrivalTimes by setting it to NULL.]
 
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int fVerbose )
+Abc_Ntk_t * Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrivalTimes, int fVerbose )
 {
-    int i, j;
     Ses_Man_t * pSes;
-    Abc_Ntk_t * pNtk;
+    Abc_Ntk_t * pNtk = NULL;
+    abctime timeStart;
 
     /* some checks */
-    assert( nVars >= 2 && nVars <= 6 );
+    assert( nVars >= 2 && nVars <= 8 );
+
+    timeStart = Abc_Clock();
 
+    pSes = Ses_ManAlloc( pTruth, nVars, nFunc, nMaxDepth, pArrivalTimes, 0, fVerbose );
     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" );
-        }
-    }
+        Ses_ManPrintFuncs( pSes );
+
+    if ( Ses_ManFindMinimumSize( pSes ) )
+        pNtk = Ses_ManExtractNtk( pSes );
+
+    pSes->timeTotal = Abc_Clock() - timeStart;
+
+    if ( fVerbose )
+        Ses_ManPrintRuntime( pSes );
+
+    /* cleanup */
+    Ses_ManClean( pSes );
+
+    return pNtk;
+}
+
+Gia_Man_t * Gia_ManFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrivalTimes, int fVerbose )
+{
+    Ses_Man_t * pSes;
+    Gia_Man_t * pGia = NULL;
+    abctime timeStart;
+
+    /* some checks */
+    assert( nVars >= 2 && nVars <= 8 );
+
+    timeStart = Abc_Clock();
 
-    pSes = Ses_ManAlloc( pTruth, nVars, nFunc, nMaxDepth, fVerbose );
-    pNtk = Ses_ManFindMinimumSize( pSes );
+    pSes = Ses_ManAlloc( pTruth, nVars, nFunc, nMaxDepth, pArrivalTimes, 1, fVerbose );
+    if ( fVerbose )
+        Ses_ManPrintFuncs( pSes );
+
+    if ( Ses_ManFindMinimumSize( pSes ) )
+        pGia = Ses_ManExtractGia( pSes );
+
+    pSes->timeTotal = Abc_Clock() - timeStart;
 
     if ( fVerbose )
         Ses_ManPrintRuntime( pSes );
@@ -666,9 +890,118 @@ Abc_Ntk_t * Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth
     /* cleanup */
     Ses_ManClean( pSes );
 
+    return pGia;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Some test cases.]
+
+***********************************************************************/
+
+Abc_Ntk_t * Abc_NtkFromTruthTable( word * pTruth, int nVars )
+{
+    Abc_Ntk_t * pNtk;
+    Mem_Flex_t * pMan;
+    char * pSopCover;
+
+    pMan = Mem_FlexStart();
+    pSopCover = Abc_SopCreateFromTruth( pMan, nVars, (unsigned*)pTruth );
+    pNtk = Abc_NtkCreateWithNode( pSopCover );
+    Abc_NtkShortNames( pNtk );
+    Mem_FlexStop( pMan, 0 );
+
     return pNtk;
 }
 
+void Abc_ExactTestSingleOutput( int fVerbose )
+{
+    extern void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit );
+
+    word pTruth[4] = {0xcafe, 0, 0, 0};
+    Abc_Ntk_t * pNtk, * pNtk2, * pNtk3, * pNtk4;
+    int pArrivalTimes[4] = {6, 2, 8, 5};
+
+    pNtk = Abc_NtkFromTruthTable( pTruth, 4 );
+
+    pNtk2 = Abc_NtkFindExact( pTruth, 4, 1, -1, NULL, fVerbose );
+    Abc_NtkShortNames( pNtk2 );
+    Abc_NtkCecSat( pNtk, pNtk2, 10000, 0 );
+    assert( pNtk2 );
+    assert( Abc_NtkNodeNum( pNtk2 ) == 6 );
+    Abc_NtkDelete( pNtk2 );
+
+    pNtk3 = Abc_NtkFindExact( pTruth, 4, 1, 3, NULL, fVerbose );
+    Abc_NtkShortNames( pNtk3 );
+    Abc_NtkCecSat( pNtk, pNtk3, 10000, 0 );
+    assert( pNtk3 );
+    assert( Abc_NtkLevel( pNtk3 ) <= 3 );
+    Abc_NtkDelete( pNtk3 );
+
+    pNtk4 = Abc_NtkFindExact( pTruth, 4, 1, 9, pArrivalTimes, fVerbose );
+    Abc_NtkShortNames( pNtk4 );
+    Abc_NtkCecSat( pNtk, pNtk4, 10000, 0 );
+    assert( pNtk4 );
+    assert( Abc_NtkLevel( pNtk4 ) <= 9 );
+    Abc_NtkDelete( pNtk4 );
+
+    assert( !Abc_NtkFindExact( pTruth, 4, 1, 2, NULL, fVerbose ) );
+
+    assert( !Abc_NtkFindExact( pTruth, 4, 1, 8, pArrivalTimes, fVerbose ) );
+
+    Abc_NtkDelete( pNtk );
+}
+
+void Abc_ExactTestSingleOutputAIG( int fVerbose )
+{
+    word pTruth[4] = {0xcafe, 0, 0, 0};
+    Abc_Ntk_t * pNtk;
+    Gia_Man_t * pGia, * pGia2, * pGia3, * pGia4, * pMiter;
+    Cec_ParCec_t ParsCec, * pPars = &ParsCec;
+    int pArrivalTimes[4] = {6, 2, 8, 5};
+
+    Cec_ManCecSetDefaultParams( pPars );
+
+    pNtk = Abc_NtkFromTruthTable( pTruth, 4 );
+    Abc_NtkToAig( pNtk );
+    pGia = Abc_NtkAigToGia( pNtk, 1 );
+
+    pGia2 = Gia_ManFindExact( pTruth, 4, 1, -1, NULL, fVerbose );
+    pMiter = Gia_ManMiter( pGia, pGia2, 0, 1, 0, 0, 1 );
+    assert( pMiter );
+    Cec_ManVerify( pMiter, pPars );
+    Gia_ManStop( pMiter );
+
+    pGia3 = Gia_ManFindExact( pTruth, 4, 1, 3, NULL, fVerbose );
+    pMiter = Gia_ManMiter( pGia, pGia3, 0, 1, 0, 0, 1 );
+    assert( pMiter );
+    Cec_ManVerify( pMiter, pPars );
+    Gia_ManStop( pMiter );
+
+    pGia4 = Gia_ManFindExact( pTruth, 4, 1, 9, pArrivalTimes, fVerbose );
+    pMiter = Gia_ManMiter( pGia, pGia4, 0, 1, 0, 0, 1 );
+    assert( pMiter );
+    Cec_ManVerify( pMiter, pPars );
+    Gia_ManStop( pMiter );
+
+    assert( !Gia_ManFindExact( pTruth, 4, 1, 2, NULL, fVerbose ) );
+
+    assert( !Gia_ManFindExact( pTruth, 4, 1, 8, pArrivalTimes, fVerbose ) );
+
+    Gia_ManStop( pGia );
+    Gia_ManStop( pGia2 );
+    Gia_ManStop( pGia3 );
+    Gia_ManStop( pGia4 );
+}
+
+void Abc_ExactTest( int fVerbose )
+{
+    Abc_ExactTestSingleOutput( fVerbose );
+    Abc_ExactTestSingleOutputAIG( fVerbose );
+
+    printf( "\n" );
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///