path: root/src/aig/gia/giaCSat3.c

/**CFile****************************************************************

  FileName    [giaCSat.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Scalable AIG package.]

  Synopsis    [A simple circuit-based solver.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 20, 2005.]

  Revision    [$Id: giaCSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

***********************************************************************/

#include "gia.h"

ABC_NAMESPACE_IMPL_START


////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

typedef struct Cbs3_Par_t_ Cbs3_Par_t;
struct Cbs3_Par_t_
{
    // conflict limits
    int           nBTLimit;     // limit on the number of conflicts
    int           nJustLimit;   // limit on the size of justification queue
    int           nRestLimit;   // limit on the number of restarts
    // current parameters
    int           nBTThis;      // number of conflicts
    int           nJustThis;    // max size of the frontier
    int           nBTTotal;     // total number of conflicts
    int           nJustTotal;   // total size of the frontier
    // other
    int           fVerbose;
};

typedef struct Cbs3_Que_t_ Cbs3_Que_t;
struct Cbs3_Que_t_
{
    int           iHead;        // beginning of the queue
    int           iTail;        // end of the queue
    int           nSize;        // allocated size
    int *         pData;        // nodes stored in the queue
};
 
typedef struct Cbs3_Man_t_ Cbs3_Man_t;
struct Cbs3_Man_t_
{
    Cbs3_Par_t    Pars;         // parameters
    Gia_Man_t *   pAig;         // AIG manager
    Cbs3_Que_t    pProp;        // propagation queue
    Cbs3_Que_t    pJust;        // justification queue
    Cbs3_Que_t    pClauses;     // clause queue
    Vec_Int_t *   vModel;       // satisfying assignment
    Vec_Int_t *   vTemp;        // temporary storage
    // circuit structure
    int           nVars;
    int           nVarsAlloc;
    int           var_inc;
    Vec_Int_t     vMap;
    Vec_Int_t     vRef;
    Vec_Int_t     vFans;
    Vec_Wec_t     vImps;
    // internal data
    Vec_Str_t     vAssign;
    Vec_Str_t     vMark;
    Vec_Int_t     vLevReason;
    Vec_Int_t     vActs;
    Vec_Int_t     vWatches;
    Vec_Int_t     vWatchUpds;
    // SAT calls statistics
    int           nSatUnsat;    // the number of proofs
    int           nSatSat;      // the number of failure
    int           nSatUndec;    // the number of timeouts
    int           nSatTotal;    // the number of calls
    // conflicts
    int           nConfUnsat;   // conflicts in unsat problems
    int           nConfSat;     // conflicts in sat problems
    int           nConfUndec;   // conflicts in undec problems
    // runtime stats
    abctime       timeJFront;
    abctime       timeSatLoad;  // SAT solver loading time
    abctime       timeSatUnsat; // unsat
    abctime       timeSatSat;   // sat
    abctime       timeSatUndec; // undecided
    abctime       timeTotal;    // total runtime
    // other statistics
    int           nPropCalls[3];
    int           nFails[2];
    int           nClauseConf;
    int           nDecs;
};

static inline int   Cbs3_VarUnused( Cbs3_Man_t * p, int iVar )                     { return Vec_IntEntry(&p->vLevReason, 3*iVar) == -1; }
static inline void  Cbs3_VarSetUnused( Cbs3_Man_t * p, int iVar )                  { Vec_IntWriteEntry(&p->vLevReason, 3*iVar, -1);     } 

static inline int   Cbs3_VarMark0( Cbs3_Man_t * p, int iVar )                      { return Vec_StrEntry(&p->vMark, iVar);              }
static inline void  Cbs3_VarSetMark0( Cbs3_Man_t * p, int iVar, int Value )        { Vec_StrWriteEntry(&p->vMark, iVar, (char)Value);   } 

static inline int   Cbs3_VarIsAssigned( Cbs3_Man_t * p, int iVar )                 { return Vec_StrEntry(&p->vAssign, iVar) < 2;        }
static inline void  Cbs3_VarUnassign( Cbs3_Man_t * p, int iVar )                   { assert( Cbs3_VarIsAssigned(p, iVar)); Vec_StrWriteEntry(&p->vAssign, iVar, (char)(2+Vec_StrEntry(&p->vAssign, iVar))); Cbs3_VarSetUnused(p, iVar); }

static inline int   Cbs3_VarValue( Cbs3_Man_t * p, int iVar )                      { return Vec_StrEntry(&p->vAssign, iVar);            }
static inline void  Cbs3_VarSetValue( Cbs3_Man_t * p, int iVar, int v )            { assert( !Cbs3_VarIsAssigned(p, iVar)); Vec_StrWriteEntry(&p->vAssign, iVar, (char)v);                                  }

static inline int   Cbs3_VarLit0( Cbs3_Man_t * p, int iVar )                       { return Vec_IntEntry( &p->vFans, Abc_Var2Lit(iVar, 0) );                             } 
static inline int   Cbs3_VarLit1( Cbs3_Man_t * p, int iVar )                       { return Vec_IntEntry( &p->vFans, Abc_Var2Lit(iVar, 1) );                             } 
static inline int   Cbs3_VarIsPi( Cbs3_Man_t * p, int iVar )                       { return Vec_IntEntry( &p->vFans, Abc_Var2Lit(iVar, 0) ) == 0;                        } 
static inline int   Cbs3_VarIsJust( Cbs3_Man_t * p, int iVar )                     { int * pLits = Vec_IntEntryP(&p->vFans, Abc_Var2Lit(iVar, 0)); return pLits[0] > 0 && Cbs3_VarValue(p, Abc_Lit2Var(pLits[0])) >= 2 && Cbs3_VarValue(p, Abc_Lit2Var(pLits[1])) >= 2; } 

static inline int   Cbs3_VarDecLevel( Cbs3_Man_t * p, int iVar )                   { assert( !Cbs3_VarUnused(p, iVar) ); return Vec_IntEntry(&p->vLevReason, 3*iVar);    }
static inline int   Cbs3_VarReason0( Cbs3_Man_t * p, int iVar )                    { assert( !Cbs3_VarUnused(p, iVar) ); return Vec_IntEntry(&p->vLevReason, 3*iVar+1);  }
static inline int   Cbs3_VarReason1( Cbs3_Man_t * p, int iVar )                    { assert( !Cbs3_VarUnused(p, iVar) ); return Vec_IntEntry(&p->vLevReason, 3*iVar+2);  }
static inline int * Cbs3_VarReasonP( Cbs3_Man_t * p, int iVar )                    { assert( !Cbs3_VarUnused(p, iVar) ); return Vec_IntEntryP(&p->vLevReason, 3*iVar+1); }
static inline int   Cbs3_ClauseDecLevel( Cbs3_Man_t * p, int hClause )             { return Cbs3_VarDecLevel( p, p->pClauses.pData[hClause] );                           }

static inline int   Cbs3_ClauseSize( Cbs3_Man_t * p, int hClause )                 { return p->pClauses.pData[hClause];                                                  }
static inline int * Cbs3_ClauseLits( Cbs3_Man_t * p, int hClause )                 { return p->pClauses.pData+hClause+1;                                                 }
static inline int   Cbs3_ClauseLit( Cbs3_Man_t * p, int hClause, int i )           { return p->pClauses.pData[hClause+1+i];                                              }
static inline int * Cbs3_ClauseNext1p( Cbs3_Man_t * p, int hClause )               { return p->pClauses.pData+hClause+Cbs3_ClauseSize(p, hClause)+2;                     }

