Proof-logging in the updated solver.

src/sat/bsat/satProof.c

@@ -60,15 +60,18 @@ static inline cla     Proof_NodeHandle (Vec_Int_t* p, satset* c)  { return satse
 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;     }
 
+// iterating through nodes in the proof
 #define Proof_ForeachNode( p, pNode, h )                         \
     for ( h = 1; (h < Vec_IntSize(p)) && ((pNode) = Proof_NodeRead(p, h)); h += Proof_NodeSize(pNode->nEnts) )
 #define Proof_ForeachNodeVec( pVec, p, pNode, i )            \
     for ( i = 0; (i < Vec_IntSize(pVec)) && ((pNode) = Proof_NodeRead(p, Vec_IntEntry(pVec,i))); i++ )
+
+// iterating through fanins of a proof node
 #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] >> 2)), 1); i++ )
 #define Proof_NodeForeachLeaf( pLeaves, pNode, pLeaf, i )    \
     for ( i = 0; (i < (int)pNode->nEnts) && (((pLeaf) = (pNode->pEnts[i] & 1) ? Proof_NodeRead(pLeaves, pNode->pEnts[i] >> 2) : NULL), 1); i++ )
-#define Proof_NodeForeachFaninRoot( p, pLeaves, pNode, pFanin, i )    \
+#define Proof_NodeForeachFaninLeaf( p, pLeaves, pNode, pFanin, i )    \
     for ( i = 0; (i < (int)pNode->nEnts) && ((pFanin) = (pNode->pEnts[i] & 1) ? Proof_NodeRead(pLeaves, pNode->pEnts[i] >> 2) : Proof_NodeRead(p, pNode->pEnts[i] >> 2)); i++ )
 
 ////////////////////////////////////////////////////////////////////////
