Version abc80130_2

16 files changed, 135 insertions, 65 deletions

diff --git a/src/sat/msat/msat.h b/src/sat/msat/msat.h
index 21ddcb81..53353ba6 100644
--- a/src/sat/msat/msat.h
+++ b/src/sat/msat/msat.h
@@ -21,6 +21,10 @@
 #ifndef __MSAT_H__
 #define __MSAT_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -65,7 +69,7 @@ typedef enum { MSAT_FALSE = -1, MSAT_UNKNOWN = 0, MSAT_TRUE = 1 } Msat_Type_t;
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                       MACRO DEFITIONS                            ///
+///                       MACRO DEFINITIONS                          ///
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
@@ -76,10 +80,10 @@ typedef enum { MSAT_FALSE = -1, MSAT_UNKNOWN = 0, MSAT_TRUE = 1 } Msat_Type_t;
 extern bool             Msat_SolverParseDimacs( FILE * pFile, Msat_Solver_t ** p, int fVerbose );
 /*=== satSolver.c ===========================================================*/
 // adding vars, clauses, simplifying the database, and solving
-extern bool             Msat_SolverAddVar( Msat_Solver_t * p );
+extern bool             Msat_SolverAddVar( Msat_Solver_t * p, int Level );
 extern bool             Msat_SolverAddClause( Msat_Solver_t * p, Msat_IntVec_t * pLits );
 extern bool             Msat_SolverSimplifyDB( Msat_Solver_t * p );
-extern bool             Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * pVecAssumps, int nBackTrackLimit );
+extern bool             Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * pVecAssumps, int nBackTrackLimit, int nTimeLimit );
 // printing stats, assignments, and clauses
 extern void             Msat_SolverPrintStats( Msat_Solver_t * p );
 extern void             Msat_SolverPrintAssignment( Msat_Solver_t * p );
@@ -87,17 +91,20 @@ extern void             Msat_SolverPrintClauses( Msat_Solver_t * p );
 extern void             Msat_SolverWriteDimacs( Msat_Solver_t * p, char * pFileName );
 // access to the solver internal data
 extern int              Msat_SolverReadVarNum( Msat_Solver_t * p );
+extern int              Msat_SolverReadClauseNum( Msat_Solver_t * p );
 extern int              Msat_SolverReadVarAllocNum( Msat_Solver_t * p );
 extern int *            Msat_SolverReadAssignsArray( Msat_Solver_t * p );
 extern int *            Msat_SolverReadModelArray( Msat_Solver_t * p );
 extern unsigned         Msat_SolverReadTruth( Msat_Solver_t * p );
 extern int              Msat_SolverReadBackTracks( Msat_Solver_t * p );
+extern int              Msat_SolverReadInspects( Msat_Solver_t * p );
 extern void             Msat_SolverSetVerbosity( Msat_Solver_t * p, int fVerbose );
 extern void             Msat_SolverSetProofWriting( Msat_Solver_t * p, int fProof );
 extern void             Msat_SolverSetVarTypeA( Msat_Solver_t * p, int Var );
 extern void             Msat_SolverSetVarMap( Msat_Solver_t * p, Msat_IntVec_t * vVarMap );
 extern void             Msat_SolverMarkLastClauseTypeA( Msat_Solver_t * p );
 extern void             Msat_SolverMarkClausesStart( Msat_Solver_t * p );
+extern float *          Msat_SolverReadFactors( Msat_Solver_t * p );
 // returns the solution after incremental solving
 extern int              Msat_SolverReadSolutions( Msat_Solver_t * p );
 extern int *            Msat_SolverReadSolutionsArray( Msat_Solver_t * p );
@@ -153,8 +160,13 @@ extern double           Msat_VarHeapReadMaxWeight( Msat_VarHeap_t * p );
 extern int              Msat_VarHeapCountNodes( Msat_VarHeap_t * p, double WeightLimit );  
 extern int              Msat_VarHeapReadMax( Msat_VarHeap_t * p );  
 extern int              Msat_VarHeapGetMax( Msat_VarHeap_t * p );  
