delta faction to control double lookahead eagerness

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/sat/sat_config.cpp

@@ -123,8 +123,11 @@ namespace sat {
         m_lookahead_cube_psat_clause_base = p.lookahead_cube_psat_clause_base();
         m_lookahead_cube_psat_trigger = p.lookahead_cube_psat_trigger();
         m_lookahead_global_autarky = p.lookahead_global_autarky();
+        m_lookahead_delta_fraction = p.lookahead_delta_fraction();
         m_lookahead_use_learned = p.lookahead_use_learned();
-
+        if (m_lookahead_delta_fraction < 0 || m_lookahead_delta_fraction > 1.0) {
+            throw sat_param_exception("invalid value for delta fraction. It should be a number in the interval 0 to 1"); 
+        }
 
         // These parameters are not exposed
         m_next_simplify1  = _p.get_uint("next_simplify", 30000);

src/sat/sat_config.h

@@ -129,6 +129,7 @@ namespace sat {
         double             m_lookahead_cube_psat_trigger;
         reward_t           m_lookahead_reward;
         bool               m_lookahead_global_autarky;
+        double             m_lookahead_delta_fraction;
         bool               m_lookahead_use_learned;
 
         bool               m_incremental;

src/sat/sat_lookahead.cpp

@@ -997,6 +997,7 @@ namespace sat {
     void lookahead::init(bool learned) {
         m_delta_trigger = 0.0;
         m_delta_decrease = 0.0;
+        m_delta_fraction = m_s.m_config.m_lookahead_delta_fraction;
         m_config.m_dl_success = 0.8;
         m_inconsistent = false;
         m_qhead = 0;
@@ -1814,7 +1815,7 @@ namespace sat {
                     ++m_stats.m_double_lookahead_rounds;
                     num_units = double_look(l, base);
                     if (!inconsistent()) {
-                        m_delta_trigger = get_lookahead_reward(l);
+                        m_delta_trigger = m_delta_fraction*get_lookahead_reward(l);
                         dl_disable(l);
                     }
                 }
@@ -2098,7 +2099,9 @@ namespace sat {
                 m_cube_state.m_freevars_threshold = m_freevars.size();     
                 m_cube_state.m_psat_threshold = m_config.m_cube_cutoff == adaptive_psat_cutoff ? psat_heur() : dbl_max;  // MN. only compute PSAT if enabled
                 m_cube_state.inc_conflict();
-                if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return l_false;                
+                if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) {
+                    return l_false; 
+                }               
                 continue;
             }
         pick_up_work:
@@ -2131,7 +2134,9 @@ namespace sat {
                 m_cube_state.m_freevars_threshold = prev_nfreevars;
                 m_cube_state.m_psat_threshold = prev_psat;
                 m_cube_state.inc_conflict();
-                if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return l_false;
+                if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) {
+                    return l_false;
+                }
                 continue;
             }
             if (lit == null_literal) {

src/sat/sat_lookahead.h

@@ -198,6 +198,7 @@ namespace sat {
         config                 m_config;
         double                 m_delta_trigger;
         double                 m_delta_decrease;
+        double                 m_delta_fraction;
 
         drat                   m_drat;
         literal_vector         m_assumptions;

src/sat/sat_params.pyg

@@ -74,6 +74,7 @@ def_module_params('sat',
                           ('lookahead.use_learned', BOOL, False, 'use learned clauses when selecting lookahead literal'),
                           ('lookahead_simplify.bca', BOOL, True, 'add learned binary clauses as part of lookahead simplification'),
                           ('lookahead.global_autarky', BOOL, False, 'prefer to branch on variables that occur in clauses that are reduced'),
+                          ('lookahead.delta_fraction', DOUBLE, 1.0, 'number between 0 and 1, the smaller the more literals are selected for double lookahead'),
                           ('lookahead.reward', SYMBOL, 'march_cu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu'))
                           # reward function used to determine which literal to cube on.
                           # - ternary: reward function useful for random 3-SAT instances. Used by Heule and Knuth in March.

src/sat/sat_solver/inc_sat_solver.cpp

@@ -332,18 +332,6 @@ public:
         }
         sat::literal_vector lits;
         lbool result = m_solver.cube(vars, lits, backtrack_level);
-        switch (result) {
-        case l_true:
-            return last_cube(true);
-        case l_false: 
-            return last_cube(false);
-        default: 
-            break;
-        }
-        if (lits.empty()) {
-            set_reason_unknown(m_solver.get_reason_unknown());
-            return expr_ref_vector(m);
-        }
         expr_ref_vector fmls(m);
         expr_ref_vector lit2expr(m);
         lit2expr.resize(m_solver.num_vars() * 2);
@@ -358,6 +346,17 @@ public:
                 vs.push_back(x);
             }
         }
+        switch (result) {
+        case l_true:
+            return last_cube(true);
+        case l_false: 
+            return last_cube(false);
+        default: 
+            break;
+        }
+        if (lits.empty()) {
+            set_reason_unknown(m_solver.get_reason_unknown());
+        }
         return fmls;
     }