diff --git a/src/tactic/sls/sls_compilation_settings.h b/src/tactic/sls/sls_compilation_settings.h
index 8e52596e0..4d8c83599 100644
--- a/src/tactic/sls/sls_compilation_settings.h
+++ b/src/tactic/sls/sls_compilation_settings.h
@@ -43,7 +43,7 @@ Notes:
 #define _RESTART_LIMIT_ 10
 // 0 = initialize with all zero, 1 initialize with random value
 #define _RESTART_INIT_ 0
-// 0 = even intervals, 1 = pseudo luby, 2 = real luby, 3 = armin, 4 = rapid
+// 0 = even intervals, 1 = pseudo luby, 2 = real luby, 3 = armin, 4 = rapid, 5 = minisat
 #define _RESTART_SCHEME_ 1
 // base value c for armin restart scheme using c^inner - only applies for _RESTART_SCHEME_ 3
 #define _RESTART_CONST_ARMIN_ 3.0
@@ -105,6 +105,10 @@ Notes:
 // 0 = initialize with one, 1 = initialize with number of assertions
 #define _UCT_INIT_ 1
 
+// do we gradually reduce the touched values of _UCT_?
+#define _UCT_FORGET_ 0
+#define _UCT_FORGET_FACTOR_ 0.5
+
 // shall we use addition/subtraction?
 #define _USE_ADDSUB_ 1
 
diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp
index 0f157d3a6..a9b110224 100644
--- a/src/tactic/sls/sls_tactic.cpp
+++ b/src/tactic/sls/sls_tactic.cpp
@@ -26,7 +26,6 @@ Notes:
 #include"elim_uncnstr_tactic.h"
 #include"nnf_tactic.h"
 #include"stopwatch.h"
-
 #include"sls_tactic.h"
 #include"sls_params.hpp"
 #include"sls_engine.h"
@@ -163,7 +162,7 @@ tactic * mk_preamble(ast_manager & m, params_ref const & p) {
                         // Andreas: It would be cool to get rid of shared top level assertions but which simplification is doing this?
                         //mk_ctx_simplify_tactic(m, ctx_p),
                         // Andreas: This one at least eliminates top level duplicates ...
-                        mk_simplify_tactic(m),
+                        //mk_simplify_tactic(m),
                         // Andreas: How does a NNF actually look like? Can it contain ITE operators?
                         mk_nnf_tactic(m, p));
 }
diff --git a/src/tactic/sls/sls_tracker.h b/src/tactic/sls/sls_tracker.h
index 7d1d4c0f1..6ac054246 100644
--- a/src/tactic/sls/sls_tracker.h
+++ b/src/tactic/sls/sls_tracker.h
@@ -276,6 +276,20 @@ public:
     }
 #endif
 
+    void uct_forget(goal_ref const & g) {
+        expr * e;
+        unsigned touched_old, touched_new;
+
+        for (unsigned i = 0; i < g->size(); i++)
+        {
+            e = g->form(i);
+            touched_old = m_scores.find(e).touched;
+            touched_new = (unsigned)((touched_old - 1) * _UCT_FORGET_FACTOR_ + 1);
+            m_scores.find(e).touched = touched_new;
+            m_touched += touched_new - touched_old;
+        }
+    }
+
     void initialize(app * n) {
         // Build score table
         if (!m_scores.contains(n)) {
@@ -1196,6 +1210,8 @@ public:
                 double q = vscore.score + _UCT_CONSTANT_ * sqrt(log((double)m_touched)/vscore.touched); 
 #elif _UCT_ == 2
                 double q = vscore.score + (_UCT_CONSTANT_ * (flip - vscore.touched)) / sz; 
+#elif _UCT_ == 3
+                double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched) + (get_random_uint(16) * 0.1 / (2<<16)); 
 #endif
                 if (q > max && m_mpz_manager.neq(get_value(e), m_one) ) { max = q; pos = i; }
             }
@@ -1203,7 +1219,7 @@ public:
             if (pos == static_cast<unsigned>(-1))
                 return m_temp_constants;
 
-#if _UCT_ == 1
+#if _UCT_ == 1 || _UCT_ == 3
             m_scores.find(g->form(pos)).touched++;
             m_touched++;
 #elif _UCT_ == 2
@@ -1344,6 +1360,8 @@ public:
                 double q = vscore.score + _UCT_CONSTANT_ * sqrt(log((double)m_touched) / vscore.touched);
 #elif _UCT_ == 2
             double q = vscore.score + (_UCT_CONSTANT_ * (flip - vscore.touched)) / sz; 
+#elif _UCT_ == 3
+            double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched) + (get_random_uint(16) * 0.1 / (2<<16)); 
 #endif
             if (q > max && m_mpz_manager.neq(get_value(e), m_one) ) { max = q; pos = i; }
             }
@@ -1351,7 +1369,7 @@ public:
         if (pos == static_cast<unsigned>(-1))
             return 0;
 
-#if _UCT_ == 1
+#if _UCT_ == 1 || _UCT_ == 3
         m_scores.find(g->form(pos)).touched++;
         m_touched++;
 #elif _UCT_ == 2