+ 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-#endif
diff --git a/src/sat/msat/msatActivity.c b/src/sat/msat/msatActivity.c
index c9a518ce..1cd795bd 100644
--- a/src/sat/msat/msatActivity.c
+++ b/src/sat/msat/msatActivity.c
@@ -25,7 +25,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -45,7 +45,9 @@ void Msat_SolverVarBumpActivity( Msat_Solver_t * p, Msat_Lit_t Lit )
     if ( p->dVarDecay < 0 ) // (negative decay means static variable order -- don't bump)
         return;
     Var = MSAT_LIT2VAR(Lit);
-    if ( (p->pdActivity[Var] += p->dVarInc) > 1e100 )
+    p->pdActivity[Var] += p->dVarInc;
+//    p->pdActivity[Var] += p->dVarInc * p->pFactors[Var];
+    if ( p->pdActivity[Var] > 1e100 )
         Msat_SolverVarRescaleActivity( p );
     Msat_OrderUpdate( p->pOrder, Var );
 }
diff --git a/src/sat/msat/msatClause.c b/src/sat/msat/msatClause.c
index dc39bee6..2ba8cd32 100644
--- a/src/sat/msat/msatClause.c
+++ b/src/sat/msat/msatClause.c
@@ -36,7 +36,7 @@ struct Msat_Clause_t_
 };
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -82,6 +82,10 @@ bool Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearned,
         // nSeenId - 1 stands for negative
         // nSeenId     stands for positive
         // Remove false literals
+
+        // there is a bug here!!!!
+        // when the same var in opposite polarities is given, it drops one polarity!!!
+
         for ( i = j = 0; i < nLits; i++ ) {
             // get the corresponding variable
             Var  = MSAT_LIT2VAR(pLits[i]);
@@ -190,6 +194,7 @@ bool Msat_ClauseCreate( Msat_Solver_t * p, Msat_IntVec_t * vLits, bool fLearned,
         {
             Msat_SolverVarBumpActivity( p, pLits[i] );
 //            Msat_SolverVarBumpActivity( p, pLits[i] );
+//            p->pFreq[ MSAT_LIT2VAR(pLits[i]) ]++;
         }
     }
 
diff --git a/src/sat/msat/msatClauseVec.c b/src/sat/msat/msatClauseVec.c
index 7c24619f..04691cf2 100644
--- a/src/sat/msat/msatClauseVec.c
+++ b/src/sat/msat/msatClauseVec.c
@@ -25,7 +25,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
diff --git a/src/sat/msat/msatInt.h b/src/sat/msat/msatInt.h
index 037616f6..03903abe 100644
--- a/src/sat/msat/msatInt.h
+++ b/src/sat/msat/msatInt.h
@@ -56,10 +56,10 @@ typedef long long   int64;
 #define ALLOC(type, num)    \
     ((type *) malloc(sizeof(type) * (num)))
 #define REALLOC(type, obj, num)    \
-    (obj) ? ((type *) realloc((char *) obj, sizeof(type) * (num))) : \
-        ((type *) malloc(sizeof(type) * (num)))
+    ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
+        ((type *) malloc(sizeof(type) * (num))))
 #define FREE(obj)        \
-    ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
+    ((obj) ? (free((char *)(obj)), (obj) = 0) : 0)
 
 // By default, custom memory management is used
 // which guarantees constant time allocation/deallocation 
@@ -119,6 +119,7 @@ struct Msat_Solver_t_
     double              dClaDecay;   // INVERSE decay factor for clause activity: stores 1/decay.
 
     double *            pdActivity;  // A heuristic measurement of the activity of a variable.
+    float *             pFactors;    // the multiplicative factors of variable activity
     double              dVarInc;     // Amount to bump next variable with.
     double              dVarDecay;   // INVERSE decay factor for variable activity: stores 1/decay. Use negative value for static variable order.
     Msat_Order_t *      pOrder;      // Keeps track of the decision variable order.
@@ -151,6 +152,7 @@ struct Msat_Solver_t_
     int                 nSeenId;     // the id of current seeing
     Msat_IntVec_t *     vReason;     // the temporary array of literals
     Msat_IntVec_t *     vTemp;       // the temporary array of literals
+    int *               pFreq;       // the number of times each var participated in conflicts
 
     // the memory manager
     Msat_MmStep_t *     pMem;
