Version abc90405

author: Alan Mishchenko <alanmi@berkeley.edu> 2009-04-05 08:01:00 -0700
committer: Alan Mishchenko <alanmi@berkeley.edu> 2009-04-05 08:01:00 -0700
commit: e3e2918eb8a4750b9ce51de821ea6b58941fe65c (patch)
tree: d678ac6820fb09638f5196501f94aa4c31c60d97
parent: 23fd11037a006089898cb13494305e402a11ec76 (diff)
download: abc-e3e2918eb8a4750b9ce51de821ea6b58941fe65c.tar.gz
abc-e3e2918eb8a4750b9ce51de821ea6b58941fe65c.tar.bz2
abc-e3e2918eb8a4750b9ce51de821ea6b58941fe65c.zip
23 files changed, 1410 insertions, 418 deletions
diff --git a/abclib.dsp b/abclib.dsp
index e11e9b9e..ffe0a866 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -3695,6 +3695,10 @@ SOURCE=.\src\aig\gia\giaCSat.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\gia\giaCSatOld.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\gia\giaDfs.c
 # End Source File
 # Begin Source File
diff --git a/src/aig/cec/cec.c b/src/aig/cec/cec.c
index a017f831..17b27ec5 100644
--- a/src/aig/cec/cec.c
+++ b/src/aig/cec/cec.c
@@ -4,7 +4,7 @@
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName [Combinatinoal equivalence checking.]
+  PackageName [Combinational equivalence checking.]
 
   Synopsis    []
 
diff --git a/src/aig/cec/cec.h b/src/aig/cec/cec.h
index e26455ba..a965730f 100644
--- a/src/aig/cec/cec.h
+++ b/src/aig/cec/cec.h
@@ -4,7 +4,7 @@
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName [Combinatinoal equivalence checking.]
+  PackageName [Combinational equivalence checking.]
 
   Synopsis    [External declarations.]
 
@@ -44,6 +44,7 @@ struct Cec_ParSat_t_
     int              nBTLimit;      // conflict limit at a node
     int              nSatVarMax;    // the max number of SAT variables
     int              nCallsRecycle; // calls to perform before recycling SAT solver
+    int              fNonChrono;    // use non-chronological backtracling (for circuit SAT only)
     int              fPolarFlip;    // flops polarity of variables
     int              fCheckMiter;   // the circuit is the miter
     int              fFirstStop;    // stop on the first sat output
diff --git a/src/aig/cec/cecCec.c b/src/aig/cec/cecCec.c
index f3d3dea9..82df6008 100644
--- a/src/aig/cec/cecCec.c
+++ b/src/aig/cec/cecCec.c
@@ -4,7 +4,7 @@
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName [Combinatinoal equivalence checking.]
+  PackageName [Combinational equivalence checking.]
 
   Synopsis    [Integrated combinatinal equivalence checker.]
 
diff --git a/src/aig/cec/cecChoice.c b/src/aig/cec/cecChoice.c
index ff30e1bb..2a619e39 100644
--- a/src/aig/cec/cecChoice.c
+++ b/src/aig/cec/cecChoice.c
@@ -4,7 +4,7 @@
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName [Combinatinoal equivalence checking.]
+  PackageName [Combinational equivalence checking.]
 
   Synopsis    [Computation of structural choices.]
 
diff --git a/src/aig/cec/cecClass.c b/src/aig/cec/cecClass.c
index a8ed017a..49930836 100644
--- a/src/aig/cec/cecClass.c
+++ b/src/aig/cec/cecClass.c
@@ -4,9 +4,9 @@
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName [Combinatinoal equivalence checking.]
+  PackageName [Combinational equivalence checking.]
 
-  Synopsis    [Equivalence class representation.]
+  Synopsis    [Equivalence class refinement.]
 
   Author      [Alan Mishchenko]
   
@@ -838,6 +838,8 @@ int Cec_ManSimClassesPrepare( Cec_ManSim_t * p )
     // allocate representation
     p->pAig->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p->pAig) );
     p->pAig->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p->pAig) );
+    // create references
+    Gia_ManSetRefs( p->pAig );
     // set starting representative of internal nodes to be constant 0
     if ( p->pPars->fLatchCorr )
         Gia_ManForEachObj( p->pAig, pObj, i )
@@ -848,9 +850,9 @@ int Cec_ManSimClassesPrepare( Cec_ManSim_t * p )
     // if sequential simulation, set starting representative of ROs to be constant 0
     if ( p->pPars->fSeqSimulate )
         Gia_ManForEachRo( p->pAig, pObj, i )
-            Gia_ObjSetRepr( p->pAig, Gia_ObjId(p->pAig, pObj), 0 );
+            if ( pObj->Value )
+                Gia_ObjSetRepr( p->pAig, Gia_ObjId(p->pAig, pObj), 0 );
     // perform simulation
-    Gia_ManSetRefs( p->pAig );
     p->nWords = 1;
     do {
         if ( p->pPars->fVerbose )
diff --git a/src/aig/cec/cecCore.c b/src/aig/cec/cecCore.c
index d3c54948..7759428e 100644
--- a/src/aig/cec/cecCore.c
+++ b/src/aig/cec/cecCore.c
@@ -4,7 +4,7 @@
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName [Combinatinoal equivalence checking.]
+  PackageName [Combinational equivalence checking.]
 
   Synopsis    [Core procedures.]
 
@@ -42,9 +42,10 @@
 void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p )
 {
     memset( p, 0, sizeof(Cec_ParSat_t) );
-    p->nBTLimit       =      10;  // conflict limit at a node
+    p->nBTLimit       =     100;  // conflict limit at a node
     p->nSatVarMax     =    2000;  // the max number of SAT variables
     p->nCallsRecycle  =     200;  // calls to perform before recycling SAT solver
+    p->fNonChrono     =       0;  // use non-chronological backtracling (for circuit SAT only)
     p->fPolarFlip     =       1;  // flops polarity of variables
     p->fCheckMiter    =       0;  // the circuit is the miter
     p->fFirstStop     =       0;  // stop on the first sat output
@@ -399,7 +400,7 @@ p->timeSat += clock() - clk;
 //        if ( p->nAllFailed && !p->nAllProved && !p->nAllDisproved )
         if ( p->nAllFailed > p->nAllProved + p->nAllDisproved )
         {
-            if ( pParsSat->nBTLimit >= 10000 )
+            if ( pParsSat->nBTLimit >= 10001 )
                 break;
             pParsSat->nBTLimit *= 10;
             if ( p->pPars->fVerbose )
@@ -413,7 +414,7 @@ p->timeSat += clock() - clk;
                 }
             }
         }
