Version abc60916

12 files changed, 1404 insertions, 16 deletions

diff --git a/src/sat/asat/added.c b/src/sat/asat/added.c
index 100b823b..222693ad 100644
--- a/src/sat/asat/added.c
+++ b/src/sat/asat/added.c
@@ -220,7 +220,7 @@ void Asat_SolverSetPrefVars(solver * s, int * pPrefVars, int nPrefVars)
   SeeAlso     []
 
 ***********************************************************************/
-void Asat_SolverSetFactors(solver * s, int * pFactors)
+void Asat_SolverSetFactors(solver * s, float * pFactors)
 {
     assert( s->factors == NULL );
     s->factors = pFactors;
diff --git a/src/sat/asat/solver.c b/src/sat/asat/solver.c
index f2642c38..34b4d233 100644
--- a/src/sat/asat/solver.c
+++ b/src/sat/asat/solver.c
@@ -253,12 +253,11 @@ static inline void act_var_rescale(solver* s) {
 
 static inline void act_var_bump(solver* s, int v) {
     double* activity = s->activity;
-    if ((activity[v] += s->var_inc) > 1e100)
-//    if ((activity[v] += s->var_inc*s->factors[v]/100000000) > 1e100)
+    activity[v] += s->var_inc;
+//    activity[v] += s->var_inc * s->factors[v];
+    if (activity[v] > 1e100)
         act_var_rescale(s);
-
     //printf("bump %d %f\n", v-1, activity[v]);
-
     if ( s->pJMan == NULL && s->orderpos[v] != -1 )
         order_update(s,v);
 
@@ -842,6 +841,7 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts)
 
     int     conflictC       = 0;
     veci    learnt_clause;
+    int     i;
 
     assert(s->root_level == solver_dlevel(s));
 
@@ -851,6 +851,12 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts)
     veci_resize(&s->model,0);
     veci_new(&learnt_clause);
 
+    // reset the activities
+    if ( s->factors )
+        for ( i = 0; i < s->size; i++ )
+            s->activity[i] = (double)s->factors[i];
+//            s->activity[i] = 1.0;
+
     for (;;){
         clause* confl = solver_propagate(s);
         if (confl != 0){
diff --git a/src/sat/asat/solver.h b/src/sat/asat/solver.h
index 7edfb537..7a5e5be6 100644
--- a/src/sat/asat/solver.h
+++ b/src/sat/asat/solver.h
@@ -89,7 +89,7 @@ extern void    Asat_SolverWriteDimacs( solver * pSat, char * pFileName,
                                        int incrementVars);
 extern void    Asat_SatPrintStats( FILE * pFile, solver * p );
 extern void    Asat_SolverSetPrefVars( solver * s, int * pPrefVars, int nPrefVars );
-extern void    Asat_SolverSetFactors( solver * s, int * pFactors );
+extern void    Asat_SolverSetFactors( solver * s, float * pFactors );
 
 // J-frontier support
 extern Asat_JMan_t * Asat_JManStart( solver * pSat, void * vCircuit );
@@ -128,7 +128,7 @@ struct solver_t
 
     vec*     wlists;        // 
     double*  activity;      // A heuristic measurement of the activity of a variable.
-    int *    factors;       // the factor of variable activity
+    float *  factors;       // the factor of variable activity
     lbool*   assigns;       // Current values of variables.
     int*     orderpos;      // Index in variable order.
     clause** reasons;       //
diff --git a/src/sat/asat_fixed/satSolver.c b/src/sat/asat_fixed/satSolver.c
new file mode 100644
index 00000000..d3b99c9d
--- /dev/null
+++ b/src/sat/asat_fixed/satSolver.c
@@ -0,0 +1,1191 @@
+/**************************************************************************************************
+MiniSat -- Copyright (c) 2005, Niklas Sorensson
+http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko
+
+#include <stdio.h>
+#include <assert.h>
+#include <math.h>
+
+#include "solver.h"
+
+//=================================================================================================
+// Debug:
+
+//#define VERBOSEDEBUG
+
+// For derivation output (verbosity level 2)
+#define L_IND    "%-*d"
+#define L_ind    solver_dlevel(s)*3+3,solver_dlevel(s)
+#define L_LIT    "%sx%d"
+#define L_lit(p) lit_sign(p)?"~":"", (lit_var(p))
+
+// Just like 'assert()' but expression will be evaluated in the release version as well.
+static inline void check(int expr) { assert(expr); }
+
+static void printlits(lit* begin, lit* end)
+{
+    int i;
+    for (i = 0; i < end - begin; i++)
+        printf(L_LIT" ",L_lit(begin[i]));
+}
+
+//=================================================================================================
+// Random numbers:
+
+
+// Returns a random float 0 <= x < 1. Seed must never be 0.
+static inline double drand(double* seed) {
+    int q;
+    *seed *= 1389796;
+    q = (int)(*seed / 2147483647);
+    *seed -= (double)q * 2147483647;
+    return *seed / 2147483647; }
+
+
+// Returns a random integer 0 <= x < size. Seed must never be 0.
+static inline int irand(double* seed, int size) {
+    return (int)(drand(seed) * size); }
+
+
+//=================================================================================================
+// Predeclarations:
+
+void sort(void** array, int size, int(*comp)(const void *, const void *));
+
+//=================================================================================================
+// Clause datatype + minor functions:
+
+struct clause_t
+{
+    int size_learnt;
+    lit lits[0];
+};
+
+static inline int   clause_size       (clause* c)          { return c->size_learnt >> 1; }
+static inline lit*  clause_begin      (clause* c)          { return c->lits; }
+static inline int   clause_learnt     (clause* c)          { return c->size_learnt & 1; }
+static inline float clause_activity   (clause* c)          { return *((float*)&c->lits[c->size_learnt>>1]); }
+static inline void  clause_setactivity(clause* c, float a) { *((float*)&c->lits[c->size_learnt>>1]) = a; }
+
+//=================================================================================================
+// Encode literals in clause pointers:
+
+clause* clause_from_lit (lit l)     { return (clause*)((unsigned long)l + (unsigned long)l + 1);  }
+bool    clause_is_lit   (clause* c) { return ((unsigned long)c & 1);                              }
+lit     clause_read_lit (clause* c) { return (lit)((unsigned long)c >> 1);                        }
+
+//=================================================================================================
+// Simple helpers:
+
+static inline int     solver_dlevel(solver* s)    { return veci_size(&s->trail_lim); }
+static inline vecp*   solver_read_wlist     (solver* s, lit l){ return &s->wlists[l]; }
+static inline void    vecp_remove(vecp* v, void* e)
+{
+    void** ws = vecp_begin(v);
+    int    j  = 0;
+
+    for (; ws[j] != e  ; j++);
+    assert(j < vecp_size(v));
+    for (; j < vecp_size(v)-1; j++) ws[j] = ws[j+1];
+    vecp_resize(v,vecp_size(v)-1);
+}
+
+//=================================================================================================
+// Variable order functions:
+
+static inline void order_update(solver* s, int v) // updateorder
+{
+    int*    orderpos = s->orderpos;
+    double* activity = s->activity;
+    int*    heap     = veci_begin(&s->order);
+    int     i        = orderpos[v];
+    int     x        = heap[i];
+    int     parent   = (i - 1) / 2;
+
+    assert(s->orderpos[v] != -1);
+
+    while (i != 0 && activity[x] > activity[heap[parent]]){
+        heap[i]           = heap[parent];
+        orderpos[heap[i]] = i;
+        i                 = parent;
+        parent            = (i - 1) / 2;
+    }
+    heap[i]     = x;
+    orderpos[x] = i;
+}
+
+static inline void order_assigned(solver* s, int v) 
+{
+}
+
+static inline void order_unassigned(solver* s, int v) // undoorder
+{
+    int* orderpos = s->orderpos;
+    if (orderpos[v] == -1){
+        orderpos[v] = veci_size(&s->order);
+        veci_push(&s->order,v);
+        order_update(s,v);
+    }
+}
+
+static int  order_select(solver* s, float random_var_freq) // selectvar
+{
+    int*    heap;
+    double* activity;
+    int*    orderpos;
+
+    lbool* values = s->assigns;
+
+    // Random decision:
+    if (drand(&s->random_seed) < random_var_freq){
+        int next = irand(&s->random_seed,s->size);
+        assert(next >= 0 && next < s->size);
+        if (values[next] == l_Undef)
+            return next;
+    }
+
+    // Activity based decision:
+
+    heap     = veci_begin(&s->order);
+    activity = s->activity;
+    orderpos = s->orderpos;
+
+
+    while (veci_size(&s->order) > 0){
+        int    next  = heap[0];
+        int    size  = veci_size(&s->order)-1;
+        int    x     = heap[size];
+
+        veci_resize(&s->order,size);
+
+        orderpos[next] = -1;
+
+        if (size > 0){
+            double act   = activity[x];
+
+            int    i     = 0;
+            int    child = 1;
+
+
+            while (child < size){
+                if (child+1 < size && activity[heap[child]] < activity[heap[child+1]])
+                    child++;
+
+                assert(child < size);
+
+                if (act >= activity[heap[child]])
+                    break;
+
+                heap[i]           = heap[child];
+                orderpos[heap[i]] = i;
+                i                 = child;
+                child             = 2 * child + 1;
+            }
+            heap[i]           = x;
+            orderpos[heap[i]] = i;
+        }
+
+        if (values[next] == l_Undef)
+            return next;
+    }
+
+    return var_Undef;
+}
+
+//=================================================================================================
+// Activity functions:
+
+static inline void act_var_rescale(solver* s) {
+    double* activity = s->activity;
+    int i;
+    for (i = 0; i < s->size; i++)
+        activity[i] *= 1e-100;
+    s->var_inc *= 1e-100;
+}
+
+static inline void act_var_bump(solver* s, int v) {
+    double* activity = s->activity;
+    if ((activity[v] += s->var_inc) > 1e100)
+        act_var_rescale(s);
+
+    //printf("bump %d %f\n", v-1, activity[v]);
+
+    if (s->orderpos[v] != -1)
+        order_update(s,v);
+
+}
+
+static inline void act_var_decay(solver* s) { s->var_inc *= s->var_decay; }
+
+static inline void act_clause_rescale(solver* s) {
+    clause** cs = (clause**)vecp_begin(&s->learnts);
+    int i;
+    for (i = 0; i < vecp_size(&s->learnts); i++){
+        float a = clause_activity(cs[i]);
+        clause_setactivity(cs[i], a * (float)1e-20);
+    }
+    s->cla_inc *= (float)1e-20;
+}
+
+
+static inline void act_clause_bump(solver* s, clause *c) {
+    float a = clause_activity(c) + s->cla_inc;
+    clause_setactivity(c,a);
+    if (a > 1e20) act_clause_rescale(s);
+}
+
+static inline void act_clause_decay(solver* s) { s->cla_inc *= s->cla_decay; }
+
+
+//=================================================================================================
+// Clause functions:
+
+/* pre: size > 1 && no variable occurs twice
+ */
+static clause* clause_new(solver* s, lit* begin, lit* end, int learnt)
+{
+    int size;
+    clause* c;
+    int i;
+
+    assert(end - begin > 1);
+    assert(learnt >= 0 && learnt < 2);
+    size           = end - begin;
+    c              = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
+    c->size_learnt = (size << 1) | learnt;
+    assert(((unsigned int)c & 1) == 0);
+
+    for (i = 0; i < size; i++)
+        c->lits[i] = begin[i];
+
+    if (learnt)
+        *((float*)&c->lits[size]) = 0.0;
+
+    assert(begin[0] >= 0);
+    assert(begin[0] < s->size*2);
+    assert(begin[1] >= 0);
+    assert(begin[1] < s->size*2);
+
+    assert(lit_neg(begin[0]) < s->size*2);
+    assert(lit_neg(begin[1]) < s->size*2);
+
+    //vecp_push(solver_read_wlist(s,lit_neg(begin[0])),(void*)c);
+    //vecp_push(solver_read_wlist(s,lit_neg(begin[1])),(void*)c);
+
+    vecp_push(solver_read_wlist(s,lit_neg(begin[0])),(void*)(size > 2 ? c : clause_from_lit(begin[1])));
+    vecp_push(solver_read_wlist(s,lit_neg(begin[1])),(void*)(size > 2 ? c : clause_from_lit(begin[0])));
+
+    return c;
+}
+
+
+static void clause_remove(solver* s, clause* c)
+{
+    lit* lits = clause_begin(c);
+    assert(lit_neg(lits[0]) < s->size*2);
+    assert(lit_neg(lits[1]) < s->size*2);
+
+    //vecp_remove(solver_read_wlist(s,lit_neg(lits[0])),(void*)c);
+    //vecp_remove(solver_read_wlist(s,lit_neg(lits[1])),(void*)c);
+
+    assert(lits[0] < s->size*2);
+    vecp_remove(solver_read_wlist(s,lit_neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1])));
+    vecp_remove(solver_read_wlist(s,lit_neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0])));
+
+    if (clause_learnt(c)){
+        s->stats.learnts--;
+        s->stats.learnts_literals -= clause_size(c);
+    }else{
+        s->stats.clauses--;
+        s->stats.clauses_literals -= clause_size(c);
+    }
+
+    free(c);
+}
+
+
+static lbool clause_simplify(solver* s, clause* c)
+{
+    lit*   lits   = clause_begin(c);
+    lbool* values = s->assigns;
+    int i;
+
+    assert(solver_dlevel(s) == 0);
+
+    for (i = 0; i < clause_size(c); i++){
+        lbool sig = !lit_sign(lits[i]); sig += sig - 1;
+        if (values[lit_var(lits[i])] == sig)
+            return l_True;
+    }
+    return l_False;
+}
+
+//=================================================================================================
+// Minor (solver) functions:
+
+void solver_setnvars(solver* s,int n)
+{
+    int var;
+
+    if (s->cap < n){
+
+        while (s->cap < n) s->cap = s->cap*2+1;
+
+        s->wlists    = (vecp*)   realloc(s->wlists,   sizeof(vecp)*s->cap*2);
+        s->activity  = (double*) realloc(s->activity, sizeof(double)*s->cap);
+        s->assigns   = (lbool*)  realloc(s->assigns,  sizeof(lbool)*s->cap);
+        s->orderpos  = (int*)    realloc(s->orderpos, sizeof(int)*s->cap);
+        s->reasons   = (clause**)realloc(s->reasons,  sizeof(clause*)*s->cap);
+        s->levels    = (int*)    realloc(s->levels,   sizeof(int)*s->cap);
+        s->tags      = (lbool*)  realloc(s->tags,     sizeof(lbool)*s->cap);
+        s->trail     = (lit*)    realloc(s->trail,    sizeof(lit)*s->cap);
+    }
+
+    for (var = s->size; var < n; var++){
+        vecp_new(&s->wlists[2*var]);
+        vecp_new(&s->wlists[2*var+1]);
+        s->activity [var] = 0;
+        s->assigns  [var] = l_Undef;
+        s->orderpos [var] = veci_size(&s->order);
+        s->reasons  [var] = (clause*)0;
+        s->levels   [var] = 0;
+        s->tags     [var] = l_Undef;
+        
+        /* does not hold because variables enqueued at top level will not be reinserted in the heap
+           assert(veci_size(&s->order) == var); 
+         */
+        veci_push(&s->order,var);
+        order_update(s, var);
+    }
+
+    s->size = n > s->size ? n : s->size;
+}
+
+
+static inline bool enqueue(solver* s, lit l, clause* from)
+{
+    lbool* values = s->assigns;
+    int    v      = lit_var(l);
+    lbool  val    = values[v];
+#ifdef VERBOSEDEBUG
+    printf(L_IND"enqueue("L_LIT")\n", L_ind, L_lit(l));
+#endif
+
+    lbool sig = !lit_sign(l); sig += sig - 1;
+    if (val != l_Undef){
+        return val == sig;
+    }else{
+        // New fact -- store it.
+#ifdef VERBOSEDEBUG
+        printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(l));
+#endif
+        int*     levels  = s->levels;
+        clause** reasons = s->reasons;
+
+        values [v] = sig;
+        levels [v] = solver_dlevel(s);
+        reasons[v] = from;
+        s->trail[s->qtail++] = l;
+
+        order_assigned(s, v);
+        return true;
+    }
+}
+
+
+static inline void assume(solver* s, lit l){
+    assert(s->qtail == s->qhead);
+    assert(s->assigns[lit_var(l)] == l_Undef);
+#ifdef VERBOSEDEBUG
+    printf(L_IND"assume("L_LIT")\n", L_ind, L_lit(l));
+#endif
+    veci_push(&s->trail_lim,s->qtail);
+    enqueue(s,l,(clause*)0);
+}
+
+
+static inline void solver_canceluntil(solver* s, int level) {
+    lit*     trail;   
+    lbool*   values;  
+    clause** reasons; 
+    int      bound;
+    int      c;
+    
+    if (solver_dlevel(s) <= level)
+        return;
+
+    trail   = s->trail;
+    values  = s->assigns;
+    reasons = s->reasons;
+    bound   = (veci_begin(&s->trail_lim))[level];
+
+    for (c = s->qtail-1; c >= bound; c--) {
+        int     x  = lit_var(trail[c]);
+        values [x] = l_Undef;
+        reasons[x] = (clause*)0;
+    }
+
+    for (c = s->qhead-1; c >= bound; c--)
+        order_unassigned(s,lit_var(trail[c]));
+
+    s->qhead = s->qtail = bound;
+    veci_resize(&s->trail_lim,level);
+}
+
+static void solver_record(solver* s, veci* cls)
+{
+    lit*    begin = veci_begin(cls);
+    lit*    end   = begin + veci_size(cls);
+    clause* c     = (veci_size(cls) > 1) ? clause_new(s,begin,end,1) : (clause*)0;
+    enqueue(s,*begin,c);
+
+    assert(veci_size(cls) > 0);
+
+    if (c != 0) {
+        vecp_push(&s->learnts,c);
+        act_clause_bump(s,c);
+        s->stats.learnts++;
+        s->stats.learnts_literals += veci_size(cls);
+    }
+}
+
+
+static double solver_progress(solver* s)
+{
+    lbool*  values = s->assigns;
+    int*    levels = s->levels;
+    int     i;
+
+    double  progress = 0;
+    double  F        = 1.0 / s->size;
+    for (i = 0; i < s->size; i++)
+        if (values[i] != l_Undef)
+            progress += pow(F, levels[i]);
+    return progress / s->size;
+}
+
+//=================================================================================================
+// Major methods:
+
+static bool solver_lit_removable(solver* s, lit l, int minl)
+{
+    lbool*   tags    = s->tags;
+    clause** reasons = s->reasons;
+    int*     levels  = s->levels;
+    int      top     = veci_size(&s->tagged);
+
+    assert(lit_var(l) >= 0 && lit_var(l) < s->size);
+    assert(reasons[lit_var(l)] != 0);
+    veci_resize(&s->stack,0);
+    veci_push(&s->stack,lit_var(l));
+
+    while (veci_size(&s->stack) > 0){
+        clause* c;
+        int v = veci_begin(&s->stack)[veci_size(&s->stack)-1];
+        assert(v >= 0 && v < s->size);
+        veci_resize(&s->stack,veci_size(&s->stack)-1);
+        assert(reasons[v] != 0);
+        c    = reasons[v];
+
+        if (clause_is_lit(c)){
+            int v = lit_var(clause_read_lit(c));
+            if (tags[v] == l_Undef && levels[v] != 0){
+                if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){
+                    veci_push(&s->stack,v);
+                    tags[v] = l_True;
+                    veci_push(&s->tagged,v);
+                }else{
+                    int* tagged = veci_begin(&s->tagged);
+                    int j;
+                    for (j = top; j < veci_size(&s->tagged); j++)
+                        tags[tagged[j]] = l_Undef;
+                    veci_resize(&s->tagged,top);
+                    return false;
+                }
+            }
+        }else{
+            lit*    lits = clause_begin(c);
+            int     i, j;
+
+            for (i = 1; i < clause_size(c); i++){
+                int v = lit_var(lits[i]);
+                if (tags[v] == l_Undef && levels[v] != 0){
+                    if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){
+
+                        veci_push(&s->stack,lit_var(lits[i]));
+                        tags[v] = l_True;
+                        veci_push(&s->tagged,v);
+                    }else{
+                        int* tagged = veci_begin(&s->tagged);
+                        for (j = top; j < veci_size(&s->tagged); j++)
+                            tags[tagged[j]] = l_Undef;
+                        veci_resize(&s->tagged,top);
+                        return false;
+                    }
+                }
+            }
+        }
+    }
+
+    return true;
+}
+
+static void solver_analyze(solver* s, clause* c, veci* learnt)
+{
+    lit*     trail   = s->trail;
+    lbool*   tags    = s->tags;
+    clause** reasons = s->reasons;
+    int*     levels  = s->levels;
+    int      cnt     = 0;
+    lit      p       = lit_Undef;
+    int      ind     = s->qtail-1;
+    lit*     lits;
+    int      i, j, minl;
+    int*     tagged;
+
+    veci_push(learnt,lit_Undef);
+
+    do{
+        assert(c != 0);
+
+        if (clause_is_lit(c)){
+            lit q = clause_read_lit(c);
+            assert(lit_var(q) >= 0 && lit_var(q) < s->size);
+            if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){
+                tags[lit_var(q)] = l_True;
+                veci_push(&s->tagged,lit_var(q));
+                act_var_bump(s,lit_var(q));
+                if (levels[lit_var(q)] == solver_dlevel(s))
+                    cnt++;
+                else
+                    veci_push(learnt,q);
+            }
+        }else{
+
+            if (clause_learnt(c))
+                act_clause_bump(s,c);
+
+            lits = clause_begin(c);
+            //printlits(lits,lits+clause_size(c)); printf("\n");
+            for (j = (p == lit_Undef ? 0 : 1); j < clause_size(c); j++){
+                lit q = lits[j];
+                assert(lit_var(q) >= 0 && lit_var(q) < s->size);
+                if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){
+                    tags[lit_var(q)] = l_True;
+                    veci_push(&s->tagged,lit_var(q));
+                    act_var_bump(s,lit_var(q));
+                    if (levels[lit_var(q)] == solver_dlevel(s))
+                        cnt++;
+                    else
+                        veci_push(learnt,q);
+                }
+            }
+        }
+
+        while (tags[lit_var(trail[ind--])] == l_Undef);
+
+        p = trail[ind+1];
+        c = reasons[lit_var(p)];
+        cnt--;
+
+    }while (cnt > 0);
+
+    *veci_begin(learnt) = lit_neg(p);
+
+    lits = veci_begin(learnt);
+    minl = 0;
+    for (i = 1; i < veci_size(learnt); i++){
+        int lev = levels[lit_var(lits[i])];
+        minl    |= 1 << (lev & 31);
+    }
+
+    // simplify (full)
+    for (i = j = 1; i < veci_size(learnt); i++){
+        if (reasons[lit_var(lits[i])] == 0 || !solver_lit_removable(s,lits[i],minl))
+            lits[j++] = lits[i];
+    }
+
+    // update size of learnt + statistics
+    s->stats.max_literals += veci_size(learnt);
+    veci_resize(learnt,j);
+    s->stats.tot_literals += j;
+
+    // clear tags
+    tagged = veci_begin(&s->tagged);
+    for (i = 0; i < veci_size(&s->tagged); i++)
+        tags[tagged[i]] = l_Undef;
+    veci_resize(&s->tagged,0);
+
+#ifdef DEBUG
+    for (i = 0; i < s->size; i++)
+        assert(tags[i] == l_Undef);
+#endif
+
+#ifdef VERBOSEDEBUG
+    printf(L_IND"Learnt {", L_ind);
+    for (i = 0; i < veci_size(learnt); i++) printf(" "L_LIT, L_lit(lits[i]));
+#endif
+    if (veci_size(learnt) > 1){
+        int max_i = 1;
+        int max   = levels[lit_var(lits[1])];
+        lit tmp;
+
+        for (i = 2; i < veci_size(learnt); i++)
+            if (levels[lit_var(lits[i])] > max){
+                max   = levels[lit_var(lits[i])];
+                max_i = i;
+            }
+
+        tmp         = lits[1];
+        lits[1]     = lits[max_i];
+        lits[max_i] = tmp;
+    }
+#ifdef VERBOSEDEBUG
+    {
+        int lev = veci_size(learnt) > 1 ? levels[lit_var(lits[1])] : 0;
+        printf(" } at level %d\n", lev);
+    }
+#endif
+}
+
+
+clause* solver_propagate(solver* s)
+{
+    lbool*  values = s->assigns;
+    clause* confl  = (clause*)0;
+    lit*    lits;
+
+    //printf("solver_propagate\n");
+    while (confl == 0 && s->qtail - s->qhead > 0){
+        lit  p  = s->trail[s->qhead++];
+        vecp* ws = solver_read_wlist(s,p);
+        clause **begin = (clause**)vecp_begin(ws);
+        clause **end   = begin + vecp_size(ws);
+        clause **i, **j;
+
+        s->stats.propagations++;
+        s->simpdb_props--;
+
+        //printf("checking lit %d: "L_LIT"\n", veci_size(ws), L_lit(p));
+        for (i = j = begin; i < end; ){
+            if (clause_is_lit(*i)){
+                *j++ = *i;
+                if (!enqueue(s,clause_read_lit(*i),clause_from_lit(p))){
+                    confl = s->binary;
+                    (clause_begin(confl))[1] = lit_neg(p);
+                    (clause_begin(confl))[0] = clause_read_lit(*i++);
+
+                    // Copy the remaining watches:
+                    while (i < end)
+                        *j++ = *i++;
+                }
+            }else{
+                lit false_lit;
+                lbool sig;
+
+                lits = clause_begin(*i);
+
+                // Make sure the false literal is data[1]:
+                false_lit = lit_neg(p);
+                if (lits[0] == false_lit){
+                    lits[0] = lits[1];
+                    lits[1] = false_lit;
+                }
+                assert(lits[1] == false_lit);
+                //printf("checking clause: "); printlits(lits, lits+clause_size(*i)); printf("\n");
+
+                // If 0th watch is true, then clause is already satisfied.
+                sig = !lit_sign(lits[0]); sig += sig - 1;
+                if (values[lit_var(lits[0])] == sig){
+                    *j++ = *i;
+                }else{
+                    // Look for new watch:
+                    lit* stop = lits + clause_size(*i);
+                    lit* k;
+                    for (k = lits + 2; k < stop; k++){
+                        lbool sig = lit_sign(*k); sig += sig - 1;
+                        if (values[lit_var(*k)] != sig){
+                            lits[1] = *k;
+                            *k = false_lit;
+                            vecp_push(solver_read_wlist(s,lit_neg(lits[1])),*i);
+                            goto next; }
+                    }
+
+                    *j++ = *i;
+                    // Clause is unit under assignment:
+                    if (!enqueue(s,lits[0], *i)){
+                        confl = *i++;
+                        // Copy the remaining watches:
+                        while (i < end)
+                            *j++ = *i++;
+                    }
+                }
+            }
+        next:
+            i++;
+        }
+
+        s->stats.inspects += j - (clause**)vecp_begin(ws);
+        vecp_resize(ws,j - (clause**)vecp_begin(ws));
+    }
+
+    return confl;
+}
+
+static inline int clause_cmp (const void* x, const void* y) {
+    return clause_size((clause*)x) > 2 && (clause_size((clause*)y) == 2 || clause_activity((clause*)x) < clause_activity((clause*)y)) ? -1 : 1; }
+
+void solver_reducedb(solver* s)
+{
+    int      i, j;
+    double   extra_lim = s->cla_inc / vecp_size(&s->learnts); // Remove any clause below this activity
+    clause** learnts = (clause**)vecp_begin(&s->learnts);
+    clause** reasons = s->reasons;
+
+    sort(vecp_begin(&s->learnts), vecp_size(&s->learnts), &clause_cmp);
+
+    for (i = j = 0; i < vecp_size(&s->learnts) / 2; i++){
+        if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i])
+            clause_remove(s,learnts[i]);
+        else
+            learnts[j++] = learnts[i];
+    }
+    for (; i < vecp_size(&s->learnts); i++){
+        if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i] && clause_activity(learnts[i]) < extra_lim)
+            clause_remove(s,learnts[i]);
+        else
+            learnts[j++] = learnts[i];
+    }
+
+    //printf("reducedb deleted %d\n", vecp_size(&s->learnts) - j);
+
+
+    vecp_resize(&s->learnts,j);
+}
+
+static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts)
+{
+    int*    levels          = s->levels;
+    double  var_decay       = 0.95;
+    double  clause_decay    = 0.999;
+    double  random_var_freq = 0.02;
+
+    int     conflictC       = 0;
+    veci    learnt_clause;
+
+    assert(s->root_level == solver_dlevel(s));
+
+    s->stats.starts++;
+    s->var_decay = (float)(1 / var_decay   );
+    s->cla_decay = (float)(1 / clause_decay);
+    veci_resize(&s->model,0);
+    veci_new(&learnt_clause);
+
+    for (;;){
+        clause* confl = solver_propagate(s);
+        if (confl != 0){
+            // CONFLICT
+            int blevel;
+
+#ifdef VERBOSEDEBUG
+            printf(L_IND"**CONFLICT**\n", L_ind);
+#endif
+            s->stats.conflicts++; conflictC++;
+            if (solver_dlevel(s) == s->root_level){
+                veci_delete(&learnt_clause);
+                return l_False;
+            }
+
+            veci_resize(&learnt_clause,0);
+            solver_analyze(s, confl, &learnt_clause);
+            blevel = veci_size(&learnt_clause) > 1 ? levels[lit_var(veci_begin(&learnt_clause)[1])] : s->root_level;
+            blevel = s->root_level > blevel ? s->root_level : blevel;
+            solver_canceluntil(s,blevel);
+            solver_record(s,&learnt_clause);
+            act_var_decay(s);
+            act_clause_decay(s);
+
+        }else{
+            // NO CONFLICT
+            int next;
+
+            if (nof_conflicts >= 0 && conflictC >= nof_conflicts){
+                // Reached bound on number of conflicts:
+                s->progress_estimate = solver_progress(s);
+                solver_canceluntil(s,s->root_level);
+                veci_delete(&learnt_clause);
+                return l_Undef; }
+
+            if (solver_dlevel(s) == 0)
+                // Simplify the set of problem clauses:
+                solver_simplify(s);
+
+            if (nof_learnts >= 0 && vecp_size(&s->learnts) - s->qtail >= nof_learnts)
+                // Reduce the set of learnt clauses:
+                solver_reducedb(s);
+
+            // New variable decision:
+            s->stats.decisions++;
+            next = order_select(s,(float)random_var_freq);
+
+            if (next == var_Undef){
+                // Model found:
+                lbool* values = s->assigns;
+                int i;
+                for (i = 0; i < s->size; i++) veci_push(&s->model,(int)values[i]);
+                solver_canceluntil(s,s->root_level);
+                veci_delete(&learnt_clause);
+
+                /*
+                veci apa; veci_new(&apa);
+                for (i = 0; i < s->size; i++) 
+                    veci_push(&apa,(int)(s->model.ptr[i] == l_True ? toLit(i) : lit_neg(toLit(i))));
+                printf("model: "); printlits((lit*)apa.ptr, (lit*)apa.ptr + veci_size(&apa)); printf("\n");
+                veci_delete(&apa);
+                */
+
+                return l_True;
+            }
+
+            assume(s,lit_neg(toLit(next)));
+        }
+    }
+
+    return l_Undef; // cannot happen
+}
+
+//=================================================================================================
+// External solver functions:
+
+solver* solver_new(void)
+{
+    solver* s = (solver*)malloc(sizeof(solver));
+
+    // initialize vectors
+    vecp_new(&s->clauses);
+    vecp_new(&s->learnts);
+    veci_new(&s->order);
+    veci_new(&s->trail_lim);
+    veci_new(&s->tagged);
+    veci_new(&s->stack);
+    veci_new(&s->model);
+
+    // initialize arrays
+    s->wlists    = 0;
+    s->activity  = 0;
+    s->assigns   = 0;
+    s->orderpos  = 0;
+    s->reasons   = 0;
+    s->levels    = 0;
+    s->tags      = 0;
+    s->trail     = 0;
+
+
+    // initialize other vars
+    s->size                   = 0;
+    s->cap                    = 0;
+    s->qhead                  = 0;
+    s->qtail                  = 0;
+    s->cla_inc                = 1;
+    s->cla_decay              = 1;
+    s->var_inc                = 1;
+    s->var_decay              = 1;
+    s->root_level             = 0;
+    s->simpdb_assigns         = 0;
+    s->simpdb_props           = 0;
+    s->random_seed            = 91648253;
+    s->progress_estimate      = 0;
+    s->binary                 = (clause*)malloc(sizeof(clause) + sizeof(lit)*2);
+    s->binary->size_learnt    = (2 << 1);
+    s->verbosity              = 0;
+
+    s->stats.starts           = 0;
+    s->stats.decisions        = 0;
+    s->stats.propagations     = 0;
+    s->stats.inspects         = 0;
+    s->stats.conflicts        = 0;
+    s->stats.clauses          = 0;
+    s->stats.clauses_literals = 0;
+    s->stats.learnts          = 0;
+    s->stats.learnts_literals = 0;
+    s->stats.max_literals     = 0;
+    s->stats.tot_literals     = 0;
+
+    return s;
+}
+
+
+void solver_delete(solver* s)
+{
+    int i;
+    for (i = 0; i < vecp_size(&s->clauses); i++)
+        free(vecp_begin(&s->clauses)[i]);
+
+    for (i = 0; i < vecp_size(&s->learnts); i++)
+        free(vecp_begin(&s->learnts)[i]);
+
+    // delete vectors
+    vecp_delete(&s->clauses);
+    vecp_delete(&s->learnts);
+    veci_delete(&s->order);
+    veci_delete(&s->trail_lim);
+    veci_delete(&s->tagged);
+    veci_delete(&s->stack);
+    veci_delete(&s->model);
+    free(s->binary);
+
+    // delete arrays
+    if (s->wlists != 0){
+        int i;
+        for (i = 0; i < s->size*2; i++)
+            vecp_delete(&s->wlists[i]);
+
+        // if one is different from null, all are
+        free(s->wlists);
+        free(s->activity );
+        free(s->assigns  );
+        free(s->orderpos );
+        free(s->reasons  );
+        free(s->levels   );
+        free(s->trail    );
+        free(s->tags     );
+    }
+
+    free(s);
+}
+
+
+bool solver_addclause(solver* s, lit* begin, lit* end)
+{
+    lit *i,*j;
+    int maxvar;
+    lbool* values;
+    lit last;
+
+    if (begin == end) return false;
+
+    //printlits(begin,end); printf("\n");
+    // insertion sort
+    maxvar = lit_var(*begin);
+    for (i = begin + 1; i < end; i++){
+        lit l = *i;
+        maxvar = lit_var(l) > maxvar ? lit_var(l) : maxvar;
+        for (j = i; j > begin && *(j-1) > l; j--)
+            *j = *(j-1);
+        *j = l;
+    }
+    solver_setnvars(s,maxvar+1);
+
+    //printlits(begin,end); printf("\n");
+    values = s->assigns;
+
+    // delete duplicates
+    last = lit_Undef;
+    for (i = j = begin; i < end; i++){
+        //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]));
+        lbool sig = !lit_sign(*i); sig += sig - 1;
+        if (*i == lit_neg(last) || sig == values[lit_var(*i)])
+            return true;   // tautology
+        else if (*i != last && values[lit_var(*i)] == l_Undef)
+            last = *j++ = *i;
+    }
+
+    //printf("final: "); printlits(begin,j); printf("\n");
+
+    if (j == begin)          // empty clause
+        return false;
+    else if (j - begin == 1) // unit clause
+        return enqueue(s,*begin,(clause*)0);
+
+    // create new clause
+    vecp_push(&s->clauses,clause_new(s,begin,j,0));
+
+
+    s->stats.clauses++;
+    s->stats.clauses_literals += j - begin;
+
+    return true;
+}
+
+
+bool   solver_simplify(solver* s)
+{
+    clause** reasons;
+    int type;
+
+    assert(solver_dlevel(s) == 0);
+
+    if (solver_propagate(s) != 0)
+        return false;
+
+    if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0)
+        return true;
+
+    reasons = s->reasons;
+    for (type = 0; type < 2; type++){
+        vecp*    cs  = type ? &s->learnts : &s->clauses;
+        clause** cls = (clause**)vecp_begin(cs);
+
+        int i, j;
+        for (j = i = 0; i < vecp_size(cs); i++){
+            if (reasons[lit_var(*clause_begin(cls[i]))] != cls[i] &&
+                clause_simplify(s,cls[i]) == l_True)
+                clause_remove(s,cls[i]);
+            else
+                cls[j++] = cls[i];
+        }
+        vecp_resize(cs,j);
+    }
+
+    s->simpdb_assigns = s->qhead;
+    // (shouldn't depend on 'stats' really, but it will do for now)
+    s->simpdb_props   = (int)(s->stats.clauses_literals + s->stats.learnts_literals);
+
+    return true;
+}
+
+
+bool   solver_solve(solver* s, lit* begin, lit* end)
+{
+    double  nof_conflicts = 100;
+    double  nof_learnts   = solver_nclauses(s) / 3;
+    lbool   status        = l_Undef;
+    lbool*  values        = s->assigns;
+    lit*    i;
+    
+    //printf("solve: "); printlits(begin, end); printf("\n");
+    for (i = begin; i < end; i++){
+        switch (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]){
+        case 1: /* l_True: */
+            break;
+        case 0: /* l_Undef */
+            assume(s, *i);
+            if (solver_propagate(s) == NULL)
+                break;
+            // falltrough
+        case -1: /* l_False */
+            solver_canceluntil(s, 0);
+            return false;
+        }
+    }
+
+    s->root_level = solver_dlevel(s);
+
+    if (s->verbosity >= 1){
+        printf("==================================[MINISAT]===================================\n");
+        printf("| Conflicts |     ORIGINAL     |              LEARNT              | Progress |\n");
+        printf("|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |\n");
+        printf("==============================================================================\n");
+    }
+
+    while (status == l_Undef){
+        double Ratio = (s->stats.learnts == 0)? 0.0 :
+            s->stats.learnts_literals / (double)s->stats.learnts;
+
+        if (s->verbosity >= 1){
+            printf("| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %6.3f %% |\n", 
+                (double)s->stats.conflicts,
+                (double)s->stats.clauses, 
+                (double)s->stats.clauses_literals,
+                (double)nof_learnts, 
+                (double)s->stats.learnts, 
+                (double)s->stats.learnts_literals,
+                Ratio,
+                s->progress_estimate*100);
+            fflush(stdout);
+        }
+        status = solver_search(s,(int)nof_conflicts, (int)nof_learnts);
+        nof_conflicts *= 1.5;
+        nof_learnts   *= 1.1;
+    }
+    if (s->verbosity >= 1)
+        printf("==============================================================================\n");
+
+    solver_canceluntil(s,0);
+    return status != l_False;
+}
+
+
+int solver_nvars(solver* s)
+{
+    return s->size;
+}
+
+
+int solver_nclauses(solver* s)
+{
+    return vecp_size(&s->clauses);
+}
+
+
+int solver_nconflicts(solver* s)
+{
+    return (int)s->stats.conflicts;
+}
+
+//=================================================================================================
+// Sorting functions (sigh):
+
+static inline void selectionsort(void** array, int size, int(*comp)(const void *, const void *))
+{
+    int     i, j, best_i;
+    void*   tmp;
+
+    for (i = 0; i < size-1; i++){
+        best_i = i;
+        for (j = i+1; j < size; j++){
+            if (comp(array[j], array[best_i]) < 0)
+                best_i = j;
+        }
+        tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp;
+    }
+}
+
+
+static void sortrnd(void** array, int size, int(*comp)(const void *, const void *), double* seed)
+{
+    if (size <= 15)
+        selectionsort(array, size, comp);
+
+    else{
+        void*       pivot = array[irand(seed, size)];
+        void*       tmp;
+        int         i = -1;
+        int         j = size;
+
+        for(;;){
+            do i++; while(comp(array[i], pivot)<0);
+            do j--; while(comp(pivot, array[j])<0);
+
+            if (i >= j) break;
+
+            tmp = array[i]; array[i] = array[j]; array[j] = tmp;
+        }
+
+        sortrnd(array    , i     , comp, seed);
+        sortrnd(&array[i], size-i, comp, seed);
+    }
+}
+
+void sort(void** array, int size, int(*comp)(const void *, const void *))
+{
+    double seed = 91648253;
+    sortrnd(array,size,comp,&seed);
+}
diff --git a/src/sat/asat_fixed/satSolver.h b/src/sat/asat_fixed/satSolver.h
new file mode 100644
index 00000000..c9ce0219
--- /dev/null
+++ b/src/sat/asat_fixed/satSolver.h
@@ -0,0 +1,137 @@
+/**************************************************************************************************
+MiniSat -- Copyright (c) 2005, Niklas Sorensson
+http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko
+
+#ifndef solver_h
+#define solver_h
+
+#ifdef _WIN32
+#define inline __inline // compatible with MS VS 6.0
+#endif
+
+#include "vec.h"
+
+//=================================================================================================
+// Simple types:
+
+// does not work for c++
+typedef int  bool;
+static const bool  true      = 1;
+static const bool  false     = 0;
+
+typedef int                lit;
+typedef char               lbool;
+
+#ifdef _WIN32
+typedef signed __int64     uint64;   // compatible with MS VS 6.0
+#else
+typedef unsigned long long uint64;
+#endif
+
+static const int   var_Undef = -1;
+static const lit   lit_Undef = -2;
+
+static const lbool l_Undef   =  0;
+static const lbool l_True    =  1;
+static const lbool l_False   = -1;
+
+static inline lit  toLit   (int v) { return v + v; }
+static inline lit  lit_neg (lit l) { return l ^ 1; }
+static inline int  lit_var (lit l) { return l >> 1; }
+static inline int  lit_sign(lit l) { return (l & 1); }
+
+
+//=================================================================================================
+// Public interface:
+
+struct solver_t;
+typedef struct solver_t solver;
+
+extern solver* solver_new(void);
+extern void    solver_delete(solver* s);
+
+extern bool    solver_addclause(solver* s, lit* begin, lit* end);
+extern bool    solver_simplify(solver* s);
+extern bool    solver_solve(solver* s, lit* begin, lit* end);
+
+extern int     solver_nvars(solver* s);
+extern int     solver_nclauses(solver* s);
+extern int     solver_nconflicts(solver* s);
+
+extern void    solver_setnvars(solver* s,int n);
+
+struct stats_t
+{
+    uint64   starts, decisions, propagations, inspects, conflicts;
+    uint64   clauses, clauses_literals, learnts, learnts_literals, max_literals, tot_literals;
+};
+typedef struct stats_t stats;
+
+//=================================================================================================
+// Solver representation:
+
+struct clause_t;
+typedef struct clause_t clause;
+
+struct solver_t
+{
+    int      size;          // nof variables
+    int      cap;           // size of varmaps
+    int      qhead;         // Head index of queue.
+    int      qtail;         // Tail index of queue.
+
+    // clauses
+    vecp     clauses;       // List of problem constraints. (contains: clause*)
+    vecp     learnts;       // List of learnt clauses. (contains: clause*)
+
+    // activities
+    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.
+
+    vecp*    wlists;        // 
+    double*  activity;      // A heuristic measurement of the activity of a variable.
+    lbool*   assigns;       // Current values of variables.
+    int*     orderpos;      // Index in variable order.
+    clause** reasons;       //
+    int*     levels;        //
+    lit*     trail;
+
+    clause*  binary;        // A temporary binary clause
+    lbool*   tags;          //
+    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     model;         // If problem is solved, this vector contains the model (contains: lbool).
+
+    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
+
+    stats    stats;
+};
+
+#endif
diff --git a/src/sat/fraig/fraigFeed.c b/src/sat/fraig/fraigFeed.c
index 18b8bfcb..8a3cc6c7 100644
--- a/src/sat/fraig/fraigFeed.c
+++ b/src/sat/fraig/fraigFeed.c
@@ -463,6 +463,10 @@ Fraig_NodeVec_t * Fraig_FeedBackCoveringStart( Fraig_Man_t * p )
             Fraig_NodeVecPush( p->vCones, pEntD );
         if ( p->vCones->nSize == 1 )
             continue;
+        //////////////////////////////// bug fix by alanmi, September 14, 2006
+        if ( p->vCones->nSize > 20 ) 
+            continue;
+        ////////////////////////////////
 
         for ( k = 0; k < p->vCones->nSize; k++ )
             for ( m = k+1; m < p->vCones->nSize; m++ )
diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c
index 1a56cf0e..af0f13ce 100644
--- a/src/sat/fraig/fraigSat.c
+++ b/src/sat/fraig/fraigSat.c
@@ -34,6 +34,7 @@ static void Fraig_SupergateAddClausesExor( Fraig_Man_t * pMan, Fraig_Node_t * pN
 static void Fraig_SupergateAddClausesMux( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
 //static void Fraig_DetectFanoutFreeCone( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
 static void Fraig_DetectFanoutFreeConeMux( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
+static void Fraig_SetActivity( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew );
 
 extern void * Msat_ClauseVecReadEntry( void * p, int i );
 
@@ -355,6 +356,9 @@ if ( fVerbose )
     printf( "%d(%d) - ", Fraig_CountPis(p,p->vVarsInt), Msat_IntVecReadSize(p->vVarsInt) );
 
 
+    // prepare variable activity
+    Fraig_SetActivity( p, pOld, pNew );
+
     // get the complemented attribute
     fComp = Fraig_NodeComparePhase( pOld, pNew );
 //Msat_SolverPrintClauses( p->pSat );
@@ -1396,6 +1400,40 @@ printf( "%d(%d)", vFanins->nSize, nCubes );
 }
 
 
+
+/**Function*************************************************************
+
+  Synopsis    [Collect variables using their proximity from the nodes.]
+
+  Description [This procedure creates a variable order based on collecting
+  first the nodes that are the closest to the given two target nodes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fraig_SetActivity( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew )
+{
+    Fraig_Node_t * pNode;
+    int i, Number, MaxLevel;
+    float * pFactors = Msat_SolverReadFactors(pMan->pSat);
+    if ( pFactors == NULL )
+        return;
+    MaxLevel = FRAIG_MAX( pOld->Level, pNew->Level );
+    // create the variable order
+    for ( i = 0; i < Msat_IntVecReadSize(pMan->vVarsInt); i++ )
+    {
+        // get the new node on the frontier
+        Number = Msat_IntVecReadEntry(pMan->vVarsInt, i);
+        pNode = pMan->vNodes->pArray[Number];
+        pFactors[pNode->Num] = (float)pow( 0.97, MaxLevel - pNode->Level );
+//        if ( pNode->Num % 50 == 0 )
+//        printf( "(%d) %.2f  ", MaxLevel - pNode->Level, pFactors[pNode->Num] );
+    }
+//    printf( "\n" );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/msat/msat.h b/src/sat/msat/msat.h
index 1d9c0005..53353ba6 100644
--- a/src/sat/msat/msat.h
+++ b/src/sat/msat/msat.h
@@ -104,6 +104,7 @@ 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 );
diff --git a/src/sat/msat/msatActivity.c b/src/sat/msat/msatActivity.c
index 23925669..1cd795bd 100644
--- a/src/sat/msat/msatActivity.c
+++ b/src/sat/msat/msatActivity.c
@@ -45,8 +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 )
-//    if ( (p->pdActivity[Var] += p->dVarInc * (1.0 + 0.005*p->pActLevels[Var])) > 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/msatInt.h b/src/sat/msat/msatInt.h
index 7845ec0b..03903abe 100644
--- a/src/sat/msat/msatInt.h
+++ b/src/sat/msat/msatInt.h
@@ -119,7 +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.
-    int *               pActLevels;  // the levels of the variables
+    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.
diff --git a/src/sat/msat/msatSolverApi.c b/src/sat/msat/msatSolverApi.c
index 9317dcac..ee3507a6 100644
--- a/src/sat/msat/msatSolverApi.c
+++ b/src/sat/msat/msatSolverApi.c
@@ -64,6 +64,7 @@ void               Msat_SolverClausesIncrementL( Msat_Solver_t * p )           {
 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*************************************************************
 
@@ -174,11 +175,11 @@ Msat_Solver_t * Msat_SolverAlloc( int nVarsAlloc,
     p->dVarDecay = dVarDecay;
 
     p->pdActivity = ALLOC( double, p->nVarsAlloc );
-    p->pActLevels = ALLOC( int, p->nVarsAlloc );
+    p->pFactors   = ALLOC( float, p->nVarsAlloc );
     for ( i = 0; i < p->nVarsAlloc; i++ )
     {
-        p->pdActivity[i] = 0;
-        p->pActLevels[i] = 0;
+        p->pdActivity[i] = 0.0;
+        p->pFactors[i]   = 1.0;
     }
 
     p->pAssigns  = ALLOC( int, p->nVarsAlloc ); 
@@ -243,9 +244,12 @@ void Msat_SolverResize( Msat_Solver_t * p, int nVarsAlloc )
     p->nVarsAlloc = nVarsAlloc;
 
     p->pdActivity = REALLOC( double, p->pdActivity, p->nVarsAlloc );
-    p->pActLevels = REALLOC( int, p->pActLevels, 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 );
@@ -399,7 +403,7 @@ void Msat_SolverFree( Msat_Solver_t * p )
     Msat_ClauseVecFree( p->vLearned );
 
     FREE( p->pdActivity );
-    FREE( p->pActLevels );
+    FREE( p->pFactors );
     Msat_OrderFree( p->pOrder );
 
     for ( i = 0; i < 2 * p->nVarsAlloc; i++ )
diff --git a/src/sat/msat/msatSolverSearch.c b/src/sat/msat/msatSolverSearch.c
index 4b73d6b3..11a6540c 100644
--- a/src/sat/msat/msatSolverSearch.c
+++ b/src/sat/msat/msatSolverSearch.c
@@ -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 )
     {