@@ -184,7 +186,7 @@ struct Msat_IntVec_t_
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                       MACRO DEFITIONS                            ///
+///                       MACRO DEFINITIONS                          ///
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/msat/msatMem.c b/src/sat/msat/msatMem.c
index 2d178094..30bf4a96 100644
--- a/src/sat/msat/msatMem.c
+++ b/src/sat/msat/msatMem.c
@@ -72,7 +72,7 @@ struct Msat_MmStep_t_
 };
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -231,7 +231,7 @@ void Msat_MmFixedRestart( Msat_MmFixed_t * p )
     int i;
     char * pTemp;
 
-    // delocate all chunks except the first one
+    // deallocate all chunks except the first one
     for ( i = 1; i < p->nChunks; i++ )
         free( p->pChunks[i] );
     p->nChunks = 1;
diff --git a/src/sat/msat/msatOrderH.c b/src/sat/msat/msatOrderH.c
index ca034233..956e7fc6 100644
--- a/src/sat/msat/msatOrderH.c
+++ b/src/sat/msat/msatOrderH.c
@@ -58,7 +58,7 @@ static void Msat_HeapPercolateDown( Msat_Order_t * p, int i );
 extern int timeSelect;
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
diff --git a/src/sat/msat/msatOrderJ.c b/src/sat/msat/msatOrderJ.c
index 6067b40f..4db7ff7b 100644
--- a/src/sat/msat/msatOrderJ.c
+++ b/src/sat/msat/msatOrderJ.c
@@ -38,7 +38,7 @@ struct Msat_OrderVar_t_
 {
     Msat_OrderVar_t    * pNext;
     Msat_OrderVar_t    * pPrev;
-    int                 Num;
+    int                  Num;
 };
 
 // the ring of variables data structure (J-boundary)
@@ -82,7 +82,7 @@ extern int timeSelect;
 extern int timeAssign;
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -170,7 +170,8 @@ int Msat_OrderCheck( Msat_Order_t * p )
     Msat_OrderVar_t * pVar, * pNext;
     Msat_IntVec_t * vRound;
     int * pRound, nRound;
-    int * pVars, nVars, i;
+    int * pVars, nVars, i, k;
+    int Counter = 0;
 
     // go through all the variables in the boundary
     Msat_OrderRingForEachEntry( p->rVars.pRoot, pVar, pNext )
@@ -188,10 +189,14 @@ int Msat_OrderCheck( Msat_Order_t * p )
             if ( Msat_OrderVarIsAssigned(p, pRound[i]) )
                 break;
         }
-        assert( i != nRound );
-        if ( i != nRound )
-            return 0;
+//        assert( i != nRound );
+//        if ( i == nRound )
+//            return 0;
+        if ( i == nRound )
+            Counter++;
     }
+    if ( Counter > 0 )
+        printf( "%d(%d) ", Counter, p->rVars.nItems );
 
     // we may also check other unassigned variables in the cone
     // to make sure that if they are not in J-boundary, 
@@ -209,16 +214,16 @@ int Msat_OrderCheck( Msat_Order_t * p )
         vRound = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( p->pSat->vAdjacents, pVars[i] );
         nRound = Msat_IntVecReadSize( vRound );
         pRound = Msat_IntVecReadArray( vRound );
-        for ( i = 0; i < nRound; i++ )
+        for ( k = 0; k < nRound; k++ )
         {
-            if ( !Msat_OrderVarIsUsedInCone(p, pRound[i]) )
+            if ( !Msat_OrderVarIsUsedInCone(p, pRound[k]) )
                 continue;
-            if ( Msat_OrderVarIsAssigned(p, pRound[i]) )
+            if ( Msat_OrderVarIsAssigned(p, pRound[k]) )
                 break;
         }
-        assert( i == nRound );
-        if ( i == nRound )
-            return 0;
+//        assert( k == nRound );
+//        if ( k != nRound )
+//            return 0;
     }
     return 1;
 }
@@ -256,7 +261,7 @@ int Msat_OrderVarSelect( Msat_Order_t * p )
     Msat_OrderVar_t * pVar, * pNext, * pVarBest;
     double * pdActs = p->pSat->pdActivity;
     double dfActBest;
-    int clk = clock();
+//    int clk = clock();
 
     pVarBest = NULL;
     dfActBest = -1.0;
