Proof-logging in the updated solver.

4 files changed, 524 insertions, 391 deletions

diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c
index 5b3901a1..e2f907bb 100644
--- a/src/sat/bsat/satProof.c
+++ b/src/sat/bsat/satProof.c
@@ -18,7 +18,7 @@
 
 ***********************************************************************/
 
-#include "satSolver.h"
+#include "satSolver2.h"
 #include "vec.h"
 #include "aig.h"
 
@@ -33,30 +33,41 @@ ABC_NAMESPACE_IMPL_START
     Label is initialized to 0.
     Root clauses are 1-based. They are marked by prepending bit 1;
 */
+/*
+
+typedef struct satset_t satset;
+struct satset_t 
+{
+    unsigned learnt :  1;
+    unsigned mark   :  1;
+    unsigned partA  :  1;
+    unsigned nEnts  : 29;
+    int      Id;
+    lit      pEnts[0];
+};
+
+#define satset_foreach_entry( p, c, h, s )  \
+    for ( h = s; (h < veci_size(p)) && (((c) = satset_read(p, h)), 1); h += satset_size(c->nEnts) )
+*/
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-typedef struct Sat_Set_t_ Sat_Set_t;
-struct Sat_Set_t_
-{
-    int nEnts;
-    int Label;
-    int pEnts[0];
-};
+static inline satset* Proof_NodeRead   (Vec_Int_t* p, cla h )     { return satset_read( (veci*)p, h );   }
+static inline cla     Proof_NodeHandle (Vec_Int_t* p, satset* c)  { return satset_handle( (veci*)p, c ); }
+static inline int     Proof_NodeCheck  (Vec_Int_t* p, satset* c)  { return satset_check( (veci*)p, c );  }
+static inline int     Proof_NodeSize   (int nEnts)                { return sizeof(satset)/4 + nEnts;     }
 
-static inline int          Sat_SetCheck( Vec_Int_t * p, Sat_Set_t * pNode ) { return (int *)pNode > Vec_IntArray(p) && (int *)pNode < Vec_IntLimit(p); }
-static inline int          Sat_SetId( Vec_Int_t * p, Sat_Set_t * pNode )    { return (int *)pNode - Vec_IntArray(p);                                   }
-static inline Sat_Set_t *  Sat_SetFromId( Vec_Int_t * p, int i )            { return (Sat_Set_t *)(Vec_IntArray(p) + i);                              }
-static inline int          Sat_SetSize( Sat_Set_t * pNode )                 { return pNode->nEnts + 2;          }
+#define Proof_ForeachNode( p, pNode, hNode )             \
+    satset_foreach_entry( ((veci*)p), pNode, hNode, 1 )
+#define Proof_ForeachNodeVec( pVec, p, pNode, i )        \
+    for ( i = 0; (i < Vec_IntSize(pVec)) && ((pNode) = Proof_NodeRead(p, Vec_IntEntry(pVec,i))); i++ )
+#define Proof_NodeForeachFanin( p, pNode, pFanin, i )    \
+    for ( i = 0; (i < (int)pNode->nEnts) && (((pFanin) = ((pNode->pEnts[i] & 1) ? NULL : Proof_NodeRead(p, pNode->pEnts[i] >> 1))), 1); i++ )
+#define Proof_NodeForeachFanin2( p, pNode, pFanin, iFanin, i )    \
+    for ( i = 0; (i < (int)pNode->nEnts) && (((pFanin) = ((pNode->pEnts[i] & 1) ? NULL : Proof_NodeRead(p, pNode->pEnts[i] >> 1))), ((iFanin) = ((pNode->pEnts[i] & 1) ? pNode->pEnts[i] >> 1 : 0)), 1); i++ )
 