-        if ( pPars->fDualOut && pPars->fColorDiff && Gia_ManAndNum(p->pAig) < 100000 )
+        if ( pPars->fDualOut && pPars->fColorDiff && (Gia_ManAndNum(p->pAig) < 100000 || p->nAllProved + p->nAllDisproved < 10) )
         {
             if ( p->pPars->fVerbose )
                 printf( "Switching into reduced mode.\n" );
diff --git a/src/aig/cec/cecCorr.c b/src/aig/cec/cecCorr.c
index abc76416..05259bc7 100644
--- a/src/aig/cec/cecCorr.c
+++ b/src/aig/cec/cecCorr.c
@@ -1,12 +1,12 @@
 /**CFile****************************************************************
 
-  FileName    [cecLcorr.c]
+  FileName    [cecCorr.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName [Combinatinoal equivalence checking.]
+  PackageName [Combinational equivalence checking.]
 
-  Synopsis    [Flop correspondence computation.]
+  Synopsis    [Latch/signal correspondence computation.]
 
   Author      [Alan Mishchenko]
   
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: cecLcorr.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: cecCorr.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
@@ -74,13 +74,10 @@ void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pOb
         return;
     if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
     {
-        if ( !Gia_ObjIsFailedPair(p, Gia_ObjId(p, pRepr), Gia_ObjId(p, pObj)) )
-        {
-            Gia_ManCorrSpecReduce_rec( pNew, p, pRepr, f );
-            iLitNew = Gia_LitNotCond( Gia_ObjCopyF(p, f, pRepr), Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
-            Gia_ObjSetCopyF( p, f, pObj, iLitNew );
-            return;
-        }
+        Gia_ManCorrSpecReduce_rec( pNew, p, pRepr, f );
+        iLitNew = Gia_LitNotCond( Gia_ObjCopyF(p, f, pRepr), Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
+        Gia_ObjSetCopyF( p, f, pObj, iLitNew );
+        return;
     }
     assert( Gia_ObjIsCand(pObj) );
     iLitNew = Gia_ManCorrSpecReal( pNew, p, pObj, f );
@@ -117,10 +114,7 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
         Gia_ObjSetCopyF( p, 0, pObj, Gia_ManAppendCi(pNew) );
     Gia_ManForEachRo( p, pObj, i )
         if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
-        {
-            if ( !Gia_ObjIsFailedPair(p, Gia_ObjId(p, pRepr), Gia_ObjId(p, pObj)) )
-                Gia_ObjSetCopyF( p, 0, pObj, Gia_ObjCopyF(p, 0, pRepr) );
-        }
+            Gia_ObjSetCopyF( p, 0, pObj, Gia_ObjCopyF(p, 0, pRepr) );
     for ( f = 0; f < nFrames+fScorr; f++ )
     { 
         Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 );
@@ -135,8 +129,6 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
         {
             if ( Gia_ObjIsConst( p, i ) )
             {
-                if ( Gia_ObjIsFailedPair(p, 0, i) )
-                    continue;
                 iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames );
                 iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pObj) );
                 if ( iObjNew != 0 )
@@ -151,11 +143,6 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
                 iPrev = i;
                 Gia_ClassForEachObj1( p, i, iObj )
                 {
-                    if ( Gia_ObjIsFailedPair(p, iPrev, iObj) )
-                    {
-                        iPrev = iObj;
-                        continue;
-                    }
                     iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames );
                     iObjNew  = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames );
                     iPrevNew = Gia_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
@@ -169,8 +156,6 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
                     iPrev = iObj;
                 }
                 iObj = i;
-                if ( Gia_ObjIsFailedPair(p, iPrev, iObj) )
-                    continue;
                 iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames );
                 iObjNew  = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames );
                 iPrevNew = Gia_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
@@ -191,8 +176,6 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
             pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
             if ( pRepr == NULL )
                 continue;
-            if ( Gia_ObjIsFailedPair(p, Gia_ObjRepr(p, i), i) )
-                continue;
             iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, nFrames );
             iObjNew  = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames );
             iObjNew  = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
@@ -216,6 +199,38 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
     return pNew;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Initializes simulation info for lcorr/scorr counter-examples.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManStartSimInfo( Vec_Ptr_t * vInfo, int nFlops )
+{
+    unsigned * pInfo;
+    int k, w, nWords;
+    nWords = Vec_PtrReadWordsSimInfo( vInfo );
+    assert( nFlops <= Vec_PtrSize(vInfo) );
+    for ( k = 0; k < nFlops; k++ )
+    {
+        pInfo = Vec_PtrEntry( vInfo, k );
+        for ( w = 0; w < nWords; w++ )
+            pInfo[w] = 0;
+    }
+    for ( k = nFlops; k < Vec_PtrSize(vInfo); k++ )
+    {
+        pInfo = Vec_PtrEntry( vInfo, k );
+        for ( w = 0; w < nWords; w++ )
+            pInfo[w] = Aig_ManRandom( 0 );
+    }
+}
+
 /**Function*************************************************************
 
   Synopsis    [Remaps simulation info from SRM to the original AIG.]
@@ -257,7 +272,7 @@ void Gia_ManCorrRemapSimInfo( Gia_Man_t * p, Vec_Ptr_t * vInfo )
 
 /**Function*************************************************************
 
-  Synopsis    [Remaps simulation info from SRM to the original AIG.]
+  Synopsis    [Collects information about remapping.]
 
   Description []
                
@@ -276,8 +291,8 @@ Vec_Int_t * Gia_ManCorrCreateRemapping( Gia_Man_t * p )
     {
         // skip ROs without representatives
         pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
-//        if ( pRepr == NULL || Gia_ObjIsConst0(pRepr) || Gia_ObjFailed(p, Gia_ObjId(p,pObj)) )
-        if ( pRepr == NULL || Gia_ObjIsConst0(pRepr) || Gia_ObjIsFailedPair(p, Gia_ObjId(p, pRepr), Gia_ObjId(p, pObj)) )
+        if ( pRepr == NULL || Gia_ObjIsConst0(pRepr) || Gia_ObjFailed(p, Gia_ObjId(p,pObj)) )
+//        if ( pRepr == NULL || Gia_ObjIsConst0(pRepr) || Gia_ObjIsFailedPair(p, Gia_ObjId(p, pRepr), Gia_ObjId(p, pObj)) )
             continue;
         assert( Gia_ObjIsRo(p, pRepr) );
 //        printf( "%d -> %d    ", Gia_ObjId(p,pObj), Gia_ObjId(p, pRepr) );
@@ -319,51 +334,7 @@ void Gia_ManCorrPerformRemapping( Vec_Int_t * vPairs, Vec_Ptr_t * vInfo )
 
 /**Function*************************************************************
 
-  Synopsis    [Updates equivalence classes by marking those that timed out.]
-
-  Description [Returns 1 if all ndoes are proved.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Gia_ManCheckRefinements( Gia_Man_t * p, Vec_Str_t * vStatus, Vec_Int_t * vOutputs, Cec_ManSim_t * pSim, int fRings )
-{
-    int i, status, iRepr, iObj;
-    assert( 2 * Vec_StrSize(vStatus) == Vec_IntSize(vOutputs) );
-    Vec_StrForEachEntry( vStatus, status, i )
-    {
-        iRepr = Vec_IntEntry( vOutputs, 2*i );
-        iObj  = Vec_IntEntry( vOutputs, 2*i+1 );
-        if ( status == 1 )
-            continue;
-        if ( status == 0 )
-        {
-//            if ( Gia_ObjHasSameRepr(p, iRepr, iObj) )
-//                printf( "Gia_ManCheckRefinements(): Disproved equivalence (%d,%d) is not refined!\n", iRepr, iObj );
-            if ( Gia_ObjHasSameRepr(p, iRepr, iObj) )
-                Cec_ManSimClassRemoveOne( pSim, iObj );
-            continue;
-        }
-        if ( status == -1 )
-        {
-//            if ( !Gia_ObjFailed( p, iObj ) )
-//                printf( "Gia_ManCheckRefinements(): Failed equivalence is not marked as failed!\n" );
-//            Gia_ObjSetFailed( p, iRepr );
-//            Gia_ObjSetFailed( p, iObj );        
-            if ( fRings )
-            Cec_ManSimClassRemoveOne( pSim, iRepr );
-            Cec_ManSimClassRemoveOne( pSim, iObj );
-            continue;
-        }
-    }
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Marks all the nodes as proved.]
+  Synopsis    [Packs one counter-examples into the array of simulation info.]
 
   Description []
                
@@ -371,67 +342,33 @@ int Gia_ManCheckRefinements( Gia_Man_t * p, Vec_Str_t * vStatus, Vec_Int_t * vOu
 
   SeeAlso     []
 
-***********************************************************************/
-void Gia_ManSetProvedNodes( Gia_Man_t * p )
+*************************************`**********************************/
+int Cec_ManLoadCounterExamplesTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBit, int * pLits, int nLits )
 {
-    Gia_Obj_t * pObj;
-    int i, nLits = 0;
-    Gia_ManForEachObj1( p, pObj, i )
-    {
-        if ( Gia_ObjRepr(p, i) == GIA_VOID )
-            continue;
-        if ( Gia_ObjIsFailedPair( p, Gia_ObjRepr(p, i), i ) )
-            continue;
-        Gia_ObjSetProved( p, i );
-        nLits++;
-    }
-//    printf( "Identified %d proved literals.\n", nLits );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cec_ManLCorrPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int Time )
-{ 
-    int nLits, CounterX = 0, Counter0 = 0, Counter = 0;
-    int i, Entry, nProve = 0, nDispr = 0, nFail = 0;
-    for ( i = 1; i < Gia_ManObjNum(p); i++ )
+    unsigned * pInfo, * pPres;
+    int i;
+    for ( i = 0; i < nLits; i++ )
     {
-        if ( Gia_ObjIsNone(p, i) )
-            CounterX++;
-        else if ( Gia_ObjIsConst(p, i) )
-            Counter0++;
-        else if ( Gia_ObjIsHead(p, i) )
-            Counter++;
+        pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
+        pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
+        if ( Aig_InfoHasBit( pPres, iBit ) && 
+             Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
+             return 0;
     }
-    CounterX -= Gia_ManCoNum(p);
-    nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
-    printf( "%3d : c =%8d  cl =%7d  lit =%8d  ", iIter, Counter0, Counter, nLits );
-    if ( vStatus )
-    Vec_StrForEachEntry( vStatus, Entry, i )
+    for ( i = 0; i < nLits; i++ )
     {
-        if ( Entry == 1 )
-            nProve++;
-        else if ( Entry == 0 )
-            nDispr++;
-        else if ( Entry == -1 )
-            nFail++;
+        pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
+        pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
+        Aig_InfoSetBit( pPres, iBit );
+        if ( Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
+            Aig_InfoXorBit( pInfo, iBit );
     }
-    printf( "p =%6d  d =%6d  f =%6d  ", nProve, nDispr, nFail );
-    ABC_PRT( "T", Time );
+    return 1;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Sets register values from the counter-example.]
+  Synopsis    [Performs bitpacking of counter-examples.]
 
   Description []
                
@@ -440,29 +377,44 @@ void Cec_ManLCorrPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int
   SeeAlso     []
 
 ***********************************************************************/
-void Cec_ManStartSimInfo( Vec_Ptr_t * vInfo, int nFlops )
-{
-    unsigned * pInfo;
-    int k, w, nWords;
-    nWords = Vec_PtrReadWordsSimInfo( vInfo );
-    assert( nFlops <= Vec_PtrSize(vInfo) );
-    for ( k = 0; k < nFlops; k++ )
-    {
-        pInfo = Vec_PtrEntry( vInfo, k );
-        for ( w = 0; w < nWords; w++ )
-            pInfo[w] = 0;
-    }
-    for ( k = nFlops; k < Vec_PtrSize(vInfo); k++ )
+int Cec_ManLoadCounterExamples( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iStart )
+{ 
+    Vec_Int_t * vPat;
+    Vec_Ptr_t * vPres;
+    int nWords = Vec_PtrReadWordsSimInfo(vInfo);
+    int nBits = 32 * nWords; 
+    int k, nSize, iBit = 1, kMax = 0;
+    vPat  = Vec_IntAlloc( 100 );
+    vPres = Vec_PtrAllocSimInfo( Vec_PtrSize(vInfo), nWords );
+    Vec_PtrCleanSimInfo( vPres, 0, nWords );
+    while ( iStart < Vec_IntSize(vCexStore) )
     {
-        pInfo = Vec_PtrEntry( vInfo, k );
-        for ( w = 0; w < nWords; w++ )
-            pInfo[w] = Aig_ManRandom( 0 );
+        // skip the output number
+        iStart++;
+        // get the number of items
+        nSize = Vec_IntEntry( vCexStore, iStart++ );
+        if ( nSize <= 0 )
+            continue;
+        // extract pattern
+        Vec_IntClear( vPat );
+        for ( k = 0; k < nSize; k++ )
+            Vec_IntPush( vPat, Vec_IntEntry( vCexStore, iStart++ ) );
+        // add pattern to storage
+        for ( k = 1; k < nBits; k++ )
+            if ( Cec_ManLoadCounterExamplesTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) ) )
+                break;
+        kMax = AIG_MAX( kMax, k );
+        if ( k == nBits-1 )
+            break;
     }
+    Vec_PtrFree( vPres );
+    Vec_IntFree( vPat );
+    return iStart;
 }
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Performs bitpacking of counter-examples.]
 
   Description []
                
@@ -503,7 +455,7 @@ int Cec_ManLoadCounterExamples2( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int i
 
 /**Function*************************************************************
 
-  Synopsis    [Packs patterns into array of simulation info.]
+  Synopsis    [Resimulates counter-examples derived by the SAT solver.]
 
   Description []
                
@@ -511,33 +463,86 @@ int Cec_ManLoadCounterExamples2( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int i
 
   SeeAlso     []
 
-*************************************`**********************************/
-int Cec_ManLoadCounterExamplesTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBit, int * pLits, int nLits )
-{
-    unsigned * pInfo, * pPres;
-    int i;
-    for ( i = 0; i < nLits; i++ )
+***********************************************************************/
+int Cec_ManResimulateCounterExamples( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore, int nFrames )
+{ 
+    Vec_Int_t * vPairs;
+    Vec_Ptr_t * vSimInfo; 
+    int RetValue = 0, iStart = 0;
+    vPairs = Gia_ManCorrCreateRemapping( pSim->pAig );
+    Gia_ManSetRefs( pSim->pAig );
+//    pSim->pPars->nWords  = 63;
+    pSim->pPars->nRounds = nFrames;
+    vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pSim->pAig) + Gia_ManPiNum(pSim->pAig) * nFrames, pSim->pPars->nWords );
+    while ( iStart < Vec_IntSize(vCexStore) )
     {
-        pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
-        pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
-        if ( Aig_InfoHasBit( pPres, iBit ) && 
-             Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
-             return 0;
+        Cec_ManStartSimInfo( vSimInfo, Gia_ManRegNum(pSim->pAig) );
+        iStart = Cec_ManLoadCounterExamples( vSimInfo, vCexStore, iStart );
+//        iStart = Cec_ManLoadCounterExamples2( vSimInfo, vCexStore, iStart );
+//        Gia_ManCorrRemapSimInfo( pSim->pAig, vSimInfo );
+        Gia_ManCorrPerformRemapping( vPairs, vSimInfo );
+        RetValue |= Cec_ManSeqResimulate( pSim, vSimInfo );
+//        Cec_ManSeqResimulateInfo( pSim->pAig, vSimInfo, NULL );
     }
-    for ( i = 0; i < nLits; i++ )
+//Gia_ManEquivPrintOne( pSim->pAig, 85, 0 );
+    assert( iStart == Vec_IntSize(vCexStore) );
+    Vec_PtrFree( vSimInfo );
+    Vec_IntFree( vPairs );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates equivalence classes by marking those that timed out.]
+
+  Description [Returns 1 if all ndoes are proved.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManCheckRefinements( Gia_Man_t * p, Vec_Str_t * vStatus, Vec_Int_t * vOutputs, Cec_ManSim_t * pSim, int fRings )
+{
+    int i, status, iRepr, iObj;
+    int Counter = 0;
+    assert( 2 * Vec_StrSize(vStatus) == Vec_IntSize(vOutputs) );
+    Vec_StrForEachEntry( vStatus, status, i )
     {
-        pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
-        pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
-        Aig_InfoSetBit( pPres, iBit );
-        if ( Aig_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
-            Aig_InfoXorBit( pInfo, iBit );
+        iRepr = Vec_IntEntry( vOutputs, 2*i );
+        iObj  = Vec_IntEntry( vOutputs, 2*i+1 );
+        if ( status == 1 )
+            continue;
+        if ( status == 0 )
+        {
+            if ( Gia_ObjHasSameRepr(p, iRepr, iObj) )
+                Counter++;
+//            if ( Gia_ObjHasSameRepr(p, iRepr, iObj) )
+//                printf( "Gia_ManCheckRefinements(): Disproved equivalence (%d,%d) is not refined!\n", iRepr, iObj );
+//            if ( Gia_ObjHasSameRepr(p, iRepr, iObj) )
+//                Cec_ManSimClassRemoveOne( pSim, iObj );
+            continue;
+        }
+        if ( status == -1 )
+        {
+//            if ( !Gia_ObjFailed( p, iObj ) )
+//                printf( "Gia_ManCheckRefinements(): Failed equivalence is not marked as failed!\n" );
+//            Gia_ObjSetFailed( p, iRepr );
+//            Gia_ObjSetFailed( p, iObj );        
+//            if ( fRings )
+//            Cec_ManSimClassRemoveOne( pSim, iRepr );
+            Cec_ManSimClassRemoveOne( pSim, iObj );
+            continue;
+        }
     }
+//    if ( Counter )
+//    printf( "Gia_ManCheckRefinements(): Could not refine %d nodes.\n", Counter );
     return 1;
 }
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Marks all the nodes as proved.]
 
   Description []
                
@@ -546,54 +551,23 @@ int Cec_ManLoadCounterExamplesTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBi
   SeeAlso     []
 
 ***********************************************************************/
-int Cec_ManLoadCounterExamples( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iStart )
-{ 
-    Vec_Int_t * vPat;
-    Vec_Ptr_t * vPres;
-    int nWords = Vec_PtrReadWordsSimInfo(vInfo);
-    int nBits = 32 * nWords; 
-    int k, nSize, iBit = 1, kMax = 0;
-    vPat  = Vec_IntAlloc( 100 );
-    vPres = Vec_PtrAllocSimInfo( Vec_PtrSize(vInfo), nWords );
-    Vec_PtrCleanSimInfo( vPres, 0, nWords );
-    while ( iStart < Vec_IntSize(vCexStore) )
+void Gia_ManSetProvedNodes( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i, nLits = 0;
+    Gia_ManForEachObj1( p, pObj, i )
     {
-        // skip the output number
-        iStart++;
-        // get the number of items
-        nSize = Vec_IntEntry( vCexStore, iStart++ );
-        if ( nSize <= 0 )
+        if ( Gia_ObjRepr(p, i) == GIA_VOID )
             continue;
-        // extract pattern
-        Vec_IntClear( vPat );
-        for ( k = 0; k < nSize; k++ )
-        {
-            Vec_IntPush( vPat, Vec_IntEntry( vCexStore, iStart++ ) );
-//            printf( "%d(%d) ", Vec_IntEntryLast(vPat)/2, (Vec_IntEntryLast(vPat)&1)==0 );
-        }
-//        printf( "\n" );
-        // add pattern to storage
-        for ( k = 1; k < nBits; k++ )
-            if ( Cec_ManLoadCounterExamplesTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) ) )
-                break;
-//        for ( i = 0; i < 27; i++ )
-//            printf( "%d(%d) ", i, Aig_InfoHasBit(Vec_PtrEntry(vInfo,i), k) );
-//        printf( "\n" );
-
-        kMax = AIG_MAX( kMax, k );
-        if ( k == nBits-1 )
-            break;
+        Gia_ObjSetProved( p, i );
+        nLits++;
     }
-//        printf( "\n" );
-//    printf( "kMax = %d.\n", kMax );
-    Vec_PtrFree( vPres );
-    Vec_IntFree( vPat );
-    return iStart;
+//    printf( "Identified %d proved literals.\n", nLits );
 }
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Prints statistics during solving.]
 
   Description []
                