@@ -268,12 +273,13 @@ int Msat_OrderVarSelect( Msat_Order_t * p )
             pVarBest  = pVar;
         }
     }
-timeSelect += clock() - clk;
-timeAssign += clock() - clk;
+//timeSelect += clock() - clk;
+//timeAssign += clock() - clk;
 
 //if ( pVarBest && pVarBest->Num % 1000 == 0 )
 //printf( "%d ", p->rVars.nItems );
 
+//    Msat_OrderCheck( p );
     if ( pVarBest )
     {
         assert( Msat_OrderVarIsUsedInCone(p, pVarBest->Num) );
@@ -296,7 +302,7 @@ timeAssign += clock() - clk;
 void Msat_OrderVarAssigned( Msat_Order_t * p, int Var )
 {
     Msat_IntVec_t * vRound;
-    int i, clk = clock();
+    int i;//, clk = clock();
 
     // make sure the variable is in the boundary
     assert( Var < p->nVarsAlloc );
@@ -316,7 +322,7 @@ void Msat_OrderVarAssigned( Msat_Order_t * p, int Var )
             continue;
         Msat_OrderRingAddLast( &p->rVars, &p->pVars[vRound->pArray[i]] );
     }
-timeSelect += clock() - clk;
+//timeSelect += clock() - clk;
 //    Msat_OrderCheck( p );
 }
 
@@ -334,7 +340,7 @@ timeSelect += clock() - clk;
 void Msat_OrderVarUnassigned( Msat_Order_t * p, int Var )
 {
     Msat_IntVec_t * vRound, * vRound2;
-    int i, k, clk = clock();
+    int i, k;//, clk = clock();
 
     // make sure the variable is not in the boundary
     assert( Var < p->nVarsAlloc );
@@ -363,7 +369,7 @@ void Msat_OrderVarUnassigned( Msat_Order_t * p, int Var )
             if ( k == vRound2->nSize ) // there is no assigned vars, delete this one
                 Msat_OrderRingRemove( &p->rVars, &p->pVars[vRound->pArray[i]] );
         }
-timeSelect += clock() - clk;
+//timeSelect += clock() - clk;
 //    Msat_OrderCheck( p );
 }
 
@@ -450,7 +456,7 @@ void Msat_OrderRingRemove( Msat_OrderRing_t * pRing, Msat_OrderVar_t * pVar )
         pRing->pRoot = pVar->pNext;
     // move the root to the next entry after pVar
     // this way all the additions to the list will be traversed first
-//    pRing->pRoot = pVar->pNext;
+//    pRing->pRoot = pVar->pPrev;
     // delete the node
     pVar->pPrev->pNext = pVar->pNext;
     pVar->pNext->pPrev = pVar->pPrev;
diff --git a/src/sat/msat/msatQueue.c b/src/sat/msat/msatQueue.c
index c12cc75d..5938e042 100644
--- a/src/sat/msat/msatQueue.c
+++ b/src/sat/msat/msatQueue.c
@@ -33,7 +33,7 @@ struct Msat_Queue_t_
 };
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
diff --git a/src/sat/msat/msatRead.c b/src/sat/msat/msatRead.c
index b8e585a4..738562ef 100644
--- a/src/sat/msat/msatRead.c
+++ b/src/sat/msat/msatRead.c
@@ -27,7 +27,7 @@
 static char * Msat_FileRead( FILE * pFile );
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
diff --git a/src/sat/msat/msatSolverApi.c b/src/sat/msat/msatSolverApi.c
index ba506993..ee3507a6 100644
--- a/src/sat/msat/msatSolverApi.c
+++ b/src/sat/msat/msatSolverApi.c
@@ -27,7 +27,7 @@
 static void Msat_SolverSetupTruthTables( unsigned uTruths[][2] );
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -41,27 +41,30 @@ static void Msat_SolverSetupTruthTables( unsigned uTruths[][2] );
   SeeAlso     []
 
 ***********************************************************************/
-int                Msat_SolverReadVarNum( Msat_Solver_t * p )                  { return p->nVars;     }
-int                Msat_SolverReadVarAllocNum( Msat_Solver_t * p )             { return p->nVarsAlloc;}
+int                Msat_SolverReadVarNum( Msat_Solver_t * p )                  { return p->nVars;      }
+int                Msat_SolverReadClauseNum( Msat_Solver_t * p )               { return p->nClauses;   }
+int                Msat_SolverReadVarAllocNum( Msat_Solver_t * p )             { return p->nVarsAlloc; }
 int                Msat_SolverReadDecisionLevel( Msat_Solver_t * p )           { return Msat_IntVecReadSize(p->vTrailLim); }
