diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp
index 24d2bca9b..bd2a48ff2 100644
--- a/src/sat/sat_config.cpp
+++ b/src/sat/sat_config.cpp
@@ -112,8 +112,21 @@ namespace sat {
             throw sat_param_exception("invalid reward type supplied: accepted heuristics are 'ternary', 'heuleu', 'unit' or 'heule_schur'");
         }
 
+        if (p.lookahead_cube_cutoff() == symbol("adaptive")) {
+            m_lookahead_cube_cutoff = adaptive_cutoff;
+        }
+        else if (p.lookahead_cube_cutoff() == symbol("fixed_depth")) {
+            m_lookahead_cube_cutoff = fixed_depth_cutoff;
+        }
+        else if (p.lookahead_cube_cutoff() == symbol("fixed_freevars")) {
+            m_lookahead_cube_cutoff = fixed_freevars_cutoff;
+        }
+        else {
+            throw sat_param_exception("invalid cutoff type supplied: accepted cutoffs are 'adaptive', 'fixed_depth', 'fixed_freevars'");
+        }
         m_lookahead_cube_fraction = p.lookahead_cube_fraction();
-        m_lookahead_cube_cutoff = p.lookahead_cube_cutoff();
+        m_lookahead_cube_depth = p.lookahead_cube_depth();
+        m_lookahead_cube_freevars = p.lookahead_cube_freevars();
         m_lookahead_global_autarky = p.lookahead_global_autarky();
 
         // These parameters are not exposed
diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h
index 9a20bbc63..f6f6774fc 100644
--- a/src/sat/sat_config.h
+++ b/src/sat/sat_config.h
@@ -65,6 +65,12 @@ namespace sat {
         march_cu_reward
     };
 
