From 24dd047892ea2729a0bf3aed00bb775cadecddd9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 18 Mar 2020 11:06:19 -0700 Subject: [PATCH] fix #3397, use it or lose it Signed-off-by: Nikolaj Bjorner --- src/sat/sat_config.cpp | 4 +--- src/sat/sat_config.h | 3 +-- src/sat/sat_params.pyg | 2 +- src/sat/sat_solver.cpp | 15 +-------------- 4 files changed, 4 insertions(+), 20 deletions(-) diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index b4a038eb3..0adb8c94a 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -204,10 +204,8 @@ namespace sat { m_branching_heuristic = BH_VSIDS; else if (p.branching_heuristic() == symbol("chb")) m_branching_heuristic = BH_CHB; - else if (p.branching_heuristic() == symbol("lrb")) - m_branching_heuristic = BH_LRB; else - throw sat_param_exception("invalid branching heuristic: accepted heuristics are 'vsids', 'lrb' or 'chb'"); + throw sat_param_exception("invalid branching heuristic: accepted heuristics are 'vsids' or 'chb'"); m_anti_exploration = p.branching_anti_exploration(); m_step_size_init = 0.40; diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index 38bbfb00e..2586fb537 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -49,8 +49,7 @@ namespace sat { enum branching_heuristic { BH_VSIDS, - BH_CHB, - BH_LRB + BH_CHB }; enum pb_resolve { diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 8ebf2459a..1198fb4f8 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -22,7 +22,7 @@ def_module_params('sat', ('variable_decay', UINT, 110, 'multiplier (divided by 100) for the VSIDS activity increment'), ('inprocess.max', UINT, UINT_MAX, 'maximal number of inprocessing passes'), ('inprocess.out', SYMBOL, '', 'file to dump result of the first inprocessing step and exit'), - ('branching.heuristic', SYMBOL, 'vsids', 'branching heuristic vsids, lrb or chb'), + ('branching.heuristic', SYMBOL, 'vsids', 'branching heuristic vsids, chb'), ('branching.anti_exploration', BOOL, False, 'apply anti-exploration heuristic for branch selection'), ('random_freq', DOUBLE, 0.01, 'frequency of random case splits'), ('random_seed', UINT, 0, 'random seed'), diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 39217f6f0..5e274c3ce 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -878,10 +878,6 @@ namespace sat { case BH_CHB: m_last_propagation[v] = m_stats.m_conflict; break; - case BH_LRB: - m_participated[v] = 0; - m_reasoned[v] = 0; - break; } if (m_config.m_anti_exploration) { @@ -3472,8 +3468,7 @@ namespace sat { \brief Reset the mark of the variables in the current lemma. */ void solver::reset_lemma_var_marks() { - if (m_config.m_branching_heuristic == BH_LRB || - m_config.m_branching_heuristic == BH_VSIDS) { + if (m_config.m_branching_heuristic == BH_VSIDS) { update_lrb_reasoned(); } literal_vector::iterator it = m_lemma.begin(); @@ -3715,14 +3710,6 @@ namespace sat { m_assignment[(~l).index()] = l_undef; SASSERT(value(v) == l_undef); m_case_split_queue.unassign_var_eh(v); - if (m_config.m_branching_heuristic == BH_LRB) { - uint64_t interval = m_stats.m_conflict - m_last_propagation[v]; - if (interval > 0) { - auto activity = m_activity[v]; - auto reward = (m_config.m_reward_offset * (m_participated[v] + m_reasoned[v])) / interval; - set_activity(v, static_cast(m_step_size * reward + ((1 - m_step_size) * activity))); - } - } if (m_config.m_anti_exploration) { m_canceled[v] = m_stats.m_conflict; }