@@ -602,37 +576,39 @@ int Cec_ManLoadCounterExamples( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iS
   SeeAlso     []
 
 ***********************************************************************/
-int Cec_ManResimulateCounterExamples( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore, int nFrames )
+void Cec_ManLCorrPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int Time )
 { 
-    Vec_Int_t * vPairs;
-    Vec_Ptr_t * vSimInfo; 
-    int RetValue = 0, iStart = 0;
-    vPairs = Gia_ManCorrCreateRemapping( pSim->pAig );
-    Gia_ManSetRefs( pSim->pAig );
-//    pSim->pPars->nWords  = 63;
-    pSim->pPars->nRounds = nFrames;
-    vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pSim->pAig) + Gia_ManPiNum(pSim->pAig) * nFrames, pSim->pPars->nWords );
-    while ( iStart < Vec_IntSize(vCexStore) )
+    int nLits, CounterX = 0, Counter0 = 0, Counter = 0;
+    int i, Entry, nProve = 0, nDispr = 0, nFail = 0;
+    for ( i = 1; i < Gia_ManObjNum(p); i++ )
     {
-//Gia_ManEquivPrintOne( pSim->pAig, 85, 0 );
-        Cec_ManStartSimInfo( vSimInfo, Gia_ManRegNum(pSim->pAig) );
-        iStart = Cec_ManLoadCounterExamples( vSimInfo, vCexStore, iStart );
-//        iStart = Cec_ManLoadCounterExamples2( vSimInfo, vCexStore, iStart );
-//        Gia_ManCorrRemapSimInfo( pSim->pAig, vSimInfo );
-        Gia_ManCorrPerformRemapping( vPairs, vSimInfo );
-        RetValue |= Cec_ManSeqResimulate( pSim, vSimInfo );
-//        Cec_ManSeqResimulateInfo( pSim->pAig, vSimInfo, NULL );
+        if ( Gia_ObjIsNone(p, i) )
+            CounterX++;
+        else if ( Gia_ObjIsConst(p, i) )
+            Counter0++;
+        else if ( Gia_ObjIsHead(p, i) )
+            Counter++;
     }
-//Gia_ManEquivPrintOne( pSim->pAig, 85, 0 );
-    assert( iStart == Vec_IntSize(vCexStore) );
-    Vec_PtrFree( vSimInfo );
-    Vec_IntFree( vPairs );
-    return RetValue;
+    CounterX -= Gia_ManCoNum(p);
+    nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
+    printf( "%3d : c =%8d  cl =%7d  lit =%8d  ", iIter, Counter0, Counter, nLits );
+    if ( vStatus )
+    Vec_StrForEachEntry( vStatus, Entry, i )
+    {
+        if ( Entry == 1 )
+            nProve++;
+        else if ( Entry == 0 )
+            nDispr++;
+        else if ( Entry == -1 )
+            nFail++;
+    }
+    printf( "p =%6d  d =%6d  f =%6d  ", nProve, nDispr, nFail );
+    ABC_PRT( "T", Time );
 }
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Top-level procedure for register correspondence.]
 
   Description []
                
@@ -643,7 +619,7 @@ int Cec_ManResimulateCounterExamples( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore
 ***********************************************************************/
 Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
 {  
-    int nAddFrames = 2; // additional timeframes to simulate
+    int nAddFrames = 1; // additional timeframes to simulate
     Vec_Str_t * vStatus;
     Vec_Int_t * vOutputs;
     Vec_Int_t * vCexStore;
@@ -701,11 +677,10 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
             break;
         }
 //Gia_DumpAiger( pSrm, "corrsrm", r, 2 );
-
         // found counter-examples to speculation
         clk2 = clock();
         if ( pPars->fUseCSat )
-            vCexStore = Cbs_ManSolveMiter( pSrm, pPars->nBTLimit, &vStatus );
+            vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
         else
             vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
         Gia_ManStop( pSrm );
@@ -725,28 +700,36 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
         Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
         if ( pPars->fVerbose )
             Cec_ManLCorrPrintStats( pAig, vStatus, r+1, clock() - clk );
-//Gia_ManEquivPrintClasses( pAig, 1, 0 );
         Vec_StrFree( vStatus );
         Vec_IntFree( vOutputs );
+//Gia_ManEquivPrintClasses( pAig, 1, 0 );
     }
+    if ( r == 100000 )
+        printf( "The refinement was not finished. The result may be incorrect.\n" );
     Cec_ManSimStop( pSim );
     clkTotal = clock() - clkTotal;
     if ( pPars->fVerbose )
         Cec_ManLCorrPrintStats( pAig, NULL, r+1, clock() - clk );
+    // derive reduced AIG
+    Gia_ManSetProvedNodes( pAig );
+    pNew = Gia_ManEquivReduce( pAig, 0, 0, 0 );
+//Gia_WriteAiger( pNew, "reduced.aig", 0, 0 );
+    pNew = Gia_ManSeqCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    // report the results
     if ( pPars->fVerbose )
     {
+        printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%).  RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", 
+            Gia_ManAndNum(pAig), Gia_ManAndNum(pNew), 
+            100.0*(Gia_ManAndNum(pAig)-Gia_ManAndNum(pNew))/(Gia_ManAndNum(pAig)?Gia_ManAndNum(pAig):1), 
+            Gia_ManRegNum(pAig), Gia_ManRegNum(pNew), 
+            100.0*(Gia_ManRegNum(pAig)-Gia_ManRegNum(pNew))/(Gia_ManRegNum(pAig)?Gia_ManRegNum(pAig):1) );
         ABC_PRTP( "Srm  ", clkSrm,                        clkTotal );
         ABC_PRTP( "Sat  ", clkSat,                        clkTotal );
         ABC_PRTP( "Sim  ", clkSim,                        clkTotal );
         ABC_PRTP( "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal );
         ABC_PRT( "TOTAL",  clkTotal );
     }
-    // derive reduced AIG
-    Gia_ManSetProvedNodes( pAig );
-    pNew = Gia_ManEquivReduce( pAig, 0, 0, 0 );
-//Gia_WriteAiger( pNew, "reduced.aig", 0, 0 );
-    pNew = Gia_ManSeqCleanup( pTemp = pNew );
-    Gia_ManStop( pTemp );
     return pNew;
 }
 
diff --git a/src/aig/cec/cecInt.h b/src/aig/cec/cecInt.h
index 86af2614..22bd292b 100644
--- a/src/aig/cec/cecInt.h
+++ b/src/aig/cec/cecInt.h
@@ -4,7 +4,7 @@
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName [Combinatinoal equivalence checking.]
+  PackageName [Combinational equivalence checking.]
 
   Synopsis    [External declarations.]
 
diff --git a/src/aig/cec/cecIso.c b/src/aig/cec/cecIso.c
index 08d4b7ec..ddb539c2 100644
--- a/src/aig/cec/cecIso.c
+++ b/src/aig/cec/cecIso.c
@@ -4,7 +4,7 @@
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName [Combinatinoal equivalence checking.]
+  PackageName [Combinational equivalence checking.]
 
   Synopsis    [Detection of structural isomorphism.]
 
diff --git a/src/aig/cec/cecMan.c b/src/aig/cec/cecMan.c
index 430d961e..eb582e4c 100644
--- a/src/aig/cec/cecMan.c
+++ b/src/aig/cec/cecMan.c
@@ -4,9 +4,9 @@
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName [Combinatinoal equivalence checking.]
+  PackageName [Combinational equivalence checking.]
 
-  Synopsis    [Manager pcocures.]
+  Synopsis    [Manager procedures.]
 
   Author      [Alan Mishchenko]
   
diff --git a/src/aig/cec/cecPat.c b/src/aig/cec/cecPat.c
index dacc5daf..a5be4c1c 100644
--- a/src/aig/cec/cecPat.c
+++ b/src/aig/cec/cecPat.c
@@ -4,7 +4,7 @@
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName [Combinatinoal equivalence checking.]
+  PackageName [Combinational equivalence checking.]
 
   Synopsis    [Simulation pattern manager.]
 
diff --git a/src/aig/cec/cecSeq.c b/src/aig/cec/cecSeq.c
index e69b526e..3d05172f 100644
--- a/src/aig/cec/cecSeq.c
+++ b/src/aig/cec/cecSeq.c
@@ -4,7 +4,7 @@
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName [Combinatinoal equivalence checking.]
+  PackageName [Combinational equivalence checking.]
 
   Synopsis    [Refinement of sequential equivalence classes.]
 
diff --git a/src/aig/cec/cecSim.c b/src/aig/cec/cecSim.c
index dbd3bd5e..61610a46 100644
--- a/src/aig/cec/cecSim.c
+++ b/src/aig/cec/cecSim.c
@@ -4,7 +4,7 @@
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName [Combinatinoal equivalence checking.]
+  PackageName [Combinational equivalence checking.]
 
   Synopsis    [Simulation manager.]
 
diff --git a/src/aig/cec/cecSolve.c b/src/aig/cec/cecSolve.c
index a69d1d2a..fc2d5d7f 100644
--- a/src/aig/cec/cecSolve.c
+++ b/src/aig/cec/cecSolve.c
@@ -4,7 +4,7 @@
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName [Combinatinoal equivalence checking.]
+  PackageName [Combinational equivalence checking.]
 
   Synopsis    [Performs one round of SAT solving.]
 