static inline void  Cbs3_ClauseSetSize( Cbs3_Man_t * p, int hClause, int x )       { p->pClauses.pData[hClause] = x;                                                     }
static inline void  Cbs3_ClauseSetLit( Cbs3_Man_t * p, int hClause, int i, int x ) { p->pClauses.pData[hClause+i+1] = x;                                                 }
static inline void  Cbs3_ClauseSetNext( Cbs3_Man_t * p, int hClause, int n, int x ){ p->pClauses.pData[hClause+Cbs3_ClauseSize(p, hClause)+1+n] = x;                     }


#define Cbs3_QueForEachEntry( Que, iObj, i )                         \
    for ( i = (Que).iHead; (i < (Que).iTail) && ((iObj) = (Que).pData[i]); i++ )

#define Cbs3_ClauseForEachEntry( p, hClause, iObj, i )               \
    for ( i = 1; i <= Cbs3_ClauseSize(p, hClause) && (iObj = (p)->pClauses.pData[hClause+i]); i++ )
#define Cbs3_ClauseForEachEntry1( p, hClause, iObj, i )              \
    for ( i = 2; i <= Cbs3_ClauseSize(p, hClause) && (iObj = (p)->pClauses.pData[hClause+i]); i++ )

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

/**Function*************************************************************

  Synopsis    [Sets default values of the parameters.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cbs3_SetDefaultParams( Cbs3_Par_t * pPars )
{
    memset( pPars, 0, sizeof(Cbs3_Par_t) );
    pPars->nBTLimit    =  1000;   // limit on the number of conflicts
    pPars->nJustLimit  =   500;   // limit on the size of justification queue
    pPars->nRestLimit  =    10;   // limit on the number of restarts
    pPars->fVerbose    =     1;   // print detailed statistics
}
void Cbs3_ManSetConflictNum( Cbs3_Man_t * p, int Num )
{
    p->Pars.nBTLimit = Num;
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Cbs3_Man_t * Cbs3_ManAlloc( Gia_Man_t * pGia )
{
    Cbs3_Man_t * p;
    p = ABC_CALLOC( Cbs3_Man_t, 1 );
    p->pProp.nSize = p->pJust.nSize = p->pClauses.nSize = 10000;
    p->pProp.pData = ABC_ALLOC( int, p->pProp.nSize );
    p->pJust.pData = ABC_ALLOC( int, p->pJust.nSize );
    p->pClauses.pData = ABC_ALLOC( int, p->pClauses.nSize );
    p->pClauses.iHead = p->pClauses.iTail = 1;
    p->vModel   = Vec_IntAlloc( 1000 );
    p->vTemp    = Vec_IntAlloc( 1000 );
    p->pAig     = pGia;
    Cbs3_SetDefaultParams( &p->Pars );
    // circuit structure
    Vec_IntPush( &p->vMap, -1 );
    Vec_IntPush( &p->vRef, -1 );
    Vec_IntPushTwo( &p->vFans, -1, -1 );
    Vec_WecPushLevel( &p->vImps );
    Vec_WecPushLevel( &p->vImps );
    p->nVars = 1;
    // internal data
    p->nVarsAlloc = 1000;
    Vec_StrFill( &p->vAssign,      p->nVarsAlloc, 2 );
    Vec_StrFill( &p->vMark,        p->nVarsAlloc, 0 );
    Vec_IntFill( &p->vLevReason, 3*p->nVarsAlloc, -1 );
    Vec_IntFill( &p->vActs,        p->nVarsAlloc, 0 );
    Vec_IntFill( &p->vWatches,   2*p->nVarsAlloc, 0 );
    Vec_IntGrow( &p->vWatchUpds, 1000 );
    return p;
}
static inline void Cbs3_ManReset( Cbs3_Man_t * p )
{
    assert( p->nVars == Vec_IntSize(&p->vMap) );
    Vec_IntShrink( &p->vMap, 1 );
    Vec_IntShrink( &p->vRef, 1 );
    Vec_IntShrink( &p->vFans, 2 );
    Vec_WecShrink( &p->vImps, 2 );
    p->nVars = 1;
}
static inline void Cbs3_ManGrow( Cbs3_Man_t * p )
{
    if ( p->nVarsAlloc < p->nVars )
    {
        p->nVarsAlloc = 2*p->nVars;
        Vec_StrFill( &p->vAssign,      p->nVarsAlloc, 2 );
        Vec_StrFill( &p->vMark,        p->nVarsAlloc, 0 );
        Vec_IntFill( &p->vLevReason, 3*p->nVarsAlloc, -1 );
        Vec_IntFill( &p->vActs,        p->nVarsAlloc, 0 );
        Vec_IntFill( &p->vWatches,   2*p->nVarsAlloc, 0 );
    }
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cbs3_ManStop( Cbs3_Man_t * p )
{
    // circuit structure
    Vec_IntErase( &p->vMap );
    Vec_IntErase( &p->vRef );
    Vec_IntErase( &p->vFans );
    Vec_WecErase( &p->vImps );
    // internal data
    Vec_StrErase( &p->vAssign );
    Vec_StrErase( &p->vMark );
    Vec_IntErase( &p->vLevReason );
    Vec_IntErase( &p->vActs );
    Vec_IntErase( &p->vWatches );
    Vec_IntErase( &p->vWatchUpds );
    Vec_IntFree( p->vModel );
    Vec_IntFree( p->vTemp );
    ABC_FREE( p->pClauses.pData );
    ABC_FREE( p->pProp.pData );
    ABC_FREE( p->pJust.pData );
    ABC_FREE( p );
}
int Cbs3_ManMemory( Cbs3_Man_t * p )
{
    int nMem = sizeof(Cbs3_Man_t);
    nMem += (int)Vec_IntMemory( &p->vMap );
    nMem += (int)Vec_IntMemory( &p->vRef );
    nMem += (int)Vec_IntMemory( &p->vFans );
    nMem += (int)Vec_WecMemory( &p->vImps );
    nMem += (int)Vec_StrMemory( &p->vAssign );
    nMem += (int)Vec_StrMemory( &p->vMark );
    nMem += (int)Vec_IntMemory( &p->vActs );
    nMem += (int)Vec_IntMemory( &p->vWatches );
    nMem += (int)Vec_IntMemory( &p->vWatchUpds );
    nMem += (int)Vec_IntMemory( p->vModel );
    nMem += (int)Vec_IntMemory( p->vTemp );
    nMem += 4*p->pClauses.nSize;
    nMem += 4*p->pProp.nSize;
    nMem += 4*p->pJust.nSize;
    return nMem;
}

/**Function*************************************************************

  Synopsis    [Returns satisfying assignment.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Cbs3_ReadModel( Cbs3_Man_t * p )
{
    return p->vModel;
}


/**Function*************************************************************

  Synopsis    [Activity.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
//#define USE_ACTIVITY

#ifdef USE_ACTIVITY
static inline void Cbs3_ActReset( Cbs3_Man_t * p ) 
{
    int i, * pAct = Vec_IntArray(&p->vActs);
    for ( i = 0; i < p->nVars; i++ )
        pAct[i] = (1 << 10);
    p->var_inc = (1 << 5);
}
static inline void Cbs3_ActRescale( Cbs3_Man_t * p ) 
{
    int i, * pAct = Vec_IntArray(&p->vActs);
    for ( i = 0; i < p->nVars; i++ )
        pAct[i] >>= 19;
    p->var_inc >>= 19;
    p->var_inc = Abc_MaxInt( (unsigned)p->var_inc, (1<<5) );
}
static inline void Cbs3_ActBumpVar( Cbs3_Man_t * p, int iVar ) 
{
    int * pAct = Vec_IntArray(&p->vActs);
    pAct[iVar] += p->var_inc;
    if ((unsigned)pAct[iVar] & 0x80000000)
        Cbs3_ActRescale(p);
}
static inline void Cbs3_ActDecay( Cbs3_Man_t * p ) 
{
    p->var_inc += (p->var_inc >>  4); 
}
#else
static inline void Cbs3_ActReset( Cbs3_Man_t * p )              {}
static inline void Cbs3_ActRescale( Cbs3_Man_t * p )            {}
static inline void Cbs3_ActBumpVar( Cbs3_Man_t * p, int iVar )  {}
static inline void Cbs3_ActDecay( Cbs3_Man_t * p )              {}
#endif


/**Function*************************************************************

  Synopsis    [Returns 1 if the solver is out of limits.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Cbs3_ManCheckLimits( Cbs3_Man_t * p )
{
    p->nFails[0] += p->Pars.nJustThis > p->Pars.nJustLimit;
    p->nFails[1] += p->Pars.nBTThis > p->Pars.nBTLimit;
    return p->Pars.nJustThis > p->Pars.nJustLimit || p->Pars.nBTThis > p->Pars.nBTLimit;
}

/**Function*************************************************************

  Synopsis    [Saves the satisfying assignment as an array of literals.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline void Cbs3_ManSaveModel( Cbs3_Man_t * p, Vec_Int_t * vCex )
{
    int i, iLit;
    Vec_IntClear( vCex );
    p->pProp.iHead = 0;
    Cbs3_QueForEachEntry( p->pProp, iLit, i )
        if ( Cbs3_VarIsPi(p, Abc_Lit2Var(iLit)) )
            Vec_IntPush( vCex, Abc_Lit2LitV(Vec_IntArray(&p->vMap), iLit)-2 );
} 
static inline void Cbs3_ManSaveModelAll( Cbs3_Man_t * p, Vec_Int_t * vCex )
{
    int i, iLit;
    Vec_IntClear( vCex );
    p->pProp.iHead = 0;
    Cbs3_QueForEachEntry( p->pProp, iLit, i )
    {
        int iVar = Abc_Lit2Var(iLit);
        Vec_IntPush( vCex, Abc_Var2Lit(iVar, !Cbs3_VarValue(p, iVar)) );
    }
} 

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Cbs3_QueIsEmpty( Cbs3_Que_t * p )
{
    return p->iHead == p->iTail;
}
static inline int Cbs3_QueSize( Cbs3_Que_t * p )
{
    return p->iTail - p->iHead;
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline void Cbs3_QuePush( Cbs3_Que_t * p, int iObj )
{
    if ( p->iTail == p->nSize )
    {
        p->nSize *= 2;
        p->pData = ABC_REALLOC( int, p->pData, p->nSize ); 
    }
    p->pData[p->iTail++] = iObj;
}
static inline void Cbs3_QueGrow( Cbs3_Que_t * p, int Plus )
{
    if ( p->iTail + Plus > p->nSize )
    {
        p->nSize *= 2;
        p->pData = ABC_REALLOC( int, p->pData, p->nSize ); 
    }
    assert( p->iTail + Plus <= p->nSize );
}

/**Function*************************************************************

  Synopsis    [Returns 1 if the object in the queue.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Cbs3_QueHasNode( Cbs3_Que_t * p, int iObj )
{
    int i, iTemp;
    Cbs3_QueForEachEntry( *p, iTemp, i )
        if ( iTemp == iObj )
            return 1;
    return 0;
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline void Cbs3_QueStore( Cbs3_Que_t * p, int * piHeadOld, int * piTailOld )
{
    int i;
    *piHeadOld = p->iHead;
    *piTailOld = p->iTail;
    for ( i = *piHeadOld; i < *piTailOld; i++ )
        Cbs3_QuePush( p, p->pData[i] );
    p->iHead = *piTailOld;
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline void Cbs3_QueRestore( Cbs3_Que_t * p, int iHeadOld, int iTailOld )
{
    p->iHead = iHeadOld;
    p->iTail = iTailOld;
}

/**Function*************************************************************

  Synopsis    [Find variable with the highest ID.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Cbs3_ManDecide( Cbs3_Man_t * p )
{
    int i, iObj, iObjMax = 0;
#ifdef USE_ACTIVITY
    Cbs3_QueForEachEntry( p->pJust, iObj, i )
        if ( iObjMax == 0 || 
             Vec_IntEntry(&p->vActs, iObjMax) <  Vec_IntEntry(&p->vActs, iObj) || 
            (Vec_IntEntry(&p->vActs, iObjMax) == Vec_IntEntry(&p->vActs, iObj) && Vec_IntEntry(&p->vMap, iObjMax) < Vec_IntEntry(&p->vMap, iObj)) )
             iObjMax = iObj;
#else
    Cbs3_QueForEachEntry( p->pJust, iObj, i )
//       if ( iObjMax == 0 || iObjMax < iObj )
       if ( iObjMax == 0 || Vec_IntEntry(&p->vMap, iObjMax) < Vec_IntEntry(&p->vMap, iObj) )
            iObjMax = iObj;
#endif
    return iObjMax;
}


/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline void Cbs3_ManCancelUntil( Cbs3_Man_t * p, int iBound )
{
    int i, iLit;
    assert( iBound <= p->pProp.iTail );
    p->pProp.iHead = iBound;
    Cbs3_QueForEachEntry( p->pProp, iLit, i )
        Cbs3_VarUnassign( p, Abc_Lit2Var(iLit) );
    p->pProp.iTail = iBound;
}

/**Function*************************************************************

  Synopsis    [Assigns the variables a value.]

  Description [Returns 1 if conflict; 0 if no conflict.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline void Cbs3_ManAssign( Cbs3_Man_t * p, int iLit, int Level, int iRes0, int iRes1 )
{
    int iObj = Abc_Lit2Var(iLit);
    assert( Cbs3_VarUnused(p, iObj) );
    assert( !Cbs3_VarIsAssigned(p, iObj) );
    Cbs3_VarSetValue( p, iObj, !Abc_LitIsCompl(iLit) );
    Cbs3_QuePush( &p->pProp, iLit );
    Vec_IntWriteEntry( &p->vLevReason, 3*iObj,   Level );
    Vec_IntWriteEntry( &p->vLevReason, 3*iObj+1, iRes0 );
    Vec_IntWriteEntry( &p->vLevReason, 3*iObj+2, iRes1 );
}




/**Function*************************************************************

  Synopsis    [Prints conflict clause.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline void Cbs3_ManPrintClause( Cbs3_Man_t * p, int Level, int hClause )
{
    int i, iLit;
    assert( Cbs3_QueIsEmpty( &p->pClauses ) );
    printf( "Level %2d : ", Level );
    Cbs3_ClauseForEachEntry( p, hClause, iLit, i )
        printf( "%c%d ", Abc_LitIsCompl(iLit) ? '-':'+', Abc_Lit2Var(iLit) );
//        printf( "%d=%d(%d) ", iObj, Cbs3_VarValue(p, Abc_Lit2Var(iLit)), Cbs3_VarDecLevel(p, Abc_Lit2Var(iLit)) );
    printf( "\n" );
}
static inline void Cbs3_ManPrintCube( Cbs3_Man_t * p, int Level, int hClause )
{
    int i, iObj;
    assert( Cbs3_QueIsEmpty( &p->pClauses ) );
    printf( "Level %2d : ", Level );
    Cbs3_ClauseForEachEntry( p, hClause, iObj, i )
        printf( "%c%d ", Cbs3_VarValue(p, iObj)? '+':'-', iObj );
    printf( "\n" );
}

/**Function*************************************************************

  Synopsis    [Finalized the clause.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline void Cbs3_ManCleanWatch( Cbs3_Man_t * p )
{
    int i, iLit;
    Vec_IntForEachEntry( &p->vWatchUpds, iLit, i )
        Vec_IntWriteEntry( &p->vWatches, iLit, 0 );
    Vec_IntClear( &p->vWatchUpds );
    //Vec_IntForEachEntry( &p->vWatches, iLit, i )
    //    assert( iLit == 0 );
}
static inline void Cbs3_ManWatchClause( Cbs3_Man_t * p, int hClause, int Lit )
{
    int * pLits = Cbs3_ClauseLits( p, hClause );
    int * pPlace = Vec_IntEntryP( &p->vWatches, Abc_LitNot(Lit) );
    if ( *pPlace == 0 )
        Vec_IntPush( &p->vWatchUpds, Abc_LitNot(Lit) );
/*
    if ( pClause->pLits[0] == Lit )
        pClause->pNext0 = p->pWatches[lit_neg(Lit)];  
    else
    {
        assert( pClause->pLits[1] == Lit );
        pClause->pNext1 = p->pWatches[lit_neg(Lit)];  
    }
    p->pWatches[lit_neg(Lit)] = pClause;
*/
    assert( Lit == pLits[0] || Lit == pLits[1] );
    Cbs3_ClauseSetNext( p, hClause, Lit == pLits[1], *pPlace );
    *pPlace = hClause;
}
static inline int Cbs3_QueFinish( Cbs3_Man_t * p, int Level )
{
    Cbs3_Que_t * pQue = &(p->pClauses); 
    int i, iObj, hClauseC, hClause = pQue->iHead, Size = pQue->iTail - pQue->iHead - 1;
    assert( pQue->iHead+1 < pQue->iTail );
    Cbs3_ClauseSetSize( p, pQue->iHead, Size );
    hClauseC = pQue->iHead = pQue->iTail;
    //printf( "Adding cube: " ); Cbs3_ManPrintCube(p, Level, hClause);
    if ( Size == 1 )
        return hClause;
    // create watched clause
    pQue->iHead = hClause;
    Cbs3_QueForEachEntry( p->pClauses, iObj, i )
    {
        if ( i == hClauseC )
            break;
        else if ( i == hClause ) // nlits
            Cbs3_QuePush( pQue, iObj );
        else // literals
            Cbs3_QuePush( pQue, Abc_Var2Lit(iObj, Cbs3_VarValue(p, iObj)) ); // complement
    }
    Cbs3_QuePush( pQue, 0 ); // next0
    Cbs3_QuePush( pQue, 0 ); // next1
    pQue->iHead = pQue->iTail;
    Cbs3_ManWatchClause( p, hClauseC, Cbs3_ClauseLit(p, hClauseC, 0) );
    Cbs3_ManWatchClause( p, hClauseC, Cbs3_ClauseLit(p, hClauseC, 1) );
    //printf( "Adding clause %d: ", hClauseC ); Cbs3_ManPrintClause(p, Level, hClauseC);
    Cbs3_ActDecay( p );
    return hClause;
}