-#define Sat_PoolForEachSet( p, pNode, i )  \
-    for ( i = 1; (i < Vec_IntSize(p)) && ((pNode) = Sat_SetFromId(p, Vec_IntEntry(p,i))); i += Sat_SetSize(pNode) )
-#define Sat_SetForEachSet( p, pSet, pNode, i )  \
-    for ( i = 0; (i < pSet->nEnts) && (((pNode) = ((pSet->pEnts[i] & 1) ? NULL : Sat_SetFromId(p, pSet->pEnts[i]))), 1); i++ )
-#define Sat_VecForEachSet( pVec, p, pNode, i )  \
-    for ( i = 0; (i < Vec_IntSize(pVec)) && ((pNode) = Sat_SetFromId(p, Vec_IntEntry(pVec,i))); i++ )
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -64,7 +75,7 @@ static inline int          Sat_SetSize( Sat_Set_t * pNode )                 { re
 
 /**Function*************************************************************
 
-  Synopsis    [Recursively visits useful proof nodes.]
+  Synopsis    [Collects all resolution nodes belonging to the proof.]
 
   Description []
                
@@ -73,48 +84,20 @@ static inline int          Sat_SetSize( Sat_Set_t * pNode )                 { re
   SeeAlso     []
 
 ***********************************************************************/
-int Sat_ProofReduceOne( Vec_Int_t * p, Sat_Set_t * pNode, int * pnSize, Vec_Int_t * vStack )
+Vec_Int_t * Proof_CollectAll( Vec_Int_t * p )
 {
-    Sat_Set_t * pNext;
-    int i, NodeId;
-    if ( pNode->Label )
-        return pNode->Label;
-    // start with node
-    pNode->Label = 1;
-    Vec_IntPush( vStack, Sat_SetId(p, pNode) );
-    // perform DFS search
-    while ( Vec_IntSize(vStack) )
-    {
-        NodeId = Vec_IntPop( vStack );
-        if ( NodeId & 1 ) // extrated second time
-        {
-            pNode = Sat_SetFromId( p, NodeId ^ 1 );
-            pNode->Label = *pnSize;
-            *pnSize += Sat_SetSize(pNode);
-            // update fanins
-            Sat_SetForEachSet( p, pNode, pNext, i )
-                if ( pNext )
-                    pNode->pEnts[i] = pNext->Label;
-            continue;
-        }
-        // extracted first time
-        // add second time
-        Vec_IntPush( vStack, NodeId ^ 1 );
-        // add its anticedents
-        pNode = Sat_SetFromId( p, NodeId );
-        Sat_SetForEachSet( p, pNode, pNext, i )
-            if ( pNext && !pNext->Label )
-            {
-                pNext->Label = 1;
-                Vec_IntPush( vStack, Sat_SetId(p, pNode) ); // add first time
-            }
-    }
-    return pNode->Label;
+    Vec_Int_t * vUsed;
+    satset * pNode;
+    int hNode;
+    vUsed = Vec_IntAlloc( 1000 );
+    Proof_ForeachNode( p, pNode, hNode )
+        Vec_IntPush( vUsed, hNode );
+    return vUsed;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Recursively visits useful proof nodes.]
+  Synopsis    [Cleans collected resultion nodes belonging to the proof.]
 
   Description []
                
@@ -123,63 +106,55 @@ int Sat_ProofReduceOne( Vec_Int_t * p, Sat_Set_t * pNode, int * pnSize, Vec_Int_
   SeeAlso     []
 
 ***********************************************************************/
-/*
-int Sat_ProofReduce_rec( Vec_Int_t * p, Sat_Set_t * pNode, int * pnSize )
+void Proof_CleanCollected( Vec_Int_t * vProof, Vec_Int_t * vUsed )
 {
-    int * pBeg;
-    assert( Sat_SetCheck(p, pNode) );
-    if ( pNode->Label )
-        return pNode->Label;
-    for ( pBeg = pNode->pEnts; pBeg < pNode->pEnts + pNode->nEnts; pBeg++ )
-        if ( !(*pBeg & 1) )
-            *pBeg = Sat_ProofReduce_rec( p, Sat_SetFromId(p, *pBeg), pnSize );
-    pNode->Label = *pnSize;
-    *pnSize += Sat_SetSize(pNode);
-    return pNode->Label;
+    satset * pNode;
+    int hNode;
+    Proof_ForeachNodeVec( vUsed, vProof, pNode, hNode )
+        pNode->Id = 0;
 }
-*/
 
 /**Function*************************************************************
 
-  Synopsis    [Reduces the proof to contain only roots and their children.]
+  Synopsis    [Recursively visits useful proof nodes.]
 
-  Description [The result is updated proof and updated roots.]
+  Description []
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-void Sat_ProofReduce( Vec_Int_t * p, Vec_Int_t * vRoots )
+void Proof_CollectUsedInt( Vec_Int_t * p, satset * pNode, Vec_Int_t * vUsed, Vec_Int_t * vStack )
 {
-    int i, nSize = 1;
-    int * pBeg, * pEnd, * pNew;
-    Vec_Int_t * vStack;
-    Sat_Set_t * pNode;
-    // mark used nodes
-    vStack = Vec_IntAlloc( 1000 );
-    Sat_VecForEachSet( vRoots, p, pNode, i )
-        vRoots->pArray[i] = Sat_ProofReduceOne( p, pNode, &nSize, vStack );
-    Vec_IntFree( vStack );
-    // compact proof
-    pNew = Vec_IntArray(p) + 1;
-    Sat_PoolForEachSet( p, pNode, i )
+    satset * pNext;
+    int i, hNode;
+    if ( pNode->Id )
+        return;
+    // start with node
+    pNode->Id = 1;
+    Vec_IntPush( vStack, Proof_NodeHandle(p, pNode) << 1 );
+    // perform DFS search
+    while ( Vec_IntSize(vStack) )
     {
-        if ( !pNode->Label )
+        hNode = Vec_IntPop( vStack );
+        if ( hNode & 1 ) // extrated second time
+        {
+            Vec_IntPush( vUsed, hNode >> 1 );
             continue;
-        assert( pNew - Vec_IntArray(p) == pNode->Label );
-        pNode->Label = 0;
-        pBeg = (int *)pNode;
-        pEnd = pBeg + Sat_SetSize(pNode);
-        while ( pBeg < pEnd )
-            *pNew++ = *pBeg++;
+        }
+        // extracted first time        
+        Vec_IntPush( vStack, hNode ^ 1 ); // add second time
+        // add its anticedents        ;
+        pNode = Proof_NodeRead( p, hNode >> 1 );
+        Proof_NodeForeachFanin( p, pNode, pNext, i )
+            if ( pNext && !pNext->Id )
+            {
+                pNext->Id = 1;
+                Vec_IntPush( vStack, Proof_NodeHandle(p, pNext) << 1 ); // add first time
+            }
     }
-    // report the result
-    printf( "The proof was reduced from %d to %d (by %6.2f %%)\n", 
-        Vec_IntSize(p), nSize, 100.0 * (Vec_IntSize(p) - nSize) / Vec_IntSize(p) );
-    assert( pNew - Vec_IntArray(p) == nSize );
-    Vec_IntShrink( p, nSize );
-}   
+}
 
 /**Function*************************************************************
 
@@ -192,80 +167,51 @@ void Sat_ProofReduce( Vec_Int_t * p, Vec_Int_t * vRoots )
   SeeAlso     []
 
 ***********************************************************************/
-void Sat_ProofLabel( Vec_Int_t * p, Sat_Set_t * pNode, Vec_Int_t * vUsed, Vec_Int_t * vStack )
+void Proof_CollectUsedRec( Vec_Int_t * p, satset * pNode, Vec_Int_t * vUsed )
 {
-    Sat_Set_t * pNext;
-    int i, NodeId;
-    if ( pNode->Label )
+    satset * pNext;
+    int i;
+    if ( pNode->Id )
         return;
-    // start with node
-    pNode->Label = 1;
-    Vec_IntPush( vStack, Sat_SetId(p, pNode) );
-    // perform DFS search
-    while ( Vec_IntSize(vStack) )
-    {
-        NodeId = Vec_IntPop( vStack );
-        if ( NodeId & 1 ) // extrated second time
-        {
-            Vec_IntPush( vUsed, NodeId ^ 1 );
-            continue;
-        }
-        // extracted first time
-        // add second time
-        Vec_IntPush( vStack, NodeId ^ 1 );
-        // add its anticedents
-        pNode = Sat_SetFromId( p, NodeId );
-        Sat_SetForEachSet( p, pNode, pNext, i )
-            if ( pNext && !pNext->Label )
-            {
-                pNext->Label = 1;
-                Vec_IntPush( vStack, Sat_SetId(p, pNode) ); // add first time
-            }
-    }
+    pNode->Id = 1;
+    Proof_NodeForeachFanin( p, pNode, pNext, i )
+        if ( pNext && !pNext->Id )
+            Proof_CollectUsedRec( p, pNext, vUsed );
+    Vec_IntPush( vUsed, Proof_NodeHandle(p, pNode) );
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Computes UNSAT core.]
+  Synopsis    [Recursively visits useful proof nodes.]
 
-  Description [The result is the array of root clause indexes.]
+  Description []
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Sat_ProofCore( Vec_Int_t * p, int nRoots, int * pBeg, int * pEnd )
+Vec_Int_t * Proof_CollectUsed( Vec_Int_t * vProof, Vec_Int_t * vRoots, int hRoot )
 {
-    unsigned * pSeen;
-    Vec_Int_t * vCore, * vUsed, * vStack;
-    Sat_Set_t * pNode;
-    int i;
-    // collect visited clauses
+    Vec_Int_t * vUsed, * vStack;
+    assert( (hRoot > 0) ^ (vRoots != NULL) );
     vUsed = Vec_IntAlloc( 1000 );
     vStack = Vec_IntAlloc( 1000 );
-    while ( pBeg < pEnd )
-        Sat_ProofLabel( p, Sat_SetFromId(p, *pBeg++), vUsed, vStack );
-    Vec_IntFree( vStack );
-    // find the core
-    vCore = Vec_IntAlloc( 1000 );
-    pSeen = ABC_CALLOC( unsigned, Aig_BitWordNum(nRoots) );
-    Sat_VecForEachSet( vUsed, p, pNode, i )
+    if ( hRoot )
+//        Proof_CollectUsedInt( vProof, Proof_NodeRead(vProof, hRoot), vUsed, vStack );
+        Proof_CollectUsedRec( vProof, Proof_NodeRead(vProof, hRoot), vUsed );
+    else
     {
-        pNode->Label = 0;
-        for ( pBeg = pNode->pEnts; pBeg < pNode->pEnts + pNode->nEnts; pBeg++ )
-            if ( (*pBeg & 1) && !Aig_InfoHasBit(pBeg, *pBeg>>1) )
-            {
-                Aig_InfoSetBit( pBeg, *pBeg>>1 );
-                Vec_IntPush( vCore, (*pBeg>>1)-1 );
-            }
+        satset * pNode;
+        int i;
+        Proof_ForeachNodeVec( vRoots, vProof, pNode, i )
+//            Proof_CollectUsedInt( vProof, pNode, vUsed, vStack );
+            Proof_CollectUsedRec( vProof, pNode, vUsed );
     }
-    Vec_IntFree( vUsed );
-    ABC_FREE( pSeen );
-    return vCore;
+    Vec_IntFree( vStack );
+    return vUsed;
 }
-
-
+ 
 /**Function*************************************************************
 
   Synopsis    [Performs one resultion step.]
@@ -277,12 +223,14 @@ Vec_Int_t * Sat_ProofCore( Vec_Int_t * p, int nRoots, int * pBeg, int * pEnd )
   SeeAlso     []
 
 ***********************************************************************/
-Sat_Set_t * Sat_ProofResolve( Vec_Int_t * p, Sat_Set_t * c1, Sat_Set_t * c2 )
+satset * Proof_ResolveOne( Vec_Int_t * p, satset * c1, satset * c2 )
 {
+    satset * c;
     int i, k, Id, Var = -1, Count = 0;
+
     // find resolution variable
-    for ( i = 0; i < c1->nEnts; i++ )
-    for ( k = 0; k < c2->nEnts; k++ )
+    for ( i = 0; i < (int)c1->nEnts; i++ )
+    for ( k = 0; k < (int)c2->nEnts; k++ )
         if ( (c1->pEnts[i] ^ c2->pEnts[k]) == 1 )
         {
             Var = (c1->pEnts[i] >> 1);
@@ -302,7 +250,7 @@ Sat_Set_t * Sat_ProofResolve( Vec_Int_t * p, Sat_Set_t * c1, Sat_Set_t * c2 )
     Id = Vec_IntSize( p );
     Vec_IntPush( p, 0 ); // placeholder
     Vec_IntPush( p, 0 );
-    for ( i = 0; i < c1->nEnts; i++ )
+    for ( i = 0; i < (int)c1->nEnts; i++ )
     {
         if ( (c1->pEnts[i] >> 1) == Var )
             continue;
@@ -312,7 +260,7 @@ Sat_Set_t * Sat_ProofResolve( Vec_Int_t * p, Sat_Set_t * c1, Sat_Set_t * c2 )
         if ( k == Vec_IntSize(p) )
             Vec_IntPush( p, c1->pEnts[i] );
     }
-    for ( i = 0; i < c2->nEnts; i++ )
+    for ( i = 0; i < (int)c2->nEnts; i++ )
     {
         if ( (c2->pEnts[i] >> 1) == Var )
             continue;
@@ -322,8 +270,9 @@ Sat_Set_t * Sat_ProofResolve( Vec_Int_t * p, Sat_Set_t * c1, Sat_Set_t * c2 )
         if ( k == Vec_IntSize(p) )
             Vec_IntPush( p, c2->pEnts[i] );
     }
-    Vec_IntWriteEntry( p, Id, Vec_IntSize(p) - Id - 2 );
-    return Sat_SetFromId( p, Id );
+    c = Proof_NodeRead( p, Id );
+    c->nEnts = Vec_IntSize(p) - Id - 2;
+    return c;
 }
 
 /**Function*************************************************************
@@ -337,13 +286,15 @@ Sat_Set_t * Sat_ProofResolve( Vec_Int_t * p, Sat_Set_t * c1, Sat_Set_t * c2 )
   SeeAlso     []
 
 ***********************************************************************/
-Sat_Set_t * Sat_ProofCheckGetOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Int_t * vResolves, int iAnt )
+satset * Proof_CheckReadOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Int_t * vResolves, int iAnt )
 {
-    Sat_Set_t * pAnt;
+    satset * pAnt;
     if ( iAnt & 1 )
-        return Sat_SetFromId( vClauses, iAnt >> 1 );
-    pAnt = Sat_SetFromId( vProof, iAnt );
-    return Sat_SetFromId( vResolves, pAnt->Label );
+        return Proof_NodeRead( vClauses, iAnt >> 1 );
+    assert( iAnt > 0 );
+    pAnt = Proof_NodeRead( vProof, iAnt >> 1 );
+    assert( pAnt->Id > 0 );
+    return Proof_NodeRead( vResolves, pAnt->Id );
 }
 
 /**Function*************************************************************
@@ -357,117 +308,247 @@ Sat_Set_t * Sat_ProofCheckGetOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_
   SeeAlso     []
 
 ***********************************************************************/
-void Sat_ProofCheck( Vec_Int_t * vClauses, Vec_Int_t * vProof, int iRoot )
+void Proof_Check( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hRoot )
 {
-    Vec_Int_t * vOrigs, * vStack, * vUsed, * vResolves;
-    Sat_Set_t * pSet, * pSet0, * pSet1;
-    int i, k;
-    // collect original clauses
-    vOrigs = Vec_IntAlloc( 1000 );
-    Vec_IntPush( vOrigs, -1 );
-    Sat_PoolForEachSet( vClauses, pSet, i )
-        Vec_IntPush( vOrigs, Sat_SetId(vClauses, pSet) );
+    Vec_Int_t * vUsed, * vResolves;
+    satset * pSet, * pSet0, * pSet1;
+    int i, k, Counter = 0; 
     // collect visited clauses
-    vUsed = Vec_IntAlloc( 1000 );
-    vStack = Vec_IntAlloc( 1000 );
-    Sat_ProofLabel( vProof, Sat_SetFromId(vProof, iRoot), vUsed, vStack );
-    Vec_IntFree( vStack );
+    vUsed = Proof_CollectUsed( vProof, NULL, hRoot );
+    Proof_CleanCollected( vProof, vUsed );
     // perform resolution steps
     vResolves = Vec_IntAlloc( 1000 );
     Vec_IntPush( vResolves, -1 );
-    Sat_VecForEachSet( vUsed, vProof, pSet, i )
+    Proof_ForeachNodeVec( vUsed, vProof, pSet, i )
     {
-        pSet0 = Sat_ProofCheckGetOne( vOrigs, vProof, vResolves, pSet->pEnts[0] );
-        for ( k = 1; k < pSet->nEnts; k++ )
+        pSet0 = Proof_CheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[0] );
+        for ( k = 1; k < (int)pSet->nEnts; k++ )
         {
-            pSet1 = Sat_ProofCheckGetOne( vOrigs, vProof, vResolves, pSet->pEnts[k] );
-            pSet0 = Sat_ProofResolve( vResolves, pSet0, pSet1 );
+            pSet1 = Proof_CheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[k] );
+            pSet0 = Proof_ResolveOne( vResolves, pSet0, pSet1 );
         }
-        pSet->Label = Sat_SetId( vResolves, pSet0 );
+        pSet->Id = Proof_NodeHandle( vResolves, pSet0 );
+        Counter++;
     }
     // clean the proof