diff --git a/src/aig/cec/cecSweep.c b/src/aig/cec/cecSweep.c
index 3024ac24..f5e5bd06 100644
--- a/src/aig/cec/cecSweep.c
+++ b/src/aig/cec/cecSweep.c
@@ -1,10 +1,10 @@
 /**CFile****************************************************************
 
-  FileName    [ceFraeep.c]
+  FileName    [cecSweep.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName [Combinatinoal equivalence checking.]
+  PackageName [Combinational equivalence checking.]
 
   Synopsis    [SAT sweeping manager.]
 
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: ceFraeep.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: cecSweep.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 87c85516..5395f361 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -459,8 +459,10 @@ extern Aig_Man_t *         Gia_ManToAig( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ReadAiger( char * pFileName, int fCheck );
 extern void                Gia_WriteAiger( Gia_Man_t * p, char * pFileName, int fWriteSymbols, int fCompact );
 extern void                Gia_DumpAiger( Gia_Man_t * p, char * pFilePrefix, int iFileNum, int nFileNumDigits );
+/*=== giaCsatOld.c ============================================================*/
+extern Vec_Int_t *         Cbs_ManSolveMiter( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
 /*=== giaCsat.c ============================================================*/
-extern Vec_Int_t *         Cbs_ManSolveMiter( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus );
+extern Vec_Int_t *         Cbs_ManSolveMiterNc( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
 /*=== giaCof.c =============================================================*/
 extern void                Gia_ManPrintFanio( Gia_Man_t * pGia, int nNodes );
 extern Gia_Man_t *         Gia_ManDupCof( Gia_Man_t * p, int iVar );
diff --git a/src/aig/gia/giaCSat.c b/src/aig/gia/giaCSat.c
index 5fa9f40f..15faea72 100644
--- a/src/aig/gia/giaCSat.c
+++ b/src/aig/gia/giaCSat.c
@@ -32,6 +32,7 @@ struct Cbs_Par_t_
     int           nJustLimit;   // limit on the size of justification queue
     // current parameters
     int           nBTThis;      // number of conflicts
+    int           nBTThisNc;    // number of conflicts
     int           nJustThis;    // max size of the frontier
     int           nBTTotal;     // total number of conflicts
     int           nJustTotal;   // total size of the frontier
@@ -48,7 +49,7 @@ struct Cbs_Que_t_
 {
     int           iHead;        // beginning of the queue
     int           iTail;        // end of the queue
-   int           nSize;        // allocated size
+    int           nSize;        // allocated size
     Gia_Obj_t **  pData;        // nodes stored in the queue
 };
  
@@ -59,7 +60,11 @@ struct Cbs_Man_t_
     Gia_Man_t *   pAig;         // AIG manager
     Cbs_Que_t     pProp;        // propagation queue
     Cbs_Que_t     pJust;        // justification queue
+    Cbs_Que_t     pClauses;     // clause queue
+    Gia_Obj_t **  pIter;        // iterator through clause vars
+    Vec_Int_t *   vLevReas;     // levels and decisions
     Vec_Int_t *   vModel;       // satisfying assignment
+    Vec_Ptr_t *   vTemp;        // temporary storage
     // SAT calls statistics
     int           nSatUnsat;    // the number of proofs
     int           nSatSat;      // the number of failure
@@ -78,16 +83,26 @@ struct Cbs_Man_t_
 
 static inline int   Cbs_VarIsAssigned( Gia_Obj_t * pVar )      { return pVar->fMark0;                        }
 static inline void  Cbs_VarAssign( Gia_Obj_t * pVar )          { assert(!pVar->fMark0); pVar->fMark0 = 1;    }
-static inline void  Cbs_VarUnassign( Gia_Obj_t * pVar )        { assert(pVar->fMark0);  pVar->fMark0 = 0; pVar->fMark1 = 0;         }
+static inline void  Cbs_VarUnassign( Gia_Obj_t * pVar )        { assert(pVar->fMark0);  pVar->fMark0 = 0; pVar->fMark1 = 0; pVar->Value = ~0; }
 static inline int   Cbs_VarValue( Gia_Obj_t * pVar )           { assert(pVar->fMark0);  return pVar->fMark1; }
 static inline void  Cbs_VarSetValue( Gia_Obj_t * pVar, int v ) { assert(pVar->fMark0);  pVar->fMark1 = v;    }
 static inline int   Cbs_VarIsJust( Gia_Obj_t * pVar )          { return Gia_ObjIsAnd(pVar) && !Cbs_VarIsAssigned(Gia_ObjFanin0(pVar)) && !Cbs_VarIsAssigned(Gia_ObjFanin1(pVar)); } 
 static inline int   Cbs_VarFanin0Value( Gia_Obj_t * pVar )     { return !Cbs_VarIsAssigned(Gia_ObjFanin0(pVar)) ? 2 : (Cbs_VarValue(Gia_ObjFanin0(pVar)) ^ Gia_ObjFaninC0(pVar)); }
 static inline int   Cbs_VarFanin1Value( Gia_Obj_t * pVar )     { return !Cbs_VarIsAssigned(Gia_ObjFanin1(pVar)) ? 2 : (Cbs_VarValue(Gia_ObjFanin1(pVar)) ^ Gia_ObjFaninC1(pVar)); }
 
-#define Cbs_QueForEachEntry( Que, pObj, i )                    \
+static inline int         Cbs_VarDecLevel( Cbs_Man_t * p, Gia_Obj_t * pVar )  { assert( pVar->Value != ~0 ); return Vec_IntEntry(p->vLevReas, 3*pVar->Value);          }
+static inline Gia_Obj_t * Cbs_VarReason0( Cbs_Man_t * p, Gia_Obj_t * pVar )   { assert( pVar->Value != ~0 ); return pVar + Vec_IntEntry(p->vLevReas, 3*pVar->Value+1); }
+static inline Gia_Obj_t * Cbs_VarReason1( Cbs_Man_t * p, Gia_Obj_t * pVar )   { assert( pVar->Value != ~0 ); return pVar + Vec_IntEntry(p->vLevReas, 3*pVar->Value+2); }
+static inline int         Cbs_ClauseDecLevel( Cbs_Man_t * p, int hClause )    { return Cbs_VarDecLevel( p, p->pClauses.pData[hClause] );                               }
+
+#define Cbs_QueForEachEntry( Que, pObj, i )                         \
     for ( i = (Que).iHead; (i < (Que).iTail) && ((pObj) = (Que).pData[i]); i++ )
 
+#define Cbs_ClauseForEachVar( p, hClause, pObj )                    \
+    for ( (p)->pIter = (p)->pClauses.pData + hClause; (pObj = *pIter); (p)->pIter++ )
+#define Cbs_ClauseForEachVar1( p, hClause, pObj )                   \
+    for ( (p)->pIter = (p)->pClauses.pData+hClause+1; (pObj = *pIter); (p)->pIter++ )
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -129,10 +144,14 @@ Cbs_Man_t * Cbs_ManAlloc()
 {
     Cbs_Man_t * p;
     p = ABC_CALLOC( Cbs_Man_t, 1 );
-    p->pProp.nSize = p->pJust.nSize = 10000;
+    p->pProp.nSize = p->pJust.nSize = p->pClauses.nSize = 10000;
     p->pProp.pData = ABC_ALLOC( Gia_Obj_t *, p->pProp.nSize );
     p->pJust.pData = ABC_ALLOC( Gia_Obj_t *, p->pJust.nSize );
-    p->vModel = Vec_IntAlloc( 1000 );
+    p->pClauses.pData = ABC_ALLOC( Gia_Obj_t *, p->pClauses.nSize );
+    p->pClauses.iHead = p->pClauses.iTail = 1;
+    p->vModel   = Vec_IntAlloc( 1000 );
+    p->vLevReas = Vec_IntAlloc( 1000 );
+    p->vTemp    = Vec_PtrAlloc( 1000 );
     Cbs_SetDefaultParams( &p->Pars );
     return p;
 }
@@ -150,7 +169,10 @@ Cbs_Man_t * Cbs_ManAlloc()
 ***********************************************************************/
 void Cbs_ManStop( Cbs_Man_t * p )
 {
+    Vec_IntFree( p->vLevReas );
     Vec_IntFree( p->vModel );
+    Vec_PtrFree( p->vTemp );
+    ABC_FREE( p->pClauses.pData );
     ABC_FREE( p->pProp.pData );
     ABC_FREE( p->pJust.pData );
     ABC_FREE( p );
@@ -310,6 +332,26 @@ static inline void Cbs_QueRestore( Cbs_Que_t * p, int iHeadOld, int iTailOld )
     p->iTail = iTailOld;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Finalized the clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Cbs_QueFinish( Cbs_Que_t * p )
+{
+    int iHeadOld = p->iHead;
+    assert( p->iHead < p->iTail );
+    Cbs_QuePush( p, NULL );
+    p->iHead = p->iTail;
+    return iHeadOld;
+}
+
 
 /**Function*************************************************************
 
@@ -400,7 +442,7 @@ static inline Gia_Obj_t * Cbs_ManDecideMaxFF( Cbs_Man_t * p )
             pObjMax = pObj;
         }
     }
-    return pObjMax;
+    return pObjMax; 
 }
 
 
@@ -425,6 +467,7 @@ static inline void Cbs_ManCancelUntil( Cbs_Man_t * p, int iBound )
     Cbs_QueForEachEntry( p->pProp, pVar, i )
         Cbs_VarUnassign( pVar );
     p->pProp.iTail = iBound;
+    Vec_IntShrink( p->vLevReas, 3*iBound );
 }
 
 /**Function*************************************************************
@@ -438,28 +481,244 @@ static inline void Cbs_ManCancelUntil( Cbs_Man_t * p, int iBound )
   SeeAlso     []
 
 ***********************************************************************/
-static inline void Cbs_ManAssign( Cbs_Man_t * p, Gia_Obj_t * pObj )
+static inline void Cbs_ManAssign( Cbs_Man_t * p, Gia_Obj_t * pObj, int Level, Gia_Obj_t * pRes0, Gia_Obj_t * pRes1 )
 {
     Gia_Obj_t * pObjR = Gia_Regular(pObj);
     assert( Gia_ObjIsCand(pObjR) );
     assert( !Cbs_VarIsAssigned(pObjR) );
     Cbs_VarAssign( pObjR );
     Cbs_VarSetValue( pObjR, !Gia_IsComplement(pObj) );
+    assert( pObjR->Value == ~0 );
+    pObjR->Value = p->pProp.iTail;
     Cbs_QuePush( &p->pProp, pObjR );
+    Vec_IntPush( p->vLevReas, Level );
+    Vec_IntPush( p->vLevReas, pRes0 ? pRes0-pObjR : 0 );
+    Vec_IntPush( p->vLevReas, pRes1 ? pRes1-pObjR : 0 );
+    assert( Vec_IntSize(p->vLevReas) == 3 * p->pProp.iTail );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns clause size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Cbs_ManClauseSize( Cbs_Man_t * p, int hClause )
+{
+    Cbs_Que_t * pQue = &(p->pClauses);
+    Gia_Obj_t ** pIter;
+    for ( pIter = pQue->pData + hClause; *pIter; pIter++ );
+    return pIter - pQue->pData - hClause ;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints conflict clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Cbs_ManPrintClause( Cbs_Man_t * p, int Level, int hClause )
+{
+    Cbs_Que_t * pQue = &(p->pClauses);
+    Gia_Obj_t * pObj;
+    int i;
+    assert( Cbs_QueIsEmpty( pQue ) );
+    printf( "Level %2d : ", Level );
+    for ( i = hClause; (pObj = pQue->pData[i]); i++ )
+        printf( "%d=%d(%d) ", Gia_ObjId(p->pAig, pObj), Cbs_VarValue(pObj), Cbs_VarDecLevel(p, pObj) );
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints conflict clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Cbs_ManPrintClauseNew( Cbs_Man_t * p, int Level, int hClause )
+{
+    Cbs_Que_t * pQue = &(p->pClauses);
+    Gia_Obj_t * pObj;
+    int i;
+    assert( Cbs_QueIsEmpty( pQue ) );
+    printf( "Level %2d : ", Level );
+    for ( i = hClause; (pObj = pQue->pData[i]); i++ )
+        printf( "%c%d ", Cbs_VarValue(pObj)? '+':'-', Gia_ObjId(p->pAig, pObj) );
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns conflict clause.]
+
+  Description [Performs conflict analysis.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Cbs_ManDeriveReason( Cbs_Man_t * p, int Level )
+{
+    Cbs_Que_t * pQue = &(p->pClauses);
+    Gia_Obj_t * pObj, * pReason;
+    int i, k, iLitLevel;
+    assert( pQue->pData[pQue->iHead] == NULL );
+    assert( pQue->iHead + 1 < pQue->iTail );
+/*
+    for ( i = pQue->iHead + 1; i < pQue->iTail; i++ )
+    {
+        pObj = pQue->pData[i];
+        assert( pObj->fMark0 == 1 );
+    }
+*/
+    // compact literals
+    Vec_PtrClear( p->vTemp );
+    for ( i = k = pQue->iHead + 1; i < pQue->iTail; i++ )
+    {
+        pObj = pQue->pData[i];
+        if ( !pObj->fMark0 ) // unassigned - seen again
+            continue;
+        // assigned - seen first time
+        pObj->fMark0 = 0;
+        Vec_PtrPush( p->vTemp, pObj );
+        // check decision level
+        iLitLevel = Cbs_VarDecLevel( p, pObj );
+        if ( iLitLevel < Level )
+        {
+            pQue->pData[k++] = pObj;
+            continue;
+        }
+        assert( iLitLevel == Level );
+        pReason = Cbs_VarReason0( p, pObj );
+        if ( pReason == pObj ) // no reason
+        {
+            assert( pQue->pData[pQue->iHead] == NULL );
+            pQue->pData[pQue->iHead] = pObj;
+            continue;
+        }
+        Cbs_QuePush( pQue, pReason );
+        pReason = Cbs_VarReason1( p, pObj );
+        if ( pReason != pObj ) // second reason
+            Cbs_QuePush( pQue, pReason );
+    }
+    assert( pQue->pData[pQue->iHead] != NULL );
+    pQue->iTail = k;
+    // clear the marks
+    Vec_PtrForEachEntry( p->vTemp, pObj, i )
+        pObj->fMark0 = 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns conflict clause.]
+
+  Description [Performs conflict analysis.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Cbs_ManAnalyze( Cbs_Man_t * p, int Level, Gia_Obj_t * pVar, Gia_Obj_t * pFan0, Gia_Obj_t * pFan1 )
+{
+    Cbs_Que_t * pQue = &(p->pClauses);
+    assert( Cbs_VarIsAssigned(pVar) );
+    assert( Cbs_VarIsAssigned(pFan0) );
+    assert( pFan1 == NULL || Cbs_VarIsAssigned(pFan1) );
+    assert( Cbs_QueIsEmpty( pQue ) );
+    Cbs_QuePush( pQue, NULL );
+    Cbs_QuePush( pQue, pVar );
+    Cbs_QuePush( pQue, pFan0 );
+    if ( pFan1 )
+        Cbs_QuePush( pQue, pFan1 );
+    Cbs_ManDeriveReason( p, Level );
+    return Cbs_QueFinish( pQue );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Performs resolution of two clauses.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Cbs_ManResolve( Cbs_Man_t * p, int Level, int hClause0, int hClause1 )
+{
+    Cbs_Que_t * pQue = &(p->pClauses);
+    Gia_Obj_t * pObj;
+    int i, LevelMax = -1, LevelCur;
+    assert( pQue->pData[hClause0] != NULL );
+    assert( pQue->pData[hClause0] == pQue->pData[hClause1] );
+/*
+    for ( i = hClause0 + 1; (pObj = pQue->pData[i]); i++ )
+        assert( pObj->fMark0 == 1 );
+    for ( i = hClause1 + 1; (pObj = pQue->pData[i]); i++ )
+        assert( pObj->fMark0 == 1 );
+*/
+    assert( Cbs_QueIsEmpty( pQue ) );
+    Cbs_QuePush( pQue, NULL );
+    for ( i = hClause0 + 1; (pObj = pQue->pData[i]); i++ )
+    {
+        if ( !pObj->fMark0 ) // unassigned - seen again
+            continue;
+        // assigned - seen first time
+        pObj->fMark0 = 0;
+        Cbs_QuePush( pQue, pObj );
+        LevelCur = Cbs_VarDecLevel( p, pObj );
+        if ( LevelMax < LevelCur )
+            LevelMax = LevelCur;
+    }
+    for ( i = hClause1 + 1; (pObj = pQue->pData[i]); i++ )
+    {
+        if ( !pObj->fMark0 ) // unassigned - seen again
+            continue;
+        // assigned - seen first time
+        pObj->fMark0 = 0;
+        Cbs_QuePush( pQue, pObj );
+        LevelCur = Cbs_VarDecLevel( p, pObj );
+        if ( LevelMax < LevelCur )
+            LevelMax = LevelCur;
+    }
+    for ( i = pQue->iHead + 1; i < pQue->iTail; i++ )
+        pQue->pData[i]->fMark0 = 1;
+    Cbs_ManDeriveReason( p, LevelMax );
+    return Cbs_QueFinish( pQue );
 }
 
 /**Function*************************************************************
 
   Synopsis    [Propagates a variable.]
 
-  Description [Returns 1 if conflict; 0 if no conflict.]
+  Description [Returns clause handle if conflict; 0 if no conflict.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Cbs_ManPropagateOne( Cbs_Man_t * p, Gia_Obj_t * pVar )
+static inline int Cbs_ManPropagateOne( Cbs_Man_t * p, Gia_Obj_t * pVar, int Level )
 {
     int Value0, Value1;
     assert( !Gia_IsComplement(pVar) );
@@ -472,24 +731,31 @@ static inline int Cbs_ManPropagateOne( Cbs_Man_t * p, Gia_Obj_t * pVar )
     if ( Cbs_VarValue(pVar) )
     { // value is 1
         if ( Value0 == 0 || Value1 == 0 ) // one is 0
-            return 1;
+        {
+            if ( Value0 == 0 && Value1 != 0 )
+                return Cbs_ManAnalyze( p, Level, pVar, Gia_ObjFanin0(pVar), NULL );
+            if ( Value0 != 0 && Value1 == 0 )
+                return Cbs_ManAnalyze( p, Level, pVar, Gia_ObjFanin1(pVar), NULL );
+            assert( Value0 == 0 && Value1 == 0 );
+            return Cbs_ManAnalyze( p, Level, pVar, Gia_ObjFanin0(pVar), Gia_ObjFanin1(pVar) );
+        }
         if ( Value0 == 2 ) // first is unassigned
-            Cbs_ManAssign( p, Gia_ObjChild0(pVar) );
+            Cbs_ManAssign( p, Gia_ObjChild0(pVar), Level, pVar, NULL );
         if ( Value1 == 2 ) // first is unassigned
-            Cbs_ManAssign( p, Gia_ObjChild1(pVar) );
+            Cbs_ManAssign( p, Gia_ObjChild1(pVar), Level, pVar, NULL );
         return 0;
     }
     // value is 0
     if ( Value0 == 0 || Value1 == 0 ) // one is 0
         return 0;
     if ( Value0 == 1 && Value1 == 1 ) // both are 1
-        return 1;
+        return Cbs_ManAnalyze( p, Level, pVar, Gia_ObjFanin0(pVar), Gia_ObjFanin1(pVar) );
     if ( Value0 == 1 || Value1 == 1 ) // one is 1 
     {
         if ( Value0 == 2 ) // first is unassigned
-            Cbs_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)) );
-        if ( Value1 == 2 ) // first is unassigned
-            Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)) );
+            Cbs_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)), Level, pVar, Gia_ObjFanin1(pVar) );
+        if ( Value1 == 2 ) // second is unassigned
+            Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)), Level, pVar, Gia_ObjFanin0(pVar) );
         return 0;
     }
     assert( Cbs_VarIsJust(pVar) );
@@ -509,7 +775,7 @@ static inline int Cbs_ManPropagateOne( Cbs_Man_t * p, Gia_Obj_t * pVar )
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Cbs_ManPropagateTwo( Cbs_Man_t * p, Gia_Obj_t * pVar )
+static inline int Cbs_ManPropagateTwo( Cbs_Man_t * p, Gia_Obj_t * pVar, int Level )
 {
     int Value0, Value1;
     assert( !Gia_IsComplement(pVar) );
@@ -522,12 +788,12 @@ static inline int Cbs_ManPropagateTwo( Cbs_Man_t * p, Gia_Obj_t * pVar )
     if ( Value0 == 0 || Value1 == 0 ) // one is 0
         return 0;
     if ( Value0 == 1 && Value1 == 1 ) // both are 1
-        return 1;
+        return Cbs_ManAnalyze( p, Level, pVar, Gia_ObjFanin0(pVar), Gia_ObjFanin1(pVar) );
     assert( Value0 == 1 || Value1 == 1 );
     if ( Value0 == 2 ) // first is unassigned
-        Cbs_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)) );
+        Cbs_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)), Level, pVar, Gia_ObjFanin1(pVar) );
     if ( Value1 == 2 ) // first is unassigned
-        Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)) );
+        Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)), Level, pVar, Gia_ObjFanin0(pVar) );
     return 0;
 }
 
@@ -542,16 +808,17 @@ static inline int Cbs_ManPropagateTwo( Cbs_Man_t * p, Gia_Obj_t * pVar )
   SeeAlso     []
 
 ***********************************************************************/
-int Cbs_ManPropagate( Cbs_Man_t * p )
+int Cbs_ManPropagate( Cbs_Man_t * p, int Level )
 {
+    int hClause;
     Gia_Obj_t * pVar;
     int i, k;
     while ( 1 )
     {
         Cbs_QueForEachEntry( p->pProp, pVar, i )
         {
-            if ( Cbs_ManPropagateOne( p, pVar ) )
-                return 1;
+            if ( (hClause = Cbs_ManPropagateOne( p, pVar, Level )) )
+                return hClause;
         }
         p->pProp.iHead = p->pProp.iTail;
         k = p->pJust.iHead;
@@ -559,8 +826,8 @@ int Cbs_ManPropagate( Cbs_Man_t * p )
         {
             if ( Cbs_VarIsJust( pVar ) )
                 p->pJust.pData[k++] = pVar;
-            else if ( Cbs_ManPropagateTwo( p, pVar ) )
-                return 1;
+            else if ( (hClause = Cbs_ManPropagateTwo( p, pVar, Level )) )
+                return hClause;
         }
         if ( k == p->pJust.iTail )
             break;
@@ -573,30 +840,31 @@ int Cbs_ManPropagate( Cbs_Man_t * p )
 
   Synopsis    [Solve the problem recursively.]
 
-  Description [Returns 1 if unsat or undecided; 0 if satisfiable.]
+  Description [Returns learnt clause if unsat, NULL if sat or undecided.]
                
   SideEffects []
 
   SeeAlso     []
-
+ 
 ***********************************************************************/
-int Cbs_ManSolve_rec( Cbs_Man_t * p )
-{
-    Gia_Obj_t * pVar;
+int Cbs_ManSolve_rec( Cbs_Man_t * p, int Level )
+{ 
+    Cbs_Que_t * pQue = &(p->pClauses);
+    Gia_Obj_t * pVar, * pDecVar;
+    int hClause, hLearn0, hLearn1;
     int iPropHead, iJustHead, iJustTail;
     // propagate assignments
     assert( !Cbs_QueIsEmpty(&p->pProp) );
-    if ( Cbs_ManPropagate( p ) )
-        return 1;
+    if ( (hClause = Cbs_ManPropagate( p, Level )) )
+        return hClause;
     // check for satisfying assignment
     assert( Cbs_QueIsEmpty(&p->pProp) );
     if ( Cbs_QueIsEmpty(&p->pJust) )
         return 0;
     // quit using resource limits
-    p->Pars.nBTThis++;
     p->Pars.nJustThis = ABC_MAX( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead );
     if ( Cbs_ManCheckLimits( p ) )
-        return 1;
+        return 0;
     // remember the state before branching
     iPropHead = p->pProp.iHead;
     Cbs_QueStore( &p->pJust, &iJustHead, &iJustTail );
@@ -609,38 +877,31 @@ int Cbs_ManSolve_rec( Cbs_Man_t * p )
         pVar = Cbs_ManDecideMaxFF( p );
     else assert( 0 );
     assert( Cbs_VarIsJust( pVar ) );
-    // decide using fanout count!
-    if ( Gia_ObjRefs(p->pAig, Gia_ObjFanin0(pVar)) < Gia_ObjRefs(p->pAig, Gia_ObjFanin1(pVar)) )
-    {
-        // decide on first fanin
-        Cbs_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)) );
-        if ( !Cbs_ManSolve_rec( p ) )
-            return 0;
-        if ( Cbs_ManCheckLimits( p ) )
-            return 1;
-        Cbs_ManCancelUntil( p, iPropHead );
-        Cbs_QueRestore( &p->pJust, iJustHead, iJustTail );
-        // decide on second fanin
-        Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)) );
-    }
+    // chose decision variable using fanout count
+    if ( Gia_ObjRefs(p->pAig, Gia_ObjFanin0(pVar)) > Gia_ObjRefs(p->pAig, Gia_ObjFanin1(pVar)) )
+        pDecVar = Gia_Not(Gia_ObjChild0(pVar));
     else
-    {
-        // decide on first fanin
-        Cbs_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)) );
-        if ( !Cbs_ManSolve_rec( p ) )
-            return 0;
-        if ( Cbs_ManCheckLimits( p ) )
-            return 1;
-        Cbs_ManCancelUntil( p, iPropHead );
-        Cbs_QueRestore( &p->pJust, iJustHead, iJustTail );
-        // decide on second fanin
-        Cbs_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)) );
-    }
-    if ( !Cbs_ManSolve_rec( p ) )
+        pDecVar = Gia_Not(Gia_ObjChild1(pVar));
+    // decide on first fanin
+    Cbs_ManAssign( p, pDecVar, Level+1, NULL, NULL );
+    if ( !(hLearn0 = Cbs_ManSolve_rec( p, Level+1 )) )
         return 0;
-    if ( Cbs_ManCheckLimits( p ) )
-        return 1;
-    return 1;
+    if ( pQue->pData[hLearn0] != Gia_Regular(pDecVar) )
+        return hLearn0;
+    Cbs_ManCancelUntil( p, iPropHead );
+    Cbs_QueRestore( &p->pJust, iJustHead, iJustTail );
+    // decide on second fanin
+    Cbs_ManAssign( p, Gia_Not(pDecVar), Level+1, NULL, NULL );
+    if ( !(hLearn1 = Cbs_ManSolve_rec( p, Level+1 )) )
+        return 0;
+    if ( pQue->pData[hLearn1] != Gia_Regular(pDecVar) )
+        return hLearn1;
+    hClause = Cbs_ManResolve( p, Level, hLearn0, hLearn1 );
+//    Cbs_ManPrintClauseNew( p, Level, hClause );
+//    if ( Level > Cbs_ClauseDecLevel(p, hClause) )
+//        p->Pars.nBTThisNc++;
+    p->Pars.nBTThis++;
+    return hClause;
 }
 
 /**Function*************************************************************
@@ -658,103 +919,28 @@ int Cbs_ManSolve_rec( Cbs_Man_t * p )
 ***********************************************************************/
 int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj )
 {
-//    Gia_Obj_t * pTemp;
-//    int i;
-    int RetValue;
-//    Gia_ManForEachObj( p->pAig, pTemp, i )
-//        assert( pTemp->fMark0 == 0 );
+    int RetValue = 0;
     assert( !p->pProp.iHead && !p->pProp.iTail );
     assert( !p->pJust.iHead && !p->pJust.iTail );
-    p->Pars.nBTThis = p->Pars.nJustThis = 0;
-    Cbs_ManAssign( p, pObj );
-    RetValue = Cbs_ManSolve_rec( p );
-    if ( RetValue == 0 )
+    assert( p->pClauses.iHead == 1 && p->pClauses.iTail == 1 );
+    p->Pars.nBTThis = p->Pars.nJustThis = p->Pars.nBTThisNc = 0;
+    Cbs_ManAssign( p, pObj, 0, NULL, NULL );
+    if ( !Cbs_ManSolve_rec(p, 0) && !Cbs_ManCheckLimits(p) )
         Cbs_ManSaveModel( p, p->vModel );
+    else
+        RetValue = 1;
     Cbs_ManCancelUntil( p, 0 );
     p->pJust.iHead = p->pJust.iTail = 0;
+    p->pClauses.iHead = p->pClauses.iTail = 1;
     p->Pars.nBTTotal += p->Pars.nBTThis;
     p->Pars.nJustTotal = ABC_MAX( p->Pars.nJustTotal, p->Pars.nJustThis );
     if ( Cbs_ManCheckLimits( p ) )
-        return -1;
+        RetValue = -1;
     return RetValue;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Procedure to test the new SAT solver.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cbs_ManSolveTest( Gia_Man_t * pGia )
-{
-    extern void Gia_SatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vCex, Vec_Int_t * vVisit );
-    int nConfsMax = 1000;
-    int CountUnsat, CountSat, CountUndec;
-    Cbs_Man_t * p; 
-    Vec_Int_t * vCex;
-    Vec_Int_t * vVisit;
-    Gia_Obj_t * pRoot; 
-    int i, RetValue, clk = clock();
-    Gia_ManCreateRefs( pGia );
-    // create logic network
-    p = Cbs_ManAlloc();
-    p->pAig = pGia;
-    // prepare AIG
-    Gia_ManCleanValue( pGia );
-    Gia_ManCleanMark0( pGia );
-    Gia_ManCleanMark1( pGia );
-//    vCex   = Vec_IntAlloc( 100 );
-    vVisit = Vec_IntAlloc( 100 );
-    // solve for each output
-    CountUnsat = CountSat = CountUndec = 0;
-    Gia_ManForEachCo( pGia, pRoot, i )
-    {
-        if ( Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) )
-            continue;
-
-//        Gia_ManIncrementTravId( pGia );
-
-//printf( "Output %6d : ", i );
-//        iLit = Gia_Var2Lit( Gia_ObjHandle(Gia_ObjFanin0(pRoot)), Gia_ObjFaninC0(pRoot) );
-//        RetValue = Cbs_ManSolve( p, &iLit, 1, nConfsMax, vCex );
-        RetValue = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) );
-        if ( RetValue == 1 )
-            CountUnsat++;
-        else if ( RetValue == -1 )
-            CountUndec++;
-        else 
-        {
-//            int iLit, k;
-            vCex = Cbs_ReadModel( p );
-
-//        printf( "complemented = %d.  ", Gia_ObjFaninC0(pRoot) );
-//printf( "conflicts = %6d  max-frontier = %6d \n", p->Pars.nBTThis, p->Pars.nJustThis );
-//            Vec_IntForEachEntry( vCex, iLit, k )
-//                printf( "%s%d ", Gia_LitIsCompl(iLit)? "!": "", Gia_ObjCioId(Gia_ManObj(pGia,Gia_Lit2Var(iLit))) );
-//            printf( "\n" );
-
-            Gia_SatVerifyPattern( pGia, pRoot, vCex, vVisit );
-            assert( RetValue == 0 );
-            CountSat++;
-        }
-//        Gia_ManCheckMark0( p );
-//        Gia_ManCheckMark1( p );
-    }
-    Cbs_ManStop( p );
-//    Vec_IntFree( vCex );
-    Vec_IntFree( vVisit );
-    printf( "Unsat = %d. Sat = %d. Undec = %d.  ", CountUnsat, CountSat, CountUndec );
-    ABC_PRT( "Time", clock() - clk );
-}
-
-
-/**Function*************************************************************
-
   Synopsis    [Prints statistics of the manager.]
 
   Description []
@@ -793,7 +979,7 @@ void Cbs_ManSatPrintStats( Cbs_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus )
+Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int fVerbose )
 {
     extern void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out );
     Cbs_Man_t * p; 
@@ -806,6 +992,7 @@ Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStat
     Gia_ManCreateRefs( pAig );
     Gia_ManCleanMark0( pAig );
     Gia_ManCleanMark1( pAig );
+    Gia_ManFillValue( pAig ); // maps nodes into trail ids
     // create logic network
     p = Cbs_ManAlloc();
     p->Pars.nBTLimit = nConfs;
@@ -829,7 +1016,7 @@ Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStat
             }
             else
             {
-                printf( "Constant 0 output of SRM!!!\n" );
+//                printf( "Constant 0 output of SRM!!!\n" );
                 Vec_StrPush( vStatus, 1 );
             }
             continue;
@@ -838,12 +1025,15 @@ Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStat
         p->Pars.fUseHighest = 1;
         p->Pars.fUseLowest  = 0;
         status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) );
+//        printf( "\n" );
+/*
         if ( status == -1 )
         {
             p->Pars.fUseHighest = 0;
             p->Pars.fUseLowest  = 1;
             status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) );
         }
+*/
         Vec_StrPush( vStatus, (char)status );
         if ( status == -1 )
         {
@@ -861,7 +1051,7 @@ Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStat
             continue;
         }
         p->nSatSat++;