@@ -77,6 +80,26 @@ static inline int     Proof_NodeSize   (int nEnts)                { return sizeo
 
 /**Function*************************************************************
 
+  Synopsis    [Returns the number of proof nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Proof_CountAll( Vec_Int_t * p )
+{
+    satset * pNode;
+    int hNode, Counter = 0;
+    Proof_ForeachNode( p, pNode, hNode )
+        Counter++;
+    return Counter;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Collects all resolution nodes belonging to the proof.]
 
   Description []
@@ -187,7 +210,8 @@ Vec_Int_t * Proof_CollectUsedIter( Vec_Int_t * vProof, Vec_Int_t * vRoots, int h
             Proof_CollectUsed_iter( vProof, pNode, vUsed, vStack );
     }
     Vec_IntFree( vStack );
-    Abc_PrintTime( 1, "Iterative clause collection time", clock() - clk );
+//    Abc_PrintTime( 1, "Iterative clause collection time", clock() - clk );
+
 /*
     // verify topological order
     iPrev = 0;
@@ -200,7 +224,7 @@ Vec_Int_t * Proof_CollectUsedIter( Vec_Int_t * vProof, Vec_Int_t * vRoots, int h
     clk = clock();
 //    Vec_IntSort( vUsed, 0 );
     Abc_Sort( Vec_IntArray(vUsed), Vec_IntSize(vUsed) );
-    Abc_PrintTime( 1, "Postprocessing with sorting time", clock() - clk );
+//    Abc_PrintTime( 1, "Postprocessing with sorting time", clock() - clk );
 
     // verify topological order
     iPrev = 0;
@@ -394,46 +418,6 @@ void Proof_Check( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hRoot )
 
 /**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 * vProof, Vec_Int_t * vRoots )
-{
-    Vec_Int_t * vUsed;
-    satset * pNode, * pFanin;
-    int i, k, nSize = 1;
-    // collect visited nodes
-    vUsed = Proof_CollectUsedIter( vProof, vRoots, 0 );
-    // relabel nodes to use smaller space
-    Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
-    {
-        pNode->Id = nSize;
-        nSize += Proof_NodeSize(pNode->nEnts);
-        Proof_NodeForeachFanin( vProof, pNode, pFanin, k )
-            if ( pFanin )
-                pNode->pEnts[i] = (pFanin->Id << 2) | (pNode->pEnts[i] & 2);
-    }
-    // compact the nodes
-    Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
-    {
-        memmove( Vec_IntArray(vProof) + pNode->Id, pNode, Proof_NodeSize(pNode->nEnts) );
-        pNode->Id = 0;
-    }
-    // report the result
-    printf( "The proof was reduced from %d to %d (by %6.2f %%)\n", 
-        Vec_IntSize(vProof), nSize, 100.0 * (Vec_IntSize(vProof) - nSize) / Vec_IntSize(vProof) );
-    Vec_IntShrink( vProof, nSize );
-}
-
-
-/**Function*************************************************************
-
   Synopsis    [Collects nodes belonging to the UNSAT core.]
 
   Description [The result is the array of root clause indexes.]
@@ -545,7 +529,7 @@ Aig_Man_t * Sat_ProofInterpolant( Vec_Int_t * vClauses, Vec_Int_t * vProof, int
     Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
     {
         assert( pNode->nEnts > 1 );
-        Proof_NodeForeachFaninRoot( vProof, vClauses, pNode, pFanin, k )
+        Proof_NodeForeachFaninLeaf( vProof, vClauses, pNode, pFanin, k )
         {
             if ( k == 0 )
                 pObj = Aig_ObjFromLit( pAig, pFanin->Id );
@@ -573,7 +557,66 @@ Aig_Man_t * Sat_ProofInterpolant( Vec_Int_t * vClauses, Vec_Int_t * vProof, int
     Vec_IntFree( vCoreNums );
     return pAig;
 }
+ 
+/**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( veci * pProof, veci * pRoots )
+{
+    int fVerbose = 0;
+    Vec_Int_t * vProof = (Vec_Int_t *)pProof;
+    Vec_Int_t * vRoots = (Vec_Int_t *)pRoots;
+    Vec_Int_t * vUsed;
+    satset * pNode, * pFanin;
+    int i, k, hTemp, hNewHandle = 1, clk = clock();
+    static int TimeTotal = 0;
+
+    // collect visited nodes
+    vUsed = Proof_CollectUsedIter( vProof, vRoots, 0 );
+//    printf( "The proof uses %d out of %d proof nodes (%.2f %%)\n", 
+//        Vec_IntSize(vUsed), Proof_CountAll(vProof), 
+//        100.0 * Vec_IntSize(vUsed) / Proof_CountAll(vProof) );
+
+    // relabel nodes to use smaller space
+    Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
+    {
+        pNode->Id = hNewHandle; hNewHandle += Proof_NodeSize(pNode->nEnts);
+        Proof_NodeForeachFanin( vProof, pNode, pFanin, k )
+            if ( pFanin )
+            {
+                assert( (pNode->pEnts[k] >> 2) == Proof_NodeHandle(vProof, pFanin) );
+                pNode->pEnts[k] = (pFanin->Id << 2) | (pNode->pEnts[k] & 2);
+            }
+    }
+    // update roots
+    Proof_ForeachNodeVec( vRoots, vProof, pNode, i )
+        Vec_IntWriteEntry( vRoots, i, pNode->Id );
+    // compact the nodes
+    Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
+    {
+        hTemp = pNode->Id; pNode->Id = 0;
+        memmove( Vec_IntArray(vProof) + hTemp, pNode, sizeof(int)*Proof_NodeSize(pNode->nEnts) );
+    }
+    Vec_IntFree( vUsed );
 
+    // report the result
+    if ( fVerbose )
+    {
+        printf( "The proof was reduced from %10d to %10d integers (by %6.2f %%)  ", 
+            Vec_IntSize(vProof), hNewHandle, 100.0 * (Vec_IntSize(vProof) - hNewHandle) / Vec_IntSize(vProof) );
+        TimeTotal += clock() - clk;
+        Abc_PrintTime( 1, "Time", TimeTotal );
+    }
+    Vec_IntShrink( vProof, hNewHandle );
+}
 
 /**Function*************************************************************
 
@@ -591,7 +634,7 @@ void Sat_ProofTest( veci * pClauses, veci * pProof, veci * pRoots, int hRoot )
     Vec_Int_t * vClauses  = (Vec_Int_t *)pClauses;
     Vec_Int_t * vProof    = (Vec_Int_t *)pProof;
     Vec_Int_t * vRoots    = (Vec_Int_t *)pRoots;
-    Vec_Int_t * vUsed, * vCore;
+//    Vec_Int_t * vUsed, * vCore;
 //    int i, Entry;
 /*
     // collect visited clauses
@@ -600,6 +643,7 @@ void Sat_ProofTest( veci * pClauses, veci * pProof, veci * pRoots, int hRoot )
     printf( "Found %d useful resolution nodes.\n", Vec_IntSize(vUsed) );
     Vec_IntFree( vUsed );
 */
+/*
     // collect visited clauses
     vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot );
     Proof_CleanCollected( vProof, vUsed );
@@ -608,7 +652,7 @@ void Sat_ProofTest( veci * pClauses, veci * pProof, veci * pRoots, int hRoot )
 
     vCore = Sat_ProofCore( vClauses, vProof, hRoot );
     Vec_IntFree( vCore );
-
+*/
 /*
     printf( "Found %d useful resolution nodes.\n", Vec_IntSize(vUsed) );
     Vec_IntFree( vUsed );

src/sat/bsat/satSolver.c

@@ -805,7 +805,6 @@ static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt)
     }
 
     // update size of learnt + statistics
-    s->stats.max_literals += veci_size(learnt);
     veci_resize(learnt,j);
     s->stats.tot_literals += j;
 
@@ -1150,7 +1149,6 @@ sat_solver* sat_solver_new(void)
     s->stats.clauses_literals = 0;
     s->stats.learnts          = 0;
     s->stats.learnts_literals = 0;
-    s->stats.max_literals     = 0;
     s->stats.tot_literals     = 0;
 
 #ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT

src/sat/bsat/satSolver2.h

@@ -103,8 +103,8 @@ struct sat_solver2_t
     // clauses
     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)
+    int             hLearntFirst;   // the first learnt clause 
+    int             hLearntLast;    // in proof-logging mode, the ID of the final conflict clause (conf_final)
 
     // activities
 #ifdef USE_FLOAT_ACTIVITY
@@ -139,10 +139,10 @@ struct sat_solver2_t
     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
+    veci            learnt_live;    // remaining clauses after reduce DB
 
     // proof logging
-    veci            proof_clas;     // sequence of proof clauses
+    veci            proofs;         // sequence of proof records
     int             iStartChain;    // temporary variable to remember beginning of the current chain in proof logging
     int             nUnits;         // the total number of unit clauses
 
@@ -178,6 +178,8 @@ static inline void    satset_print  (satset * c)          {
 
 #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) )
+#define satset_foreach_entry_vec( pVec, p, c, i )     \
+    for ( i = 0; (i < veci_size(pVec)) && ((c) = satset_read(p, veci_begin(pVec)[i])); i++ )
 #define satset_foreach_var( p, var, i, start )        \
     for ( i = start; (i < (int)(p)->nEnts) && ((var) = lit_var((p)->pEnts[i])); i++ )
 

src/sat/bsat/satVec.h

@@ -139,8 +139,9 @@ static inline int  lit_check(lit l, int n) { return l >= 0 && lit_var(l) < n;
 
 struct stats_t
 {
-    ABC_INT64_T   starts, decisions, propagations, inspects, conflicts;
-    ABC_INT64_T   clauses, clauses_literals, learnts, learnts_literals, max_literals, tot_literals;
+    unsigned starts, clauses, learnts;
+    ABC_INT64_T decisions, propagations, inspects, conflicts;
+    ABC_INT64_T clauses_literals, learnts_literals, tot_literals;
 };
 typedef struct stats_t stats_t;