/**Function*************************************************************

  Synopsis    [Returns conflict clause.]

  Description [Performs conflict analysis.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Cbs3_ManDeriveReason( Cbs3_Man_t * p, int Level )
{
    Cbs3_Que_t * pQue = &(p->pClauses);
    int i, k, iObj, iLitLevel, * pReason;
    assert( pQue->pData[pQue->iHead] == 0 );
    assert( pQue->pData[pQue->iHead+1] == 0 );
    assert( pQue->iHead + 2 < pQue->iTail );
    //for ( i = pQue->iHead + 2; i < pQue->iTail; i++ )
    //    assert( !Cbs3_VarMark0(p, pQue->pData[i]) );
    // compact literals
    Vec_IntClear( p->vTemp );
    for ( i = k = pQue->iHead + 2; i < pQue->iTail; i++ )
    {
        iObj = pQue->pData[i];
        if ( Cbs3_VarMark0(p, iObj) ) // unassigned - seen again
            continue;
        //if ( Vec_IntEntry(&p->vActivity, iObj) == 0 )
        //    Vec_IntPush( &p->vActStore, iObj );
        //Vec_IntAddToEntry( &p->vActivity, iObj, 1 );
        // assigned - seen first time
        Cbs3_VarSetMark0(p, iObj, 1);
        Cbs3_ActBumpVar(p, iObj);
        Vec_IntPush( p->vTemp, iObj );
        // check decision level
        iLitLevel = Cbs3_VarDecLevel( p, iObj );
        if ( iLitLevel < Level )
        {
            pQue->pData[k++] = iObj;
            continue;
        }
        assert( iLitLevel == Level );
        pReason = Cbs3_VarReasonP( p, iObj );
        if ( pReason[0] == 0 && pReason[1] == 0 ) // no reason
        {
            assert( pQue->pData[pQue->iHead+1] == 0 );
            pQue->pData[pQue->iHead+1] = iObj;
        }
        else if ( pReason[0] != 0 ) // circuit reason
        {
            Cbs3_QuePush( pQue, pReason[0] );
            if ( pReason[1] )
            Cbs3_QuePush( pQue, pReason[1] );
        }
        else // clause reason
        {
            int i, * pLits, nLits = Cbs3_ClauseSize( p, pReason[1] );
            assert( pReason[1] );
            Cbs3_QueGrow( pQue, nLits );
            pLits = Cbs3_ClauseLits( p, pReason[1] );
            assert( iObj == Abc_Lit2Var(pLits[0]) );
            for ( i = 1; i < nLits; i++ )
                Cbs3_QuePush( pQue, Abc_Lit2Var(pLits[i]) );
        }
    }
    assert( pQue->pData[pQue->iHead] == 0 );
    assert( pQue->pData[pQue->iHead+1] != 0 );
    pQue->iTail = k;
    // clear the marks
    Vec_IntForEachEntry( p->vTemp, iObj, i )
        Cbs3_VarSetMark0(p, iObj, 0);
    return Cbs3_QueFinish( p, Level );
}
static inline int Cbs3_ManAnalyze( Cbs3_Man_t * p, int Level, int iVar, int iFan0, int iFan1 )
{
    Cbs3_Que_t * pQue = &(p->pClauses); 
    assert( Cbs3_VarIsAssigned(p, iVar) );
    assert( Cbs3_QueIsEmpty( pQue ) );
    Cbs3_QuePush( pQue, 0 );
    Cbs3_QuePush( pQue, 0 );
    if ( iFan0 ) // circuit conflict
    {
        assert( Cbs3_VarIsAssigned(p, iFan0) );
        assert( iFan1 == 0 || Cbs3_VarIsAssigned(p, iFan1) );
        Cbs3_QuePush( pQue, iVar );
        Cbs3_QuePush( pQue, iFan0 );
        if ( iFan1 )
        Cbs3_QuePush( pQue, iFan1 );
    }
    else // clause conflict
    {
        int i, * pLits, nLits = Cbs3_ClauseSize( p, iFan1 );
        assert( iFan1 );
        Cbs3_QueGrow( pQue, nLits );
        pLits = Cbs3_ClauseLits( p, iFan1 );
        assert( iVar == Abc_Lit2Var(pLits[0]) );
        assert( Cbs3_VarValue(p, iVar) == Abc_LitIsCompl(pLits[0]) );
        for ( i = 0; i < nLits; i++ )
            Cbs3_QuePush( pQue, Abc_Lit2Var(pLits[i]) );
    }
    return Cbs3_ManDeriveReason( p, Level );
}


/**Function*************************************************************

  Synopsis    [Propagate one assignment.]

  Description [Returns handle of the conflict clause, if conflict occurs.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Cbs3_ManPropagateClauses( Cbs3_Man_t * p, int Level, int Lit )
{
    int i, Value, Cur, LitF = Abc_LitNot(Lit);
    int * pPrev = Vec_IntEntryP( &p->vWatches, Lit );
    //for ( pCur = p->pWatches[Lit]; pCur; pCur = *ppPrev )
    for ( Cur = *pPrev; Cur; Cur = *pPrev )
    {
        int nLits = Cbs3_ClauseSize( p, Cur );
        int * pLits = Cbs3_ClauseLits( p, Cur );
        p->nPropCalls[1]++;
//printf( "  Watching literal %c%d on level %d.\n", Abc_LitIsCompl(Lit) ? '-':'+', Abc_Lit2Var(Lit), Level );
        // make sure the false literal is in the second literal of the clause
        //if ( pCur->pLits[0] == LitF )
        if ( pLits[0] == LitF )
        {
            //pCur->pLits[0] = pCur->pLits[1];
            pLits[0] = pLits[1];
            //pCur->pLits[1] = LitF;
            pLits[1] = LitF;
            //pTemp = pCur->pNext0;
            //pCur->pNext0 = pCur->pNext1;
            //pCur->pNext1 = pTemp;
            ABC_SWAP( int, pLits[nLits], pLits[nLits+1] );
        }
        //assert( pCur->pLits[1] == LitF );
        assert( pLits[1] == LitF );

        // if the first literal is true, the clause is satisfied
        //if ( pCur->pLits[0] == p->pAssigns[lit_var(pCur->pLits[0])] )
        if ( Cbs3_VarValue(p, Abc_Lit2Var(pLits[0])) == !Abc_LitIsCompl(pLits[0]) )
        {
            //ppPrev = &pCur->pNext1;
            pPrev = Cbs3_ClauseNext1p(p, Cur);
            continue;
        }

        // look for a new literal to watch
        for ( i = 2; i < nLits; i++ )
        {
            // skip the case when the literal is false
            //if ( lit_neg(pCur->pLits[i]) == p->pAssigns[lit_var(pCur->pLits[i])] )
            if ( Cbs3_VarValue(p, Abc_Lit2Var(pLits[i])) == Abc_LitIsCompl(pLits[i]) )
                continue;
            // the literal is either true or unassigned - watch it
            //pCur->pLits[1] = pCur->pLits[i];
            //pCur->pLits[i] = LitF;
            pLits[1] = pLits[i];
            pLits[i] = LitF;
            // remove this clause from the watch list of Lit
            //*ppPrev = pCur->pNext1;
            *pPrev = *Cbs3_ClauseNext1p(p, Cur);
            // add this clause to the watch list of pCur->pLits[i] (now it is pCur->pLits[1])
            //Intb_ManWatchClause( p, pCur, pCur->pLits[1] );
            Cbs3_ManWatchClause( p, Cur, Cbs3_ClauseLit(p, Cur, 1) );
            break;
        }
        if ( i < nLits ) // found new watch
            continue;

        // clause is unit - enqueue new implication
        //if ( Inta_ManEnqueue(p, pCur->pLits[0], pCur) )
        //{
        //    ppPrev = &pCur->pNext1;
        //    continue;
        //}

        // clause is unit - enqueue new implication
        Value = Cbs3_VarValue(p, Abc_Lit2Var(pLits[0]));
        if ( Value >= 2 ) // unassigned
        {
            Cbs3_ManAssign( p, pLits[0], Level, 0, Cur );
            pPrev = Cbs3_ClauseNext1p(p, Cur);
            continue;
        }

        // conflict detected - return the conflict clause
        //return pCur;
        if ( Value == Abc_LitIsCompl(pLits[0]) )
        {
            p->nClauseConf++;
            return Cbs3_ManAnalyze( p, Level, Abc_Lit2Var(pLits[0]), 0, Cur );
        }
    }
    return 0;
}


/**Function*************************************************************

  Synopsis    [Performs resolution of two clauses.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Cbs3_ManResolve( Cbs3_Man_t * p, int Level, int hClause0, int hClause1 )
{
    Cbs3_Que_t * pQue = &(p->pClauses);
    int i, iObj, LevelMax = -1, LevelCur;
    assert( pQue->pData[hClause0+1] != 0 );
    assert( pQue->pData[hClause0+1] == pQue->pData[hClause1+1] );
    //Cbs3_ClauseForEachEntry1( p, hClause0, iObj, i )
    //    assert( !Cbs3_VarMark0(p, iObj) );
    //Cbs3_ClauseForEachEntry1( p, hClause1, iObj, i )
    //    assert( !Cbs3_VarMark0(p, iObj) );
    assert( Cbs3_QueIsEmpty( pQue ) );
    Cbs3_QuePush( pQue, 0 );
    Cbs3_QuePush( pQue, 0 );
//    for ( i = hClause0 + 1; (iObj = pQue->pData[i]); i++ )
    Cbs3_ClauseForEachEntry1( p, hClause0, iObj, i )
    {
        if ( Cbs3_VarMark0(p, iObj) ) // unassigned - seen again
            continue;
        //if ( Vec_IntEntry(&p->vActivity, iObj) == 0 )
        //    Vec_IntPush( &p->vActStore, iObj );
        //Vec_IntAddToEntry( &p->vActivity, iObj, 1 );
        // assigned - seen first time
        Cbs3_VarSetMark0(p, iObj, 1);
        Cbs3_ActBumpVar(p, iObj);
        Cbs3_QuePush( pQue, iObj );
        LevelCur = Cbs3_VarDecLevel( p, iObj );
        if ( LevelMax < LevelCur )
            LevelMax = LevelCur;
    }
//    for ( i = hClause1 + 1; (iObj = pQue->pData[i]); i++ )
    Cbs3_ClauseForEachEntry1( p, hClause1, iObj, i )
    {
        if ( Cbs3_VarMark0(p, iObj) ) // unassigned - seen again
            continue;
        //if ( Vec_IntEntry(&p->vActivity, iObj) == 0 )
        //    Vec_IntPush( &p->vActStore, iObj );
        //Vec_IntAddToEntry( &p->vActivity, iObj, 1 );
        // assigned - seen first time
        Cbs3_VarSetMark0(p, iObj, 1);
        Cbs3_ActBumpVar(p, iObj);
        Cbs3_QuePush( pQue, iObj );
        LevelCur = Cbs3_VarDecLevel( p, iObj );
        if ( LevelMax < LevelCur )
            LevelMax = LevelCur;
    }
    for ( i = pQue->iHead + 2; i < pQue->iTail; i++ )
        Cbs3_VarSetMark0(p, pQue->pData[i], 0);
    return Cbs3_ManDeriveReason( p, LevelMax );
}

/**Function*************************************************************

  Synopsis    [Propagates a variable.]

  Description [Returns clause handle if conflict; 0 if no conflict.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cbs3_ManUpdateJFrontier( Cbs3_Man_t * p )
{
    //abctime clk = Abc_Clock();
    int iVar, iLit, i, k = p->pJust.iTail;
    Cbs3_QueGrow( &p->pJust, Cbs3_QueSize(&p->pJust) + Cbs3_QueSize(&p->pProp) );
    Cbs3_QueForEachEntry( p->pJust, iVar, i )
        if ( Cbs3_VarIsJust(p, iVar) )
            p->pJust.pData[k++] = iVar;
    Cbs3_QueForEachEntry( p->pProp, iLit, i )
        if ( Cbs3_VarIsJust(p, Abc_Lit2Var(iLit)) )
            p->pJust.pData[k++] = Abc_Lit2Var(iLit);
    p->pJust.iHead = p->pJust.iTail;
    p->pJust.iTail = k;
    //p->timeJFront += Abc_Clock() - clk;
}
int Cbs3_ManPropagateNew( Cbs3_Man_t * p, int Level )
{
    int i, k, iLit, hClause, nLits, * pLits;
    p->nPropCalls[0]++;
    Cbs3_QueForEachEntry( p->pProp, iLit, i )
    {
        if ( (hClause = Cbs3_ManPropagateClauses(p, Level, iLit)) )
            return hClause;
        p->nPropCalls[2]++;
        nLits = Vec_IntSize(Vec_WecEntry(&p->vImps, iLit));
        pLits = Vec_IntArray(Vec_WecEntry(&p->vImps, iLit)); 
        for ( k = 0; k < nLits; k += 2 )
        {
            int Value0 = Cbs3_VarValue(p, Abc_Lit2Var(pLits[k]));
            int Value1 = pLits[k+1] ? Cbs3_VarValue(p, Abc_Lit2Var(pLits[k+1])) : -1;
            if ( Value1 == -1 || Value1 == Abc_LitIsCompl(pLits[k+1]) ) // pLits[k+1] is false
            {
                if ( Value0 >= 2 ) // pLits[k] is unassigned
                    Cbs3_ManAssign( p, pLits[k], Level, Abc_Lit2Var(iLit), Abc_Lit2Var(pLits[k+1]) );
                else if ( Value0 == Abc_LitIsCompl(pLits[k]) ) // pLits[k] is false
                    return Cbs3_ManAnalyze( p, Level, Abc_Lit2Var(iLit), Abc_Lit2Var(pLits[k]), Abc_Lit2Var(pLits[k+1]) );
            }
            if ( Value1 != -1 && Value0 == Abc_LitIsCompl(pLits[k]) ) // pLits[k] is false
            {
                if ( Value1 >= 2 ) // pLits[k+1] is unassigned
                    Cbs3_ManAssign( p, pLits[k+1], Level, Abc_Lit2Var(iLit), Abc_Lit2Var(pLits[k]) );
                else if ( Value1 == Abc_LitIsCompl(pLits[k+1]) ) // pLits[k+1] is false
                    return Cbs3_ManAnalyze( p, Level, Abc_Lit2Var(iLit), Abc_Lit2Var(pLits[k]), Abc_Lit2Var(pLits[k+1]) );
            }
        }
    }
    Cbs3_ManUpdateJFrontier( p );
    // finalize propagation queue
    p->pProp.iHead = p->pProp.iTail;
    return 0;
}

/**Function*************************************************************

  Synopsis    [Solve the problem recursively.]

  Description [Returns learnt clause if unsat, NULL if sat or undecided.]
               
  SideEffects []

  SeeAlso     []
 
***********************************************************************/
int Cbs3_ManSolve2_rec( Cbs3_Man_t * p, int Level )
{ 
    Cbs3_Que_t * pQue = &(p->pClauses);
    int iPropHead, iJustHead, iJustTail;
    int hClause, hLearn0, hLearn1, iVar, iDecLit;
    int nRef0, nRef1;
    // propagate assignments
    assert( !Cbs3_QueIsEmpty(&p->pProp) );
    //if ( (hClause = Cbs3_ManPropagate( p, Level )) )
    if ( (hClause = Cbs3_ManPropagateNew( p, Level )) )
        return hClause;
    // check for satisfying assignment
    assert( Cbs3_QueIsEmpty(&p->pProp) );
    if ( Cbs3_QueIsEmpty(&p->pJust) )
        return 0;
    // quit using resource limits
    p->Pars.nJustThis = Abc_MaxInt( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead );
    if ( Cbs3_ManCheckLimits( p ) )
        return 0;
    // remember the state before branching
    iPropHead = p->pProp.iHead;
    iJustHead = p->pJust.iHead;
    iJustTail = p->pJust.iTail;
    // find the decision variable
    p->nDecs++;
    iVar = Cbs3_ManDecide( p );
    assert( !Cbs3_VarIsPi(p, iVar) );
    assert( Cbs3_VarIsJust(p, iVar) );
    // chose decision variable using fanout count
    nRef0 = Vec_IntEntry(&p->vRef, Abc_Lit2Var(Cbs3_VarLit0(p, iVar)));
    nRef1 = Vec_IntEntry(&p->vRef, Abc_Lit2Var(Cbs3_VarLit1(p, iVar)));
//    if ( nRef0 >= nRef1 || (nRef0 == nRef1) && (Abc_Random(0) & 1) )
    if ( nRef0 >= nRef1 )
        iDecLit = Abc_LitNot(Cbs3_VarLit0(p, iVar));
    else
        iDecLit = Abc_LitNot(Cbs3_VarLit1(p, iVar));
    // decide on first fanin
    Cbs3_ManAssign( p, iDecLit, Level+1, 0, 0 );
    if ( !(hLearn0 = Cbs3_ManSolve2_rec( p, Level+1 )) )
        return 0;
    if ( pQue->pData[hLearn0+1] != Abc_Lit2Var(iDecLit) )
        return hLearn0;
    Cbs3_ManCancelUntil( p, iPropHead );
    Cbs3_QueRestore( &p->pJust, iJustHead, iJustTail );
    // decide on second fanin
    Cbs3_ManAssign( p, Abc_LitNot(iDecLit), Level+1, 0, 0 );
    if ( !(hLearn1 = Cbs3_ManSolve2_rec( p, Level+1 )) )
        return 0;
    if ( pQue->pData[hLearn1+1] != Abc_Lit2Var(iDecLit) )
        return hLearn1;
    hClause = Cbs3_ManResolve( p, Level, hLearn0, hLearn1 );
    p->Pars.nBTThis++;
    return hClause;
}

