New SAT-based optimization package.

1 files changed, 232 insertions, 15 deletions

diff --git a/src/opt/sbd/sbdSat.c b/src/opt/sbd/sbdSat.c
index 16405c06..4ae8654c 100644
--- a/src/opt/sbd/sbdSat.c
+++ b/src/opt/sbd/sbdSat.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "sbdInt.h"
+#include "misc/util/utilTruth.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -51,7 +52,7 @@ sat_solver * Sbd_SolverTopo( int M, int N, int K, int pVars[MAX_N][MAX_M+MAX_N][
     sat_solver * pSat = NULL;
     Vec_Int_t * vTemp = Vec_IntAlloc(100);
     // assign vars
-    int RetValue, n, i, k, nVars = 0;
+    int RetValue, n, i, j, k, nVars = 0;
     for ( n = 0; n < N; n++ )
     for ( i = 0; i < M+N; i++ )
     for ( k = 0; k < K; k++ )
@@ -85,14 +86,32 @@ sat_solver * Sbd_SolverTopo( int M, int N, int K, int pVars[MAX_N][MAX_M+MAX_N][
     for ( i = 0; i < M+N; i++ )
     for ( k = 0; k < K;   k++ )
     {
-        int n2, i2, k2;
-        for ( n2 = 0; n2 <=n;   n2++ )
-        for ( i2 = i; i2 < M+N; i2++ )
-        for ( k2 = k; k2 < K;   k2++ )
+        int n2 = n, i2 = i, k2 = k;
+        for ( n2 = 0; n2 <= n;   n2++ )
+        for ( i2 = i; i2 <  M+N; i2++ )
+        for ( k2 = 0; k2 <= k;   k2++ )
         {
             if ( n2 == n && i2 == i && k2 == k )
                 continue;
-            Vec_IntPushTwo( vTemp, Abc_Var2Lit(pVars[n][i][k], 1), Abc_Var2Lit(pVars[n2][i2][k2], 1) );
+            Vec_IntFillTwo( vTemp, 2, Abc_Var2Lit(pVars[n][i][k], 1), Abc_Var2Lit(pVars[n2][i2][k2], 1) );
+            RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
+            assert( RetValue );
+        }
+    }
+    // exclude fanins of two-input nodes
+    if ( K == 2 )
+    for ( n = 0; n < N;   n++ )
+    for ( i = M; i < M+N; i++ )
+    for ( k = 0; k < K;   k++ )
+    {
+        int k2;
+        for ( j = 0;  j < i;  j++ )
+        for ( k2 = 0; k2 < K; k2++ )
+        {
+            Vec_IntClear( vTemp );
+            Vec_IntPush( vTemp, Abc_Var2Lit(pVars[n][i][k], 1) );
+            Vec_IntPush( vTemp, Abc_Var2Lit(pVars[n][j][!k], 1) );
+            Vec_IntPush( vTemp, Abc_Var2Lit(pVars[i-M][j][k2], 1) );
             RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
             assert( RetValue );
         }
@@ -104,9 +123,13 @@ void Sbd_SolverTopoPrint( sat_solver * pSat, int M, int N, int K, int pVars[MAX_
 {
     int n, i, k;
     printf( "Solution:\n" );
-    for ( i = M+N-1; i >= 0; i-- )
+    printf( "     | " );
+    for ( n = 0; n < N; n++ )
+        printf( "%2d  ", M+n );
+    printf( "\n" );
+    for ( i = M+N-2; i >= 0; i-- )
     {
-        printf( "%2d %c : ", i, i < M ? 'i' : 'n' );
+        printf( "%2d %c | ", i, i < M ? 'i' : ' ' );
         for ( n = 0; n < N; n++ )
         {
             for ( k = 0; k < K; k++ )
@@ -118,15 +141,15 @@ void Sbd_SolverTopoPrint( sat_solver * pSat, int M, int N, int K, int pVars[MAX_
 }
 void Sbd_SolverTopoTest()
 {
-    int M = 4; // inputs
-    int N = 3; // nodes
-    int K = 2; // lutsize
-    int status, nCalls, v, nVars;
+    int M = 4;  //  6;  // inputs
+    int N = 4;  // 16;  // nodes
+    int K = 2;  //  2;  // lutsize
+    int status, v, nVars, nIter, nSols = 0;
     int pVars[MAX_N][MAX_M+MAX_N][MAX_K]; // 20 x 32 x 6 = 3840
     Vec_Int_t * vLits = Vec_IntAlloc(100);
     sat_solver * pSat = Sbd_SolverTopo( M, N, K, pVars );
     nVars = sat_solver_nvars( pSat );
-    for ( nCalls = 0; nCalls < 1000000; nCalls++ )
+    for ( nIter = 0; nIter < 1000000; nIter++ )
     {
         // find onset minterm
         status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
@@ -135,6 +158,7 @@ void Sbd_SolverTopoTest()
         if ( status == l_False )
             break;
         assert( status == l_True );
+        nSols++;
         // print solution
         Sbd_SolverTopoPrint( pSat, M, N, K, pVars );
         // remember variable values
@@ -144,14 +168,207 @@ void Sbd_SolverTopoTest()
                 Vec_IntPush( vLits, Abc_Var2Lit(v, 1) );
         // add breaking clause
         status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits) );
-        assert( status );
+        if ( status == 0 )
+            break;
     }
-    printf( "Found %d solutions.\n", nCalls );
+    printf( "Found %d solutions.\n", nSols );
     sat_solver_delete( pSat );
     Vec_IntFree( vLits );
 }
 
 
+
+/**Function*************************************************************
+
+  Synopsis    [Compute truth table for the given parameter settings.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+word Sbd_SolverTruth( int M, int N, int K, int pLuts[MAX_N][MAX_K], int pValues[MAX_N*((1<<MAX_K)-1)] )
+{
+    word Truths[MAX_M+MAX_N];
+    int i, k, v, nLutPars = (1 << K) - 1;
+    assert( M <= 6 );
+    assert( N <= MAX_N );
+    for ( i = 0; i < M; i++ )
+        Truths[i] = s_Truths6[i];
+    for ( i = 0; i < N; i++ )
+    {
+        word Truth = 0, Mint;
+        for ( k = 1; k <= nLutPars; k++ )
+        {            
+            if ( !pValues[i*nLutPars+k-1] )
+                continue;
+            Mint = ~(word)0;
+            for ( v = 0; v < K; v++ )
+                Mint &= ((k >> v) & 1) ? Truths[pLuts[i][v]] :  ~Truths[pLuts[i][v]];
+            Truth |= Mint;
+        }
+        Truths[M+i] = Truth;
+    }
+    return Truths[M+N-1];
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sbd_SolverFunc( int M, int N, int K, int pLuts[MAX_N][MAX_K], word TruthInit, int * pValues ) 
+{
+    int fVerbose = 0;
+    sat_solver * pSat = NULL;
+    int pLits[MAX_K+2], pLits2[MAX_K+2], nLits;
+    int nLutPars = (1 << K) - 1, nVars = N * nLutPars;
+    int i, k, m, status, iMint, Iter, fCompl = (int)(TruthInit & 1);
+    word TruthNew, Truth = (TruthInit & 1) ? ~TruthInit : TruthInit;
+    word Mask = M < 6 ? Abc_Tt6Mask(1 << M) : ~(word)0;
+    printf( "Number of parameters %d x %d = %d.\n", N, nLutPars, nVars );
+    // create solver
+    pSat = sat_solver_new();
+    sat_solver_setnvars( pSat, nVars );
+    // start with the last minterm
+    iMint = (1 << M) - 1;
+    for ( Iter = 0; Iter < (1 << M); Iter++ )
+    {
+        // assign the first intermediate variable
+        int nVarStart = sat_solver_nvars(pSat);
+        sat_solver_setnvars( pSat, nVarStart + N - 1 );
+
+        // add clauses for nodes
+        if ( fVerbose )
+            printf( "\nIter %3d : Minterm %d\n", Iter, iMint );
+        for ( i = 0; i < N; i++ )
+        for ( m = 0; m <= nLutPars; m++ )
+        {
+            if ( fVerbose )
+                printf( "i = %d.  m = %d.\n", i, m );
+            // selector variables
+            nLits = 0;
+            for ( k = 0; k < K; k++ ) 
+            {
+                if ( pLuts[i][k] >= M )
+                {
+                    assert( pLuts[i][k] - M < N - 1 );
+                    pLits[nLits] = pLits2[nLits] = Abc_Var2Lit( nVarStart + pLuts[i][k] - M, (m >> k) & 1 ); 
+                    nLits++;
+                }
+                else if ( ((iMint >> pLuts[i][k]) & 1) != ((m >> k) & 1) )
+                    break;
+            }
+            if ( k < K )
+                continue;
+            // add parameter
+            if ( m )
+            {
+                pLits[nLits]  = Abc_Var2Lit( i*nLutPars + m-1, 1 );
+                pLits2[nLits] = Abc_Var2Lit( i*nLutPars + m-1, 0 );
+                nLits++;
+            }
+            // node variable
+            if ( i != N - 1 ) 
+            {
+                pLits[nLits]  = Abc_Var2Lit( nVarStart + i, 0 );
+                pLits2[nLits] = Abc_Var2Lit( nVarStart + i, 1 );
+                nLits++;
+            }
+            // add clauses
+            if ( i != N - 1 || ((TruthInit >> iMint) & 1) != fCompl )
+            {
+                status = sat_solver_addclause( pSat, pLits2, pLits2 + nLits );
+                if ( status == 0 )
+                {
+                    fCompl = -1;
+                    goto finish;
+                }
+            }
+            if ( (i != N - 1 || ((TruthInit >> iMint) & 1) == fCompl) && m > 0 )
+            {
+                status = sat_solver_addclause( pSat, pLits, pLits + nLits );
+                if ( status == 0 )
+                {
+                    fCompl = -1;
+                    goto finish;
+                }
+            }
+        }
+
+        // run SAT solver
+        status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
+        if ( status == l_Undef )
+            break;
+        if ( status == l_False )
+        {
+            fCompl = -1;
+            goto finish;
+        }
+        assert( status == l_True );
+
+        // collect values
+        for ( i = 0; i < nVars; i++ )
+            pValues[i] = sat_solver_var_value(pSat, i);
+        TruthNew = Sbd_SolverTruth( M, N, K, pLuts, pValues );
+        if ( fVerbose )
+        {
+            for ( i = 0; i < nVars; i++ )
+                printf( "%d=%d ", i, pValues[i] );
+            printf( "  " );
+            for ( i = nVars; i < sat_solver_nvars(pSat); i++ )
+                printf( "%d=%d ", i, sat_solver_var_value(pSat, i) );
+            printf( "\n" );
+            Extra_PrintBinary( stdout, (unsigned *)&Truth, (1 << M) );    printf( "\n" );
+            Extra_PrintBinary( stdout, (unsigned *)&TruthNew, (1 << M) ); printf( "\n" );
+        }
+        if ( (Truth & Mask) == (Mask & TruthNew) )
+            break;
+
+        // get new minterm
+        iMint = Abc_Tt6FirstBit( Truth ^ TruthNew );
+    }
+finish:
+    printf( "Finished after %d iterations and %d conflicts.\n", Iter, sat_solver_nconflicts(pSat) );
+    sat_solver_delete( pSat );
+    return fCompl;
+}
+void Sbd_SolverFuncTest() 
+{
+//    int M = 4;  //  6;  // inputs
+//    int N = 3;  // 16;  // nodes
+//    int K = 2;  //  2;  // lutsize
+    int M = 6;  //  6;  // inputs
+    int N = 5;  // 16;  // nodes
+    int K = 2;  //  2;  // lutsize
+//    word Truth = ~(word)(1 << 0);
+    word Truth = ~(word)(23423);
+    int pLuts[MAX_N][MAX_K] = { {0,1}, {2,3}, {4,5}, {6,7}, {8,9} };
+    int pValues[MAX_N*((1<<MAX_K)-1)];
+    int i, k, nLutPars = (1 << K) - 1;
+    int Res = Sbd_SolverFunc( M, N, K, pLuts, Truth, pValues );
+    if ( Res == -1 )
+    {
+        printf( "Solution does not exist.\n" );
+        return;
+    }
+    printf( "Result (compl = %d):\n", Res );
+    for ( i = 0; i < N; i++ )
+    {
+        for ( k = nLutPars-1; k >= 0; k-- )
+            printf( "%d", pValues[i*nLutPars+k] );
+        printf( "0\n" );
+    }
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////