From ddb9e6e8d4110bba82307d7210e681a543f5f9c8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 Aug 2014 18:30:06 -0700 Subject: [PATCH] fix flipper Signed-off-by: Nikolaj Bjorner --- src/opt/maxres.cpp | 2 +- src/sat/sat_mus.cpp | 3 +- src/sat/sat_mus.h | 2 ++ src/sat/sat_probing.cpp | 1 + src/sat/sat_sls.cpp | 71 +++++++++++++++++++++++++++++++++++------ src/sat/sat_sls.h | 8 +++-- src/sat/sat_solver.cpp | 15 +++++++-- 7 files changed, 86 insertions(+), 16 deletions(-) diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index f31c9e048..ae5396f32 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -179,7 +179,7 @@ public: lbool mus_mss_solver() { init(); init_local(); - //enable_sls(m_asms); + enable_sls(m_asms); ptr_vector mcs; vector > cores; while (m_lower < m_upper) { diff --git a/src/sat/sat_mus.cpp b/src/sat/sat_mus.cpp index 6295513a9..e6c9376ea 100644 --- a/src/sat/sat_mus.cpp +++ b/src/sat/sat_mus.cpp @@ -24,7 +24,7 @@ Notes: namespace sat { - mus::mus(solver& s):s(s) {} + mus::mus(solver& s):s(s), m_is_active(false) {} mus::~mus() {} @@ -42,6 +42,7 @@ namespace sat { lbool mus::operator()() { flet _disable_min(s.m_config.m_minimize_core, false); flet _disable_opt(s.m_config.m_optimize_model, false); + flet _is_active(m_is_active, true); TRACE("sat", tout << "old core: " << s.get_core() << "\n";); IF_VERBOSE(2, verbose_stream() << "(sat.mus " << s.get_core() << ")\n";); reset(); diff --git a/src/sat/sat_mus.h b/src/sat/sat_mus.h index c91464394..2f5879a0e 100644 --- a/src/sat/sat_mus.h +++ b/src/sat/sat_mus.h @@ -23,12 +23,14 @@ namespace sat { class mus { literal_vector m_core; literal_vector m_mus; + bool m_is_active; solver& s; public: mus(solver& s); ~mus(); lbool operator()(); + bool is_active() const { return m_is_active; } private: lbool mus2(); void mr(); diff --git a/src/sat/sat_probing.cpp b/src/sat/sat_probing.cpp index e9710c2d4..165d39ad8 100644 --- a/src/sat/sat_probing.cpp +++ b/src/sat/sat_probing.cpp @@ -196,6 +196,7 @@ namespace sat { s.propagate(false); // make sure propagation queue is empty if (s.inconsistent()) return true; + SASSERT(s.m_qhead == s.m_trail.size()); CASSERT("probing", s.check_invariant()); if (!force && m_counter > 0) return true; diff --git a/src/sat/sat_sls.cpp b/src/sat/sat_sls.cpp index fdb9bd5e2..839519760 100644 --- a/src/sat/sat_sls.cpp +++ b/src/sat/sat_sls.cpp @@ -363,6 +363,7 @@ namespace sat { m_clause_weights.resize(m_clauses.size(), 1); m_sscore.resize(s.num_vars(), 0.0); m_hscore.resize(s.num_vars(), 0); + m_marked.resize(s.num_vars(), false); unsigned num_violated = 0; for (unsigned i = 0; i < m_soft.size(); ++i) { literal lit = m_soft[i]; @@ -453,7 +454,7 @@ namespace sat { else { lit = m_min_vars[m_rand(m_min_vars.size())]; } - TRACE("sat", tout << "flip soft(" << m_min_vars.size() << ") " << lit << "\n";); + TRACE("sat", tout << "flip soft(" << m_min_vars.size() << ", " << m_sscore[lit.var()] << ") " << lit << "\n";); } SASSERT(value_at(lit, m_model) == l_false); @@ -464,9 +465,10 @@ namespace sat { void wsls::wflip(literal lit) { flip(lit); unsigned v = lit.var(); - m_hscore[v] = compute_hscore(v); m_sscore[v] = -m_sscore[v]; + m_hscore[v] = compute_hscore(v); refresh_scores(v); + recompute_hscores(v); } void wsls::update_hard_weights() { @@ -517,7 +519,7 @@ namespace sat { return result; } - int wsls::compute_hscore(unsigned v) { + int wsls::compute_hscore(bool_var v) { literal lit(v, false); if (value_at(lit, m_model) == l_false) { lit.neg(); @@ -548,15 +550,65 @@ namespace sat { return hs; } - void wsls::refresh_scores(unsigned v) { - if (m_hscore[v] > 0) { + void wsls::recompute_hscores(bool_var v) { + literal lit(v, false); + if (value_at(lit, m_model) == l_false) { + lit.neg(); + } + m_marked[v] = true; + unsigned_vector const& use1 = get_use(~lit); + unsigned sz = use1.size(); + unsigned csz; + for (unsigned i = 0; i < sz; ++i) { + unsigned cl = use1[i]; + if (m_num_true[cl] > 2) continue; + clause const& c = *m_clauses[cl]; + csz = c.size(); + for (unsigned j = 0; j < csz; ++j) { + add_refresh(c[j].var()); + } + } + unsigned_vector const& use2 = get_use(lit); + sz = use2.size(); + for (unsigned i = 0; i < sz; ++i) { + unsigned cl = use2[i]; + if (m_num_true[cl] > 2) continue; + clause const& c = *m_clauses[cl]; + csz = c.size(); + for (unsigned j = 0; j < csz; ++j) { + add_refresh(c[j].var()); + } + } + m_marked[v] = false; + for (unsigned i = 0; i < m_to_refresh.size(); ++i) { + v = m_to_refresh[i]; + int hs = compute_hscore(v); + if (hs != m_hscore[v]) { + TRACE("sat_verbose", tout << "refresh: " << v << " from " << m_hscore[v] << " to " << hs << "\n";); + m_hscore[v] = hs; + refresh_scores(v); + } + m_marked[v] = false; + } + m_to_refresh.reset(); + } + + void wsls::add_refresh(bool_var v) { + if (!m_marked[v]) { + m_to_refresh.push_back(v); + m_marked[v] = true; + } + } + + void wsls::refresh_scores(bool_var v) { + if (m_hscore[v] > 0 && !m_tabu[v] && m_sscore[v] == 0) { m_H.insert(v); } else { m_H.remove(v); } if (m_sscore[v] > 0) { - if (m_hscore[v] == 0) { + if (m_hscore[v] == 0 && !m_tabu[v]) { m_S.insert(v); } else { @@ -575,6 +627,7 @@ namespace sat { // - Sum weight(c) for num_true(c) = 1 and (v in c, M(v) or !v in c and !M(v)) for (unsigned v = 0; v < s.num_vars(); ++v) { int hs = compute_hscore(v); + CTRACE("sat", hs != m_hscore[v], display(tout << v << " - computed: " << hs << " - assigned: " << m_hscore[v] << "\n");); SASSERT(m_hscore[v] == hs); } @@ -585,14 +638,14 @@ namespace sat { SASSERT(m_sscore[v] == ss); } - // m_H are values such that m_hscore >= 0. + // m_H are values such that m_hscore > 0 and sscore = 0. for (bool_var v = 0; v < m_hscore.size(); ++v) { - SASSERT(m_hscore[v] > 0 == m_H.contains(v)); + SASSERT((m_hscore[v] > 0 && !m_tabu[v] && m_sscore[v] == 0) == m_H.contains(v)); } // m_S are values such that hscore = 0, sscore > 0 for (bool_var v = 0; v < m_sscore.size(); ++v) { - SASSERT((m_hscore[v] == 0 && m_sscore[v] > 0) == m_S.contains(v)); + SASSERT((m_hscore[v] == 0 && m_sscore[v] > 0 && !m_tabu[v]) == m_S.contains(v)); } } diff --git a/src/sat/sat_sls.h b/src/sat/sat_sls.h index 57b883994..adcc67ec7 100644 --- a/src/sat/sat_sls.h +++ b/src/sat/sat_sls.h @@ -91,6 +91,8 @@ namespace sat { model m_best_model; index_set m_H, m_S; unsigned m_smoothing_probability; + svector m_marked; + unsigned_vector m_to_refresh; public: wsls(solver& s); virtual ~wsls(); @@ -106,8 +108,10 @@ namespace sat { bool pick_wflip(literal & lit); double evaluate_model(); virtual void check_invariant(); - void refresh_scores(unsigned v); - int compute_hscore(unsigned v); + void refresh_scores(bool_var v); + int compute_hscore(bool_var v); + void recompute_hscores(bool_var v); + void add_refresh(bool_var v); }; }; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index e779c9495..a0ba9c391 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -692,6 +692,7 @@ namespace sat { } wlist.set_end(it2); } + SASSERT(m_qhead == m_trail.size()); SASSERT(!m_inconsistent); return true; } @@ -952,10 +953,15 @@ namespace sat { /** \brief Apply all simplifications. + */ void solver::simplify_problem() { - pop(scope_lvl()); - m_trail.reset(); + + // Disable simplification during MUS computation. + // if (m_mus.is_active()) return; + TRACE("sat", tout << "simplify\n";); + + pop(scope_lvl()); SASSERT(scope_lvl() == 0); @@ -990,6 +996,9 @@ namespace sat { m_ext->clauses_modifed(); m_ext->simplify(); } + + TRACE("sat", display(tout << "consistent: " << (!inconsistent()) << "\n");); + reinit_assumptions(); } @@ -2144,7 +2153,7 @@ namespace sat { // ----------------------- void solver::push() { SASSERT(!inconsistent()); - TRACE("sat", tout << "q:" << m_qhead << " trail: " << m_trail.size() << "\n";); + TRACE("sat_verbose", tout << "q:" << m_qhead << " trail: " << m_trail.size() << "\n";); SASSERT(m_qhead == m_trail.size()); m_scopes.push_back(scope()); scope & s = m_scopes.back();