-int *              Msat_SolverReadDecisionLevelArray( Msat_Solver_t * p )      { return p->pLevel;    }
-Msat_Clause_t **    Msat_SolverReadReasonArray( Msat_Solver_t * p )             { return p->pReasons;  }
+int *              Msat_SolverReadDecisionLevelArray( Msat_Solver_t * p )      { return p->pLevel;     }
+Msat_Clause_t **    Msat_SolverReadReasonArray( Msat_Solver_t * p )            { return p->pReasons;   }
 Msat_Lit_t          Msat_SolverReadVarValue( Msat_Solver_t * p, Msat_Var_t Var ) { return p->pAssigns[Var]; }
-Msat_ClauseVec_t *  Msat_SolverReadLearned( Msat_Solver_t * p )                 { return p->vLearned;  }
-Msat_ClauseVec_t ** Msat_SolverReadWatchedArray( Msat_Solver_t * p )            { return p->pvWatched; }
-int *              Msat_SolverReadAssignsArray( Msat_Solver_t * p )            { return p->pAssigns;  }
-int *              Msat_SolverReadModelArray( Msat_Solver_t * p )              { return p->pModel;  }
-int                Msat_SolverReadBackTracks( Msat_Solver_t * p )              { return p->nBackTracks; }
-Msat_MmStep_t *     Msat_SolverReadMem( Msat_Solver_t * p )                     { return p->pMem;      }
-int *              Msat_SolverReadSeenArray( Msat_Solver_t * p )               { return p->pSeen;     }
-int                Msat_SolverIncrementSeenId( Msat_Solver_t * p )             { return ++p->nSeenId; }
+Msat_ClauseVec_t *  Msat_SolverReadLearned( Msat_Solver_t * p )                { return p->vLearned;   }
+Msat_ClauseVec_t ** Msat_SolverReadWatchedArray( Msat_Solver_t * p )           { return p->pvWatched;  }
+int *              Msat_SolverReadAssignsArray( Msat_Solver_t * p )            { return p->pAssigns;   }
+int *              Msat_SolverReadModelArray( Msat_Solver_t * p )              { return p->pModel;     }
+int                Msat_SolverReadBackTracks( Msat_Solver_t * p )              { return (int)p->Stats.nConflicts; }
+int                Msat_SolverReadInspects( Msat_Solver_t * p )                { return (int)p->Stats.nInspects;  }
+Msat_MmStep_t *     Msat_SolverReadMem( Msat_Solver_t * p )                    { return p->pMem;       }
+int *              Msat_SolverReadSeenArray( Msat_Solver_t * p )               { return p->pSeen;      }
+int                Msat_SolverIncrementSeenId( Msat_Solver_t * p )             { return ++p->nSeenId;  }
 void               Msat_SolverSetVerbosity( Msat_Solver_t * p, int fVerbose )  { p->fVerbose = fVerbose; }
-void               Msat_SolverClausesIncrement( Msat_Solver_t * p )            { p->nClausesAlloc++;  }
-void               Msat_SolverClausesDecrement( Msat_Solver_t * p )            { p->nClausesAlloc--;  }
-void               Msat_SolverClausesIncrementL( Msat_Solver_t * p )           { p->nClausesAllocL++; }
-void               Msat_SolverClausesDecrementL( Msat_Solver_t * p )           { p->nClausesAllocL--; }
+void               Msat_SolverClausesIncrement( Msat_Solver_t * p )            { p->nClausesAlloc++;   }
+void               Msat_SolverClausesDecrement( Msat_Solver_t * p )            { p->nClausesAlloc--;   }
+void               Msat_SolverClausesIncrementL( Msat_Solver_t * p )           { p->nClausesAllocL++;  }
+void               Msat_SolverClausesDecrementL( Msat_Solver_t * p )           { p->nClausesAllocL--;  }
 void               Msat_SolverMarkLastClauseTypeA( Msat_Solver_t * p )         { Msat_ClauseSetTypeA( Msat_ClauseVecReadEntry( p->vClauses, Msat_ClauseVecReadSize(p->vClauses)-1 ), 1 ); }
 void               Msat_SolverMarkClausesStart( Msat_Solver_t * p )            { p->nClausesStart = Msat_ClauseVecReadSize(p->vClauses); }
