From 2fe0c055562323842b94c42df522d64a84448437 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 28 Aug 2015 20:25:25 -0700 Subject: [PATCH] tuning pd-maxres Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 264 +++++++++++++++++++++++++++++------------ src/sat/sat_solver.h | 11 +- 2 files changed, 199 insertions(+), 76 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 38f2469e5..50575e945 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -54,6 +54,7 @@ namespace sat { m_conflicts = 0; m_next_simplify = 0; m_num_checkpoints = 0; + m_initializing_preferred = false; } solver::~solver() { @@ -407,6 +408,7 @@ namespace sat { for (unsigned i = 1; i < num_lits; i++) { literal l = cls[i]; lbool val = value(l); + CTRACE("sat", val != l_false, tout << l << ":=" << val;); SASSERT(val == l_false); if (max_false_idx == UINT_MAX || lvl(l) > lvl(cls[max_false_idx])) max_false_idx = i; @@ -894,8 +896,7 @@ namespace sat { } retry_init_assumptions: - m_assumptions.reset(); - m_assumption_set.reset(); + reset_assumptions(); push(); propagate(false); @@ -931,25 +932,19 @@ namespace sat { for (unsigned i = 0; !inconsistent() && i < num_lits; ++i) { literal lit = lits[i]; SASSERT(is_external(lit.var())); - m_assumption_set.insert(lit); - m_assumptions.push_back(lit); + add_assumption(lit); assign(lit, justification()); } } - void solver::resolve_weighted() { - flet _min1(m_config.m_minimize_core, false); - flet _min2(m_config.m_minimize_core_partial, false); - m_conflict_lvl = m_scope_lvl; - resolve_conflict_for_unsat_core(); - } bool solver::init_weighted_assumptions(unsigned num_lits, literal const* lits, double const* weights, double max_weight) { - double weight = 0; - literal_vector blocker; + flet _min1(m_config.m_minimize_core, false); + flet _min2(m_config.m_minimize_core_partial, false); + m_weight = 0; + m_blocker.reset(); m_min_core_valid = false; m_min_core.reset(); - unsigned old_sz = 0; for (unsigned i = 0; !inconsistent() && i < num_lits; ++i) { literal lit = lits[i]; SASSERT(is_external(lit.var())); @@ -958,55 +953,42 @@ namespace sat { switch(value(lit)) { case l_undef: - m_assumption_set.insert(lit); - m_assumptions.push_back(lit); - old_sz = m_qhead; + add_assumption(lit); assign(lit, justification()); propagate(false); if (inconsistent()) { - resolve_weighted(); - m_assumption_set.pop(); - m_assumptions.pop_back(); - unassign_vars(old_sz); - m_inconsistent = false; - update_min_core(); - blocker.reset(); - for (unsigned j = 0; j < m_core.size(); ++j) { - blocker.push_back(~m_core[j]); + pop_assumption(); + flet _init(m_initializing_preferred, true); + while (inconsistent()) { + if (!resolve_conflict()) { + return true; + } + propagate(true); } - TRACE("sat", tout << "Blocker: " << blocker << "\n";); - mk_clause(blocker); - propagate(false); - if (inconsistent()) { - // - // TBD: this could be improved by emulating normal - // conflict resolution and backjumping directly and - // continuing with the backjumped state instead of - // baling out using the best core so far. - // - resolve_weighted(); - update_min_core(); - IF_VERBOSE(1, verbose_stream() << "Conflicting assignment: " << m_core << "\n" - << "Core: " << m_min_core << "\n";); - pop_to_base_level(); - reassert_min_core(); - return true; + if (m_scope_lvl == 0) { + return false; } - SASSERT(value(lit) == l_false); - IF_VERBOSE(11, - verbose_stream() << "undef: " << lit << " : " << blocker << "\n"; - verbose_stream() << m_assumptions << "\n";); + for (; i < num_lits; ++i) { + literal lit = lits[i]; + if (value(lit) == l_undef) { + assign(lit, justification()); + add_assumption(lit); + } + } + return true; } - blocker.push_back(~lit); break; case l_false: - m_assumption_set.insert(lit); - m_assumptions.push_back(lit); + add_assumption(lit); SASSERT(!inconsistent()); set_conflict(justification(), ~lit); - resolve_weighted(); - weight += weights[i]; + m_conflict_lvl = m_scope_lvl; + resolve_conflict_for_unsat_core(); + m_weight += weights[i]; + if (m_weight <= max_weight) { + m_blocker.push_back(lit); + } TRACE("sat", tout << "core: " << m_core << "\nassumptions: " << m_assumptions << "\n";); SASSERT(m_core.size() <= m_assumptions.size()); SASSERT(m_assumptions.size() <= i+1); @@ -1018,34 +1000,37 @@ namespace sat { } update_min_core(); SASSERT(m_min_core_valid); - VERIFY(m_assumptions.back() == m_assumption_set.pop()); - m_assumptions.pop_back(); + pop_assumption(); m_inconsistent = false; - if (weight < max_weight) { - blocker.push_back(lit); - } break; - case l_true: + case l_true: { + justification j = m_justification[lit.var()]; + if (j.get_kind() == justification::NONE) { + add_assumption(lit); + } break; } + } } TRACE("sat", tout << "initialized\n";); - IF_VERBOSE(11, verbose_stream() << "Blocker: " << blocker << " - " << m_min_core << "\n";); - if (m_min_core_valid && blocker.size() >= m_min_core.size()) { + IF_VERBOSE(11, verbose_stream() << "Blocker: " << m_blocker << "\nCore: " << m_min_core << "\n";); + if (m_min_core_valid && m_blocker.size() >= m_min_core.size()) { reassert_min_core(); } - else if (weight > max_weight) { - ++m_stats.m_blocked_corr_sets; - TRACE("opt", tout << "blocking soft correction set: " << blocker << "\n";); + else if (m_weight >= max_weight) { // block the current correction set candidate. - IF_VERBOSE(11, verbose_stream() << "blocking " << blocker << "\n";); + ++m_stats.m_blocked_corr_sets; + TRACE("opt", tout << "blocking soft correction set: " << m_blocker << "\n";); + IF_VERBOSE(11, verbose_stream() << "blocking " << m_blocker << "\n";); pop_to_base_level(); - mk_clause(blocker); + mk_clause(m_blocker); return false; } return true; } + + void solver::update_min_core() { if (!m_min_core_valid || m_core.size() < m_min_core.size()) { m_min_core.reset(); @@ -1054,17 +1039,31 @@ namespace sat { } } + void solver::reset_assumptions() { + m_assumptions.reset(); + m_assumption_set.reset(); + } + + void solver::add_assumption(literal lit) { + m_assumption_set.insert(lit); + m_assumptions.push_back(lit); + } + + void solver::pop_assumption() { + VERIFY(m_assumptions.back() == m_assumption_set.pop()); + m_assumptions.pop_back(); + } + void solver::reassert_min_core() { SASSERT(m_min_core_valid); pop_to_base_level(); push(); - m_assumption_set.reset(); - m_assumptions.reset(); + reset_assumptions(); + TRACE("sat", tout << "reassert: " << m_min_core << "\n";); for (unsigned i = 0; i < m_min_core.size(); ++i) { literal lit = m_min_core[i]; - SASSERT(is_external(lit.var())); - m_assumption_set.insert(lit); - m_assumptions.push_back(lit); + SASSERT(is_external(lit.var())); + add_assumption(lit); assign(lit, justification()); } propagate(false); @@ -1629,6 +1628,10 @@ namespace sat { if (m_not_l == literal()) tout << "null literal\n"; else tout << m_not_l << "\n";); + if (m_initializing_preferred) { + SASSERT(m_conflict_lvl <= 1); + return resolve_conflict_for_init(); + } if (m_conflict_lvl <= 1 && tracking_assumptions()) { resolve_conflict_for_unsat_core(); return false; @@ -1656,7 +1659,7 @@ namespace sat { do { TRACE("sat_conflict_detail", tout << "processing consequent: " << consequent << "\n"; - tout << "num_marks: " << num_marks << ", js kind: " << js.get_kind() << "\n";); + tout << "num_marks: " << num_marks << ", js: " << js << "\n";); switch (js.get_kind()) { case justification::NONE: break; @@ -1814,6 +1817,120 @@ namespace sat { } } + bool solver::resolve_conflict_for_init() { + if (m_conflict_lvl == 0) { + return false; + } + m_lemma.reset(); + m_lemma.push_back(null_literal); // asserted literal + if (m_not_l != null_literal) { + TRACE("sat", tout << "not_l: " << m_not_l << "\n";); + process_antecedent_for_init(m_not_l); + } + literal consequent = m_not_l; + justification js = m_conflict; + + SASSERT(m_trail.size() > 0); + unsigned idx = m_trail.size(); + while (process_consequent_for_init(consequent, js)) { + while (true) { + --idx; + literal l = m_trail[idx]; + if (is_marked(l.var())) + break; + SASSERT(idx > 0); + } + consequent = m_trail[idx]; + bool_var c_var = consequent.var(); + if (lvl(consequent) == 0) { + return false; + } + SASSERT(m_conflict_lvl == 1); + js = m_justification[c_var]; + reset_mark(c_var); + } + + unsigned new_scope_lvl = 0; + m_lemma[0] = ~consequent; + for (unsigned i = 1; i < m_lemma.size(); ++i) { + bool_var var = m_lemma[i].var(); + if (is_marked(var)) { + reset_mark(var); + new_scope_lvl = std::max(new_scope_lvl, lvl(var)); + } + else { + m_lemma[i] = m_lemma.back(); + m_lemma.pop_back(); + --i; + } + } + TRACE("sat", tout << "lemma: " << m_lemma << "\n"; display(tout); tout << "assignment:\n"; display_assignment(tout);); + if (new_scope_lvl == 0) { + pop_reinit(m_scope_lvl); + } + else { + unassign_vars(idx); + } + mk_clause_core(m_lemma.size(), m_lemma.c_ptr(), true); + TRACE("sat", tout << "Trail: " << m_trail << "\n";); + m_inconsistent = false; + return true; + } + + bool solver::process_consequent_for_init(literal consequent, justification const& js) { + switch (js.get_kind()) { + case justification::NONE: + return false; + case justification::BINARY: + process_antecedent_for_init(~(js.get_literal())); + break; + case justification::TERNARY: + process_antecedent_for_init(~(js.get_literal1())); + process_antecedent_for_init(~(js.get_literal2())); + break; + case justification::CLAUSE: { + clause & c = *(m_cls_allocator.get_clause(js.get_clause_offset())); + unsigned i = 0; + if (consequent != null_literal) { + SASSERT(c[0] == consequent || c[1] == consequent); + if (c[0] == consequent) { + i = 1; + } + else { + process_antecedent_for_init(~c[0]); + i = 2; + } + } + unsigned sz = c.size(); + for (; i < sz; i++) + process_antecedent_for_init(~c[i]); + break; + } + case justification::EXT_JUSTIFICATION: { + fill_ext_antecedents(consequent, js); + literal_vector::iterator it = m_ext_antecedents.begin(); + literal_vector::iterator end = m_ext_antecedents.end(); + for (; it != end; ++it) + process_antecedent_for_init(*it); + break; + } + default: + UNREACHABLE(); + break; + } + return true; + } + + void solver::process_antecedent_for_init(literal antecedent) { + bool_var var = antecedent.var(); + SASSERT(var < num_vars()); + if (!is_marked(var) && lvl(var) > 0) { + mark(var); + m_lemma.push_back(~antecedent); + } + } + + void solver::resolve_conflict_for_unsat_core() { TRACE("sat", display(tout); unsigned level = 0; @@ -2489,8 +2606,7 @@ namespace sat { } void solver::pop_to_base_level() { - m_assumptions.reset(); - m_assumption_set.reset(); + reset_assumptions(); pop(scope_lvl()); } @@ -2756,9 +2872,7 @@ namespace sat { } void solver::display_assignment(std::ostream & out) const { - for (unsigned i = 0; i < m_trail.size(); i++) - out << m_trail[i] << " "; - out << "\n"; + out << m_trail << "\n"; } /** diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index a58e1aace..a49fb3c31 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -300,11 +300,17 @@ namespace sat { literal_vector m_min_core; bool m_min_core_valid; + literal_vector m_blocker; + double m_weight; + bool m_initializing_preferred; void init_assumptions(unsigned num_lits, literal const* lits, double const* weights, double max_weight); bool init_weighted_assumptions(unsigned num_lits, literal const* lits, double const* weights, double max_weight); void reassert_min_core(); void update_min_core(); void resolve_weighted(); + void reset_assumptions(); + void add_assumption(literal lit); + void pop_assumption(); void reinit_assumptions(); bool tracking_assumptions() const; bool is_assumption(literal l) const; @@ -353,11 +359,14 @@ namespace sat { literal_vector m_ext_antecedents; bool resolve_conflict(); bool resolve_conflict_core(); - void resolve_conflict_for_unsat_core(); unsigned get_max_lvl(literal consequent, justification js); void process_antecedent(literal antecedent, unsigned & num_marks); + void resolve_conflict_for_unsat_core(); void process_antecedent_for_unsat_core(literal antecedent); void process_consequent_for_unsat_core(literal consequent, justification const& js); + bool resolve_conflict_for_init(); + void process_antecedent_for_init(literal antecedent); + bool process_consequent_for_init(literal consequent, justification const& js); void fill_ext_antecedents(literal consequent, justification js); unsigned skip_literals_above_conflict_level(); void forget_phase_of_vars(unsigned from_lvl);