/**Function*************************************************************

  Synopsis    [Looking for a satisfying assignment of the node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Cbs3_ManSolveInt( Cbs3_Man_t * p, int iLit )
{
    int RetValue = 0;
    assert( !p->pProp.iHead && !p->pProp.iTail );
    assert( !p->pJust.iHead && !p->pJust.iTail );
    p->Pars.nBTThis = p->Pars.nJustThis = 0;
    Cbs3_ManAssign( p, iLit, 0, 0, 0 );
    if ( !Cbs3_ManSolve2_rec(p, 0) && !Cbs3_ManCheckLimits(p) )
        Cbs3_ManSaveModel( p, p->vModel );
    else
        RetValue = 1;
    Cbs3_ManCancelUntil( p, 0 );
    p->pJust.iHead = p->pJust.iTail = 0;
    p->Pars.nBTTotal += p->Pars.nBTThis;
    p->Pars.nJustTotal = Abc_MaxInt( p->Pars.nJustTotal, p->Pars.nJustThis );
    if ( Cbs3_ManCheckLimits( p ) )
        RetValue = -1;
    return RetValue;
}
int Cbs3_ManSolve( Cbs3_Man_t * p, int iLit, int nRestarts )
{
    int i, RetValue = -1;
    assert( p->pClauses.iHead == 1 && p->pClauses.iTail == 1 );
    for ( i = 0; i < nRestarts; i++ )
        if ( (RetValue = Cbs3_ManSolveInt(p, iLit)) != -1 )
            break;
    Cbs3_ManCleanWatch( p );
    p->pClauses.iHead = p->pClauses.iTail = 1;
    return RetValue;
}

/**Function*************************************************************

  Synopsis    [Prints statistics of the manager.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cbs3_ManSatPrintStats( Cbs3_Man_t * p )
{
    printf( "CO = %8d  ", Gia_ManCoNum(p->pAig) );
    printf( "AND = %8d  ", Gia_ManAndNum(p->pAig) );
    printf( "Conf = %6d  ", p->Pars.nBTLimit );
    printf( "Restart = %2d  ", p->Pars.nRestLimit );
    printf( "JustMax = %5d  ", p->Pars.nJustLimit );
    printf( "\n" );
    printf( "Unsat calls %6d  (%6.2f %%)   Ave conf = %8.1f   ", 
        p->nSatUnsat, p->nSatTotal? 100.0*p->nSatUnsat/p->nSatTotal :0.0, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 );
    ABC_PRTP( "Time", p->timeSatUnsat, p->timeTotal );
    printf( "Sat   calls %6d  (%6.2f %%)   Ave conf = %8.1f   ", 
        p->nSatSat,   p->nSatTotal? 100.0*p->nSatSat/p->nSatTotal :0.0, p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 );
    ABC_PRTP( "Time", p->timeSatSat,   p->timeTotal );
    printf( "Undef calls %6d  (%6.2f %%)   Ave conf = %8.1f   ", 
        p->nSatUndec, p->nSatTotal? 100.0*p->nSatUndec/p->nSatTotal :0.0, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 );
    ABC_PRTP( "Time", p->timeSatUndec, p->timeTotal );
    ABC_PRT( "Total time", p->timeTotal );
}


/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Cbs3_ManAddVar( Cbs3_Man_t * p, int iGiaObj )
{
    assert( Vec_IntSize(&p->vMap) == p->nVars );
    Vec_IntPush( &p->vMap, iGiaObj );
    Vec_IntPush( &p->vRef, Gia_ObjRefNumId(p->pAig, iGiaObj) );
    Vec_IntPushTwo( &p->vFans, 0, 0 );
    Vec_WecPushLevel(&p->vImps);
    Vec_WecPushLevel(&p->vImps);
    return Abc_Var2Lit( p->nVars++, 0 );
}
static inline void Cbs3_ManAddConstr( Cbs3_Man_t * p, int x, int x0, int x1 )
{
    Vec_WecPushTwo( &p->vImps,   x ,   x0,   0  ); // ~x +  x0
    Vec_WecPushTwo( &p->vImps,   x ,   x1,   0  ); // ~x +  x1
    Vec_WecPushTwo( &p->vImps, 1^x0, 1^x ,   0  ); // ~x +  x0
    Vec_WecPushTwo( &p->vImps, 1^x1, 1^x ,   0  ); // ~x +  x1
    Vec_WecPushTwo( &p->vImps, 1^x , 1^x0, 1^x1 ); //  x + ~x0 + ~x1
    Vec_WecPushTwo( &p->vImps,   x0,   x , 1^x1 ); //  x + ~x0 + ~x1
    Vec_WecPushTwo( &p->vImps,   x1,   x , 1^x0 ); //  x + ~x0 + ~x1
}
static inline void Cbs3_ManAddAnd( Cbs3_Man_t * p, int x, int x0, int x1 )
{
    assert( x > 0 && x0 > 0 && x1 > 0 );
    Vec_IntWriteEntry( &p->vFans, x,   x0 );
    Vec_IntWriteEntry( &p->vFans, x+1, x1 );
    Cbs3_ManAddConstr( p, x, x0, x1 );
}
static inline int Cbs3_ManToSolver1_rec( Cbs3_Man_t * pSol, Gia_Man_t * p, int iObj, int Depth )
{
    Gia_Obj_t * pObj = Gia_ManObj(p, iObj); int Lit0, Lit1;
    if ( Gia_ObjUpdateTravIdCurrentId(p, iObj) )
        return pObj->Value;
    pObj->Value = Cbs3_ManAddVar( pSol, iObj );
    if ( Gia_ObjIsCi(pObj) || Depth == 0 )
        return pObj->Value;
    assert( Gia_ObjIsAnd(pObj) );
    Lit0 = Cbs3_ManToSolver1_rec( pSol, p, Gia_ObjFaninId0(pObj, iObj), Depth - Gia_ObjFaninC0(pObj) );
    Lit1 = Cbs3_ManToSolver1_rec( pSol, p, Gia_ObjFaninId1(pObj, iObj), Depth - Gia_ObjFaninC1(pObj) );
    Cbs3_ManAddAnd( pSol, pObj->Value, Lit0 ^ Gia_ObjFaninC0(pObj), Lit1 ^ Gia_ObjFaninC1(pObj) );
    return pObj->Value;
}
static inline int Cbs3_ManToSolver1( Cbs3_Man_t * pSol, Gia_Man_t * p, Gia_Obj_t * pRoot, int nRestarts, int Depth )
{
    //abctime clk = Abc_Clock();
    assert( Gia_ObjIsCo(pRoot) );
    Cbs3_ManReset( pSol );
    Gia_ManIncrementTravId( p );
    Cbs3_ManToSolver1_rec( pSol, p, Gia_ObjFaninId0p(p, pRoot), Depth );
    Cbs3_ManGrow( pSol );
    Cbs3_ActReset( pSol );
    //pSol->timeSatLoad += Abc_Clock() - clk;
    return Cbs3_ManSolve( pSol, Gia_ObjFanin0Copy(pRoot), nRestarts );
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline void Cbs3_ManPrepare( Cbs3_Man_t * p )
{
    int x, x0, x1;
    Vec_WecInit( &p->vImps, Abc_Var2Lit(p->nVars, 0) );
    Vec_IntForEachEntryDoubleStart( &p->vFans, x0, x1, x, 2 )
        if ( x0 ) Cbs3_ManAddConstr( p, x, x0, x1 );
}
static inline int Cbs3_ManAddNode( Cbs3_Man_t * p, int iGiaObj, int iLit0, int iLit1 )
{
    assert( Vec_IntSize(&p->vMap) == p->nVars );
    Vec_IntPush( &p->vMap, iGiaObj );
    Vec_IntPush( &p->vRef, Gia_ObjRefNumId(p->pAig, iGiaObj) );
    Vec_IntPushTwo( &p->vFans, iLit0, iLit1 );
    return Abc_Var2Lit( p->nVars++, 0 );
}
static inline int Cbs3_ManToSolver2_rec( Cbs3_Man_t * pSol, Gia_Man_t * p, int iObj, int Depth )
{
    Gia_Obj_t * pObj = Gia_ManObj(p, iObj); int Lit0, Lit1;
    if ( Gia_ObjUpdateTravIdCurrentId(p, iObj) )
        return pObj->Value;
    if ( Gia_ObjIsCi(pObj) || Depth == 0 )
        return pObj->Value = Cbs3_ManAddNode(pSol, iObj, 0, 0);
    assert( Gia_ObjIsAnd(pObj) );
    Lit0 = Cbs3_ManToSolver2_rec( pSol, p, Gia_ObjFaninId0(pObj, iObj), Depth - Gia_ObjFaninC0(pObj) );
    Lit1 = Cbs3_ManToSolver2_rec( pSol, p, Gia_ObjFaninId1(pObj, iObj), Depth - Gia_ObjFaninC1(pObj) );
    return pObj->Value = Cbs3_ManAddNode(pSol, iObj, Lit0 ^ Gia_ObjFaninC0(pObj), Lit1 ^ Gia_ObjFaninC1(pObj));
}
static inline int Cbs3_ManToSolver2( Cbs3_Man_t * pSol, Gia_Man_t * p, Gia_Obj_t * pRoot, int nRestarts, int Depth )
{
    //abctime clk = Abc_Clock();
    assert( Gia_ObjIsCo(pRoot) );
    Cbs3_ManReset( pSol );
    Gia_ManIncrementTravId( p );
    Cbs3_ManToSolver2_rec( pSol, p, Gia_ObjFaninId0p(p, pRoot), Depth );
    Cbs3_ManGrow( pSol );
    Cbs3_ManPrepare( pSol );
    Cbs3_ActReset( pSol );
    //pSol->timeSatLoad += Abc_Clock() - clk;
    return Cbs3_ManSolve( pSol, Gia_ObjFanin0Copy(pRoot), nRestarts );
}


/**Function*************************************************************

  Synopsis    [Procedure to test the new SAT solver.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Cbs3_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, int nRestarts, Vec_Str_t ** pvStatus, int fVerbose )
{
    extern void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out );
    Cbs3_Man_t * p; 
    Vec_Int_t * vCex, * vVisit, * vCexStore;
    Vec_Str_t * vStatus;
    Gia_Obj_t * pRoot; 
    int i, status; // 1 = unsat, 0 = sat, -1 = undec
    abctime clk, clkTotal = Abc_Clock();
    //assert( Gia_ManRegNum(pAig) == 0 );
    Gia_ManCreateRefs( pAig );
    //Gia_ManLevelNum( pAig );
    // create logic network
    p = Cbs3_ManAlloc( pAig );
    p->Pars.nBTLimit = nConfs;
    p->Pars.nRestLimit = nRestarts;
    // create resulting data-structures
    vStatus   = Vec_StrAlloc( Gia_ManPoNum(pAig) );
    vCexStore = Vec_IntAlloc( 10000 );
    vVisit    = Vec_IntAlloc( 100 );
    vCex      = Cbs3_ReadModel( p );
    // solve for each output
    Gia_ManForEachCo( pAig, pRoot, i )
    {
        if ( Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) )
        {
            Vec_IntClear( vCex );
            Vec_StrPush( vStatus, (char)(!Gia_ObjFaninC0(pRoot)) );
            if ( Gia_ObjFaninC0(pRoot) ) // const1
                Cec_ManSatAddToStore( vCexStore, vCex, i ); // trivial counter-example
            continue;
        }
        clk = Abc_Clock();
        status = Cbs3_ManToSolver2( p, pAig, pRoot, p->Pars.nRestLimit, 10000 );
        Vec_StrPush( vStatus, (char)status );
        if ( status == -1 )
        {
            p->nSatUndec++;
            p->nConfUndec += p->Pars.nBTThis;
            Cec_ManSatAddToStore( vCexStore, NULL, i ); // timeout
            p->timeSatUndec += Abc_Clock() - clk;
            continue;
        }
        if ( status == 1 )
        {
            p->nSatUnsat++;
            p->nConfUnsat += p->Pars.nBTThis;
            p->timeSatUnsat += Abc_Clock() - clk;
            continue;
        }
        p->nSatSat++;
        p->nConfSat += p->Pars.nBTThis;
        //Gia_SatVerifyPattern( pAig, pRoot, vCex, vVisit );
        Cec_ManSatAddToStore( vCexStore, vCex, i );
        p->timeSatSat += Abc_Clock() - clk;
    }
    Vec_IntFree( vVisit );
    p->nSatTotal = Gia_ManPoNum(pAig);
    p->timeTotal = Abc_Clock() - clkTotal;
    if ( fVerbose )
        Cbs3_ManSatPrintStats( p );
    if ( fVerbose )
    {
        printf( "Prop1 = %d.  Prop2 = %d.  Prop3 = %d.  ClaConf = %d.   FailJ = %d.  FailC = %d.   ", p->nPropCalls[0], p->nPropCalls[1], p->nPropCalls[2], p->nClauseConf, p->nFails[0], p->nFails[1] );
        printf( "Mem usage %.2f MB.\n", 1.0*Cbs3_ManMemory(p)/(1<<20) );
        //Abc_PrintTime( 1, "JFront", p->timeJFront );
        //Abc_PrintTime( 1, "Loading", p->timeSatLoad );
        //printf( "Decisions = %d.\n", p->nDecs );
    }
    Cbs3_ManStop( p );
    *pvStatus = vStatus;
    return vCexStore;
}


////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


ABC_NAMESPACE_IMPL_END