+float *            Msat_SolverReadFactors( Msat_Solver_t * p )                 { return p->pFactors;   }
 
 /**Function*************************************************************
 
@@ -172,8 +175,12 @@ Msat_Solver_t * Msat_SolverAlloc( int nVarsAlloc,
     p->dVarDecay = dVarDecay;
 
     p->pdActivity = ALLOC( double, p->nVarsAlloc );
+    p->pFactors   = ALLOC( float, p->nVarsAlloc );
     for ( i = 0; i < p->nVarsAlloc; i++ )
-        p->pdActivity[i] = 0;
+    {
+        p->pdActivity[i] = 0.0;
+        p->pFactors[i]   = 1.0;
+    }
 
     p->pAssigns  = ALLOC( int, p->nVarsAlloc ); 
     p->pModel    = ALLOC( int, p->nVarsAlloc ); 
@@ -237,8 +244,12 @@ void Msat_SolverResize( Msat_Solver_t * p, int nVarsAlloc )
     p->nVarsAlloc = nVarsAlloc;
 
     p->pdActivity = REALLOC( double, p->pdActivity, p->nVarsAlloc );
+    p->pFactors   = REALLOC( float, p->pFactors, p->nVarsAlloc );
     for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
-        p->pdActivity[i] = 0;
+    {
+        p->pdActivity[i] = 0.0;
+        p->pFactors[i]   = 1.0;
+    }
 
     p->pAssigns  = REALLOC( int, p->pAssigns, p->nVarsAlloc );
     p->pModel    = REALLOC( int, p->pModel, p->nVarsAlloc );
@@ -392,6 +403,7 @@ void Msat_SolverFree( Msat_Solver_t * p )
     Msat_ClauseVecFree( p->vLearned );
 
     FREE( p->pdActivity );
+    FREE( p->pFactors );
     Msat_OrderFree( p->pOrder );
 
     for ( i = 0; i < 2 * p->nVarsAlloc; i++ )
diff --git a/src/sat/msat/msatSolverCore.c b/src/sat/msat/msatSolverCore.c
index b8d9f328..f9fee73c 100644
--- a/src/sat/msat/msatSolverCore.c
+++ b/src/sat/msat/msatSolverCore.c
@@ -25,7 +25,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -39,10 +39,11 @@
   SeeAlso     []
 
 ***********************************************************************/
-bool Msat_SolverAddVar( Msat_Solver_t * p )
+bool Msat_SolverAddVar( Msat_Solver_t * p, int Level )
 {
     if ( p->nVars == p->nVarsAlloc )
         Msat_SolverResize( p, 2 * p->nVarsAlloc );
+    p->pLevel[p->nVars] = Level;
     p->nVars++;
     return 1;
 }
@@ -131,14 +132,18 @@ void Msat_SolverPrintStats( Msat_Solver_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTrackLimit )
+bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTrackLimit, int nTimeLimit )
 {
     Msat_SearchParams_t Params = { 0.95, 0.999 };
     double nConflictsLimit, nLearnedLimit;
     Msat_Type_t Status;
+    int timeStart = clock();
     int64 nConflictsOld = p->Stats.nConflicts;
     int64 nDecisionsOld = p->Stats.nDecisions;
 
+//    p->pFreq = ALLOC( int, p->nVarsAlloc );
+//    memset( p->pFreq, 0, sizeof(int) * p->nVarsAlloc );
+ 
     if ( vAssumps )
     {
         int * pAssumps, nAssumps, i;
@@ -172,11 +177,31 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra
         nConflictsLimit *= 1.5;
         nLearnedLimit   *= 1.1;
         // if the limit on the number of backtracks is given, quit the restart loop
-        if ( nBackTrackLimit > 0 )
+        if ( nBackTrackLimit > 0 && (int)p->Stats.nConflicts - p->nBackTracks > nBackTrackLimit )
+            break;
+        // if the runtime limit is exceeded, quit the restart loop
+        if ( nTimeLimit > 0 && clock() - timeStart >= nTimeLimit * CLOCKS_PER_SEC )
             break;
     }
     Msat_SolverCancelUntil( p, 0 );
     p->nBackTracks = (int)p->Stats.nConflicts - p->nBackTracks;
+/*
+    PRT( "True solver runtime", clock() - timeStart );
+    // print the statistics
+    {
+        int i, Counter = 0;
+        for ( i = 0; i < p->nVars; i++ )
+            if ( p->pFreq[i] > 0 )
+            {
+                printf( "%d ", p->pFreq[i] );
+                Counter++;
+            }
+        if ( Counter )
+            printf( "\n" );
+        printf( "Total = %d. Used = %d.  Decisions = %d. Imps = %d. Conflicts = %d. ", p->nVars, Counter, (int)p->Stats.nDecisions, (int)p->Stats.nPropagations, (int)p->Stats.nConflicts );
+        PRT( "Time", clock() - timeStart );
+    }
+*/
     return Status;
 }
 
