From 1b7cb110d34b748e2b501bd13947c943c6aaf0c4 Mon Sep 17 00:00:00 2001 From: Miguel Angelo Da Terra Neves Date: Fri, 1 Dec 2017 11:02:29 -0800 Subject: [PATCH 1/3] freevars cube cutoff Signed-off-by: Miguel Angelo Da Terra Neves --- src/sat/sat_config.cpp | 15 ++++++++++++++- src/sat/sat_config.h | 10 +++++++++- src/sat/sat_lookahead.cpp | 10 ++++++++-- src/sat/sat_lookahead.h | 11 ++++++++--- src/sat/sat_params.pyg | 9 +++++++-- 5 files changed, 46 insertions(+), 9 deletions(-) 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 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 m_ext; + scoped_ptr 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'), From e0dfbd6d1cf7341da84a315bb1e715d3767c9126 Mon Sep 17 00:00:00 2001 From: Miguel Angelo Da Terra Neves Date: Mon, 4 Dec 2017 14:33:48 -0800 Subject: [PATCH 2/3] fixed freevars and psat cube cutoffs Signed-off-by: Miguel Angelo Da Terra Neves --- src/sat/sat_config.cpp | 6 ++++++ src/sat/sat_config.h | 6 +++++- src/sat/sat_lookahead.cpp | 38 +++++++++++++++++++++++++++++++++++--- src/sat/sat_lookahead.h | 8 ++++++++ src/sat/sat_params.pyg | 4 ++-- 5 files changed, 56 insertions(+), 6 deletions(-) diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index bd2a48ff2..b0797dae9 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -121,12 +121,18 @@ namespace sat { else if (p.lookahead_cube_cutoff() == symbol("fixed_freevars")) { m_lookahead_cube_cutoff = fixed_freevars_cutoff; } + else if (p.lookahead_cube_cutoff() == symbol("psat")) { + m_lookahead_cube_cutoff = psat_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_depth = p.lookahead_cube_depth(); m_lookahead_cube_freevars = p.lookahead_cube_freevars(); + m_lookahead_cube_psat_var_exp = p.lookahead_cube_psat_var_exp(); + 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(); // These parameters are not exposed diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index f6f6774fc..1529466ee 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -68,7 +68,8 @@ namespace sat { enum cutoff_t { adaptive_cutoff, fixed_depth_cutoff, - fixed_freevars_cutoff + fixed_freevars_cutoff, + psat_cutoff }; struct config { @@ -95,6 +96,9 @@ namespace sat { double m_lookahead_cube_fraction; unsigned m_lookahead_cube_depth; double m_lookahead_cube_freevars; + double m_lookahead_cube_psat_var_exp; + double m_lookahead_cube_psat_clause_base; + double m_lookahead_cube_psat_trigger; 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 6aae5738e..3feb9455d 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -2019,6 +2019,35 @@ namespace sat { st.update("lh cube conflicts", m_cube_state.m_conflicts); } + double lookahead::psat_heur() { + double h = 0.0; + for (bool_var x : m_freevars) { + literal l(x, false); + for (literal lit : m_binary[l.index()]) { + h += l.index() > lit.index() ? 1.0 / m_config.m_cube_psat_clause_base : 0.0; + } + for (literal lit : m_binary[(~l).index()]) { + h += l.index() > lit.index() ? 1.0 / m_config.m_cube_psat_clause_base : 0.0; + } + for (binary b : m_ternary[l.index()]) { + h += l.index() > b.m_u.index() && l.index() > b.m_v.index() ? + 1.0 / pow(m_config.m_cube_psat_clause_base, 2) : + 0.0; + } + for (binary b : m_ternary[(~l).index()]) { + h += l.index() > b.m_u.index() && l.index() > b.m_v.index() ? + 1.0 / pow(m_config.m_cube_psat_clause_base, 2) : + 0.0; + } + } + for (nary * n : m_nary_clauses) { + h += 1.0 / pow(m_config.m_cube_psat_clause_base, n->size() - 1); + } + h /= pow(m_freevars.size(), m_config.m_cube_psat_var_exp); + IF_VERBOSE(10, verbose_stream() << "(sat-cube-psat :val " << h << ")\n";); + return h; + } + lbool lookahead::cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level) { scoped_ext _scoped_ext(*this); lits.reset(); @@ -2065,9 +2094,8 @@ namespace sat { depth = m_cube_state.m_cube.size(); 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_config.m_cube_cutoff == fixed_freevars_cutoff && m_freevars.size() <= m_init_freevars * m_config.m_cube_freevars) || + (m_config.m_cube_cutoff == psat_cutoff && psat_heur() >= m_config.m_cube_psat_trigger)) { m_cube_state.m_freevars_threshold *= (1.0 - pow(m_config.m_cube_fraction, depth)); set_conflict(); m_cube_state.inc_cutoff(); @@ -2085,6 +2113,7 @@ namespace sat { if (inconsistent()) { TRACE("sat", tout << "inconsistent: " << m_cube_state.m_cube << "\n";); m_cube_state.m_freevars_threshold = prev_nfreevars; + m_cube_state.inc_conflict(); if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return l_false; continue; } @@ -2503,6 +2532,9 @@ namespace sat { 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; + m_config.m_cube_psat_var_exp = m_s.m_config.m_lookahead_cube_psat_var_exp; + m_config.m_cube_psat_clause_base = m_s.m_config.m_lookahead_cube_psat_clause_base; + m_config.m_cube_psat_trigger = m_s.m_config.m_lookahead_cube_psat_trigger; } void lookahead::collect_statistics(statistics& st) const { diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index bd4198dcd..254dd614f 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -84,6 +84,9 @@ namespace sat { unsigned m_cube_depth; double m_cube_fraction; double m_cube_freevars; + double m_cube_psat_var_exp; + double m_cube_psat_clause_base; + double m_cube_psat_trigger; config() { memset(this, sizeof(*this), 0); @@ -102,6 +105,9 @@ namespace sat { m_cube_depth = 10; m_cube_fraction = 0.4; m_cube_freevars = 0.8; + m_cube_psat_var_exp = 1.0; + m_cube_psat_clause_base = 2.0; + m_cube_psat_trigger = 5.0; } }; @@ -547,6 +553,8 @@ namespace sat { void add_hyper_binary(); + double psat_heur(); + public: lookahead(solver& s) : m_s(s), diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 085f0c067..565c6dbcc 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -42,8 +42,8 @@ def_module_params('sat', ('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.cube.psat.clause_base', DOUBLE, 2, 'clause base for PSAT cutoff'), + ('lookahead.cube.psat.trigger', DOUBLE, 5, 'trigger value 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'), From 38751430df4078e14feda6d8e50f9bf5ae1b1419 Mon Sep 17 00:00:00 2001 From: Miguel Angelo Da Terra Neves Date: Tue, 5 Dec 2017 17:53:48 -0800 Subject: [PATCH 3/3] adaptive psat cutoff Signed-off-by: Miguel Angelo Da Terra Neves --- src/sat/sat_config.cpp | 19 +++++++++++-------- src/sat/sat_config.h | 9 +++++---- src/sat/sat_lookahead.cpp | 15 ++++++++++----- src/sat/sat_lookahead.h | 4 +++- src/sat/sat_params.pyg | 10 +++++----- 5 files changed, 34 insertions(+), 23 deletions(-) diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 87d84f133..660337071 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -109,20 +109,23 @@ 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; + if (p.lookahead_cube_cutoff() == symbol("depth")) { + m_lookahead_cube_cutoff = depth_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 if (p.lookahead_cube_cutoff() == symbol("freevars")) { + m_lookahead_cube_cutoff = freevars_cutoff; } else if (p.lookahead_cube_cutoff() == symbol("psat")) { m_lookahead_cube_cutoff = psat_cutoff; } + else if (p.lookahead_cube_cutoff() == symbol("adaptive_freevars")) { + m_lookahead_cube_cutoff = adaptive_freevars_cutoff; + } + else if (p.lookahead_cube_cutoff() == symbol("adaptive_psat")) { + m_lookahead_cube_cutoff = adaptive_psat_cutoff; + } else { - throw sat_param_exception("invalid cutoff type supplied: accepted cutoffs are 'adaptive', 'fixed_depth', 'fixed_freevars'"); + throw sat_param_exception("invalid cutoff type supplied: accepted cutoffs are 'depth', 'freevars', 'psat', 'adaptive_freevars' and 'adaptive_psat'"); } m_lookahead_cube_fraction = p.lookahead_cube_fraction(); m_lookahead_cube_depth = p.lookahead_cube_depth(); diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index ed7802cef..f66c0dbdf 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -66,10 +66,11 @@ namespace sat { }; enum cutoff_t { - adaptive_cutoff, - fixed_depth_cutoff, - fixed_freevars_cutoff, - psat_cutoff + depth_cutoff, + freevars_cutoff, + psat_cutoff, + adaptive_freevars_cutoff, + adaptive_psat_cutoff }; struct config { diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index a9ae3b641..ec1bf23f2 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -2092,11 +2092,14 @@ namespace sat { } backtrack_level = UINT_MAX; depth = m_cube_state.m_cube.size(); - 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_config.m_cube_cutoff == fixed_freevars_cutoff && m_freevars.size() <= m_init_freevars * m_config.m_cube_freevars) || - (m_config.m_cube_cutoff == psat_cutoff && psat_heur() >= m_config.m_cube_psat_trigger)) { - m_cube_state.m_freevars_threshold *= (1.0 - pow(m_config.m_cube_fraction, depth)); + if ((m_config.m_cube_cutoff == depth_cutoff && depth == m_config.m_cube_depth) || + (m_config.m_cube_cutoff == freevars_cutoff && m_freevars.size() <= m_init_freevars * m_config.m_cube_freevars) || + (m_config.m_cube_cutoff == psat_cutoff && psat_heur() >= m_config.m_cube_psat_trigger) || + (m_config.m_cube_cutoff == adaptive_freevars_cutoff && m_freevars.size() < m_cube_state.m_freevars_threshold) || + (m_config.m_cube_cutoff == adaptive_psat_cutoff && psat_heur() >= m_cube_state.m_psat_threshold)) { + double dec = (1.0 - pow(m_config.m_cube_fraction, depth)); + m_cube_state.m_freevars_threshold *= dec; + m_cube_state.m_psat_threshold *= dec; set_conflict(); m_cube_state.inc_cutoff(); #if 0 @@ -2109,10 +2112,12 @@ namespace sat { return l_undef; } int prev_nfreevars = m_freevars.size(); + double prev_psat = m_config.m_cube_cutoff == adaptive_psat_cutoff ? psat_heur() : DBL_MAX; // MN. only compute PSAT if enabled literal lit = choose(); if (inconsistent()) { TRACE("sat", tout << "inconsistent: " << m_cube_state.m_cube << "\n";); 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; continue; diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index 254dd614f..6a7bb7449 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -101,7 +101,7 @@ namespace sat { m_dl_max_iterations = 2; m_tc1_limit = 10000000; m_reward_type = ternary_reward; - m_cube_cutoff = adaptive_cutoff; + m_cube_cutoff = adaptive_freevars_cutoff; m_cube_depth = 10; m_cube_fraction = 0.4; m_cube_freevars = 0.8; @@ -177,6 +177,7 @@ namespace sat { svector m_is_decision; literal_vector m_cube; double m_freevars_threshold; + double m_psat_threshold; unsigned m_conflicts; unsigned m_cutoffs; cube_state() { reset(); } @@ -185,6 +186,7 @@ namespace sat { m_is_decision.reset(); m_cube.reset(); m_freevars_threshold = 0; + m_psat_threshold = DBL_MAX; reset_stats(); } void reset_stats() { m_conflicts = 0; m_cutoffs = 0; } diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 0e6823030..4432c0b16 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -37,13 +37,13 @@ def_module_params('sat', ('atmost1_encoding', SYMBOL, 'grouped', 'encoding used for at-most-1 constraints grouped, bimander, ordered'), ('local_search', BOOL, False, 'use local search instead of CDCL'), ('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'), - ('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.cutoff', SYMBOL, 'adaptive_freevars', 'cutoff type used to create lookahead cubes: depth, freevars, psat, adaptive_freevars, adaptive_psat'), + ('lookahead.cube.fraction', DOUBLE, 0.4, 'adaptive fraction to create lookahead cubes. Used when lookahead.cube.cutoff is adaptive_freevars or adaptive_psat'), + ('lookahead.cube.depth', UINT, 10, 'cut-off depth to create cubes. Used when lookahead.cube.cutoff is depth.'), + ('lookahead.cube.freevars', DOUBLE, 0.8, 'cube free fariable fraction. Used when lookahead.cube.cutoff is freevars'), ('lookahead.cube.psat.var_exp', DOUBLE, 1, 'free variable exponent for PSAT cutoff'), ('lookahead.cube.psat.clause_base', DOUBLE, 2, 'clause base for PSAT cutoff'), - ('lookahead.cube.psat.trigger', DOUBLE, 5, 'trigger value to create lookahead cubes for PSAT cutoff'), + ('lookahead.cube.psat.trigger', DOUBLE, 5, 'trigger value to create lookahead cubes for PSAT cutoff. Used when lookahead.cube.cutoff is psat'), ('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'),