diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp
index 76fb1d3a3..537111fe1 100644
--- a/src/sat/sat_config.cpp
+++ b/src/sat/sat_config.cpp
@@ -65,6 +65,8 @@ namespace sat {
 
         m_rephase_base      = p.rephase_base();
         m_reorder_base      = p.reorder_base();
+        m_reorder_itau      = p.reorder_itau();
+        m_activity_scale  = p.reorder_activity_scale();
         m_search_sat_conflicts = p.search_sat_conflicts();
         m_search_unsat_conflicts = p.search_unsat_conflicts();
         m_phase_sticky      = p.phase_sticky();
@@ -72,7 +74,6 @@ namespace sat {
         m_restart_initial = p.restart_initial();
         m_restart_factor  = p.restart_factor();
         m_restart_max     = p.restart_max();
-        m_activity_scale  = 100;
         m_propagate_prefetch = p.propagate_prefetch();
         m_inprocess_max   = p.inprocess_max();
 
diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h
index 86835b073..326a9abdd 100644
--- a/src/sat/sat_config.h
+++ b/src/sat/sat_config.h
@@ -92,6 +92,8 @@ namespace sat {
         bool               m_phase_sticky;
         unsigned           m_rephase_base;
         unsigned           m_reorder_base;
+        double             m_reorder_itau;
+        unsigned           m_reorder_activity_scale;
         bool               m_propagate_prefetch;
         restart_strategy   m_restart;
         bool               m_restart_fast;
diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg
index 4075d4425..1e72ceaa5 100644
--- a/src/sat/sat_params.pyg
+++ b/src/sat/sat_params.pyg
@@ -7,7 +7,9 @@ def_module_params('sat',
                           ('search.unsat.conflicts', UINT, 400, 'period for solving for unsat (in number of conflicts)'),
                           ('search.sat.conflicts', UINT, 400, 'period for solving for sat (in number of conflicts)'),
 	                  ('rephase.base', UINT, 1000, 'number of conflicts per rephase '),                          
-	                  ('reorder.base', UINT, UINT_MAX, 'number of conflicts per random reorder '),                          
+	                  ('reorder.base', UINT, UINT_MAX, 'number of conflicts per random reorder '),       
+                          ('reorder.itau', DOUBLE, 4.0, 'inverse temperature for softmax'),               
+                          ('reorder.activity_scale', UINT, 100, 'scaling factor for activity update'),               
                           ('propagate.prefetch', BOOL, True, 'prefetch watch lists for assigned literals'),
                           ('restart', SYMBOL, 'ema', 'restart strategy: static, luby, ema or geometric'),
                           ('restart.initial', UINT, 2, 'initial restart (number of conflicts)'),
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index e4a5f86a4..1978f967e 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -2196,7 +2196,7 @@ namespace sat {
 
     void solver::update_activity(bool_var v, double p) {
         unsigned old_act = m_activity[v];
-        unsigned new_act = (unsigned) (num_vars() * m_config.m_activity_scale *  p);
+        unsigned new_act = (unsigned) (m_config.m_activity_scale *  p);
         m_activity[v] = new_act;
         if (!was_eliminated(v) && value(v) == l_undef && new_act != old_act) {
             m_case_split_queue.activity_changed_eh(v, new_act > old_act);
@@ -3174,16 +3174,16 @@ namespace sat {
         //   exp(log(exp(logits[i])) - log(sum(exp(logits)))) 
         // =
         //   exp(logits[i] - lse)
-        svector<float> logits(vars.size(), 0.0);
-        float itau = 4.0;
-        float lse = 0;
-        float mid = m_rand.max_value()/2;
-        float max = 0;
-        for (float& f : logits) {
+        svector<double> logits(vars.size(), 0.0);
+        double itau = m_config.m_reorder_itau;
+        double lse = 0;
+        double mid = m_rand.max_value()/2;
+        double max = 0;
+        for (double& f : logits) {
             f = itau * (m_rand() - mid)/mid;
             if (f > max) max = f;
         }
-        for (float f : logits) {
+        for (double f : logits) {
             lse += log(f - max);
         }
         lse = max + exp(lse);