/**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                         ///
////////////////////////////////////////////////////////////////////////

// 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