diff --git a/src/tactic/sls/sls_compilation_settings.h b/src/tactic/sls/sls_compilation_settings.h index 5c837b4b2..707802cf4 100644 --- a/src/tactic/sls/sls_compilation_settings.h +++ b/src/tactic/sls/sls_compilation_settings.h @@ -22,10 +22,7 @@ Notes: #ifndef _SLS_COMPILATION_SETTINGS_H_ #define _SLS_COMPILATION_SETTINGS_H_ -// should we use unsat-structures as done in SLS 4 SAT instead for random or bfs selection? +// should we use unsat-structures as done in SLS 4 SAT? #define _REAL_RS_ 0 -// shall we use early pruning for incremental update? -#define _EARLY_PRUNE_ 1 - #endif \ No newline at end of file diff --git a/src/tactic/sls/sls_engine.cpp b/src/tactic/sls/sls_engine.cpp index 5d4df237e..a1c72609c 100644 --- a/src/tactic/sls/sls_engine.cpp +++ b/src/tactic/sls/sls_engine.cpp @@ -70,6 +70,8 @@ void sls_engine::updt_params(params_ref const & _p) { m_restart_next = m_restart_base; m_restart_init = p.restart_init(); + m_early_prune = p.early_prune(); + // Andreas: Would cause trouble because repick requires an assertion being picked before which is not the case in GSAT. if (m_walksat_repick && !m_walksat) NOT_IMPLEMENTED_YET(); @@ -117,7 +119,7 @@ double sls_engine::top_score() { m_tracker.set_top_sum(top_sum); - return top_sum / (double)sz; + return top_sum; } double sls_engine::rescore() { @@ -129,21 +131,21 @@ double sls_engine::rescore() { double sls_engine::serious_score(func_decl * fd, const mpz & new_value) { m_evaluator.serious_update(fd, new_value); m_stats.m_incr_evals++; - return (m_tracker.get_top_sum() / m_assertions.size()); + return m_tracker.get_top_sum(); } double sls_engine::incremental_score(func_decl * fd, const mpz & new_value) { m_evaluator.update(fd, new_value); m_stats.m_incr_evals++; - return (m_tracker.get_top_sum() / m_assertions.size()); + return m_tracker.get_top_sum(); } double sls_engine::incremental_score_prune(func_decl * fd, const mpz & new_value) { m_stats.m_incr_evals++; if (m_evaluator.update_prune(fd, new_value)) - return (m_tracker.get_top_sum() / m_assertions.size()); + return m_tracker.get_top_sum(); else - return 0.0; + return -DBL_MAX; } // checks whether the score outcome of a given move is better than the previous score @@ -160,11 +162,11 @@ bool sls_engine::what_if( m_mpz_manager.set(old_value, m_tracker.get_value(fd)); #endif -#if _EARLY_PRUNE_ - double r = incremental_score_prune(fd, temp); -#else - double r = incremental_score(fd, temp); -#endif + double r; + if (m_early_prune) + r = incremental_score_prune(fd, temp); + else + r = incremental_score(fd, temp); #ifdef Z3DEBUG TRACE("sls_whatif", tout << "WHAT IF " << fd->get_name() << " WERE " << m_mpz_manager.to_string(temp) << " --> " << r << std::endl;); @@ -342,11 +344,8 @@ double sls_engine::find_best_move( if (what_if(fd, i, temp, new_score, best_const, best_value)) move = MV_INV; } - // reset to what it was before - double check = incremental_score(fd, old_value); - // Andreas: does not hold anymore now that we use top level score caching - //SASSERT(check == score); + incremental_score(fd, old_value); } m_mpz_manager.del(old_value); @@ -381,9 +380,8 @@ double sls_engine::find_best_move_mc(ptr_vector & to_evaluate, double } } } - // reset to what it was before - double check = incremental_score(fd, old_value); + incremental_score(fd, old_value); } m_mpz_manager.del(old_value); @@ -408,7 +406,10 @@ lbool sls_engine::search() { checkpoint(); m_stats.m_moves++; if (m_stats.m_moves % m_restart_base == 0) + { m_tracker.ucb_forget(m_assertions); + //score = rescore(); + } #if _REAL_RS_ //m_tracker.debug_real(g, m_stats.m_moves); @@ -425,7 +426,7 @@ lbool sls_engine::search() { if (m_wp && m_tracker.get_random_uint(10) < m_wp) { mk_random_move(to_evaluate); - score = m_tracker.get_top_sum() / sz; + score = m_tracker.get_top_sum(); continue; } @@ -465,7 +466,7 @@ lbool sls_engine::search() { else m_evaluator.randomize_local(to_evaluate); - score = m_tracker.get_top_sum() / m_assertions.size(); + score = m_tracker.get_top_sum(); // update assertion weights if a weigthing is enabled (sp < 1024) if (m_paws) @@ -513,7 +514,6 @@ void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) { assert_expr(g->form(i)); verbose_stream() << "_REAL_RS_ " << _REAL_RS_ << std::endl; - verbose_stream() << "_EARLY_PRUNE_ " << _EARLY_PRUNE_ << std::endl; lbool res = operator()(); diff --git a/src/tactic/sls/sls_engine.h b/src/tactic/sls/sls_engine.h index 94f3fa626..ac8610871 100644 --- a/src/tactic/sls/sls_engine.h +++ b/src/tactic/sls/sls_engine.h @@ -81,8 +81,7 @@ protected: unsigned m_restart_base; unsigned m_restart_next; unsigned m_restart_init; - - ptr_vector m_old_values; + unsigned m_early_prune; typedef enum { MV_FLIP = 0, MV_INC, MV_DEC, MV_INV } move_type; diff --git a/src/tactic/sls/sls_evaluator.h b/src/tactic/sls/sls_evaluator.h index 200a0e380..e4cf3c466 100644 --- a/src/tactic/sls/sls_evaluator.h +++ b/src/tactic/sls/sls_evaluator.h @@ -554,9 +554,7 @@ public: if (m_tracker.is_top_expr(cur)) m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur)); m_tracker.set_score(cur, new_score); -#if _EARLY_PRUNE_ m_tracker.set_score_prune(cur, new_score); -#endif if (m_tracker.has_uplinks(cur)) { ptr_vector & ups = m_tracker.get_uplinks(cur); @@ -599,9 +597,6 @@ public: if (m_tracker.is_top_expr(cur)) m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur)); m_tracker.set_score(cur, new_score); -#if _EARLY_PRUNE_ - m_tracker.set_score_prune(cur, new_score); -#endif if (m_tracker.has_uplinks(cur)) { ptr_vector & ups = m_tracker.get_uplinks(cur); for (unsigned j = 0; j < ups.size(); j++) { diff --git a/src/tactic/sls/sls_params.pyg b/src/tactic/sls/sls_params.pyg index cc3e05966..98875b20d 100644 --- a/src/tactic/sls/sls_params.pyg +++ b/src/tactic/sls/sls_params.pyg @@ -2,7 +2,21 @@ def_module_params('sls', export=True, description='Experimental Stochastic Local Search Solver (for QFBV only).', params=(max_memory_param(), - ('restarts', UINT, UINT_MAX, '(max) number of restarts'), - ('plateau_limit', UINT, 10, 'pleateau limit'), - ('random_seed', UINT, 0, 'random seed') + ('max_restarts', UINT, UINT_MAX, 'maximum number of restarts'), + ('walksat', BOOL, 1, 'use walksat assertion selection (instead of gsat)'), + ('walksat_ucb', BOOL, 1, 'use bandit heuristic for walksat assertion selection (instead of random)'), + ('walksat_ucb_constant', DOUBLE, 20.0, 'the ucb constant c in the term score + c * f(touched)'), + ('walksat_ucb_init', BOOL, 0, 'initialize total ucb touched to formula size'), + ('walksat_ucb_forget', DOUBLE, 1.0, 'scale touched by this factor every base restart interval'), + ('walksat_repick', BOOL, 1, 'repick assertion if randomizing in local minima'), + ('scale_unsat', DOUBLE, 0.5, 'scale score of unsat expressions by this factor'), + ('paws_init', UINT, 40, 'initial/minimum assertion weights'), + ('paws_sp', UINT, 52, 'smooth assertion weights with probability paws_sp / 1024'), + ('wp', UINT, 0, 'random walk with probability wp / 1024'), + ('vns_mc', UINT, 0, 'in local minima, try Monte Carlo sampling vns_mc many 2-bit-flips per bit'), + ('vns_repick', BOOL, 0, 'in local minima, try picking a different assertion (only for walksat)'), + ('restart_base', UINT, 100, 'base restart interval given by moves per run'), + ('restart_init', BOOL, 0, 'initialize to 0 or random value (= 1) after restart'), + ('early_prune', BOOL, 1, 'use early pruning for score prediction'), + ('random_seed', UINT, 0, 'random seed') )) diff --git a/src/tactic/sls/sls_tracker.h b/src/tactic/sls/sls_tracker.h index a815c9ad3..507596273 100644 --- a/src/tactic/sls/sls_tracker.h +++ b/src/tactic/sls/sls_tracker.h @@ -44,11 +44,9 @@ class sls_tracker { unsynch_mpz_manager * m; mpz value; double score; -#if _EARLY_PRUNE_ double score_prune; unsigned has_pos_occ; unsigned has_neg_occ; -#endif unsigned distance; // max distance from any root unsigned touched; value_score & operator=(const value_score & other) { @@ -122,6 +120,7 @@ public: m_paws_init = p.paws_init(); } + /* Andreas: Tried to give some measure for the formula size by the following two methods but both are not used currently. unsigned get_formula_size() { return m_scores.size(); } @@ -145,7 +144,7 @@ public: } return sum / count; - } + }*/ inline void adapt_top_sum(expr * e, double add, double sub) { m_top_sum += m_weights.find(e) * (add - sub); @@ -417,6 +416,8 @@ public: } } + /* Andreas: Used this at some point to have values for the non-top-level expressions. + However, it did not give better performance but even cause some additional m/o - is not used currently. void initialize_recursive(init_proc proc, expr_mark visited, expr * e) { if (m_manager.is_and(e) || m_manager.is_or(e)) { app * a = to_app(e); @@ -445,7 +446,7 @@ public: find_func_decls_proc ffd_proc(m_manager, m_constants_occ.find(e)); expr_fast_mark1 visited; quick_for_each_expr(ffd_proc, visited, e); - } + }*/ void initialize(ptr_vector const & as) { init_proc proc(m_manager, *this); @@ -455,8 +456,6 @@ public: expr * e = as[i]; if (!m_top_expr.contains(e)) m_top_expr.insert(e); - else - printf("this is already in ...\n"); for_each_expr(proc, visited, e); } @@ -464,7 +463,6 @@ public: for (unsigned i = 0; i < sz; i++) { expr * e = as[i]; - // Andreas: Maybe not fully correct. ptr_vector t; m_constants_occ.insert_if_not_there(e, t); find_func_decls_proc ffd_proc(m_manager, m_constants_occ.find(e)); @@ -488,15 +486,16 @@ public: for (unsigned i = 0; i < sz; i++) { expr * e = as[i]; - if (!m_weights.contains(e)) + + // initialize weights + if (!m_weights.contains(e)) m_weights.insert(e, m_paws_init); + + // positive/negative occurences used for early pruning + setup_occs(as[i]); } -#if _EARLY_PRUNE_ - for (unsigned i = 0; i < sz; i++) - setup_occs(as[i]); -#endif - + // initialize ucb total touched value (individual ones are always initialized to 1) m_touched = m_ucb_init ? as.size() : 1; } @@ -738,7 +737,6 @@ public: SASSERT(!negated); app * a = to_app(n); expr * const * args = a->get_args(); - // Andreas: Seems to have no effect. Probably it is still too similar to the original version. double max = 0.0; for (unsigned i = 0; i < a->get_num_args(); i++) { double cur = get_score(args[i]); @@ -764,7 +762,6 @@ public: const mpz & v1 = get_value(arg1); if (negated) { - //res = (m_mpz_manager.eq(v0, v1)) ? 0.5 * (m_bv_util.get_bv_size(arg0) - 1.0) / m_bv_util.get_bv_size(arg0) : 1.0; res = (m_mpz_manager.eq(v0, v1)) ? 0.0 : 1.0; TRACE("sls_score", tout << "V0 = " << m_mpz_manager.to_string(v0) << " ; V1 = " << m_mpz_manager.to_string(v1) << std::endl; ); @@ -1051,10 +1048,8 @@ public: // for (unsigned i = 0; i < m_where_false.size(); i++) { // expr * e = m_list_false[i]; vscore = m_scores.find(e); - double q = vscore.score + m_ucb_constant * sqrt(log((double)m_touched) / vscore.touched); -#if _UCT_ == 3 - double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched) + (get_random_uint(16) * 0.1 / (2<<16)); -#endif + //double q = vscore.score + m_ucb_constant * sqrt(log((double)m_touched) / vscore.touched); + double q = vscore.score + m_ucb_constant * sqrt(log((double)m_touched) / vscore.touched) + (get_random_uint(8) * 0.0000002); if (q > max && m_mpz_manager.neq(get_value(e), m_one) ) { max = q; pos = i; } } if (pos == static_cast(-1))