From b9287343487fdaf208fa32e9fc5c5a55478a462d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 1 Aug 2014 16:11:52 -0700 Subject: [PATCH] perf improvements, mus Signed-off-by: Nikolaj Bjorner --- src/opt/inc_sat_solver.cpp | 16 ++-- src/opt/mus.cpp | 4 +- src/sat/sat_mus.cpp | 163 +++++++++++++++++++++++++++++++++++++ src/sat/sat_mus.h | 44 ++++++++++ src/sat/sat_params.pyg | 1 + src/sat/sat_solver.cpp | 29 ++++--- src/sat/sat_solver.h | 6 +- 7 files changed, 242 insertions(+), 21 deletions(-) create mode 100644 src/sat/sat_mus.cpp create mode 100644 src/sat/sat_mus.h diff --git a/src/opt/inc_sat_solver.cpp b/src/opt/inc_sat_solver.cpp index 72cff950a..c307ef6ae 100644 --- a/src/opt/inc_sat_solver.cpp +++ b/src/opt/inc_sat_solver.cpp @@ -43,7 +43,6 @@ class inc_sat_solver : public solver { model_ref m_model; model_converter_ref m_mc; tactic_ref m_preprocess; - statistics m_stats; unsigned m_num_scopes; sat::literal_vector m_asms; goal_ref_buffer m_subgoals; @@ -89,7 +88,8 @@ public: virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) { m_solver.pop_to_base_level(); dep2asm_t dep2asm; - + + m_model.reset(); lbool r = internalize_formulas(); if (r != l_true) return r; r = internalize_assumptions(num_assumptions, assumptions, dep2asm); @@ -98,7 +98,6 @@ public: r = m_solver.check(m_asms.size(), m_asms.c_ptr()); switch (r) { case l_true: - extract_model(); break; case l_false: // TBD: expr_dependency core is not accounted for. @@ -109,7 +108,6 @@ public: default: break; } - m_solver.collect_statistics(m_stats); return r; } virtual void set_cancel(bool f) { @@ -155,13 +153,17 @@ public: } virtual void collect_statistics(statistics & st) const { - st.copy(m_stats); + m_preprocess->collect_statistics(st); + m_solver.collect_statistics(st); } virtual void get_unsat_core(ptr_vector & r) { r.reset(); r.append(m_core.size(), m_core.c_ptr()); } virtual void get_model(model_ref & m) { + if (!m_model) { + extract_model(); + } m = m_model; } virtual proof * get_proof() { @@ -190,7 +192,6 @@ private: } catch (tactic_exception & ex) { IF_VERBOSE(0, verbose_stream() << "exception in tactic " << ex.msg() << "\n";); - m_preprocess->collect_statistics(m_stats); return l_undef; } m_mc = concat(m_mc.get(), m_mc2.get()); @@ -270,6 +271,9 @@ private: } + // TBD: this is super-expensive because of the + // bit-blasting model converter. + void extract_model() { model_ref md = alloc(model, m); sat::model const & ll_m = m_solver.get_model(); diff --git a/src/opt/mus.cpp b/src/opt/mus.cpp index 9204371bc..06d77aad9 100644 --- a/src/opt/mus.cpp +++ b/src/opt/mus.cpp @@ -123,7 +123,7 @@ struct mus::imp { TRACE("opt", display_vec(tout << "core: ", core); display_vec(tout << "mus: ", mus); - display_vec(tout << "model: ", model); + // display_vec(tout << "model: ", model); ); core.pop_back(); expr* cls = m_cls2expr[cls_id].get(); @@ -140,8 +140,8 @@ struct mus::imp { case l_true: assumptions.push_back(cls); mus.push_back(cls_id); - extract_model(model); if (m_rmr_enabled) { + extract_model(model); sz = core.size(); core.append(mus); rmr(core, mus, model); diff --git a/src/sat/sat_mus.cpp b/src/sat/sat_mus.cpp new file mode 100644 index 000000000..7000191fc --- /dev/null +++ b/src/sat/sat_mus.cpp @@ -0,0 +1,163 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + sat_mus.cpp + +Abstract: + + Faster MUS extraction based on Belov et.al. HYB (Algorithm 3, 4) + +Author: + + Nikolaj Bjorner (nbjorner) 2014-20-7 + +Notes: + + Model rotation needs fixes to ensure that hard constraints are satisfied + under pertubed model. Model rotation also has o be consistent with theories. + +--*/ + +#include "sat_solver.h" +#include "sat_mus.h" + +namespace sat { + + mus::mus(solver& s):s(s) {} + + mus::~mus() {} + + void mus::reset() { + m_core.reset(); + m_mus.reset(); + m_assumptions.reset(); + } + + void mus::set_core() { + m_core.append(m_mus); + s.m_core.reset(); + s.m_core.append(m_core); + } + + lbool mus::operator()() { + reset(); + literal_vector& core = m_core; + literal_vector& mus = m_mus; + literal_vector& assumptions = m_assumptions; + core.append(s.get_core()); + SASSERT(!core.empty()); + + if (core.size() == 1) { + return l_true; + } + while (!core.empty()) { + TRACE("sat", + tout << "core: " << core << "\n"; + tout << "mus: " << mus << "\n";); + + if (s.m_cancel) { + set_core(); + return l_undef; + } + literal lit = core.back(); + core.pop_back(); + unsigned sz = assumptions.size(); + assumptions.push_back(~lit); + assumptions.append(core); + lbool is_sat = s.check(assumptions.size(), assumptions.c_ptr()); + assumptions.resize(sz); + switch (is_sat) { + case l_undef: + core.push_back(lit); + set_core(); + return l_undef; + case l_true: { + assumptions.push_back(lit); + mus.push_back(lit); + unsigned sz = core.size(); + core.append(mus); + rmr(); + core.resize(sz); + break; + } + case l_false: + core.reset(); + for (unsigned i = 0; i < s.get_core().size(); ++i) { + literal lit = s.get_core()[i]; + if (!mus.contains(lit)) { + core.push_back(lit); + } + } + break; + } + } + return l_true; + } + + lbool mus::eval(literal l) const { + return value_at(l, s.get_model()); + } + + void mus::rmr() { + model& model = s.m_model; + literal lit = m_mus.back(); + literal assumption_lit; + SASSERT(eval(lit) == l_false); // literal is false in current model. + find_swappable(lit); + for (unsigned i = 0; i < m_toswap.size(); ++i) { + lit = m_toswap[i]; + SASSERT(eval(lit) == l_false); + model[lit.var()] = ~model[lit.var()]; // swap assignment + if (has_single_unsat(assumption_lit) && !m_mus.contains(assumption_lit)) { + m_mus.push_back(assumption_lit); + rmr(); + } + model[lit.var()] = ~model[lit.var()]; // swap assignment back + } + } + + bool mus::has_single_unsat(literal& assumption_lit) { + model const& model = s.get_model(); + return false; + } + + void mus::find_swappable(literal lit) { + m_toswap.reset(); + } + +} + +#if 0 + + + bool has_single_unsat(svector const& model, unsigned& cls_id) const { + cls_id = UINT_MAX; + for (unsigned i = 0; i < m_cls2lits.size(); ++i) { + if (!eval(model, m_cls2lits[i])) { + if (cls_id == UINT_MAX) { + cls_id = i; + } + else { + return false; + } + } + } + TRACE("opt", display_vec(tout << "clause: " << cls_id << " model: ", model);); + return cls_id != UINT_MAX; + } + + bool eval(svector const& model, smt::literal_vector const& cls) const { + bool result = false; + for (unsigned i = 0; !result && i < cls.size(); ++i) { + result = (model[cls[i].var()] != cls[i].sign()); + } + TRACE("opt", display_vec(tout << "model: ", model); + display_vec(tout << "clause: ", cls); + tout << "result: " << result << "\n";); + return result; + } + + +#endif diff --git a/src/sat/sat_mus.h b/src/sat/sat_mus.h new file mode 100644 index 000000000..70ba4d21c --- /dev/null +++ b/src/sat/sat_mus.h @@ -0,0 +1,44 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + mus.h + +Abstract: + + Faster MUS extraction based on Belov et.al. HYB (Algorithm 3, 4) + +Author: + + Nikolaj Bjorner (nbjorner) 2014-20-7 + +Notes: + +--*/ +#ifndef _SAT_MUS_H_ +#define _SAT_MUS_H_ + +namespace sat { + class mus { + literal_vector m_core; + literal_vector m_assumptions; + literal_vector m_mus; + literal_vector m_toswap; + solver& s; + public: + mus(solver& s); + ~mus(); + lbool operator()(); + private: + void rmr(); + bool has_single_unsat(literal& assumption_lit); + void find_swappable(literal lit); + void reset(); + void set_core(); + lbool eval(literal l) const; + }; + +}; + +#endif diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 570ca5276..fd35e5d64 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -18,4 +18,5 @@ def_module_params('sat', ('gc.k', UINT, 7, 'learned clauses that are inactive for k gc rounds are permanently deleted (only used in dyn_psm)'), ('minimize_lemmas', BOOL, True, 'minimize learned clauses'), ('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses'), + ('minimize_core', BOOL, False, 'minimize computed core'), ('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks'))) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index cfd83955d..d0d3236c8 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -39,13 +39,15 @@ namespace sat { m_scc(*this, p), m_asymm_branch(*this, p), m_probing(*this, p), + m_mus(*this), m_inconsistent(false), m_num_frozen(0), m_activity_inc(128), m_case_split_queue(m_activity), m_qhead(0), m_scope_lvl(0), - m_params(p) { + m_params(p), + m_minimize_core(p.get_bool("minimize_core", false)) { m_config.updt_params(p); } @@ -710,7 +712,6 @@ namespace sat { init_assumptions(num_lits, lits); propagate(false); if (inconsistent()) { - TRACE("sat", tout << "initialized -> inconsistent\n";); if (tracking_assumptions()) resolve_conflict(); return l_false; @@ -721,8 +722,7 @@ namespace sat { lbool r = bounded_search(); if (r != l_undef) return r; - pop(scope_lvl()); - SASSERT(scope_lvl() == 1); + pop_reinit(scope_lvl()); m_conflicts_since_restart = 0; m_restart_threshold = m_config.m_restart_initial; } @@ -900,10 +900,10 @@ namespace sat { void solver::reinit_assumptions() { if (tracking_assumptions() && scope_lvl() == 0) { + TRACE("sat", tout << m_assumptions.size() << "\n";); push(); for (unsigned i = 0; !inconsistent() && i < m_assumptions.size(); ++i) { - literal l = m_assumptions[i]; - assign(l, justification()); + assign(m_assumptions[i], justification()); } } } @@ -937,7 +937,8 @@ namespace sat { \brief Apply all simplifications. */ void solver::simplify_problem() { - pop_core(scope_lvl()); + pop(scope_lvl()); + m_trail.reset(); SASSERT(scope_lvl() == 0); @@ -1055,7 +1056,7 @@ namespace sat { << " :restarts " << m_stats.m_restart << mk_stat(*this) << " :time " << std::fixed << std::setprecision(2) << m_stopwatch.get_current_seconds() << ")\n";); IF_VERBOSE(30, display_status(verbose_stream());); - pop(scope_lvl()); + pop_reinit(scope_lvl()); m_conflicts_since_restart = 0; switch (m_config.m_restart) { case RS_GEOMETRIC: @@ -1508,7 +1509,7 @@ namespace sat { unsigned glue = num_diff_levels(m_lemma.size(), m_lemma.c_ptr()); - pop(m_scope_lvl - new_scope_lvl); + pop_reinit(m_scope_lvl - new_scope_lvl); TRACE("sat_conflict_detail", display(tout); tout << "assignment:\n"; display_assignment(tout);); clause * lemma = mk_clause_core(m_lemma.size(), m_lemma.c_ptr(), true); if (lemma) { @@ -1620,6 +1621,9 @@ namespace sat { } while (idx > 0); reset_unmark(old_size); + if (m_minimize_core) { + m_mus(); //ignore return value on cancelation. + } } @@ -2082,12 +2086,12 @@ namespace sat { m_ext->push(); } - void solver::pop(unsigned num_scopes) { - pop_core(num_scopes); + void solver::pop_reinit(unsigned num_scopes) { + pop(num_scopes); reinit_assumptions(); } - void solver::pop_core(unsigned num_scopes) { + void solver::pop(unsigned num_scopes) { if (num_scopes == 0) return; if (m_ext) @@ -2232,6 +2236,7 @@ namespace sat { m_probing.updt_params(p); m_scc.updt_params(p); m_rand.set_seed(p.get_uint("random_seed", 0)); + m_minimize_core = p.get_bool("minimize_core", false); } void solver::collect_param_descrs(param_descrs & d) { diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 8e4c9911b..91ecbc3fb 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -32,6 +32,7 @@ Revision History: #include"sat_asymm_branch.h" #include"sat_iff3_finder.h" #include"sat_probing.h" +#include"sat_mus.h" #include"params.h" #include"statistics.h" #include"stopwatch.h" @@ -79,6 +80,7 @@ namespace sat { scc m_scc; asymm_branch m_asymm_branch; probing m_probing; + mus m_mus; bool m_inconsistent; // A conflict is usually a single justification. That is, a justification // for false. If m_not_l is not null_literal, then m_conflict is a @@ -121,6 +123,7 @@ namespace sat { literal_vector m_assumptions; literal_set m_assumption_set; literal_vector m_core; + bool m_minimize_core; void del_clauses(clause * const * begin, clause * const * end); @@ -132,6 +135,7 @@ namespace sat { friend class asymm_branch; friend class probing; friend class iff3_finder; + friend class mus; friend struct mk_stat; public: solver(params_ref const & p, extension * ext); @@ -352,7 +356,7 @@ namespace sat { // ----------------------- void push(); void pop(unsigned num_scopes); - void pop_core(unsigned num_scopes); + void pop_reinit(unsigned num_scopes); void unassign_vars(unsigned old_sz); void reinit_clauses(unsigned old_sz);