summaryrefslogtreecommitdiffstats
path: root/src/opt/sbd/sbdSat.c
diff options
context:
space:
mode:
authorMathias Soeken <mathias.soeken@gmail.com>2016-12-07 10:08:44 +0100
committerMathias Soeken <mathias.soeken@gmail.com>2016-12-07 10:08:44 +0100
commit5af44731bff0061c724912cf76e86dddbb4f2c7a (patch)
tree77ddddb7a79d6424210a7a6b8e8f9649d845d9ba /src/opt/sbd/sbdSat.c
parentf9b7e929045f348ef6ccff9024de3be0c35c2eec (diff)
parent77ef610919b09ed0f8cb0df50e48a7f9c4b9c553 (diff)
downloadabc-5af44731bff0061c724912cf76e86dddbb4f2c7a.tar.gz
abc-5af44731bff0061c724912cf76e86dddbb4f2c7a.tar.bz2
abc-5af44731bff0061c724912cf76e86dddbb4f2c7a.zip
Merged alanmi/abc into default
Diffstat (limited to 'src/opt/sbd/sbdSat.c')
-rw-r--r--src/opt/sbd/sbdSat.c797
1 files changed, 797 insertions, 0 deletions
diff --git a/src/opt/sbd/sbdSat.c b/src/opt/sbd/sbdSat.c
new file mode 100644
index 00000000..ae865627
--- /dev/null
+++ b/src/opt/sbd/sbdSat.c
@@ -0,0 +1,797 @@
+/**CFile****************************************************************
+
+ FileName [sbd.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [SAT-based optimization using internal don't-cares.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: sbd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sbdInt.h"
+#include "misc/util/utilTruth.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+#define MAX_M 8 // max inputs
+#define MAX_N 30 // max nodes
+#define MAX_K 6 // max lutsize
+#define MAX_D 8 // max delays
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+#define SBD_LUTS_MAX 2
+#define SBD_SIZE_MAX 4
+#define SBD_DIV_MAX 16
+
+// new AIG manager
+typedef struct Sbd_Pro_t_ Sbd_Pro_t;
+struct Sbd_Pro_t_
+{
+ int nLuts; // LUT count
+ int nSize; // LUT size
+ int nDivs; // divisor count
+ int nVars; // intermediate variables (nLuts * nSize)
+ int nPars; // total parameter count (nLuts * (1 << nSize) + nLuts * nSize * nDivs)
+ int pPars1[SBD_LUTS_MAX][1<<SBD_SIZE_MAX]; // lut parameters
+ int pPars2[SBD_LUTS_MAX][SBD_SIZE_MAX][SBD_DIV_MAX]; // topo parameters
+ int pVars[SBD_LUTS_MAX][SBD_SIZE_MAX+1]; // internal variables
+ int pDivs[SBD_DIV_MAX]; // divisor variables (external)
+};
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Sbd_ProblemSetup( Sbd_Pro_t * p, int nLuts, int nSize, int nDivs )
+{
+ Vec_Int_t * vCnf = Vec_IntAlloc( 1000 );
+ int i, k, d, v, n, iVar = 0;
+ assert( nLuts >= 1 && nLuts <= 2 );
+ memset( p, 0, sizeof(Sbd_Pro_t) );
+ p->nLuts = nLuts;
+ p->nSize = nSize;
+ p->nDivs = nDivs;
+ p->nVars = nLuts * nSize;
+ p->nPars = nLuts * (1 << nSize) + nLuts * nSize * nDivs;
+ // set parameters
+ for ( i = 0; i < nLuts; i++ )
+ for ( k = 0; k < (1 << nSize); k++ )
+ p->pPars1[i][k] = iVar++;
+ for ( i = 0; i < nLuts; i++ )
+ for ( k = 0; k < nSize; k++ )
+ for ( d = 0; d < nDivs; d++ )
+ p->pPars2[i][k][d] = iVar++;
+ // set intermediate variables
+ for ( i = 0; i < nLuts; i++ )
+ for ( k = 0; k < nSize; k++ )
+ p->pVars[i][k] = iVar++;
+ // set top variables
+ for ( i = 1; i < nLuts; i++ )
+ p->pVars[i][nSize] = p->pVars[i-1][0];
+ // set divisor variables
+ for ( d = 0; d < nDivs; d++ )
+ p->pDivs[d] = iVar++;
+ assert( iVar == p->nPars + p->nVars + p->nDivs );
+
+ // input compatiblity clauses
+ for ( i = 0; i < nLuts; i++ )
+ for ( k = (i > 0); k < nSize; k++ )
+ for ( d = 0; d < nDivs; d++ )
+ for ( n = 0; n < nDivs; n++ )
+ {
+ if ( n < d )
+ {
+ Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k][d], 0) );
+ Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k][n], 0) );
+ Vec_IntPush( vCnf, -1 );
+ }
+ else if ( k < nSize-1 )
+ {
+ Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k][d], 0) );
+ Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k+1][n], 0) );
+ Vec_IntPush( vCnf, -1 );
+ }
+ }
+
+ // create LUT clauses
+ for ( i = 0; i < nLuts; i++ )
+ for ( k = 0; k < (1 << nSize); k++ )
+ for ( n = 0; n < 2; n++ )
+ {
+ for ( v = 0; v < nSize; v++ )
+ Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars1[i][v], (k >> v) & 1) );
+ Vec_IntPush( vCnf, Abc_Var2Lit(p->pVars[i][nSize], n) );
+ Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars1[i][k], !n) );
+ Vec_IntPush( vCnf, -1 );
+ }
+
+ // create input clauses
+ for ( i = 0; i < nLuts; i++ )
+ for ( k = (i > 0); k < nSize; k++ )
+ for ( d = 0; d < nDivs; d++ )
+ for ( n = 0; n < 2; n++ )
+ {
+ Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k][d], 0) );
+ Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars1[i][k], n) );
+ Vec_IntPush( vCnf, Abc_Var2Lit(p->pDivs[d], !n) );
+ Vec_IntPush( vCnf, -1 );
+ }
+
+ return vCnf;
+}
+// add clauses to the don't-care computation solver
+void Sbd_ProblemLoad1( Sbd_Pro_t * p, Vec_Int_t * vCnf, int iStartVar, int * pDivVars, int iTopVar, sat_solver * pSat )
+{
+ int pLits[8], nLits, i, k, iLit, RetValue;
+ int ThisTopVar = p->pVars[0][p->nSize];
+ int FirstDivVar = p->nPars + p->nVars;
+ // add clauses
+ for ( i = 0; i < Vec_IntSize(vCnf); i++ )
+ {
+ assert( Vec_IntEntry(vCnf, i) != -1 );
+ for ( k = i+1; k < Vec_IntSize(vCnf); k++ )
+ if ( Vec_IntEntry(vCnf, i) == -1 )
+ break;
+ nLits = 0;
+ Vec_IntForEachEntryStartStop( vCnf, iLit, i, i, k ) {
+ if ( Abc_Lit2Var(iLit) == ThisTopVar )
+ pLits[nLits++] = Abc_Var2Lit( ThisTopVar, Abc_LitIsCompl(iLit) );
+ else if ( Abc_Lit2Var(iLit) >= FirstDivVar )
+ pLits[nLits++] = Abc_Var2Lit( pDivVars[Abc_Lit2Var(iLit)-FirstDivVar], Abc_LitIsCompl(iLit) );
+ else
+ pLits[nLits++] = iLit + 2 * iStartVar;
+ }
+ assert( nLits <= 8 );
+ RetValue = sat_solver_addclause( pSat, pLits, pLits + nLits );
+ assert( RetValue );
+ }
+}
+// add clauses to the functionality evaluation solver
+void Sbd_ProblemLoad2( Sbd_Pro_t * p, Vec_Wec_t * vCnf, int iStartVar, int * pDivVarValues, int iTopVarValue, sat_solver * pSat )
+{
+ Vec_Int_t * vLevel;
+ int pLits[8], nLits, i, k, iLit, RetValue;
+ int ThisTopVar = p->pVars[0][p->nSize];
+ int FirstDivVar = p->nPars + p->nVars;
+ int FirstIntVar = p->nPars;
+ // add clauses
+ Vec_WecForEachLevel( vCnf, vLevel, i )
+ {
+ nLits = 0;
+ Vec_IntForEachEntry( vLevel, iLit, k ) {
+ if ( Abc_Lit2Var(iLit) == ThisTopVar )
+ {
+ if ( Abc_LitIsCompl(iLit) == iTopVarValue )
+ break;
+ continue;
+ }
+ else if ( Abc_Lit2Var(iLit) >= FirstDivVar )
+ {
+ if ( Abc_LitIsCompl(iLit) == pDivVarValues[Abc_Lit2Var(iLit)-FirstDivVar] )
+ break;
+ continue;
+ }
+ else if ( Abc_Lit2Var(iLit) >= FirstIntVar )
+ pLits[nLits++] = iLit + 2 * iStartVar;
+ else
+ pLits[nLits++] = iLit;
+ }
+ if ( k < Vec_IntSize(vLevel) )
+ continue;
+ assert( nLits <= 8 );
+ RetValue = sat_solver_addclause( pSat, pLits, pLits + nLits );
+ assert( RetValue );
+ }
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+sat_solver * Sbd_SolverTopo( int M, int N, int K, int pVars[MAX_N][MAX_M+MAX_N][MAX_K], int pVars2[MAX_M+MAX_N][MAX_D], int pDelays[], int Req, int * pnVars ) // inputs, nodes, lutsize
+{
+ sat_solver * pSat = NULL;
+ Vec_Int_t * vTemp = Vec_IntAlloc(100);
+ // assign vars
+ int RetValue, n, i, j, j2, k, k2, d, Count, nVars = 0;
+ for ( n = 0; n < N; n++ )
+ for ( i = 0; i < M+N; i++ )
+ for ( k = 0; k < K; k++ )
+ pVars[n][i][k] = -1;
+ for ( n = 0; n < N; n++ )
+ for ( i = 0; i < M+n; i++ )
+ for ( k = 0; k < K; k++ )
+ pVars[n][i][k] = nVars++;
+ printf( "Number of topo vars = %d.\n", nVars );
+ *pnVars = nVars;
+ // add constraints
+ pSat = sat_solver_new();
+ sat_solver_setnvars( pSat, nVars );
+ // each node is used
+ for ( i = 0; i < M+N-1; i++ )
+ {
+ Vec_IntClear( vTemp );
+ for ( n = 0; n < N; n++ )
+ for ( k = 0; k < K; k++ )
+ if ( pVars[n][i][k] >= 0 )
+ Vec_IntPush( vTemp, Abc_Var2Lit(pVars[n][i][k], 0) );
+ RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
+ assert( RetValue );
+ }
+ printf( "Added %d node connectivity constraints.\n", i );
+ // each fanin of each node is connected exactly once
+ Count = 0;
+ for ( n = 0; n < N; n++ )
+ for ( k = 0; k < K; k++ )
+ {
+ // connected
+ Vec_IntClear( vTemp );
+ for ( i = 0; i < M+n; i++ )
+ Vec_IntPush( vTemp, Abc_Var2Lit(pVars[n][i][k], 0) );
+ RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
+ assert( RetValue );
+ // exactly once
+ for ( i = 0; i < M+n; i++ )
+ for ( j = i+1; j < M+n; j++ )
+ {
+ Vec_IntFillTwo( vTemp, 2, Abc_Var2Lit(pVars[n][i][k], 1), Abc_Var2Lit(pVars[n][j][k], 1) );
+ RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
+ assert( RetValue );
+ Count++;
+ }
+ }
+ printf( "Added %d fanin connectivity constraints.\n", Count );
+ // node fanins are unique
+ Count = 0;
+ for ( n = 0; n < N; n++ )
+ for ( i = 0; i < M+n; i++ )
+ for ( k = 0; k < K; k++ )
+ for ( j = i; j < M+n; j++ )
+ for ( k2 = k+1; k2 < K; k2++ )
+ {
+ Vec_IntFillTwo( vTemp, 2, Abc_Var2Lit(pVars[n][i][k], 1), Abc_Var2Lit(pVars[n][j][k2], 1) );
+ RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
+ assert( RetValue );
+ Count++;
+ }
+ printf( "Added %d fanin exclusivity constraints.\n", Count );
+ // nodes are ordered
+ Count = 0;
+ for ( n = 1; n < N; n++ )
+ for ( i = 0; i < M+n-1; i++ )
+ {
+ // first of n cannot be smaller than first of n-1 (but can be equal)
+ for ( j = i+1; j < M+n-1; j++ )
+ {
+ Vec_IntFillTwo( vTemp, 2, Abc_Var2Lit(pVars[n][i][0], 1), Abc_Var2Lit(pVars[n-1][j][0], 1) );
+ RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
+ assert( RetValue );
+ Count++;
+ }
+ // if first nodes of n and n-1 are equal, second nodes are ordered
+ Vec_IntFillTwo( vTemp, 2, Abc_Var2Lit(pVars[n][i][0], 1), Abc_Var2Lit(pVars[n-1][i][0], 1) );
+ for ( j = 0; j < i; j++ )
+ for ( j2 = j+1; j2 < i; j2++ )
+ {
+ Vec_IntPushTwo( vTemp, Abc_Var2Lit(pVars[n][j][1], 1), Abc_Var2Lit(pVars[n-1][j2][1], 1) );
+ RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
+ assert( RetValue );
+ Vec_IntShrink( vTemp, 2 );
+ Count++;
+ }
+ }
+ printf( "Added %d node ordering constraints.\n", Count );
+ // exclude fanins of two-input nodes
+ Count = 0;
+ if ( K == 2 )
+ for ( n = 1; n < N; n++ )
+ for ( i = M; i < M+n; i++ )
+ for ( j = 0; j < i; j++ )
+ for ( k = 0; k < K; k++ )
+ {
+ Vec_IntClear( vTemp );
+ Vec_IntPush( vTemp, Abc_Var2Lit(pVars[n][i][0], 1) );
+ Vec_IntPush( vTemp, Abc_Var2Lit(pVars[n][j][1], 1) );
+ Vec_IntPush( vTemp, Abc_Var2Lit(pVars[i-M][j][k], 1) );
+ RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
+ assert( RetValue );
+ Count++;
+ }
+ printf( "Added %d two-node non-triviality constraints.\n", Count );
+
+
+ // assign delay vars
+ assert( Req < MAX_D-1 );
+ for ( i = 0; i < M+N; i++ )
+ for ( d = 0; d < MAX_D; d++ )
+ pVars2[i][d] = nVars++;
+ printf( "Number of total vars = %d.\n", nVars );
+ // set input delays
+ for ( i = 0; i < M; i++ )
+ {
+ assert( pDelays[i] < MAX_D-2 );
+ Vec_IntFill( vTemp, 1, Abc_Var2Lit(pVars2[i][pDelays[i]], 0) );
+ RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
+ assert( RetValue );
+ }
+ // set output delay
+ for ( k = Req; k < MAX_D; k++ )
+ {
+ Vec_IntFill( vTemp, 1, Abc_Var2Lit(pVars2[M+N-1][Req+1], 1) );
+ RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
+ assert( RetValue );
+ }
+ // set internal nodes
+ for ( n = 0; n < N; n++ )
+ for ( i = 0; i < M+n; i++ )
+ for ( k = 0; k < K; k++ )
+ for ( d = 0; d < MAX_D-1; d++ )
+ {
+ Vec_IntFill( vTemp, 1, Abc_Var2Lit(pVars[n][i][k], 1) );
+ Vec_IntPush( vTemp, Abc_Var2Lit(pVars2[i][d], 1) );
+ Vec_IntPush( vTemp, Abc_Var2Lit(pVars2[M+n][d+1], 0) );
+ RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
+ assert( RetValue );
+ }
+
+
+ Vec_IntFree( vTemp );
+ return pSat;
+}
+void Sbd_SolverTopoPrint( sat_solver * pSat, int M, int N, int K, int pVars[MAX_N][MAX_M+MAX_N][MAX_K] )
+{
+ int n, i, k;
+ printf( "Solution:\n" );
+ 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' : ' ' );
+ for ( n = 0; n < N; n++ )
+ {
+ for ( k = K-1; k >= 0; k-- )
+ if ( pVars[n][i][k] == -1 )
+ printf( " " );
+ else
+ printf( "%c", sat_solver_var_value(pSat, pVars[n][i][k]) ? '*' : '.' );
+ printf( " " );
+ }
+ printf( "\n" );
+ }
+}
+void Sbd_SolverTopoTest()
+{
+ int M = 8; // 6; // inputs
+ int N = 3; // 16; // nodes
+ int K = 4; // 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
+ int pVars2[MAX_M+MAX_N][MAX_D]; // 20 x 32 x 6 = 3840
+ int pDelays[MAX_M] = {1,0,0,0,1};
+ abctime clk = Abc_Clock();
+ Vec_Int_t * vLits = Vec_IntAlloc(100);
+ sat_solver * pSat = Sbd_SolverTopo( M, N, K, pVars, pVars2, pDelays, 2, &nVars );
+ for ( nIter = 0; nIter < 1000000; nIter++ )
+ {
+ // find onset minterm
+ status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
+ if ( status == l_Undef )
+ break;
+ if ( status == l_False )
+ break;
+ assert( status == l_True );
+ nSols++;
+ // print solution
+ if ( nIter < 5 )
+ Sbd_SolverTopoPrint( pSat, M, N, K, pVars );
+ // remember variable values
+ Vec_IntClear( vLits );
+ for ( v = 0; v < nVars; v++ )
+ if ( sat_solver_var_value(pSat, v) )
+ Vec_IntPush( vLits, Abc_Var2Lit(v, 1) );
+ // add breaking clause
+ status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits) );
+ if ( status == 0 )
+ break;
+ //if ( nIter == 5 )
+ // break;
+ }
+ sat_solver_delete( pSat );
+ Vec_IntFree( vLits );
+ printf( "Found %d solutions. ", nSols );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+}
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Synthesize random topology.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sbd_SolverSynth( int M, int N, int K, int pLuts[MAX_N][MAX_K] )
+{
+ int Used[MAX_M+MAX_N] = {0};
+ int nUnused = M;
+ int n, iFan0, iFan1;
+ srand( time(NULL) );
+ for ( n = 0; nUnused < N - n; n++ )
+ {
+ iFan0 = iFan1 = 0;
+ while ( (iFan0 = rand() % (M + n)) == (iFan1 = rand() % (M + n)) )
+ ;
+ pLuts[n][0] = iFan0;
+ pLuts[n][1] = iFan1;
+ if ( Used[iFan0] == 0 )
+ {
+ Used[iFan0] = 1;
+ nUnused--;
+ }
+ if ( Used[iFan1] == 0 )
+ {
+ Used[iFan1] = 1;
+ nUnused--;
+ }
+ nUnused++;
+ }
+ if ( nUnused == N - n )
+ {
+ // undo the first one
+ for ( iFan0 = 0; iFan0 < M+n; iFan0++ )
+ if ( Used[iFan0] )
+ {
+ Used[iFan0] = 0;
+ nUnused++;
+ break;
+ }
+
+ }
+ assert( nUnused == N - n + 1 );
+ for ( ; n < N; n++ )
+ {
+ for ( iFan0 = 0; iFan0 < M+n; iFan0++ )
+ if ( Used[iFan0] == 0 )
+ {
+ Used[iFan0] = 1;
+ break;
+ }
+ assert( iFan0 < M+n );
+ for ( iFan1 = 0; iFan1 < M+n; iFan1++ )
+ if ( Used[iFan1] == 0 )
+ {
+ Used[iFan1] = 1;
+ break;
+ }
+ assert( iFan1 < M+n );
+ pLuts[n][0] = iFan0;
+ pLuts[n][1] = iFan1;
+ }
+
+ printf( "{\n" );
+ for ( n = 0; n < N; n++ )
+ printf( " {%d, %d}%s // %d\n", pLuts[n][0], pLuts[n][1], n==N-1 ? "" :",", M+n );
+ printf( "};\n" );
+}
+
+
+/**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)] )
+{
+ int i, k, v, nLutPars = (1 << K) - 1;
+ word Truths[MAX_M+MAX_N];
+ assert( M <= 6 && 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];
+}
+word * Sbd_SolverTruthWord( int M, int N, int K, int pLuts[MAX_N][MAX_K], int pValues[MAX_N*((1<<MAX_K)-1)], word * pTruthsElem, int fCompl )
+{
+ int i, k, v, nLutPars = (1 << K) - 1;
+ int nWords = Abc_TtWordNum( M );
+ word * pRes = pTruthsElem + (M+N-1)*nWords;
+ assert( M <= MAX_M && N <= MAX_N );
+ for ( i = 0; i < N; i++ )
+ {
+ word * pMint, * pTruth = pTruthsElem + (M+i)*nWords;
+ Abc_TtClear( pTruth, nWords );
+ for ( k = 1; k <= nLutPars; k++ )
+ {
+ if ( !pValues[i*nLutPars+k-1] )
+ continue;
+ pMint = pTruthsElem + (M+N)*nWords;
+ Abc_TtFill( pMint, nWords );
+ for ( v = 0; v < K; v++ )
+ {
+ word * pFanin = pTruthsElem + pLuts[i][v]*nWords;
+ Abc_TtAndSharp( pMint, pMint, pFanin, nWords, ((k >> v) & 1) == 0 );
+ }
+ Abc_TtOr( pTruth, pTruth, pMint, nWords );
+ }
+ }
+ if ( fCompl )
+ Abc_TtNot( pRes, nWords );
+ return pRes;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sbd_SolverFunc( int M, int N, int K, int pLuts[MAX_N][MAX_K], word * pTruthInit, int * pValues )
+{
+ int fVerbose = 0;
+ abctime clk = Abc_Clock();
+ abctime clk2, clkOther = 0;
+ sat_solver * pSat = NULL;
+ int nWords = Abc_TtWordNum(M);
+ 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)(pTruthInit[0] & 1);
+ // create truth tables
+ word * pTruthNew, * pTruths = ABC_ALLOC( word, Abc_TtWordNum(MAX_N) * (MAX_M + MAX_N + 1) );
+ Abc_TtElemInit2( pTruths, M );
+ // create solver
+ pSat = sat_solver_new();
+ sat_solver_setnvars( pSat, nVars );
+ printf( "Number of parameters %d x %d = %d.\n", N, nLutPars, nVars );
+ // start with the last minterm
+// iMint = (1 << M) - 1;
+ iMint = 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( "Iter %3d : Mint = %3d. Conflicts =%8d.\n", Iter, iMint, sat_solver_nconflicts(pSat) );
+ 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 || Abc_TtGetBit(pTruthInit, iMint) != fCompl )
+ {
+ status = sat_solver_addclause( pSat, pLits2, pLits2 + nLits );
+ if ( status == 0 )
+ {
+ fCompl = -1;
+ goto finish;
+ }
+ }
+ if ( (i != N - 1 || Abc_TtGetBit(pTruthInit, iMint) == 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);
+
+ clk2 = Abc_Clock();
+ pTruthNew = Sbd_SolverTruthWord( M, N, K, pLuts, pValues, pTruths, fCompl );
+ clkOther += Abc_Clock() - clk2;
+
+ 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 *)pTruthInit, (1 << M) ); printf( "\n" );
+ Extra_PrintBinary( stdout, (unsigned *)pTruthNew, (1 << M) ); printf( "\n" );
+ }
+ if ( Abc_TtEqual(pTruthInit, pTruthNew, nWords) )
+ break;
+
+ // get new minterm
+ iMint = Abc_TtFindFirstDiffBit( pTruthInit, pTruthNew, M );
+ }
+finish:
+ printf( "Finished after %d iterations and %d conflicts. ", Iter, sat_solver_nconflicts(pSat) );
+ sat_solver_delete( pSat );
+ ABC_FREE( pTruths );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ Abc_PrintTime( 1, "Time", clkOther );
+ return fCompl;
+}
+void Sbd_SolverFuncTest()
+{
+// int M = 4; // 6; // inputs
+// int N = 3; // 16; // nodes
+// int K = 2; // 2; // lutsize
+// word Truth = ~((word)3 << 8);
+// int pLuts[MAX_N][MAX_K] = { {0,1}, {2,3}, {4,5}, {6,7}, {8,9} };
+
+/*
+ int M = 6; // 6; // inputs
+ int N = 19; // 16; // nodes
+ int K = 2; // 2; // lutsize
+ word pTruth[4] = { ABC_CONST(0x9ef7a8d9c7193a0f), 0, 0, 0 };
+ int pLuts[MAX_N][MAX_K] = {
+ {3, 5}, {1, 6}, {0, 5}, {8, 2}, {7, 9},
+ {0, 1}, {2, 11}, {5, 12}, {3, 13}, {1, 14},
+ {10, 15}, {11, 2}, {3, 17}, {9, 18}, {0, 13},
+ {20, 7}, {19, 21}, {4, 16}, {23, 22}
+ };
+*/
+
+/*
+ int M = 6; // 6; // inputs
+ int N = 5; // 16; // nodes
+ int K = 4; // 2; // lutsize
+ word Truth = ABC_CONST(0x9ef7a8d9c7193a0f);
+ int pLuts[MAX_N][MAX_K] = {
+ {0, 1, 2, 3}, // 6
+ {1, 2, 3, 4}, // 7
+ {2, 3, 4, 5}, // 8
+ {0, 1, 4, 5}, // 9
+ {6, 7, 8, 9} // 10
+ };
+*/
+
+/*
+ int M = 8; // 6; // inputs
+ int N = 7; // 16; // nodes
+ int K = 2; // 2; // lutsize
+// word pTruth[4] = { 0, 0, 0, ABC_CONST(0x8000000000000000) };
+// word pTruth[4] = { ABC_CONST(0x0000000000000001), 0, 0, 0 };
+ word pTruth[4] = { 0, 0, 0, ABC_CONST(0x0000000000020000) };
+ int pLuts[MAX_N][MAX_K] = { {0,1}, {2,3}, {4,5}, {6,7}, {8,9}, {10,11}, {12,13} };
+*/
+
+ int M = 8; // 6; // inputs
+ int N = 7; // 16; // nodes
+ int K = 2; // 2; // lutsize
+ word pTruth[4] = { ABC_CONST(0x0000080000020000), ABC_CONST(0x0000000000020000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000020000) };
+ int pLuts[MAX_N][MAX_K] = { {0,1}, {2,3}, {4,5}, {6,7}, {8,9}, {10,11}, {12,13} };
+
+ int pValues[MAX_N*((1<<MAX_K)-1)];
+ int Res, i, k, nLutPars = (1 << K) - 1;
+
+ //Sbd_SolverSynth( M, N, K, pLuts );
+
+ Res = Sbd_SolverFunc( M, N, K, pLuts, pTruth, 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 ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+