-    Sat_VecForEachSet( vUsed, vProof, pSet, i )
-        pSet->Label = 0;
+    Proof_ForeachNodeVec( vUsed, vProof, pSet, i )
+        pSet->Id = 0;
     // compare the final clause
     if ( pSet0->nEnts > 0 )
         printf( "Cound not derive the empty clause\n" );
     Vec_IntFree( vResolves );
     Vec_IntFree( vUsed );
-    Vec_IntFree( vOrigs );
 }
 
 
+
+
+
 /**Function*************************************************************
 
-  Synopsis    [Creates variable map.]
+  Synopsis    [Recursively visits useful proof nodes.]
 
-  Description [1=A, 2=B, neg=global]
+  Description []
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-void Sat_ProofVarMapCheck( Vec_Int_t * vClauses, Vec_Int_t * vVarMap )
+int Sat_ProofReduceOne( Vec_Int_t * p, satset * pNode, int * pnSize, Vec_Int_t * vStack )
 {
-    Sat_Set_t * pSet;
-    int i, k, fSeeA, fSeeB;
-    // make sure all clauses are either A or B
-    Sat_PoolForEachSet( vClauses, pSet, i )
+    satset * pNext;
+    int i, NodeId;
+    if ( pNode->Id )
+        return pNode->Id;
+    // start with node
+    pNode->Id = 1;
+    Vec_IntPush( vStack, Proof_NodeHandle(p, pNode) );
+    // perform DFS search
+    while ( Vec_IntSize(vStack) )
     {
-        fSeeA = fSeeB = 0;
-        for ( k = 0; k < pSet->nEnts; k++ )
+        NodeId = Vec_IntPop( vStack );
+        if ( NodeId & 1 ) // extrated second time
         {
-            fSeeA += (Vec_IntEntry(vVarMap, pSet->pEnts[k]) == 1);
-            fSeeB += (Vec_IntEntry(vVarMap, pSet->pEnts[k]) == 2);
+            pNode = Proof_NodeRead( p, NodeId ^ 1 );
+            pNode->Id = *pnSize;
+            *pnSize += Proof_NodeSize(pNode->nEnts);
+            // update fanins
+            Proof_NodeForeachFanin( p, pNode, pNext, i )
+                if ( pNext )
+                    pNode->pEnts[i] = pNext->Id;
+            continue;
         }
-        if ( fSeeA && fSeeB )
-            printf( "VarMap error!\n" );
+        // extracted first time
+        // add second time
+        Vec_IntPush( vStack, NodeId ^ 1 );
+        // add its anticedents
+        pNode = Proof_NodeRead( p, NodeId );
+        Proof_NodeForeachFanin( p, pNode, pNext, i )
+            if ( pNext && !pNext->Id )
+            {
+                pNext->Id = 1;
+                Vec_IntPush( vStack, Proof_NodeHandle(p, pNode) ); // add first time
+            }
+    }
+    return pNode->Id;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reduces the proof to contain only roots and their children.]
+
+  Description [The result is updated proof and updated roots.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sat_ProofReduce( Vec_Int_t * p, Vec_Int_t * vRoots )
+{
+    int i, nSize = 1;
+    int * pBeg, * pEnd, * pNew;
+    Vec_Int_t * vStack;
+    satset * pNode;
+    // mark used nodes
+    vStack = Vec_IntAlloc( 1000 );
+    Proof_ForeachNodeVec( vRoots, p, pNode, i )
+        vRoots->pArray[i] = Sat_ProofReduceOne( p, pNode, &nSize, vStack );
+    Vec_IntFree( vStack );
+    // compact proof
+    pNew = Vec_IntArray(p) + 1;
+    Proof_ForeachNode( p, pNode, i )
+    {
+        if ( !pNode->Id )
+            continue;
+        assert( pNew - Vec_IntArray(p) == pNode->Id );
+        pNode->Id = 0;
+        pBeg = (int *)pNode;
+        pEnd = pBeg + Proof_NodeSize(pNode->nEnts);
+        while ( pBeg < pEnd )
+            *pNew++ = *pBeg++;
+    }
+    // report the result
+    printf( "The proof was reduced from %d to %d (by %6.2f %%)\n", 
+        Vec_IntSize(p), nSize, 100.0 * (Vec_IntSize(p) - nSize) / Vec_IntSize(p) );
+    assert( pNew - Vec_IntArray(p) == nSize );
+    Vec_IntShrink( p, nSize );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes UNSAT core.]
+
+  Description [The result is the array of root clause indexes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Sat_ProofCore( Vec_Int_t * vProof, int nRoots, Vec_Int_t * vRoots )
+{
+    unsigned * pSeen;
+    Vec_Int_t * vCore, * vUsed;
+    satset * pNode;
+    int i, * pBeg;
+    // collect visited clauses
+    vUsed = Proof_CollectUsed( vProof, vRoots, 0 );
+    // find the core
+    vCore = Vec_IntAlloc( 1000 );
+    pSeen = ABC_CALLOC( unsigned, Aig_BitWordNum(nRoots) );
+    Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
+    {
+        pNode->Id = 0;
+        for ( pBeg = pNode->pEnts; pBeg < pNode->pEnts + pNode->nEnts; pBeg++ )
+            if ( (*pBeg & 1) && !Aig_InfoHasBit(pBeg, *pBeg>>1) )
+            {
+                Aig_InfoSetBit( pBeg, *pBeg>>1 );
+                Vec_IntPush( vCore, (*pBeg>>1)-1 );
+            }
     }
+    Vec_IntFree( vUsed );
+    ABC_FREE( pSeen );
+    return vCore;
 }
 
 /**Function*************************************************************
 
   Synopsis    [Computes interpolant of the proof.]
 
-  Description [Assuming that res vars are recorded, too...]
+  Description [Aassuming that global vars and A-clauses are marked.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Sat_ProofInterpolant( Vec_Int_t * vProof, int iRoot, Vec_Int_t * vClauses, Vec_Int_t * vVarMap )
+Aig_Man_t * Sat_ProofInterpolant( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hRoot, Vec_Int_t * vGlobVars )
 {
-    Vec_Int_t * vOrigs, * vUsed, * vStack;
+    Vec_Int_t * vUsed;
     Aig_Man_t * pAig;
-    Sat_Set_t * pSet;
     int i;
 
-    Sat_ProofVarMapCheck( vClauses, vVarMap );
-
-    // collect original clauses
-    vOrigs = Vec_IntAlloc( 1000 );
-    Vec_IntPush( vOrigs, -1 );
-    Sat_PoolForEachSet( vClauses, pSet, i )
-        Vec_IntPush( vOrigs, Sat_SetId(vClauses, pSet) );
-
     // collect visited clauses
-    vUsed = Vec_IntAlloc( 1000 );
-    vStack = Vec_IntAlloc( 1000 );
-    Sat_ProofLabel( vProof, Sat_SetFromId(vProof, iRoot), vUsed, vStack );
-    Vec_IntFree( vStack );
+    vUsed = Proof_CollectUsed( vProof, NULL, hRoot );
 
     // start the AIG
     pAig = Aig_ManStart( 10000 );
     pAig->pName = Aig_UtilStrsav( "interpol" );
-    for ( i = 0; i < Vec_IntSize(vVarMap); i++ )
-        if ( Vec_IntEntry(vVarMap, i) < 0 )
-            Aig_ObjCreatePi( pAig );
+    for ( i = 0; i < Vec_IntSize(vGlobVars); i++ )
+        Aig_ObjCreatePi( pAig );
  
     return pAig;
 }
 
+/*
+    Sat_ProofTest( 
+        &s->clauses,      // clauses
+        &s->proof_clas,   // proof clauses
+        &s->proof_vars,   // proof variables
+        NULL,             // proof roots
+        veci_begin(&s->claProofs)[clause_read(s, s->iLearntLast)->Id)],  // one root
+        &s->glob_vars );  // global variables (for interpolation)
+*/
+
+/**Function*************************************************************
+
+  Synopsis    [Computes interpolant of the proof.]
+
+  Description [Aassuming that global vars and A-clauses are marked.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sat_ProofTest( veci * pClauses, veci * pProof, veci * pVars, veci * pRoots, int hRoot, veci * pGlobVars )
+{
+    Vec_Int_t * vClauses  = (Vec_Int_t *)pClauses;
+    Vec_Int_t * vProof    = (Vec_Int_t *)pProof;
+    Vec_Int_t * vVars     = (Vec_Int_t *)pVars;
+    Vec_Int_t * vRoots    = (Vec_Int_t *)pRoots;
+    Vec_Int_t * vGlobVars = (Vec_Int_t *)pGlobVars;
+    Vec_Int_t * vUsed;
+//    int i, Entry;
+
+    // collect visited clauses
+    vUsed = Proof_CollectUsed( vProof, NULL, hRoot );
+    Proof_CleanCollected( vProof, vUsed );
+//    Vec_IntForEachEntry( vUsed, Entry, i )
+//        printf( "%d ", Entry );
+//    printf( "\n" );
+
+    printf( "Found %d useful resolution nodes.\n", Vec_IntSize(vUsed) );
+    Vec_IntFree( vUsed );
+    vUsed = Proof_CollectAll( vProof );
+    printf( "Found %d total  resolution nodes.\n", Vec_IntSize(vUsed) );
+    Vec_IntFree( vUsed );
+
+    Proof_Check( vClauses, vProof, hRoot );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index 72e36894..a7628239 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -86,12 +86,12 @@ struct varinfo_t
     unsigned val    :  2;  // variable value 
     unsigned pol    :  1;  // last polarity
     unsigned glo    :  1;  // global variable
-    unsigned tag    :  3;  // conflict analysis tags
-    unsigned lev    : 25;  // variable level
+    unsigned tag    :  4;  // conflict analysis tags
+    unsigned lev    : 24;  // variable level
 };
 
 int    var_is_global (sat_solver2* s, int v)            { return s->vi[v].glo; }
-void   var_set_global(sat_solver2* s, int v, int glo)   { s->vi[v].glo = glo;  }
+void   var_set_global(sat_solver2* s, int v, int glo)   { s->vi[v].glo = glo; if (glo) veci_push(&s->glob_vars, v); }
 
 static inline int     var_value     (sat_solver2* s, int v)            { return s->vi[v].val; }
 static inline int     var_polar     (sat_solver2* s, int v)            { return s->vi[v].pol; }
@@ -104,13 +104,13 @@ static inline void    var_set_level (sat_solver2* s, int v, int lev)   { s->vi[v
 // variable tags
 static inline int     var_tag       (sat_solver2* s, int v)            { return s->vi[v].tag; }
 static inline void    var_set_tag   (sat_solver2* s, int v, int tag)   { 
-    assert( tag > 0 && tag < 8 );
+    assert( tag > 0 && tag < 16 );
     if ( s->vi[v].tag == 0 )
         veci_push( &s->tagged, v );
     s->vi[v].tag = tag;                           
 }
 static inline void    var_add_tag   (sat_solver2* s, int v, int tag)   { 
-    assert( tag > 0 && tag < 8 );
+    assert( tag > 0 && tag < 16 );
     if ( s->vi[v].tag == 0 )
         veci_push( &s->tagged, v );
     s->vi[v].tag |= tag;                           
@@ -139,44 +139,30 @@ static inline void    solver2_clear_marks(sat_solver2* s)              {
     veci_resize(&s->mark_levels,0);
 }
 
-// other inlines
-//static inline int     var_reason    (sat_solver2* s, int v)            { return (s->reasons[v]&1) ? 0 : s->reasons[v] >> 1;                   } 
-//static inline int     lit_reason    (sat_solver2* s, int l)            { return (s->reasons[lit_var(l)&1]) ? 0 : s->reasons[lit_var(l)] >> 1; } 
-static inline int     var_reason    (sat_solver2* s, int v)            { return s->reasons[v]; } 
-static inline int     lit_reason    (sat_solver2* s, int l)            { return s->reasons[lit_var(l)]; } 
-
 //=================================================================================================
 // Clause datatype + minor functions:
 
-typedef struct satset_t satset;
-struct satset_t 
-{
-    unsigned learnt :  1;
-    unsigned mark   :  1;
-    unsigned partA  :  1;
-    unsigned nLits  : 29;
-    int      Id;
-    lit      pLits[0];
-};
-
-static inline satset* get_clause    (sat_solver2* s, int c)      { return c ? (satset*)(veci_begin(&s->clauses) + c) : NULL;  }
-static inline cla     clause_id     (sat_solver2* s, satset* c)  { return (cla)((int *)c - veci_begin(&s->clauses));          }
-static inline int     clause_size   (int nLits)                  { return sizeof(satset)/4 + nLits;                           }
-static inline int     clause_proofid(sat_solver2* s, satset* c)  { return c->learnt ? veci_begin(&s->claProofs)[c->Id]<<1 : (clause_id(s,c)<<1) | 1;  }
+static inline satset* clause_read   (sat_solver2* s, cla h)      { return satset_read( &s->clauses, h );    }
+static inline cla     clause_handle (sat_solver2* s, satset* c)  { return satset_handle( &s->clauses, c );  }
+static inline int     clause_check  (sat_solver2* s, satset* c)  { return satset_check( &s->clauses, c );   }
+static inline int     clause_proofid(sat_solver2* s, satset* c)  { return c->learnt ? veci_begin(&s->claProofs)[c->Id]<<1 : (clause_handle(s,c)<<1) | 1;                   }
+
+//static inline int     var_reason    (sat_solver2* s, int v)      { return (s->reasons[v]&1) ? 0 : s->reasons[v] >> 1;                   } 
+//static inline int     lit_reason    (sat_solver2* s, int l)      { return (s->reasons[lit_var(l)&1]) ? 0 : s->reasons[lit_var(l)] >> 1; } 
+//static inline satset* var_unit_clause(sat_solver2* s, int v)           { return (s->reasons[v]&1) ? clause_read(s, s->reasons[v] >> 1) : NULL;  } 
+//static inline void    var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(i && !s->reasons[v]); s->reasons[v] = (i << 1) | 1;             } 
+static inline int     var_reason    (sat_solver2* s, int v)      { return s->reasons[v];           } 
+static inline int     lit_reason    (sat_solver2* s, int l)      { return s->reasons[lit_var(l)];  } 
+static inline satset* var_unit_clause(sat_solver2* s, int v)           { return clause_read(s, s->units[v]);                                          } 
+static inline void    var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(v >= 0 && v < s->size && !s->units[v]); s->units[v] = i; s->nUnits++; } 
 
 // these two only work after creating a clause before the solver is called
-int    clause_is_partA (sat_solver2* s, int cid)                 { return get_clause(s, cid)->partA;                          }  
-void   clause_set_partA(sat_solver2* s, int cid, int partA)      { get_clause(s, cid)->partA = partA;                         }
-
-//static inline satset* var_unit_clause(sat_solver2* s, int v)           { return (s->reasons[v]&1) ? get_clause(s, s->reasons[v] >> 1) : NULL;  } 
-//static inline void    var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(i && !s->reasons[v]); s->reasons[v] = (i << 1) | 1;            } 
-static inline satset* var_unit_clause(sat_solver2* s, int v)           { return get_clause(s, s->units[v]);                                           } 
-static inline void    var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(v >= 0 && v < s->size && !s->units[v]); s->units[v] = i; s->nUnits++; } 
+int    clause_is_partA (sat_solver2* s, int h)                   { return clause_read(s, h)->partA;         }  
+void   clause_set_partA(sat_solver2* s, int h, int partA)        { clause_read(s, h)->partA = partA;        }
+int    clause_id(sat_solver2* s, int h)                          { return clause_read(s, h)->Id;            }
 
-#define sat_solver_foreach_clause( s, c, i )  \
-    for ( i = 1; (i < s->nMemSize) && (((c) = get_clause(s, i)), 1); i += clause_size(c->nLits) )
-#define sat_solver_foreach_learnt( s, c, i )  \
-    for ( i = s->iFirstLearnt; (i < s->nMemSize) && (((c) = get_clause(s, i)), 1); i += clause_size(c->nLits) )
+#define sat_solver_foreach_clause( s, c, h )  satset_foreach_entry( &s->clauses, c, h, 1 )
+#define sat_solver_foreach_learnt( s, c, h )  satset_foreach_entry( &s->clauses, c, h, s->iLearntFirst )
 
 //=================================================================================================
 // Simple helpers:
@@ -219,7 +205,7 @@ static inline int proof_chain_stop( sat_solver2* s )
         int RetValue = s->iStartChain;
         satset* c = (satset*)(veci_begin(&s->proof_clas) + s->iStartChain);
         assert( s->iStartChain > 0 && s->iStartChain < veci_size(&s->proof_clas) );
-        c->nLits = veci_size(&s->proof_clas) - s->iStartChain - 2;
+        c->nEnts = veci_size(&s->proof_clas) - s->iStartChain - 2;
         s->iStartChain = 0;
         return RetValue;
     }
@@ -396,11 +382,11 @@ static int clause_new(sat_solver2* s, lit* begin, lit* end, int learnt, int proo
     assert(nLits < 1 || lit_var(begin[0]) < s->size);
     assert(nLits < 2 || lit_var(begin[1]) < s->size);
     // add memory if needed
-    if ( veci_size(&s->clauses) + clause_size(nLits) > s->clauses.cap )
+    if ( veci_size(&s->clauses) + satset_size(nLits) > s->clauses.cap )
     {
         int nMemAlloc = s->clauses.cap ? 2 * s->clauses.cap : (1 << 20);
         s->clauses.ptr = ABC_REALLOC( int, veci_begin(&s->clauses), nMemAlloc );
-        memset( veci_begin(&s->clauses) + s->clauses.cap, 0, sizeof(int) * (nMemAlloc - s->clauses.cap) );
+//        memset( veci_begin(&s->clauses) + s->clauses.cap, 0, sizeof(int) * (nMemAlloc - s->clauses.cap) );
 //        printf( "Reallocing from %d to %d...\n", s->clauses.cap, nMemAlloc );
         s->clauses.cap = nMemAlloc;
         if ( veci_size(&s->clauses) == 0 )
@@ -408,10 +394,11 @@ static int clause_new(sat_solver2* s, lit* begin, lit* end, int learnt, int proo
     }
     // create clause
     c = (satset*)(veci_begin(&s->clauses) + veci_size(&s->clauses));
+    ((int*)c)[0] = 0;
     c->learnt = learnt;
-    c->nLits  = nLits;
+    c->nEnts  = nLits;
     for (i = 0; i < nLits; i++)
-        c->pLits[i] = begin[i];
+        c->pEnts[i] = begin[i];
     // assign clause ID
     if ( learnt )
     {
@@ -434,14 +421,14 @@ static int clause_new(sat_solver2* s, lit* begin, lit* end, int learnt, int proo
 
     // extend storage
     Cid = veci_size(&s->clauses);
-    s->clauses.size += clause_size(nLits);
+    s->clauses.size += satset_size(nLits);
     assert( veci_size(&s->clauses) <= s->clauses.cap );
     assert(((ABC_PTRUINT_T)c & 3) == 0);
 
     // remember the last one and first learnt
-    s->fLastConfId = Cid;
-    if ( learnt && s->iFirstLearnt == -1 )
-        s->iFirstLearnt = Cid;
+    s->iLearntLast = Cid;
+    if ( learnt && s->iLearntFirst == -1 )
+        s->iLearntFirst = Cid;
 
     // watch the clause
     if ( nLits > 1 ){
@@ -614,9 +601,9 @@ static int solver2_analyze_final(sat_solver2* s, satset* conf, int skip_first)
         return -1;
     proof_chain_start( s, conf );
     assert( veci_size(&s->tagged) == 0 );
-    for ( i = skip_first; i < (int)conf->nLits; i++ )
+    for ( i = skip_first; i < (int)conf->nEnts; i++ )
     {
-        x = lit_var(conf->pLits[i]);
+        x = lit_var(conf->pEnts[i]);
         if ( var_level(s,x) )
             var_set_tag(s, x, 1);
         else
@@ -627,11 +614,11 @@ static int solver2_analyze_final(sat_solver2* s, satset* conf, int skip_first)
     for (i = s->qtail-1; i >= (veci_begin(&s->trail_lim))[0]; i--){
         x = lit_var(s->trail[i]);
         if (var_tag(s,x)){
-            satset* c = get_clause(s, var_reason(s,x));
+            satset* c = clause_read(s, var_reason(s,x));
             if (c){
                 proof_chain_resolve( s, c, x );
-                for (j = 1; j < (int)c->nLits; j++) {
-                    x = lit_var(c->pLits[j]);
+                for (j = 1; j < (int)c->nEnts; j++) {
+                    x = lit_var(c->pEnts[j]);
                     if ( var_level(s,x) )
                         var_set_tag(s, x, 1);
                     else
@@ -664,14 +651,14 @@ static int solver2_lit_removable_rec(sat_solver2* s, int v)
         return (var_tag(s,v) & 4) > 0;
 
     // skip decisions on a wrong level
-    c = get_clause(s, var_reason(s,v));
+    c = clause_read(s, var_reason(s,v));
     if ( c == NULL ){
         var_add_tag(s,v,2);
         return 0;
     }
 
-    for ( i = 1; i < (int)c->nLits; i++ ){
-        x = lit_var(c->pLits[i]);
+    for ( i = 1; i < (int)c->nEnts; i++ ){
+        x = lit_var(c->pEnts[i]);
         if (var_tag(s,x) & 1)
             solver2_lit_removable_rec(s, x);
         else{
@@ -715,9 +702,9 @@ static int solver2_lit_removable(sat_solver2* s, int x)
             veci_push(&s->stack, x ^ 1 );
         }
         x >>= 1;
-        c = get_clause(s, var_reason(s,x));
-        for (i = 1; i < (int)c->nLits; i++){
-            x = lit_var(c->pLits[i]);
+        c = clause_read(s, var_reason(s,x));
+        for (i = 1; i < (int)c->nEnts; i++){
+            x = lit_var(c->pEnts[i]);
             if (var_tag(s,x) || !var_level(s,x))
                 continue;
             if (!var_reason(s,x) || !var_lev_mark(s,x)){
@@ -749,11 +736,11 @@ static void solver2_logging_order(sat_solver2* s, int x)
         }
         veci_push(&s->stack, x ^ 1 );
         x >>= 1;
-        c = get_clause(s, var_reason(s,x));
+        c = clause_read(s, var_reason(s,x));
 //        if ( !c )
 //            printf( "solver2_logging_order(): Error in conflict analysis!!!\n" );
-        for (i = 1; i < (int)c->nLits; i++){
-            x = lit_var(c->pLits[i]);
+        for (i = 1; i < (int)c->nEnts; i++){
+            x = lit_var(c->pEnts[i]);
             if ( !var_level(s,x) || (var_tag(s,x) & 1) )
                 continue;
             veci_push(&s->stack, x << 1);
@@ -762,6 +749,22 @@ static void solver2_logging_order(sat_solver2* s, int x)
     }
 }
 
+static void solver2_logging_order_rec(sat_solver2* s, int x)
+{
+    satset* c;
+    int i, y;
+    if ( (var_tag(s,x) & 8) )
+        return;
+    c = clause_read(s, var_reason(s,x));
+    for (i = 1; i < (int)c->nEnts; i++){
+        y = lit_var(c->pEnts[i]);
+        if ( var_level(s,y) && (var_tag(s,y) & 1) == 0 )
+            solver2_logging_order_rec(s, y);
+    }
+    var_add_tag(s, x, 8);
+    veci_push(&s->min_step_order, x);
+}
+
 static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt)
 {
     int cnt      = 0;
@@ -780,8 +783,8 @@ static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt)
         assert(c != 0);
         if (c->learnt)
             act_clause_bump(s,c);
-        for ( j = (int)(p != lit_Undef); j < (int)c->nLits; j++){
-            x = lit_var(c->pLits[j]);
+        for ( j = (int)(p != lit_Undef); j < (int)c->nEnts; j++){
+            x = lit_var(c->pEnts[j]);
             assert(x >= 0 && x < s->size);
             if ( var_tag(s, x) )
                 continue;
@@ -795,13 +798,13 @@ static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt)
             if (var_level(s,x) == solver2_dlevel(s))
                 cnt++;
             else
-                veci_push(learnt,c->pLits[j]);
+                veci_push(learnt,c->pEnts[j]);
         }
 
         while (!var_tag(s, lit_var(s->trail[ind--])));
 
         p = s->trail[ind+1];
-        c = get_clause(s, lit_reason(s,p));
+        c = clause_read(s, lit_reason(s,p));
         cnt--;
         if ( cnt == 0 )
             break;
@@ -818,8 +821,8 @@ static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt)
     // simplify (full)
     veci_resize(&s->min_lit_order, 0);
     for (i = j = 1; i < veci_size(learnt); i++){
-//        if (!solver2_lit_removable_rec(s,lit_var(lits[i]))) // changed to vars!!!
-        if (!solver2_lit_removable( s,lit_var(lits[i])) )
+//        if (!solver2_lit_removable( s,lit_var(lits[i])) )
+        if (!solver2_lit_removable_rec(s,lit_var(lits[i]))) // changed to vars!!!
             lits[j++] = lits[i];
     } 
 
@@ -830,16 +833,17 @@ static int solver2_analyze(sat_solver2* s, satset* c, veci* learnt)
         veci_resize(&s->min_step_order, 0);
         vars = veci_begin(&s->min_lit_order);
         for (i = 0; i < veci_size(&s->min_lit_order); i++)
-            solver2_logging_order( s, vars[i] );
+//            solver2_logging_order( s, vars[i] );
+            solver2_logging_order_rec( s, vars[i] );
 
         // add them in the reverse order
         vars = veci_begin(&s->min_step_order);
         for (i = veci_size(&s->min_step_order); i > 0; ) { i--;
-            c = get_clause(s, var_reason(s,vars[i]));
+            c = clause_read(s, var_reason(s,vars[i]));
             proof_chain_resolve( s, c, vars[i] );
-            for ( k = 1; k < (int)c->nLits; k++ )
+            for ( k = 1; k < (int)c->nEnts; k++ )
             {
-                x = lit_var(c->pLits[k]);
+                x = lit_var(c->pEnts[k]);
                 if ( var_level(s,x) == 0 )
                     proof_chain_resolve( s, NULL, x );
             }
@@ -908,8 +912,8 @@ satset* solver2_propagate(sat_solver2* s)
         s->simpdb_props--;
 
         for (i = j = begin; i < end; ){
-            c = get_clause(s,*i);
-            lits = c->pLits;
+            c = clause_read(s,*i);
+            lits = c->pEnts;
 
             // Make sure the false literal is data[1]:
             false_lit = lit_neg(p);
@@ -924,7 +928,7 @@ satset* solver2_propagate(sat_solver2* s)
                 *j++ = *i;
             else{
                 // Look for new watch:
-                stop = lits + c->nLits;
+                stop = lits + c->nEnts;
                 for (k = lits + 2; k < stop; k++){
                     if (var_value(s, lit_var(*k)) != !lit_sign(*k)){
                         lits[1] = *k;
@@ -939,9 +943,9 @@ satset* solver2_propagate(sat_solver2* s)
                     int fLitIsFalse = (var_value(s, Var) == !lit_sign(lits[0])); 
                     // Log production of top-level unit clause:
                     proof_chain_start( s, c );
-                    for ( k = 1; k < (int)c->nLits; k++ )
+                    for ( k = 1; k < (int)c->nEnts; k++ )
                     {
-                        int x = lit_var(c->pLits[k]);
+                        int x = lit_var(c->pEnts[k]);
                         assert( var_level(s, x) == 0 );
                         proof_chain_resolve( s, NULL, x );
                     }
@@ -955,7 +959,7 @@ satset* solver2_propagate(sat_solver2* s)
                         var_set_unit_clause(s, Var, Cid);
                     else{
                         // Empty clause derived:
-                        proof_chain_start( s, get_clause(s,Cid) );
+                        proof_chain_start( s, clause_read(s,Cid) );
                         proof_chain_resolve( s, NULL, Var );
                         proof_id = proof_chain_stop( s );
                         clause_new( s, lits, lits, 1, proof_id );
@@ -965,7 +969,7 @@ satset* solver2_propagate(sat_solver2* s)
                 *j++ = *i;
                 // Clause is unit under assignment:
                 if (!solver2_enqueue(s,lits[0], *i)){
-                    confl = get_clause(s,*i++);
+                    confl = clause_read(s,*i++);
                     // Copy the remaining watches:
                     while (i < end)
                         *j++ = *i++;
@@ -984,18 +988,18 @@ WatchFound: i++;
 
 static void clause_remove(sat_solver2* s, satset* c)
 {
-    assert(lit_neg(c->pLits[0]) < s->size*2);
-    assert(lit_neg(c->pLits[1]) < s->size*2);
+    assert(lit_neg(c->pEnts[0]) < s->size*2);
+    assert(lit_neg(c->pEnts[1]) < s->size*2);
 
-    veci_remove(solver2_wlist(s,lit_neg(c->pLits[0])),clause_id(s,c));
-    veci_remove(solver2_wlist(s,lit_neg(c->pLits[1])),clause_id(s,c));
+    veci_remove(solver2_wlist(s,lit_neg(c->pEnts[0])),clause_handle(s,c));
+    veci_remove(solver2_wlist(s,lit_neg(c->pEnts[1])),clause_handle(s,c));
 
     if (c->learnt){
         s->stats.learnts--;
-        s->stats.learnts_literals -= c->nLits;
+        s->stats.learnts_literals -= c->nEnts;
     }else{
         s->stats.clauses--;
-        s->stats.clauses_literals -= c->nLits;
+        s->stats.clauses_literals -= c->nEnts;
     }
 }
 
@@ -1004,8 +1008,8 @@ static lbool clause_simplify(sat_solver2* s, satset* c)
 {
     int i;
     assert(solver2_dlevel(s) == 0);
-    for (i = 0; i < (int)c->nLits; i++){
-        if (var_value(s, lit_var(c->pLits[i])) == lit_sign(c->pLits[i]))
+    for (i = 0; i < (int)c->nEnts; i++){
+        if (var_value(s, lit_var(c->pEnts[i])) == lit_sign(c->pEnts[i]))
             return l_True;
     }
     return l_False;
@@ -1026,8 +1030,8 @@ int sat_solver2_simplify(sat_solver2* s)
         int*  cls = (int*)veci_begin(cs);
         int i, j;
         for (j = i = 0; i < veci_size(cs); i++){
-            satset* c = get_clause(s,cls[i]);
-            if (lit_reason(s,c->pLits[0]) != cls[i] &&
+            satset* c = clause_read(s,cls[i]);
+            if (lit_reason(s,c->pEnts[0]) != cls[i] &&
                 clause_simplify(s,c) == l_True)
                 clause_remove(s,c), Counter++;
             else
@@ -1067,7 +1071,7 @@ void solver2_reducedb(sat_solver2* s)
         {
             assert( c->Id == k );
             c->mark = 0;
-            if ( c->nLits > 2 && lit_reason(s,c->pLits[0]) != Cid && (k < nLearnts/2 || pActs[k] < extra_lim) )
+            if ( c->nEnts > 2 && lit_reason(s,c->pEnts[0]) != Cid && (k < nLearnts/2 || pActs[k] < extra_lim) )
             {
                 c->mark = 1;
                 Counter++;
@@ -1216,14 +1220,15 @@ sat_solver2* sat_solver2_new(void)
     veci_new(&s->mark_levels);
     veci_new(&s->min_lit_order); 
     veci_new(&s->min_step_order);
+    veci_new(&s->glob_vars);
     veci_new(&s->proof_clas); veci_push(&s->proof_clas, -1);
     veci_new(&s->proof_vars); veci_push(&s->proof_vars, -1);
     veci_new(&s->claActs);    veci_push(&s->claActs,    -1);
     veci_new(&s->claProofs);  veci_push(&s->claProofs,  -1);
 
     // initialize other
-    s->iFirstLearnt           = -1; // the first learnt clause 
-    s->fLastConfId            = -1; // the last learnt clause 
+    s->iLearntFirst           = -1; // the first learnt clause 
+    s->iLearntLast            = -1; // the last learnt clause 
 #ifdef USE_FLOAT_ACTIVITY
     s->var_inc                = 1;
     s->cla_inc                = 1;
@@ -1245,9 +1250,9 @@ sat_solver2* sat_solver2_new(void)
     if ( s->fProofLogging )
     {
         s->proof_clas.cap = (1 << 20);
-        s->proof_clas.ptr = ABC_ALLOC( int, s->proof_clas.cap );
+        s->proof_clas.ptr = ABC_REALLOC( int, s->proof_clas.ptr, s->proof_clas.cap );
         s->proof_vars.cap = (1 << 20);
-        s->proof_vars.ptr = ABC_ALLOC( int, s->proof_clas.cap );
+        s->proof_vars.ptr = ABC_REALLOC( int, s->proof_vars.ptr, s->proof_clas.cap );
     }
     return s;
 }
@@ -1294,10 +1299,19 @@ void sat_solver2_setnvars(sat_solver2* s,int n)
 
 void sat_solver2_delete(sat_solver2* s)
 {
+    satset * c = clause_read(s, s->iLearntLast);
     // report statistics
     assert( veci_size(&s->proof_clas) == veci_size(&s->proof_vars) );
     printf( "Used %6.2f Mb for proof-logging.   Unit clauses = %d.\n", 8.0 * veci_size(&s->proof_clas) / (1<<20), s->nUnits );
 
+    Sat_ProofTest( 
+        &s->clauses,      // clauses
+        &s->proof_clas,   // proof clauses
+        &s->proof_vars,   // proof variables
+        NULL,             // proof roots
+        veci_begin(&s->claProofs)[c->Id],  // one root
+        &s->glob_vars );  // global variables (for interpolation)
+
     // delete vectors
     veci_delete(&s->order);
     veci_delete(&s->trail_lim);
@@ -1309,6 +1323,7 @@ void sat_solver2_delete(sat_solver2* s)
     veci_delete(&s->mark_levels);
     veci_delete(&s->min_lit_order);
     veci_delete(&s->min_step_order);
+    veci_delete(&s->glob_vars);
     veci_delete(&s->proof_clas);
     veci_delete(&s->proof_vars);
     veci_delete(&s->claActs);
@@ -1320,7 +1335,10 @@ void sat_solver2_delete(sat_solver2* s)
         int i;
         if ( s->wlists )
             for (i = 0; i < s->size*2; i++)
+            {
+//                printf( "%d ", s->wlists[i].size );
                 veci_delete(&s->wlists[i]);
+            }
         ABC_FREE(s->wlists   );
         ABC_FREE(s->vi       );
         ABC_FREE(s->trail    );
@@ -1461,7 +1479,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
 //    lbool*  values        = s->assigns;
     lit*    i;
 
-    s->fLastConfId = -1;
+    s->iLearntLast = -1;
 
     // set the external limits
 //    s->nCalls++;
@@ -1542,7 +1560,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
         veci_push(&s->trail_lim,s->qtail);
         if (!solver2_enqueue(s,p,0))
         {
-            satset* r = get_clause(s, lit_reason(s,p));
+            satset* r = clause_read(s, lit_reason(s,p));
             if (r != NULL)
             {
                 satset* confl = r;
diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h
index c64a4213..1cdc8bd9 100644
--- a/src/sat/bsat/satSolver2.h
+++ b/src/sat/bsat/satSolver2.h
@@ -41,39 +41,41 @@ struct sat_solver2_t;
 typedef struct sat_solver2_t sat_solver2;
 
 extern sat_solver2* sat_solver2_new(void);
-extern void        sat_solver2_delete(sat_solver2* s);
+extern void         sat_solver2_delete(sat_solver2* s);
 
-extern int         sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end);
-extern int         sat_solver2_simplify(sat_solver2* s);
-extern int         sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal);
+extern int          sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end);
+extern int          sat_solver2_simplify(sat_solver2* s);
+extern int          sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal);
 
-extern void        sat_solver2_setnvars(sat_solver2* s,int n);
+extern void         sat_solver2_setnvars(sat_solver2* s,int n);
 
-extern void        Sat_Solver2WriteDimacs( sat_solver2 * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars );
-extern void        Sat_Solver2PrintStats( FILE * pFile, sat_solver2 * p );
-extern int *       Sat_Solver2GetModel( sat_solver2 * p, int * pVars, int nVars );
-extern void        Sat_Solver2DoubleClauses( sat_solver2 * p, int iVar );
+extern void         Sat_Solver2WriteDimacs( sat_solver2 * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars );
+extern void         Sat_Solver2PrintStats( FILE * pFile, sat_solver2 * p );
+extern int *        Sat_Solver2GetModel( sat_solver2 * p, int * pVars, int nVars );
+extern void         Sat_Solver2DoubleClauses( sat_solver2 * p, int iVar );
 
 // trace recording
-extern void        sat_solver2TraceStart( sat_solver2 * pSat, char * pName );
-extern void        sat_solver2TraceStop( sat_solver2 * pSat );
-extern void        sat_solver2TraceWrite( sat_solver2 * pSat, int * pBeg, int * pEnd, int fRoot );
+extern void         sat_solver2TraceStart( sat_solver2 * pSat, char * pName );
+extern void         sat_solver2TraceStop( sat_solver2 * pSat );
+extern void         sat_solver2TraceWrite( sat_solver2 * pSat, int * pBeg, int * pEnd, int fRoot );
 
 // clause storage
-extern void        sat_solver2_store_alloc( sat_solver2 * s );
-extern void        sat_solver2_store_write( sat_solver2 * s, char * pFileName );
-extern void        sat_solver2_store_free( sat_solver2 * s );
-extern void        sat_solver2_store_mark_roots( sat_solver2 * s );
-extern void        sat_solver2_store_mark_clauses_a( sat_solver2 * s );
-extern void *      sat_solver2_store_release( sat_solver2 * s ); 
+extern void         sat_solver2_store_alloc( sat_solver2 * s );
+extern void         sat_solver2_store_write( sat_solver2 * s, char * pFileName );
+extern void         sat_solver2_store_free( sat_solver2 * s );
+extern void         sat_solver2_store_mark_roots( sat_solver2 * s );
+extern void         sat_solver2_store_mark_clauses_a( sat_solver2 * s );
+extern void *       sat_solver2_store_release( sat_solver2 * s ); 
 
 // global variables
-extern int         var_is_global (sat_solver2* s, int v);
-extern void        var_set_global(sat_solver2* s, int v, int glo);
+extern int          var_is_global (sat_solver2* s, int v);
+extern void         var_set_global(sat_solver2* s, int v, int glo);
 // clause grouping (these two only work after creating a clause before the solver is called)
-extern int         clause_is_partA (sat_solver2* s, int cid);
-extern void        clause_set_partA(sat_solver2* s, int cid, int partA);
-
+extern int          clause_is_partA (sat_solver2* s, int handle);
+extern void         clause_set_partA(sat_solver2* s, int handle, int partA);
+// other clause functions
+extern int          clause_id(sat_solver2* s, int h);
+ 
 
 //=================================================================================================
 // Solver representation:
@@ -83,75 +85,105 @@ typedef struct varinfo_t varinfo;
 
 struct sat_solver2_t
 {
-    int           size;          // nof variables
-    int           cap;           // size of varmaps
-    int           qhead;         // Head index of queue.
-    int           qtail;         // Tail index of queue.
-
-    int           root_level;    // Level of first proper decision.
-    int           simpdb_assigns;// Number of top-level assignments at last 'simplifyDB()'.
-    int           simpdb_props;  // Number of propagations before next 'simplifyDB()'.
-    double        random_seed;
-    double        progress_estimate;
-    int           verbosity;     // Verbosity level. 0=silent, 1=some progress report, 2=everything
-    int           fNotUseRandom; // do not allow random decisions with a fixed probability
-//    int           fSkipSimplify; // set to one to skip simplification of the clause database
-    int           fProofLogging; // enable proof-logging
+    int             size;           // nof variables
+    int             cap;            // size of varmaps
+    int             qhead;          // Head index of queue.
+    int             qtail;          // Tail index of queue.
+
+    int             root_level;     // Level of first proper decision.
+    int             simpdb_assigns; // Number of top-level assignments at last 'simplifyDB()'.
+    int             simpdb_props;   // Number of propagations before next 'simplifyDB()'.
+    double          random_seed;
+    double          progress_estimate;
+    int             verbosity;      // Verbosity level. 0=silent, 1=some progress report, 2=everything
+    int             fNotUseRandom;  // do not allow random decisions with a fixed probability
+//  int             fSkipSimplify;  // set to one to skip simplification of the clause database
+    int             fProofLogging;  // enable proof-logging
 
     // clauses
-    veci          clauses;       // clause memory
-    veci*         wlists;        // watcher lists (for each literal)
-    int           iFirstLearnt;  // the first learnt clause 
+    veci            clauses;        // clause memory
+    veci*           wlists;         // watcher lists (for each literal)
+    int             iLearntFirst;   // the first learnt clause 
+    int             iLearntLast;    // in proof-logging mode, the ID of the final conflict clause (conf_final)
 
     // activities
 #ifdef USE_FLOAT_ACTIVITY
-    double        var_inc;       // Amount to bump next variable with.
-    double        var_decay;     // INVERSE decay factor for variable activity: stores 1/decay. 
-    float         cla_inc;       // Amount to bump next clause with.
-    float         cla_decay;     // INVERSE decay factor for clause activity: stores 1/decay.
-    double*       activity;      // A heuristic measurement of the activity of a variable.
+    double          var_inc;        // Amount to bump next variable with.
+    double          var_decay;      // INVERSE decay factor for variable activity: stores 1/decay. 
+    float           cla_inc;        // Amount to bump next clause with.
+    float           cla_decay;      // INVERSE decay factor for clause activity: stores 1/decay.
+    double*         activity;       // A heuristic measurement of the activity of a variable.
 #else
-    int           var_inc;       // Amount to bump next variable with.
-    int           cla_inc;       // Amount to bump next clause with.
-    unsigned*     activity;      // A heuristic measurement of the activity of a variable.
+    int             var_inc;        // Amount to bump next variable with.
+    int             cla_inc;        // Amount to bump next clause with.
+    unsigned*       activity;       // A heuristic measurement of the activity of a variable.
 #endif
-    veci          claActs;       // clause activities
-    veci          claProofs;     // clause proofs
+    veci            claActs;        // clause activities
+    veci            claProofs;      // clause proofs
 
     // internal state
-    varinfo *     vi;            // variable information
-    lit*          trail;         // sequence of assignment and implications
-    int*          orderpos;      // Index in variable order.
-    cla*          reasons;       // reason clauses
-    cla*          units;         // unit clauses
-
-    veci          tagged;        // (contains: var)
-    veci          stack;         // (contains: var)
-    veci          order;         // Variable order. (heap) (contains: var)
-    veci          trail_lim;     // Separator indices for different decision levels in 'trail'. (contains: int)
-    veci          temp_clause;   // temporary storage for a CNF clause
-    veci          model;         // If problem is solved, this vector contains the model (contains: lbool).
-    veci          conf_final;    // If problem is unsatisfiable (possibly under assumptions),
-                                 // this vector represent the final conflict clause expressed in the assumptions.
-    veci          mark_levels;   // temporary storage for labeled levels
-    veci          min_lit_order; // ordering of removable literals
-    veci          min_step_order;// ordering of resolution steps
+    varinfo *       vi;             // variable information
+    lit*            trail;          // sequence of assignment and implications
+    int*            orderpos;       // Index in variable order.
+    cla*            reasons;        // reason clauses
+    cla*            units;          // unit clauses
+
+    veci            tagged;         // (contains: var)
+    veci            stack;          // (contains: var)
+    veci            order;          // Variable order. (heap) (contains: var)
+    veci            trail_lim;      // Separator indices for different decision levels in 'trail'. (contains: int)
+    veci            temp_clause;    // temporary storage for a CNF clause
+    veci            model;          // If problem is solved, this vector contains the model (contains: lbool).
+    veci            conf_final;     // If problem is unsatisfiable (possibly under assumptions),
+                                    // this vector represent the final conflict clause expressed in the assumptions.
+    veci            mark_levels;    // temporary storage for labeled levels
+    veci            min_lit_order;  // ordering of removable literals
+    veci            min_step_order; // ordering of resolution steps
+    veci            glob_vars;      // global variables
 
     // proof logging
-    veci          proof_clas;    // sequence of proof clauses
-    veci          proof_vars;    // sequence of proof variables 
-    int           iStartChain;   // temporary variable to remember beginning of the current chain in proof logging
-    int           fLastConfId;   // in proof-logging mode, the ID of the final conflict clause (conf_final)
-    int           nUnits;        // the total number of unit clauses
+    veci            proof_clas;     // sequence of proof clauses
+    veci            proof_vars;     // sequence of proof variables 
+    int             iStartChain;    // temporary variable to remember beginning of the current chain in proof logging
+    int             nUnits;         // the total number of unit clauses
 
     // statistics
-    stats_t       stats;
-    ABC_INT64_T   nConfLimit;    // external limit on the number of conflicts
-    ABC_INT64_T   nInsLimit;     // external limit on the number of implications
-    int           nRuntimeLimit; // external limit on runtime
+    stats_t         stats;
+    ABC_INT64_T     nConfLimit;     // external limit on the number of conflicts
+    ABC_INT64_T     nInsLimit;      // external limit on the number of implications
+    int             nRuntimeLimit;  // external limit on runtime
+};
 
+typedef struct satset_t satset;
+struct satset_t 
+{
+    unsigned learnt :  1;
+    unsigned mark   :  1;
+    unsigned partA  :  1;
+    unsigned nEnts  : 29;
+    int      Id;
+    lit      pEnts[0];
 };
 
+static inline satset* satset_read   (veci* p, cla h )     { return h ? (satset*)(veci_begin(p) + h) : NULL;                           }
+static inline cla     satset_handle (veci* p, satset* c)  { return (cla)((int *)c - veci_begin(p));                                   }
+static inline int     satset_check  (veci* p, satset* c)  { return (int*)c > veci_begin(p) && (int*)c < veci_begin(p) + veci_size(p); }
+static inline int     satset_size   (int nLits)           { return sizeof(satset)/4 + nLits;                                          }
+static inline void    satset_print  (satset * c)          { 
+    int i;
+    printf( "{ " );
+    for ( i = 0; i < (int)c->nEnts; i++ )
+        printf( "%d ", (c->pEnts[i] & 1)? -(c->pEnts[i] >> 1) : c->pEnts[i] >> 1 );
+    printf( "}\n" );
+}
+
+
+#define satset_foreach_entry( p, c, h, s )  \
+    for ( h = s; (h < veci_size(p)) && (((c) = satset_read(p, h)), 1); h += satset_size(c->nEnts) )
+
+//=================================================================================================
+// Public APIs:
+
 static inline int sat_solver2_nvars(sat_solver2* s)
 {
     return s->size;
@@ -213,6 +245,8 @@ static inline int sat_solver2_set_random(sat_solver2* s, int fNotUseRandom)
     return fNotUseRandomOld;
 }
 
+extern void Sat_ProofTest( veci * pClauses, veci * pProof, veci * pVars, veci * pRoots, int hRoot, veci * pGlobVars );
+
 ABC_NAMESPACE_HEADER_END
 
 #endif
diff --git a/src/sat/bsat/satVec.h b/src/sat/bsat/satVec.h
index 1f63ba1e..441ec974 100644
--- a/src/sat/bsat/satVec.h
+++ b/src/sat/bsat/satVec.h
@@ -29,15 +29,15 @@ ABC_NAMESPACE_HEADER_START
 
 // vector of 32-bit intergers (added for 64-bit portability)
 struct veci_t {
-    int    size;
     int    cap;
+    int    size;
     int*   ptr;
 };
 typedef struct veci_t veci;
 
 static inline void veci_new (veci* v) {
-    v->size = 0;
     v->cap  = 4;
+    v->size = 0;
     v->ptr  = (int*)ABC_ALLOC( char, sizeof(int)*v->cap);
 }
 
@@ -68,8 +68,8 @@ static inline void   veci_remove(veci* v, int e)
 
 // vector of 32- or 64-bit pointers
 struct vecp_t {
-    int    size;
     int    cap;
+    int    size;
     void** ptr;
 };
 typedef struct vecp_t vecp;