From b3924d85ed2e0db2daddc5ea31234685d9e84fc7 Mon Sep 17 00:00:00 2001 From: Andreas Froehlich Date: Fri, 25 Apr 2014 13:56:15 +0100 Subject: [PATCH] Cleaned up final SLS version. Enjoy! --- src/tactic/sls/sls_compilation_settings.h | 28 ---- src/tactic/sls/sls_engine.cpp | 43 ++++-- src/tactic/sls/sls_engine.h | 2 + src/tactic/sls/sls_evaluator.h | 8 +- src/tactic/sls/sls_params.pyg | 6 +- src/tactic/sls/sls_tracker.h | 153 ++++++++-------------- 6 files changed, 94 insertions(+), 146 deletions(-) diff --git a/src/tactic/sls/sls_compilation_settings.h b/src/tactic/sls/sls_compilation_settings.h index 707802cf4..e69de29bb 100644 --- a/src/tactic/sls/sls_compilation_settings.h +++ b/src/tactic/sls/sls_compilation_settings.h @@ -1,28 +0,0 @@ -/*++ -Copyright (c) 2014 Microsoft Corporation - -Module Name: - - sls_compilation_constants.h - -Abstract: - - Stochastic Local Search (SLS) compilation constants - -Author: - - Christoph (cwinter) 2014-03-19 - -Notes: - - This file should go away completely once we have evaluated all options. - ---*/ - -#ifndef _SLS_COMPILATION_SETTINGS_H_ -#define _SLS_COMPILATION_SETTINGS_H_ - -// should we use unsat-structures as done in SLS 4 SAT? -#define _REAL_RS_ 0 - -#endif \ No newline at end of file diff --git a/src/tactic/sls/sls_engine.cpp b/src/tactic/sls/sls_engine.cpp index a1c72609c..269790902 100644 --- a/src/tactic/sls/sls_engine.cpp +++ b/src/tactic/sls/sls_engine.cpp @@ -71,6 +71,8 @@ void sls_engine::updt_params(params_ref const & _p) { m_restart_init = p.restart_init(); m_early_prune = p.early_prune(); + m_random_offset = p.random_offset(); + m_rescore = p.rescore(); // 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) @@ -174,6 +176,9 @@ bool sls_engine::what_if( m_mpz_manager.del(old_value); #endif + // Andreas: Had this idea on my last day. Maybe we could add a noise here similar to the one that worked so well for ucb assertion selection. + // r += 0.0001 * m_tracker.get_random_uint(8); + // Andreas: For some reason it is important to use > here instead of >=. Probably related to prefering the LSB. if (r > best_score) { best_score = r; @@ -248,9 +253,15 @@ void sls_engine::mk_random_move(ptr_vector & unsat_constants) { if (m_mpz_manager.is_one(m_tracker.get_random_bool())) rnd_mv = 2; if (m_mpz_manager.is_one(m_tracker.get_random_bool())) rnd_mv++; + + // Andreas: The other option would be to scale the probability for flips according to the bit-width. + /* unsigned bv_sz2 = m_bv_util.get_bv_size(srt); + rnd_mv = m_tracker.get_random_uint(16) % (bv_sz2 + 3); + if (rnd_mv > 3) rnd_mv = 0; */ + move_type mt = (move_type)rnd_mv; - // inversion doesn't make sense, let's do a flip instead. + // Andreas: Christoph claimed inversion doesn't make sense, let's do a flip instead. Is this really true? if (mt == MV_INV) mt = MV_FLIP; unsigned bit = 0; @@ -306,10 +317,13 @@ double sls_engine::find_best_move( unsigned bv_sz; double new_score = score; - //unsigned offset = m_tracker.get_random_uint(16) % to_evaluate.size(); - //for (unsigned j = 0; j < to_evaluate.size(); j++) { - //unsigned i = (j + offset) % to_evaluate.size(); - for (unsigned i = 0; i < to_evaluate.size(); i++) { + // Andreas: Introducting a bit of randomization by using a random offset and a random direction to go through the candidate list. + unsigned sz = to_evaluate.size(); + unsigned offset = (m_random_offset) ? m_tracker.get_random_uint(16) % sz : 0; + for (unsigned j = 0; j < sz; j++) { + unsigned i = j + offset; + if (i >= sz) i -= sz; + //for (unsigned i = 0; i < to_evaluate.size(); i++) { func_decl * fd = to_evaluate[i]; sort * srt = fd->get_range(); bv_sz = (m_manager.is_bool(srt)) ? 1 : m_bv_util.get_bv_size(srt); @@ -361,7 +375,13 @@ double sls_engine::find_best_move_mc(ptr_vector & to_evaluate, double unsigned bv_sz; double new_score = score; - for (unsigned i = 0; i < to_evaluate.size(); i++) { + // Andreas: Introducting a bit of randomization by using a random offset and a random direction to go through the candidate list. + unsigned sz = to_evaluate.size(); + unsigned offset = (m_random_offset) ? m_tracker.get_random_uint(16) % sz : 0; + for (unsigned j = 0; j < sz; j++) { + unsigned i = j + offset; + if (i >= sz) i -= sz; + //for (unsigned i = 0; i < to_evaluate.size(); i++) { func_decl * fd = to_evaluate[i]; sort * srt = fd->get_range(); bv_sz = (m_manager.is_bool(srt)) ? 1 : m_bv_util.get_bv_size(srt); @@ -405,15 +425,16 @@ lbool sls_engine::search() { while (check_restart(m_stats.m_moves)) { checkpoint(); m_stats.m_moves++; + + // Andreas: Every base restart interval ... if (m_stats.m_moves % m_restart_base == 0) { + // ... potentially smooth the touched counters ... m_tracker.ucb_forget(m_assertions); - //score = rescore(); + // ... or normalize the top-level score. + if (m_rescore) score = rescore(); } -#if _REAL_RS_ - //m_tracker.debug_real(g, m_stats.m_moves); -#endif // get candidate variables ptr_vector & to_evaluate = m_tracker.get_unsat_constants(m_assertions); if (!to_evaluate.size()) @@ -513,8 +534,6 @@ void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) { for (unsigned i = 0; i < g->size(); i++) assert_expr(g->form(i)); - verbose_stream() << "_REAL_RS_ " << _REAL_RS_ << std::endl; - lbool res = operator()(); if (res == l_true) { diff --git a/src/tactic/sls/sls_engine.h b/src/tactic/sls/sls_engine.h index ac8610871..8158808fa 100644 --- a/src/tactic/sls/sls_engine.h +++ b/src/tactic/sls/sls_engine.h @@ -82,6 +82,8 @@ protected: unsigned m_restart_next; unsigned m_restart_init; unsigned m_early_prune; + unsigned m_random_offset; + unsigned m_rescore; 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 e4cf3c466..61afb7457 100644 --- a/src/tactic/sls/sls_evaluator.h +++ b/src/tactic/sls/sls_evaluator.h @@ -22,7 +22,6 @@ Notes: #include"model_evaluator.h" -#include"sls_compilation_settings.h" #include"sls_powers.h" #include"sls_tracker.h" @@ -540,19 +539,16 @@ public: (*this)(to_app(cur), new_value); m_tracker.set_value(cur, new_value); -#if _REAL_RS_ + new_score = m_tracker.score(cur); if (m_tracker.is_top_expr(cur)) { + m_tracker.adapt_top_sum(cur, new_score, m_tracker.get_score(cur)); if (m_mpz_manager.eq(new_value,m_one)) m_tracker.make_assertion(cur); else m_tracker.break_assertion(cur); } -#endif - new_score = m_tracker.score(cur); - 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); m_tracker.set_score_prune(cur, new_score); diff --git a/src/tactic/sls/sls_params.pyg b/src/tactic/sls/sls_params.pyg index 98875b20d..ad7a22675 100644 --- a/src/tactic/sls/sls_params.pyg +++ b/src/tactic/sls/sls_params.pyg @@ -8,15 +8,19 @@ def_module_params('sls', ('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_ucb_noise', DOUBLE, 0.0002, 'add noise 0 <= 256 * ucb_noise to ucb score for assertion selection'), ('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'), + ('wp', UINT, 100, '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_offset', BOOL, 1, 'use random offset vor candidate evaluation'), + ('rescore', BOOL, 1, 'rescore/normalize top-level score every base restart interval'), + ('track_unsat', BOOL, 0, 'keep a list of unsat assertions as done in SAT - currently disabled internally'), ('random_seed', UINT, 0, 'random seed') )) diff --git a/src/tactic/sls/sls_tracker.h b/src/tactic/sls/sls_tracker.h index 507596273..4356bcc9b 100644 --- a/src/tactic/sls/sls_tracker.h +++ b/src/tactic/sls/sls_tracker.h @@ -80,14 +80,13 @@ private: double m_ucb_constant; unsigned m_ucb_init; double m_ucb_forget; + double m_ucb_noise; unsigned m_touched; double m_scale_unsat; unsigned m_paws_init; -#if _REAL_RS_ - ptr_vector m_unsat_expr; obj_map m_where_false; expr** m_list_false; -#endif + unsigned m_track_unsat; obj_map m_weights; double m_top_sum; @@ -116,8 +115,12 @@ public: m_ucb_constant = p.walksat_ucb_constant(); m_ucb_init = p.walksat_ucb_init(); m_ucb_forget = p.walksat_ucb_forget(); + m_ucb_noise = p.walksat_ucb_noise(); m_scale_unsat = p.scale_unsat(); m_paws_init = p.paws_init(); + // Andreas: track_unsat is currently disabled because I cannot guarantee that it is not buggy. + // If you want to use it, you will also need to change comments in the assertion selection. + m_track_unsat = 0;//p.track_unsat(); } /* Andreas: Tried to give some measure for the formula size by the following two methods but both are not used currently. @@ -254,53 +257,6 @@ public: return m_uplinks.find(n); } -#if _REAL_RS_ - void debug_real(goal_ref const & g, unsigned flip) - { - unsigned count = 0; - for (unsigned i = 0; i < g->size(); i++) - { - expr * e = g->form(i); - if (m_mpz_manager.eq(get_value(e),m_one) && m_where_false.contains(e)) - { - printf("iteration %d: ", flip); - printf("form %d is sat but in unsat list at position %d of %d\n", i, m_where_false.find(e), m_where_false.size()); - exit(4); - } - - if (m_mpz_manager.eq(get_value(e),m_zero) && !m_where_false.contains(e)) - { - printf("iteration %d: ", flip); - printf("form %d is unsat but not in unsat list\n", i); - exit(4); - } - - if (m_mpz_manager.eq(get_value(e),m_zero) && m_where_false.contains(e)) - { - unsigned pos = m_where_false.find(e); - expr * q = m_list_false[pos]; - if (q != e) - { - printf("iteration %d: ", flip); - printf("form %d is supposed to be at pos %d in unsat list but something else was there\n", i, pos); - exit(4); - } - } - - if (m_mpz_manager.eq(get_value(e),m_zero)) - count++; - } - - // should be true now that duplicate assertions are removed - if (count != m_where_false.size()) - { - printf("iteration %d: ", flip); - printf("%d are unsat but list is of size %d\n", count, m_where_false.size()); - exit(4); - } - } -#endif - inline void ucb_forget(ptr_vector & as) { if (m_ucb_forget < 1.0) { @@ -474,14 +430,15 @@ public: TRACE("sls", tout << "Initial model:" << std::endl; show_model(tout); ); -#if _REAL_RS_ - m_list_false = new expr*[sz]; - //for (unsigned i = 0; i < sz; i++) - //{ - // if (m_mpz_manager.eq(get_value(g->form(i)),m_zero)) - // break_assertion(g->form(i)); - //} -#endif + if (m_track_unsat) + { + m_list_false = new expr*[sz]; + for (unsigned i = 0; i < sz; i++) + { + if (m_mpz_manager.eq(get_value(as[i]), m_zero)) + break_assertion(as[i]); + } + } for (unsigned i = 0; i < sz; i++) { @@ -515,44 +472,36 @@ public: return m_weights.find(e); } -#if _REAL_RS_ void make_assertion(expr * e) { - if (m_where_false.contains(e)) + if (m_track_unsat) { - unsigned pos = m_where_false.find(e); - m_where_false.erase(e); - if (pos != m_where_false.size()) + if (m_where_false.contains(e)) { - expr * q = m_list_false[m_where_false.size()]; - m_list_false[pos] = q; - m_where_false.find(q) = pos; - //printf("Moving %d from %d to %d\n", q, m_where_false.size(), pos); + unsigned pos = m_where_false.find(e); + m_where_false.erase(e); + if (pos != m_where_false.size()) + { + expr * q = m_list_false[m_where_false.size()]; + m_list_false[pos] = q; + m_where_false.find(q) = pos; + } } - //else - //printf("Erasing %d from %d to %d\n", e, pos); -// m_list_false[m_where_false.size()] = 0; -// printf("Going in %d\n", m_where_false.size()); } - //if (m_unsat_expr.contains(e)) - //m_unsat_expr.erase(e); } void break_assertion(expr * e) { - //printf("I'm broken... that's still fine.\n"); - if (!m_where_false.contains(e)) + if (m_track_unsat) { - //printf("This however is not so cool...\n"); - unsigned pos = m_where_false.size(); - m_list_false[pos] = e; - m_where_false.insert(e, pos); - // printf("Going in %d\n", m_where_false.size()); + if (!m_where_false.contains(e)) + { + unsigned pos = m_where_false.size(); + m_list_false[pos] = e; + m_where_false.insert(e, pos); + } } - //if (!m_unsat_expr.contains(e)) - //m_unsat_expr.push_back(e); } -#endif void show_model(std::ostream & out) { unsigned sz = get_num_constants(); @@ -1043,24 +992,38 @@ public: { value_score vscore; double max = -1.0; + // Andreas: Commented things here might be used for track_unsat data structures as done in SLS for SAT. But seems to have no benefit. + /* for (unsigned i = 0; i < m_where_false.size(); i++) { + expr * e = m_list_false[i]; */ for (unsigned i = 0; i < sz; i++) { expr * e = as[i]; -// 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); - 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 (m_mpz_manager.neq(get_value(e), m_one)) + { + vscore = m_scores.find(e); + // Andreas: Select the assertion with the greatest ucb score. Potentially add some noise. + // 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) + m_ucb_noise * get_random_uint(8); + if (q > max) { max = q; pos = i; } + } } if (pos == static_cast(-1)) return 0; - m_scores.find(as[pos]).touched++; m_touched++; -// return m_list_false[pos]; + m_scores.find(as[pos]).touched++; + // Andreas: Also part of track_unsat data structures. Additionally disable the previous line! + /* m_last_pos = pos; + m_scores.find(m_list_false[pos]).touched++; + return m_list_false[pos]; */ } else { + // Andreas: The track_unsat data structures for random assertion selection. + /* sz = m_where_false.size(); + if (sz == 0) + return 0; + return m_list_false[get_random_uint(16) % sz]; */ + unsigned cnt_unsat = 0; for (unsigned i = 0; i < sz; i++) if (m_mpz_manager.neq(get_value(as[i]), m_one) && (get_random_uint(16) % ++cnt_unsat == 0)) pos = i; @@ -1070,14 +1033,6 @@ public: m_last_pos = pos; return as[pos]; -#if _REAL_RS_ - //unsigned pos = m_false_list[get_random_uint(16) % m_cnt_false]; - //expr * e = m_unsat_expr[get_random_uint(16) % m_unsat_expr.size()]; - sz = m_where_false.size(); - if (sz == 0) - return 0; - return m_list_false[get_random_uint(16) % sz]; -#endif } expr * get_new_unsat_assertion(ptr_vector const & as) {