diff --git a/src/sat/msat/msatSolverIo.c b/src/sat/msat/msatSolverIo.c
index f17595a7..05b7f6a9 100644
--- a/src/sat/msat/msatSolverIo.c
+++ b/src/sat/msat/msatSolverIo.c
@@ -27,7 +27,7 @@
 static char * Msat_TimeStamp();
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
diff --git a/src/sat/msat/msatSolverSearch.c b/src/sat/msat/msatSolverSearch.c
index 13a0c403..11a6540c 100644
--- a/src/sat/msat/msatSolverSearch.c
+++ b/src/sat/msat/msatSolverSearch.c
@@ -31,7 +31,7 @@ static void            Msat_SolverAnalyze( Msat_Solver_t * p, Msat_Clause_t * pC
 static void            Msat_SolverReduceDB( Msat_Solver_t * p );
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -534,12 +534,18 @@ Msat_Type_t Msat_SolverSearch( Msat_Solver_t * p, int nConfLimit, int nLearnedLi
     Msat_Clause_t * pConf;
     Msat_Var_t Var;
     int nLevelBack, nConfs, nAssigns, Value;
+    int i;
 
     assert( Msat_SolverReadDecisionLevel(p) == p->nLevelRoot );
     p->Stats.nStarts++;
     p->dVarDecay = 1 / pPars->dVarDecay;
     p->dClaDecay = 1 / pPars->dClaDecay;
 
+    // reset the activities
+    for ( i = 0; i < p->nVars; i++ )
+       p->pdActivity[i] = (double)p->pFactors[i];
+//       p->pdActivity[i] = 0.0;
+
     nConfs = 0;
     while ( 1 )
     {
@@ -599,7 +605,7 @@ Msat_Type_t Msat_SolverSearch( Msat_Solver_t * p, int nConfLimit, int nLearnedLi
                 Msat_SolverCancelUntil( p, p->nLevelRoot );
                 return MSAT_UNKNOWN; 
             }
-            else if ( nBackTrackLimit > 0 && nConfs > nBackTrackLimit ) {
+            else if ( nBackTrackLimit > 0 && (int)p->Stats.nConflicts - p->nBackTracks > nBackTrackLimit ) {
                 // Reached bound on number of conflicts:
                 Msat_QueueClear( p->pQueue );
                 Msat_SolverCancelUntil( p, p->nLevelRoot );
diff --git a/src/sat/msat/msatSort.c b/src/sat/msat/msatSort.c
index 2198d303..3b89d102 100644
--- a/src/sat/msat/msatSort.c
+++ b/src/sat/msat/msatSort.c
@@ -41,7 +41,7 @@ static int irand(double seed, int size) {
 static void Msat_SolverSort( Msat_Clause_t ** array, int size, double seed );
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
diff --git a/src/sat/msat/msatVec.c b/src/sat/msat/msatVec.c
index 951969cf..75f53047 100644
--- a/src/sat/msat/msatVec.c
+++ b/src/sat/msat/msatVec.c
@@ -28,7 +28,7 @@ static int Msat_IntVecSortCompare1( int * pp1, int * pp2 );
 static int Msat_IntVecSortCompare2( int * pp1, int * pp2 );
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************