-        p->nConfUnsat += p->Pars.nBTThis;
+        p->nConfSat += p->Pars.nBTThis;
 //        Gia_SatVerifyPattern( pAig, pRoot, vCex, vVisit );
         Cec_ManSatAddToStore( vCexStore, vCex, i );
         p->timeSatSat += clock() - clk;
@@ -869,9 +1059,12 @@ Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStat
     Vec_IntFree( vVisit );
     p->nSatTotal = Gia_ManPoNum(pAig);
     p->timeTotal = clock() - clkTotal;
-//    Cbs_ManSatPrintStats( p );
+    if ( fVerbose )
+        Cbs_ManSatPrintStats( p );
+//    printf( "RecCalls = %8d.  RecClause = %8d.  RecNonChro = %8d.\n", p->nRecCall, p->nRecClause, p->nRecNonChro );
     Cbs_ManStop( p );
     *pvStatus = vStatus;
+
 //    printf( "Total number of cex literals = %d. (Ave = %d)\n", 
 //         Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat, 
 //        (Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat)/p->nSatSat );
diff --git a/src/aig/gia/giaCSatOld.c b/src/aig/gia/giaCSatOld.c
new file mode 100644
index 00000000..409af56c
--- /dev/null
+++ b/src/aig/gia/giaCSatOld.c
@@ -0,0 +1,797 @@
+/**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"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Cbs0_Par_t_ Cbs0_Par_t;
+struct Cbs0_Par_t_
+{
+    // conflict limits
+    int           nBTLimit;     // limit on the number of conflicts
+    int           nJustLimit;   // limit on the size of justification queue
+    // 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
+    // decision heuristics
+    int           fUseHighest;  // use node with the highest ID
+    int           fUseLowest;   // use node with the highest ID
+    int           fUseMaxFF;    // use node with the largest fanin fanout
+    // other
+    int           fVerbose;
+};
+
+typedef struct Cbs0_Que_t_ Cbs0_Que_t;
+struct Cbs0_Que_t_
+{
+    int           iHead;        // beginning of the queue
+    int           iTail;        // end of the queue
+    int           nSize;        // allocated size
+    Gia_Obj_t **  pData;        // nodes stored in the queue
+};
+ 
+typedef struct Cbs0_Man_t_ Cbs0_Man_t;
+struct Cbs0_Man_t_
+{
+    Cbs0_Par_t    Pars;         // parameters
+    Gia_Man_t *   pAig;         // AIG manager
+    Cbs0_Que_t    pProp;        // propagation queue
+    Cbs0_Que_t    pJust;        // justification queue
+    Vec_Int_t *   vModel;       // satisfying assignment
+    // 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
+    int           timeSatUnsat; // unsat
+    int           timeSatSat;   // sat
+    int           timeSatUndec; // undecided
+    int           timeTotal;    // total runtime
+};
+
+static inline int   Cbs0_VarIsAssigned( Gia_Obj_t * pVar )      { return pVar->fMark0;                        }
+static inline void  Cbs0_VarAssign( Gia_Obj_t * pVar )          { assert(!pVar->fMark0); pVar->fMark0 = 1;    }
+static inline void  Cbs0_VarUnassign( Gia_Obj_t * pVar )        { assert(pVar->fMark0);  pVar->fMark0 = 0; pVar->fMark1 = 0;         }
+static inline int   Cbs0_VarValue( Gia_Obj_t * pVar )           { assert(pVar->fMark0);  return pVar->fMark1; }
+static inline void  Cbs0_VarSetValue( Gia_Obj_t * pVar, int v ) { assert(pVar->fMark0);  pVar->fMark1 = v;    }
+static inline int   Cbs0_VarIsJust( Gia_Obj_t * pVar )          { return Gia_ObjIsAnd(pVar) && !Cbs0_VarIsAssigned(Gia_ObjFanin0(pVar)) && !Cbs0_VarIsAssigned(Gia_ObjFanin1(pVar)); } 
+static inline int   Cbs0_VarFanin0Value( Gia_Obj_t * pVar )     { return !Cbs0_VarIsAssigned(Gia_ObjFanin0(pVar)) ? 2 : (Cbs0_VarValue(Gia_ObjFanin0(pVar)) ^ Gia_ObjFaninC0(pVar)); }
+static inline int   Cbs0_VarFanin1Value( Gia_Obj_t * pVar )     { return !Cbs0_VarIsAssigned(Gia_ObjFanin1(pVar)) ? 2 : (Cbs0_VarValue(Gia_ObjFanin1(pVar)) ^ Gia_ObjFaninC1(pVar)); }
+
+#define Cbs0_QueForEachEntry( Que, pObj, i )                    \
+    for ( i = (Que).iHead; (i < (Que).iTail) && ((pObj) = (Que).pData[i]); i++ )
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Sets default values of the parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cbs0_SetDefaultParams( Cbs0_Par_t * pPars )
+{
+    memset( pPars, 0, sizeof(Cbs0_Par_t) );
+    pPars->nBTLimit    =  1000;   // limit on the number of conflicts
+    pPars->nJustLimit  =   100;   // limit on the size of justification queue
+    pPars->fUseHighest =     1;   // use node with the highest ID
+    pPars->fUseLowest  =     0;   // use node with the highest ID
+    pPars->fUseMaxFF   =     0;   // use node with the largest fanin fanout
+    pPars->fVerbose    =     1;   // print detailed statistics
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cbs0_Man_t * Cbs0_ManAlloc()
+{
+    Cbs0_Man_t * p;
+    p = ABC_CALLOC( Cbs0_Man_t, 1 );
+    p->pProp.nSize = p->pJust.nSize = 10000;
+    p->pProp.pData = ABC_ALLOC( Gia_Obj_t *, p->pProp.nSize );
+    p->pJust.pData = ABC_ALLOC( Gia_Obj_t *, p->pJust.nSize );
+    p->vModel = Vec_IntAlloc( 1000 );
+    Cbs0_SetDefaultParams( &p->Pars );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cbs0_ManStop( Cbs0_Man_t * p )
+{
+    Vec_IntFree( p->vModel );
+    ABC_FREE( p->pProp.pData );
+    ABC_FREE( p->pJust.pData );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns satisfying assignment.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Cbs0_ReadModel( Cbs0_Man_t * p )
+{
+    return p->vModel;
+}
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the solver is out of limits.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Cbs0_ManCheckLimits( Cbs0_Man_t * p )
+{
+    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 Cbs0_ManSaveModel( Cbs0_Man_t * p, Vec_Int_t * vCex )
+{
+    Gia_Obj_t * pVar;
+    int i;
+    Vec_IntClear( vCex );
+    p->pProp.iHead = 0;
+    Cbs0_QueForEachEntry( p->pProp, pVar, i )
+        if ( Gia_ObjIsCi(pVar) )
+//            Vec_IntPush( vCex, Gia_Var2Lit(Gia_ObjId(p->pAig,pVar), !Cbs0_VarValue(pVar)) );
+            Vec_IntPush( vCex, Gia_Var2Lit(Gia_ObjCioId(pVar), !Cbs0_VarValue(pVar)) );
+} 
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Cbs0_QueIsEmpty( Cbs0_Que_t * p )
+{
+    return p->iHead == p->iTail;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Cbs0_QuePush( Cbs0_Que_t * p, Gia_Obj_t * pObj )
+{
+    if ( p->iTail == p->nSize )
+    {
+        p->nSize *= 2;
+        p->pData = ABC_REALLOC( Gia_Obj_t *, p->pData, p->nSize ); 
+    }
+    p->pData[p->iTail++] = pObj;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the object in the queue.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Cbs0_QueHasNode( Cbs0_Que_t * p, Gia_Obj_t * pObj )
+{
+    Gia_Obj_t * pTemp;
+    int i;
+    Cbs0_QueForEachEntry( *p, pTemp, i )
+        if ( pTemp == pObj )
+            return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Cbs0_QueStore( Cbs0_Que_t * p, int * piHeadOld, int * piTailOld )
+{
+    int i;
+    *piHeadOld = p->iHead;
+    *piTailOld = p->iTail;
+    for ( i = *piHeadOld; i < *piTailOld; i++ )
+        Cbs0_QuePush( p, p->pData[i] );
+    p->iHead = *piTailOld;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Cbs0_QueRestore( Cbs0_Que_t * p, int iHeadOld, int iTailOld )
+{
+    p->iHead = iHeadOld;
+    p->iTail = iTailOld;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Max number of fanins fanouts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Cbs0_VarFaninFanoutMax( Cbs0_Man_t * p, Gia_Obj_t * pObj )
+{
+    int Count0, Count1;
+    assert( !Gia_IsComplement(pObj) );
+    assert( Gia_ObjIsAnd(pObj) );
+    Count0 = Gia_ObjRefs( p->pAig, Gia_ObjFanin0(pObj) );
+    Count1 = Gia_ObjRefs( p->pAig, Gia_ObjFanin1(pObj) );
+    return ABC_MAX( Count0, Count1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Find variable with the highest ID.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Gia_Obj_t * Cbs0_ManDecideHighest( Cbs0_Man_t * p )
+{
+    Gia_Obj_t * pObj, * pObjMax = NULL;
+    int i;
+    Cbs0_QueForEachEntry( p->pJust, pObj, i )
+        if ( pObjMax == NULL || pObjMax < pObj )
+            pObjMax = pObj;
+    return pObjMax;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Find variable with the lowest ID.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Gia_Obj_t * Cbs0_ManDecideLowest( Cbs0_Man_t * p )
+{
+    Gia_Obj_t * pObj, * pObjMin = NULL;
+    int i;
+    Cbs0_QueForEachEntry( p->pJust, pObj, i )
+        if ( pObjMin == NULL || pObjMin > pObj )
+            pObjMin = pObj;
+    return pObjMin;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Find variable with the maximum number of fanin fanouts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Gia_Obj_t * Cbs0_ManDecideMaxFF( Cbs0_Man_t * p )
+{
+    Gia_Obj_t * pObj, * pObjMax = NULL;
+    int i, iMaxFF = 0, iCurFF;
+    assert( p->pAig->pRefs != NULL );
+    Cbs0_QueForEachEntry( p->pJust, pObj, i )
+    {
+        iCurFF = Cbs0_VarFaninFanoutMax( p, pObj );
+        assert( iCurFF > 0 );
+        if ( iMaxFF < iCurFF )
+        {
+            iMaxFF = iCurFF;
+            pObjMax = pObj;
+        }
+    }
+    return pObjMax;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Cbs0_ManCancelUntil( Cbs0_Man_t * p, int iBound )
+{
+    Gia_Obj_t * pVar;
+    int i;
+    assert( iBound <= p->pProp.iTail );
+    p->pProp.iHead = iBound;
+    Cbs0_QueForEachEntry( p->pProp, pVar, i )
+        Cbs0_VarUnassign( pVar );
+    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 Cbs0_ManAssign( Cbs0_Man_t * p, Gia_Obj_t * pObj )
+{
+    Gia_Obj_t * pObjR = Gia_Regular(pObj);
+    assert( Gia_ObjIsCand(pObjR) );
+    assert( !Cbs0_VarIsAssigned(pObjR) );
+    Cbs0_VarAssign( pObjR );
+    Cbs0_VarSetValue( pObjR, !Gia_IsComplement(pObj) );
+    Cbs0_QuePush( &p->pProp, pObjR );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Propagates a variable.]
+
+  Description [Returns 1 if conflict; 0 if no conflict.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Cbs0_ManPropagateOne( Cbs0_Man_t * p, Gia_Obj_t * pVar )
+{
+    int Value0, Value1;
+    assert( !Gia_IsComplement(pVar) );
+    assert( Cbs0_VarIsAssigned(pVar) );
+    if ( Gia_ObjIsCi(pVar) )
+        return 0;
+    assert( Gia_ObjIsAnd(pVar) );
+    Value0 = Cbs0_VarFanin0Value(pVar);
+    Value1 = Cbs0_VarFanin1Value(pVar);
+    if ( Cbs0_VarValue(pVar) )
+    { // value is 1
+        if ( Value0 == 0 || Value1 == 0 ) // one is 0
+            return 1;
+        if ( Value0 == 2 ) // first is unassigned
+            Cbs0_ManAssign( p, Gia_ObjChild0(pVar) );
+        if ( Value1 == 2 ) // first is unassigned
+            Cbs0_ManAssign( p, Gia_ObjChild1(pVar) );
+        return 0;
+    }
+    // value is 0
+    if ( Value0 == 0 || Value1 == 0 ) // one is 0
+        return 0;
+    if ( Value0 == 1 && Value1 == 1 ) // both are 1
+        return 1;
+    if ( Value0 == 1 || Value1 == 1 ) // one is 1 
+    {
+        if ( Value0 == 2 ) // first is unassigned
+            Cbs0_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)) );
+        if ( Value1 == 2 ) // first is unassigned
+            Cbs0_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)) );
+        return 0;
+    }
+    assert( Cbs0_VarIsJust(pVar) );
+    assert( !Cbs0_QueHasNode( &p->pJust, pVar ) );
+    Cbs0_QuePush( &p->pJust, pVar );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Propagates a variable.]
+
+  Description [Returns 1 if conflict; 0 if no conflict.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Cbs0_ManPropagateTwo( Cbs0_Man_t * p, Gia_Obj_t * pVar )
+{
+    int Value0, Value1;
+    assert( !Gia_IsComplement(pVar) );
+    assert( Gia_ObjIsAnd(pVar) );
+    assert( Cbs0_VarIsAssigned(pVar) );
+    assert( !Cbs0_VarValue(pVar) );
+    Value0 = Cbs0_VarFanin0Value(pVar);
+    Value1 = Cbs0_VarFanin1Value(pVar);
+    // value is 0
+    if ( Value0 == 0 || Value1 == 0 ) // one is 0
+        return 0;
+    if ( Value0 == 1 && Value1 == 1 ) // both are 1
+        return 1;
+    assert( Value0 == 1 || Value1 == 1 );
+    if ( Value0 == 2 ) // first is unassigned
+        Cbs0_ManAssign( p, Gia_Not(Gia_ObjChild0(pVar)) );
+    if ( Value1 == 2 ) // first is unassigned
+        Cbs0_ManAssign( p, Gia_Not(Gia_ObjChild1(pVar)) );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Propagates all variables.]
+
+  Description [Returns 1 if conflict; 0 if no conflict.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cbs0_ManPropagate( Cbs0_Man_t * p )
+{
+    Gia_Obj_t * pVar;
+    int i, k;
+    while ( 1 )
+    {
+        Cbs0_QueForEachEntry( p->pProp, pVar, i )
+        {
+            if ( Cbs0_ManPropagateOne( p, pVar ) )
+                return 1;
+        }
+        p->pProp.iHead = p->pProp.iTail;
+        k = p->pJust.iHead;
+        Cbs0_QueForEachEntry( p->pJust, pVar, i )
+        {
+            if ( Cbs0_VarIsJust( pVar ) )
+                p->pJust.pData[k++] = pVar;
+            else if ( Cbs0_ManPropagateTwo( p, pVar ) )
+                return 1;
+        }
+        if ( k == p->pJust.iTail )
+            break;
+        p->pJust.iTail = k;
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Solve the problem recursively.]
+
+  Description [Returns 1 if unsat or undecided; 0 if satisfiable.]
+               
+  SideEffects []
+
+  SeeAlso     []
+ 
+***********************************************************************/
+int Cbs0_ManSolve_rec( Cbs0_Man_t * p )
+{
+    Gia_Obj_t * pVar, * pDecVar;
+    int iPropHead, iJustHead, iJustTail;
+    // propagate assignments
+    assert( !Cbs0_QueIsEmpty(&p->pProp) );
+    if ( Cbs0_ManPropagate( p ) )
+        return 1;
+    // check for satisfying assignment
+    assert( Cbs0_QueIsEmpty(&p->pProp) );
+    if ( Cbs0_QueIsEmpty(&p->pJust) )
+        return 0;
+    // quit using resource limits
+    p->Pars.nJustThis = ABC_MAX( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead );
+    if ( Cbs0_ManCheckLimits( p ) )
+        return 0;
+    // remember the state before branching
+    iPropHead = p->pProp.iHead;
+    Cbs0_QueStore( &p->pJust, &iJustHead, &iJustTail );
+    // find the decision variable
+    if ( p->Pars.fUseHighest )
+        pVar = Cbs0_ManDecideHighest( p );
+    else if ( p->Pars.fUseLowest )
+        pVar = Cbs0_ManDecideLowest( p );
+    else if ( p->Pars.fUseMaxFF )
+        pVar = Cbs0_ManDecideMaxFF( p );
+    else assert( 0 );
+    assert( Cbs0_VarIsJust( pVar ) );
+    // chose decision variable using fanout count
+    if ( Gia_ObjRefs(p->pAig, Gia_ObjFanin0(pVar)) > Gia_ObjRefs(p->pAig, Gia_ObjFanin1(pVar)) )
+        pDecVar = Gia_Not(Gia_ObjChild0(pVar));
+    else
+        pDecVar = Gia_Not(Gia_ObjChild1(pVar));
+    // decide on first fanin
+    Cbs0_ManAssign( p, pDecVar );
+    if ( !Cbs0_ManSolve_rec( p ) )
+        return 0;
+    Cbs0_ManCancelUntil( p, iPropHead );
+    Cbs0_QueRestore( &p->pJust, iJustHead, iJustTail );
+    // decide on second fanin
+    Cbs0_ManAssign( p, Gia_Not(pDecVar) );
+    if ( !Cbs0_ManSolve_rec( p ) )
+        return 0;
+    p->Pars.nBTThis++;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Looking for a satisfying assignment of the node.]
+
+  Description [Assumes that each node has flag pObj->fMark0 set to 0.
+  Returns 1 if unsatisfiable, 0 if satisfiable, and -1 if undecided.
+  The node may be complemented. ]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cbs0_ManSolve( Cbs0_Man_t * p, Gia_Obj_t * pObj )
+{
+    int RetValue;
+    assert( !p->pProp.iHead && !p->pProp.iTail );
+    assert( !p->pJust.iHead && !p->pJust.iTail );
+    p->Pars.nBTThis = p->Pars.nJustThis = 0;
+    Cbs0_ManAssign( p, pObj );
+    RetValue = Cbs0_ManSolve_rec( p );
+    if ( RetValue == 0 && !Cbs0_ManCheckLimits(p) )
+        Cbs0_ManSaveModel( p, p->vModel );
+    Cbs0_ManCancelUntil( p, 0 );
+    p->pJust.iHead = p->pJust.iTail = 0;
+    p->Pars.nBTTotal += p->Pars.nBTThis;
+    p->Pars.nJustTotal = ABC_MAX( p->Pars.nJustTotal, p->Pars.nJustThis );
+    if ( Cbs0_ManCheckLimits( p ) )
+        RetValue = -1;
+//    printf( "Outcome = %2d.  Confs = %6d.  Decision level max = %3d.\n", 
+//        RetValue, p->Pars.nBTThis, p->DecLevelMax );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints statistics of the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cbs0_ManSatPrintStats( Cbs0_Man_t * p )
+{
+    printf( "CO = %6d  ", Gia_ManCoNum(p->pAig) );
+    printf( "Conf = %5d  ", p->Pars.nBTLimit );
+    printf( "JustMax = %5d  ", p->Pars.nJustLimit );
+    printf( "\n" );
+    printf( "Unsat calls %6d  (%6.2f %%)   Ave conf = %8.1f   ", 
+        p->nSatUnsat, 100.0*p->nSatUnsat/p->nSatTotal, 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,   100.0*p->nSatSat/p->nSatTotal, 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, 100.0*p->nSatUndec/p->nSatTotal, 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    [Procedure to test the new SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int fVerbose )
+{
+    extern void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out );
+    Cbs0_Man_t * p; 
+    Vec_Int_t * vCex, * vVisit, * vCexStore;
+    Vec_Str_t * vStatus;
+    Gia_Obj_t * pRoot; 
+    int i, status, clk, clkTotal = clock();
+    assert( Gia_ManRegNum(pAig) == 0 );
+    // prepare AIG
+    Gia_ManCreateRefs( pAig );
+    Gia_ManCleanMark0( pAig );
+    Gia_ManCleanMark1( pAig );
+    // create logic network
+    p = Cbs0_ManAlloc();
+    p->Pars.nBTLimit = nConfs;
+    p->pAig   = pAig;
+    // create resulting data-structures
+    vStatus   = Vec_StrAlloc( Gia_ManPoNum(pAig) );
+    vCexStore = Vec_IntAlloc( 10000 );
+    vVisit    = Vec_IntAlloc( 100 );
+    vCex      = Cbs0_ReadModel( p );
+    // solve for each output
+    Gia_ManForEachCo( pAig, pRoot, i )
+    {
+        Vec_IntClear( vCex );
+        if ( Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) )
+        {
+            if ( Gia_ObjFaninC0(pRoot) )
+            {
+                printf( "Constant 1 output of SRM!!!\n" );
+                Cec_ManSatAddToStore( vCexStore, vCex, i ); // trivial counter-example
+                Vec_StrPush( vStatus, 0 );
+            }
+            else
+            {
+//                printf( "Constant 0 output of SRM!!!\n" );
+                Vec_StrPush( vStatus, 1 );
+            }
+            continue;
+        }
+        clk = clock();
+        p->Pars.fUseHighest = 1;
+        p->Pars.fUseLowest  = 0;
+        status = Cbs0_ManSolve( p, Gia_ObjChild0(pRoot) );
+/*
+        if ( status == -1 )
+        {
+            p->Pars.fUseHighest = 0;
+            p->Pars.fUseLowest  = 1;
+            status = Cbs0_ManSolve( p, Gia_ObjChild0(pRoot) );
+        }
+*/
+        Vec_StrPush( vStatus, (char)status );
+        if ( status == -1 )
+        {
+            p->nSatUndec++;
+            p->nConfUndec += p->Pars.nBTThis;
+            Cec_ManSatAddToStore( vCexStore, NULL, i ); // timeout
+            p->timeSatUndec += clock() - clk;
+            continue;
+        }
+        if ( status == 1 )
+        {
+            p->nSatUnsat++;
+            p->nConfUnsat += p->Pars.nBTThis;
+            p->timeSatUnsat += clock() - clk;
+            continue;
+        }
+        p->nSatSat++;
+        p->nConfSat += p->Pars.nBTThis;
+//        Gia_SatVerifyPattern( pAig, pRoot, vCex, vVisit );
+        Cec_ManSatAddToStore( vCexStore, vCex, i );
+        p->timeSatSat += clock() - clk;
+    }
+    Vec_IntFree( vVisit );
+    p->nSatTotal = Gia_ManPoNum(pAig);
+    p->timeTotal = clock() - clkTotal;
+    if ( fVerbose )
+        Cbs0_ManSatPrintStats( p );
+    Cbs0_ManStop( p );
+    *pvStatus = vStatus;
+//    printf( "Total number of cex literals = %d. (Ave = %d)\n", 
+//         Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat, 
+//        (Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat)/p->nSatSat );
+    return vCexStore;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/gia/giaRetime.c b/src/aig/gia/giaRetime.c
index 4f2c6e08..965b5981 100644
--- a/src/aig/gia/giaRetime.c
+++ b/src/aig/gia/giaRetime.c
@@ -243,6 +243,7 @@ Gia_Man_t * Gia_ManRetimeForwardOne( Gia_Man_t * p, int * pnRegFixed, int * pnRe
     // finally derive the new manager
     pNew = Gia_ManRetimeDupForward( p, vCut );
     Vec_PtrFree( vCut );
+    if ( vObjClasses )
     Vec_IntFree( vObjClasses );
     pNew->vFlopClasses = vFlopClasses;
     return pNew;
diff --git a/src/aig/gia/giaSim.c b/src/aig/gia/giaSim.c
index 7ee0ddc4..020683ad 100644
--- a/src/aig/gia/giaSim.c
+++ b/src/aig/gia/giaSim.c
@@ -405,7 +405,7 @@ int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
         if ( pPars->fVerbose )
         {
             printf( "Frame %4d out of %4d and timeout %3d sec. ", i+1, pPars->nIters, pPars->TimeLimit );
-            printf( "Time = %7.2f sec\r", (1.0*clock()-clkTotal)/CLOCKS_PER_SEC );
+            printf( "Time = %7.2f sec\r", (1.0*clock()-clk)/CLOCKS_PER_SEC );
         }
         if ( pPars->fCheckMiter && Gia_ManCheckPos( p, &iOut, &iPat ) )
         {
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index 055d7580..916414fc 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -2,6 +2,7 @@ SRC +=    src/aig/gia/gia.c \
     src/aig/gia/giaAig.c \
     src/aig/gia/giaAiger.c \
     src/aig/gia/giaCof.c \
+    src/aig/gia/giaCSatOld.c \
     src/aig/gia/giaCSat.c \
     src/aig/gia/giaDfs.c \
     src/aig/gia/giaDup.c \
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 876266af..ef7969be 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -17681,7 +17681,7 @@ usage:
     fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", nBTLimit );
 //    fprintf( pErr, "\t-G num : the max number of conflicts globally [default = %d]\n", nBTLimitAll );
 //    fprintf( pErr, "\t-D num : the delta in the number of nodes [default = %d]\n", nNodeDelta );
-    fprintf( pErr, "\t-L num : the limit on fanout count of resets/enables to cofactor [default = %d]\n", nCofFanLit? "yes": "no" );
+    fprintf( pErr, "\t-L num : the limit on fanout count of resets/enables to cofactor [default = %d]\n", nCofFanLit );
     fprintf( pErr, "\t-r     : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" );
 //    fprintf( pErr, "\t-a     : toggle SAT sweeping and SAT solving [default = %s]\n", fNewAlgo? "SAT solving": "SAT sweeping" );
     fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
@@ -23472,7 +23472,7 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fCSat = 0;
     Cec_ManSatSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CSNmfcvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CSNnmfcvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -23509,6 +23509,9 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nCallsRecycle < 0 ) 
                 goto usage;
             break;
+        case 'n':
+            pPars->fNonChrono ^= 1;
+            break;
         case 'm':
             pPars->fCheckMiter ^= 1;
             break;
@@ -23534,7 +23537,10 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
         Vec_Int_t * vCounters;
         Vec_Str_t * vStatus;
-        vCounters = Cbs_ManSolveMiter( pAbc->pAig, 10*pPars->nBTLimit, &vStatus );
+        if ( pPars->fNonChrono )
+            vCounters = Cbs_ManSolveMiterNc( pAbc->pAig, pPars->nBTLimit, &vStatus, pPars->fVerbose );
+        else
+            vCounters = Cbs_ManSolveMiter( pAbc->pAig, pPars->nBTLimit, &vStatus, pPars->fVerbose );
         Vec_IntFree( vCounters );
         Vec_StrFree( vStatus );
     }
@@ -23546,11 +23552,12 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( stdout, "usage: &sat [-CSN <num>] [-mfcvh]\n" );
+    fprintf( stdout, "usage: &sat [-CSN <num>] [-nmfcvh]\n" );
     fprintf( stdout, "\t         performs SAT solving for the combinational outputs\n" );
     fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
     fprintf( stdout, "\t-S num : the min number of variables to recycle the solver [default = %d]\n", pPars->nSatVarMax );
     fprintf( stdout, "\t-N num : the min number of calls to recycle the solver [default = %d]\n", pPars->nCallsRecycle );
+    fprintf( stdout, "\t-n     : toggle using non-chronological backtracking [default = %s]\n", pPars->fNonChrono? "yes": "no" );
     fprintf( stdout, "\t-m     : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "yes": "no" );
     fprintf( stdout, "\t-f     : toggle quitting when one PO is asserted [default = %s]\n", pPars->fFirstStop? "yes": "no" );
     fprintf( stdout, "\t-c     : toggle using circuit-based SAT solver [default = %s]\n", fCSat? "yes": "no" );
author	Alan Mishchenko <alanmi@berkeley.edu>	2009-04-05 08:01:00 -0700
committer	Alan Mishchenko <alanmi@berkeley.edu>	2009-04-05 08:01:00 -0700
commit	e3e2918eb8a4750b9ce51de821ea6b58941fe65c (patch)
tree	d678ac6820fb09638f5196501f94aa4c31c60d97
parent	23fd11037a006089898cb13494305e402a11ec76 (diff)
download	abc-e3e2918eb8a4750b9ce51de821ea6b58941fe65c.tar.gz abc-e3e2918eb8a4750b9ce51de821ea6b58941fe65c.tar.bz2 abc-e3e2918eb8a4750b9ce51de821ea6b58941fe65c.zip