diff --git a/src/sat/sat_sls.cpp b/src/sat/sat_sls.cpp index 128152952..12900e94e 100644 --- a/src/sat/sat_sls.cpp +++ b/src/sat/sat_sls.cpp @@ -18,6 +18,7 @@ Notes: --*/ #include "sat_sls.h" +#include "sat_solver.h" namespace sat { @@ -50,47 +51,170 @@ namespace sat { } sls::sls(solver& s): s(s) { - + m_max_tries = 10000; + m_prob_choose_min_var = 43; } sls::~sls() { - - } - -#if 0 - bool_var sls::pick_flip() { - unsigned clause_idx = m_false.choose(m_rand); - clause const& c = m_clauses[clause_idx]; - unsigned result = UINT_MAX; - m_min_vars.reset(); - for (unsigned i = 0; i < c.size(); ++i) { - + for (unsigned i = 0; i < m_bin_clauses.size(); ++i) { + m_alloc.del_clause(m_bin_clauses[i]); } } - void sls::flip(bool_var v) { - - } - - bool sls::local_search() { - for (unsigned i = 0; !m_false.empty() && i < m_max_flips; ++i) { - flip(pick_flip()); - } - return m_false.empty(); - } - -#endif - - lbool sls::operator()() { -#if 0 + lbool sls::operator()(unsigned sz, literal const* tabu) { + init(sz, tabu); + for (unsigned i = 0; i < m_max_tries; ++i) { - if (local_search()) { + flip(); + if (m_false.empty()) { + SASSERT(s.check_model(m_model)); return l_true; } } -#endif return l_undef; } + void sls::init(unsigned sz, literal const* tabu) { + init_clauses(); + init_model(sz, tabu); + init_use(); + } + + void sls::init_clauses() { + for (unsigned i = 0; i < m_bin_clauses.size(); ++i) { + m_alloc.del_clause(m_bin_clauses[i]); + } + m_clauses.reset(); + clause * const * it = s.begin_clauses(); + clause * const * end = s.end_clauses(); + for (; it != end; ++it) { + m_clauses.push_back(*it); + } + svector bincs; + s.collect_bin_clauses(bincs, false); + literal lits[2]; + for (unsigned i = 0; i < bincs.size(); ++i) { + lits[0] = bincs[i].first; + lits[1] = bincs[i].second; + m_clauses.push_back(m_alloc.mk_clause(2, lits, false)); + } + } + + void sls::init_model(unsigned sz, literal const* tabu) { + m_num_true.reset(); + m_model.reset(); + m_model.append(s.get_model()); + m_tabu.reset(); + m_tabu.resize(s.num_vars(), false); + for (unsigned i = 0; i < sz; ++i) { + m_model[tabu[i].var()] = tabu[i].sign()?l_false:l_true; + } + + sz = m_clauses.size(); + for (unsigned i = 0; i < sz; ++i) { + clause const& c = *m_clauses[i]; + unsigned n = 0; + unsigned csz = c.size(); + for (unsigned j = 0; j < csz; ++j) { + if (value_at(c[j], m_model) == l_true) { + ++n; + } + } + m_num_true.push_back(n); + if (n == 0) { + m_false.insert(i); + } + } + } + + void sls::init_use() { + m_use_list.reset(); + m_use_list.resize(s.num_vars()*2); + unsigned sz = m_clauses.size(); + for (unsigned i = 0; i < sz; ++i) { + clause const& c = *m_clauses[i]; + unsigned csz = c.size(); + for (unsigned j = 0; j < csz; ++j) { + m_use_list[c[j].index()].push_back(i); + } + } + } + + unsigned_vector const& sls::get_use(literal lit) { + SASSERT(lit.index() < m_use_list.size()); + return m_use_list[lit.index()]; + } + + unsigned sls::get_break_count(literal lit, unsigned min_break) { + SASSERT(value_at(lit, m_model) == l_false); + unsigned result = 0; + unsigned_vector const& uses = get_use(~lit); + unsigned sz = uses.size(); + for (unsigned i = 0; i < sz; ++i) { + if (m_num_true[uses[i]] == 1) { + ++result; + if (result > min_break) return result; + } + } + return result; + } + + bool sls::pick_flip(literal& lit) { + unsigned clause_idx = m_false.choose(m_rand); + clause const& c = *m_clauses[clause_idx]; + SASSERT(!c.satisfied_by(m_model)); + unsigned min_break = UINT_MAX; + unsigned sz = c.size(); + m_min_vars.reset(); + for (unsigned i = 0; i < sz; ++i) { + lit = c[i]; + if (m_tabu[lit.var()]) continue; + unsigned break_count = get_break_count(lit, min_break); + if (break_count < min_break) { + min_break = break_count; + m_min_vars.reset(); + m_min_vars.push_back(lit); + } + else if (break_count == min_break) { + m_min_vars.push_back(lit); + } + } + if (min_break == 0 || (m_min_vars.empty() && m_rand(100) >= m_prob_choose_min_var)) { + lit = m_min_vars[m_rand(m_min_vars.size())]; + return true; + } + else if (min_break == UINT_MAX) { + return false; + } + else { + lit = c[m_rand(c.size())]; + return !m_tabu[lit.var()]; + } + } + + void sls::flip() { + literal lit; + if (!pick_flip(lit)) return; + SASSERT(value_at(lit, m_model) == l_false); + m_model[lit.var()] = lit.sign()?l_true:l_false; + SASSERT(value_at(lit, m_model) == l_true); + unsigned_vector const& use1 = get_use(lit); + unsigned sz = use1.size(); + for (unsigned i = 0; i < sz; ++i) { + unsigned cl = use1[i]; + m_num_true[cl]++; + SASSERT(m_num_true[cl] <= m_clauses[cl]->size()); + if (m_num_true[cl] == 1) m_false.remove(cl); + } + unsigned_vector const& use2 = get_use(~lit); + sz = use2.size(); + for (unsigned i = 0; i < sz; ++i) { + unsigned cl = use2[i]; + SASSERT(m_num_true[cl] > 0); + m_num_true[cl]--; + if (m_num_true[cl] == 0) m_false.insert(cl); + } + } + }; diff --git a/src/sat/sat_sls.h b/src/sat/sat_sls.h index 80f660317..438623bcb 100644 --- a/src/sat/sat_sls.h +++ b/src/sat/sat_sls.h @@ -41,18 +41,30 @@ namespace sat { solver& s; random_gen m_rand; unsigned m_max_tries; - unsigned m_max_flips; - index_set m_false; - use_list m_use_list; - vector m_clauses; + unsigned m_prob_choose_min_var; // number between 0 and 99. + ptr_vector m_clauses; // vector of all clauses. + index_set m_false; // clauses currently false + vector m_use_list; // use lists for literals + unsigned_vector m_num_true; // per clause, count of # true literals + svector m_min_vars; // literals with smallest break count + model m_model; // current model + clause_allocator m_alloc; // clause allocator + clause_vector m_bin_clauses; // binary clauses + svector m_tabu; // variables that cannot be swapped public: sls(solver& s); ~sls(); - lbool operator()(); + lbool operator()(unsigned sz, literal const* tabu); private: bool local_search(); - bool_var pick_flip(); - void flip(bool_var v); + void init(unsigned sz, literal const* tabu); + void init_model(unsigned sz, literal const* tabu); + void init_use(); + void init_clauses(); + bool pick_flip(literal& lit); + void flip(); + unsigned get_break_count(literal lit, unsigned min_break); + unsigned_vector const& get_use(literal lit); }; }; diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index e0b386c24..804bea5ce 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -135,6 +135,7 @@ namespace sat { friend class probing; friend class iff3_finder; friend class mus; + friend class sls; friend struct mk_stat; public: solver(params_ref const & p, extension * ext);