Experiments with SAT solving.

3 files changed, 1388 insertions, 3 deletions

diff --git a/src/aig/gia/giaCSat3.c b/src/aig/gia/giaCSat3.c
new file mode 100644
index 00000000..c34c84ca
--- /dev/null
+++ b/src/aig/gia/giaCSat3.c
@@ -0,0 +1,1365 @@
+/**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
+
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index b767c49a..8cbcaa25 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -14,6 +14,7 @@ SRC +=    src/aig/gia/giaAig.c \
     src/aig/gia/giaCSatOld.c \
     src/aig/gia/giaCSat.c \
     src/aig/gia/giaCSat2.c \
+    src/aig/gia/giaCSat3.c \
     src/aig/gia/giaCTas.c \
     src/aig/gia/giaCut.c \
     src/aig/gia/giaDecs.c \
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index fd7b572c..29732bc6 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -36673,13 +36673,14 @@ usage:
 int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern Vec_Int_t * Cbs2_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
+    extern Vec_Int_t * Cbs3_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, int nRestarts, Vec_Str_t ** pvStatus, int fVerbose );
     Cec_ParSat_t ParsSat, * pPars = &ParsSat;
     Gia_Man_t * pTemp;
     int c;
-    int fNewSolver = 0, fCSat = 0, f0Proved = 0;
+    int fNewSolver = 0, fNewSolver2 = 0, fCSat = 0, f0Proved = 0, nRestarts = 1;
     Cec_ManSatSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "JCSNanmtcxzvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "JCRSNanmtcxyzvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -36705,6 +36706,17 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nBTLimit < 0 )
                 goto usage;
             break;
+        case 'R':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nRestarts = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nRestarts < 0 )
+                goto usage;
+            break;
         case 'S':
             if ( globalUtilOptind >= argc )
             {
@@ -36745,6 +36757,9 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'x':
             fNewSolver ^= 1;
             break;
+        case 'y':
+            fNewSolver2 ^= 1;
+            break;
         case 'z':
             f0Proved ^= 1;
             break;
@@ -36766,6 +36781,8 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
         Vec_Str_t * vStatus;
         if ( fNewSolver )
             vCounters = Cbs2_ManSolveMiterNc( pAbc->pGia, pPars->nBTLimit, &vStatus, pPars->fVerbose );
+        else if ( fNewSolver2 )
+            vCounters = Cbs3_ManSolveMiterNc( pAbc->pGia, pPars->nBTLimit, nRestarts, &vStatus, pPars->fVerbose );
         else if ( pPars->fLearnCls )
             vCounters = Tas_ManSolveMiterNc( pAbc->pGia, pPars->nBTLimit, &vStatus, pPars->fVerbose );
         else if ( pPars->fNonChrono )
@@ -36789,10 +36806,11 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &sat [-JCSN <num>] [-anmctxzvh]\n" );
+    Abc_Print( -2, "usage: &sat [-JCRSN <num>] [-anmctxzvh]\n" );
     Abc_Print( -2, "\t         performs SAT solving for the combinational outputs\n" );
     Abc_Print( -2, "\t-J num : the SAT solver type [default = %d]\n", pPars->SolverType );
     Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
+    Abc_Print( -2, "\t-R num : the max number of restarts at a node [default = %d]\n", nRestarts );
     Abc_Print( -2, "\t-S num : the min number of variables to recycle the solver [default = %d]\n", pPars->nSatVarMax );
     Abc_Print( -2, "\t-N num : the min number of calls to recycle the solver [default = %d]\n", pPars->nCallsRecycle );
     Abc_Print( -2, "\t-a     : toggle solving all outputs and saving counter-examples [default = %s]\n", pPars->fSaveCexes? "yes": "no" );
@@ -36801,6 +36819,7 @@ usage:
     Abc_Print( -2, "\t-c     : toggle using circuit-based SAT solver [default = %s]\n", fCSat? "yes": "no" );
     Abc_Print( -2, "\t-t     : toggle using learning in curcuit-based solver [default = %s]\n", pPars->fLearnCls? "yes": "no" );
     Abc_Print( -2, "\t-x     : toggle using new solver [default = %s]\n", fNewSolver? "yes": "no" );
+    Abc_Print( -2, "\t-y     : toggle using new solver [default = %s]\n", fNewSolver2? "yes": "no" );
     Abc_Print( -2, "\t-z     : toggle replacing proved cones by const0 [default = %s]\n", f0Proved? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");