+    enum cutoff_t {
+        adaptive_cutoff,
+        fixed_depth_cutoff,
+        fixed_freevars_cutoff
+    };
+
     struct config {
         unsigned long long m_max_memory;
         phase_selection    m_phase;
@@ -85,8 +91,10 @@ namespace sat {
         bool               m_lookahead_search;
         bool               m_lookahead_simplify;
         bool               m_lookahead_simplify_bca;
-        unsigned           m_lookahead_cube_cutoff;
+        cutoff_t           m_lookahead_cube_cutoff;
         double             m_lookahead_cube_fraction;
+        unsigned           m_lookahead_cube_depth;
+        double             m_lookahead_cube_freevars;
         reward_t           m_lookahead_reward;
         bool               m_lookahead_global_autarky;
 
diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp
index 306912b57..2784b97d2 100644
--- a/src/sat/sat_lookahead.cpp
+++ b/src/sat/sat_lookahead.cpp
@@ -1032,6 +1032,7 @@ namespace sat {
         }
         propagate();
         m_qhead = m_trail.size();
+        m_init_freevars = m_freevars.size();
         TRACE("sat", m_s.display(tout); display(tout););
     }
 
@@ -2054,8 +2055,11 @@ namespace sat {
             }
             backtrack_level = UINT_MAX;
             depth = m_cube_state.m_cube.size();
-            if ((m_config.m_cube_cutoff != 0 && depth == m_config.m_cube_cutoff) ||
-                (m_config.m_cube_cutoff == 0 && m_freevars.size() < m_cube_state.m_freevars_threshold)) {
+            if ((m_config.m_cube_cutoff == fixed_depth_cutoff && depth == m_config.m_cube_depth) ||
+                (m_config.m_cube_cutoff == adaptive_cutoff && m_freevars.size() < m_cube_state.m_freevars_threshold) ||
+                /* m_cube_cutoff is fixed_freevars */ m_freevars.size() <= m_init_freevars * m_config.m_cube_freevars) {
+            /*if ((m_config.m_cube_cutoff != 0 && depth == m_config.m_cube_cutoff) ||
+                (m_config.m_cube_cutoff == 0 && m_freevars.size() < m_cube_state.m_freevars_threshold)) {*/
                 m_cube_state.m_freevars_threshold *= (1.0 - pow(m_config.m_cube_fraction, depth));
                 set_conflict();
 #if 0
@@ -2413,6 +2417,8 @@ namespace sat {
         m_config.m_reward_type = m_s.m_config.m_lookahead_reward;
         m_config.m_cube_cutoff = m_s.m_config.m_lookahead_cube_cutoff;
         m_config.m_cube_fraction = m_s.m_config.m_lookahead_cube_fraction;
+        m_config.m_cube_depth = m_s.m_config.m_lookahead_cube_depth;
+        m_config.m_cube_freevars = m_s.m_config.m_lookahead_cube_freevars;
     }
 
     void lookahead::collect_statistics(statistics& st) const {
diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h
index 6f0c256a7..db9ebdaa4 100644
--- a/src/sat/sat_lookahead.h
+++ b/src/sat/sat_lookahead.h
@@ -80,8 +80,10 @@ namespace sat {
             unsigned m_dl_max_iterations;
             unsigned m_tc1_limit;
             reward_t m_reward_type;
-            unsigned m_cube_cutoff;
+            cutoff_t m_cube_cutoff;
+            unsigned m_cube_depth;
             double   m_cube_fraction;
+            double   m_cube_freevars;
 
             config() {
                 memset(this, sizeof(*this), 0);
@@ -96,8 +98,10 @@ namespace sat {
                 m_dl_max_iterations = 2;
                 m_tc1_limit = 10000000;
                 m_reward_type = ternary_reward;
-                m_cube_cutoff = 0;
+                m_cube_cutoff = adaptive_cutoff;
+                m_cube_depth = 10;
                 m_cube_fraction = 0.4;
+                m_cube_freevars = 0.8;
             }
         };
 
@@ -222,11 +226,12 @@ namespace sat {
         svector<prefix>        m_vprefix;       // var:     prefix where variable participates in propagation
         unsigned               m_rating_throttle; // throttle to recompute rating
         indexed_uint_set       m_freevars;
+        unsigned               m_init_freevars;
         lookahead_mode         m_search_mode;   // mode of search
         stats                  m_stats;
         model                  m_model; 
         cube_state             m_cube_state;
-        scoped_ptr<extension>   m_ext;
+        scoped_ptr<extension>  m_ext;
  
         // ---------------------------------------
         // truth values
diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg
index 4f65b100b..085f0c067 100644
--- a/src/sat/sat_params.pyg
+++ b/src/sat/sat_params.pyg
@@ -37,8 +37,13 @@ def_module_params('sat',
                           ('atmost1_encoding', SYMBOL, 'grouped', 'encoding used for at-most-1 constraints grouped, bimander, ordered'),
                           ('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'),
                           ('local_search', BOOL, False, 'use local search instead of CDCL'),
-                          ('lookahead.cube.fraction', DOUBLE, 0.4, 'adaptive fraction to create lookahead cubes. Used when lookahead_cube is true'),
-                          ('lookahead.cube.cutoff', UINT, 10, 'cut-off depth to create cubes. Only enabled when non-zero. Used when lookahead_cube is true.'),
+                          ('lookahead.cube.cutoff', SYMBOL, 'adaptive', 'cutoff type used to create lookahead cubes: adaptive, fixed_depth, fixed_freevars, psat'),
+                          ('lookahead.cube.fraction', DOUBLE, 0.4, 'adaptive fraction to create lookahead cubes. Used when lookahead.cube.cutoff is adaptive'),
+                          ('lookahead.cube.depth', UINT, 10, 'cut-off depth to create cubes. Used when lookahead.cube.cutoff is fixed_depth.'),
+                          ('lookahead.cube.freevars', DOUBLE, 0.8, 'cube free fariable fraction. Used when lookahead.cube.cutoff is fixed_freevars'),
+                          ('lookahead.cube.psat.var_exp', DOUBLE, 1, 'free variable exponent for PSAT cutoff'),
+                          ('lookahead.cube.psat.clause_base', DOUBLE, 1, 'clause base for PSAT cutoff')
+                          ('lookahead.cube.psat.probability', DOUBLE' 0.5, 'probability to create lookahead cubes for PSAT cutoff')
                           ('lookahead_search', BOOL, False, 'use lookahead solver'),
                           ('lookahead.preselect', BOOL, False, 'use pre-selection of subset of variables for branching'),
                           ('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'),