From 6ef8660adb5858c89eb8db58f3de7be23a0bf0fe Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 11 Jun 2026 09:14:00 -0700 Subject: [PATCH] Parallel tactic (#9824) Co-authored-by: Ilana Shapiro Co-authored-by: Ilana Shapiro --- src/params/smt_parallel_params.pyg | 2 +- src/sat/sat_solver.cpp | 150 ++- src/sat/sat_solver.h | 11 +- src/sat/sat_solver/inc_sat_solver.cpp | 94 +- src/sat/smt/atom2bool_var.cpp | 7 + src/sat/smt/atom2bool_var.h | 1 + src/sat/smt/bv_ackerman.cpp | 2 +- src/sat/smt/euf_ackerman.cpp | 2 +- src/smt/smt_context.cpp | 7 + src/smt/smt_context.h | 9 +- src/smt/smt_kernel.cpp | 16 + src/smt/smt_kernel.h | 8 + src/smt/smt_parallel.cpp | 3 +- src/smt/smt_parallel.h | 7 + src/smt/smt_solver.cpp | 157 ++- src/solver/parallel_params.pyg | 3 + src/solver/parallel_tactical2.cpp | 1632 +++++++++++++++++++++---- src/solver/solver.h | 46 + src/solver/solver_pool.cpp | 4 + src/util/search_tree.h | 8 + 20 files changed, 1889 insertions(+), 280 deletions(-) diff --git a/src/params/smt_parallel_params.pyg b/src/params/smt_parallel_params.pyg index dde7656ff..315d3d029 100644 --- a/src/params/smt_parallel_params.pyg +++ b/src/params/smt_parallel_params.pyg @@ -5,7 +5,7 @@ def_module_params('smt_parallel', ('inprocessing', BOOL, False, 'integrate in-processing as a heuristic simplification'), ('sls', BOOL, False, 'add sls-tactic as a separate worker thread outside the search tree parallelism'), ('num_global_bb_fl_threads', UINT, 0, 'run failed-literal backbone worker threads; default is 0 (off), supported values are 1 (negative mode only) or 2 (negative and positive mode)'), - ('num_global_bb_batch_threads', UINT, 0, 'run Janota-style chunking backbone worker threads; default is 0 (off), supported values are 1 (negative mode only) or 2 (negative and positive mode)'), + ('num_global_bb_batch_threads', UINT, 2, 'run Janota-style chunking backbone worker threads; default is 2 (negative and positive mode), supported values are 0 (off), 1 (negative mode only) or 2 (negative and positive mode)'), ('local_backbones', BOOL, False, 'enable local backbones experiment within the search tree parallelism'), ('core_minimize', BOOL, True, 'minimize unsat cores used for parallel cube backtracking'), ('ablate_backtracking', BOOL, False, 'ablation: pass entire cube as core instead of unsat core during backtracking'), diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 09f874e78..cd4793416 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -132,6 +132,8 @@ namespace sat { m_best_phase.reset(); m_phase.reset(); m_prev_phase.reset(); + m_phase_birthdate.reset(); + m_best_phase_birthdate.reset(); m_assigned_since_gc.reset(); m_last_conflict.reset(); m_last_propagation.reset(); @@ -161,6 +163,8 @@ namespace sat { m_phase[v] = src.m_phase[v]; m_best_phase[v] = src.m_best_phase[v]; m_prev_phase[v] = src.m_prev_phase[v]; + m_phase_birthdate[v] = src.m_phase_birthdate[v]; + m_best_phase_birthdate[v] = src.m_best_phase_birthdate[v]; // inherit activity: m_activity[v] = src.m_activity[v]; @@ -267,6 +271,8 @@ namespace sat { m_phase[v] = false; m_best_phase[v] = false; m_prev_phase[v] = false; + m_phase_birthdate[v] = 0; + m_best_phase_birthdate[v] = 0; m_assigned_since_gc[v] = false; m_last_conflict[v] = 0; m_last_propagation[v] = 0; @@ -308,6 +314,8 @@ namespace sat { m_phase.push_back(false); m_best_phase.push_back(false); m_prev_phase.push_back(false); + m_phase_birthdate.push_back(0); + m_best_phase_birthdate.push_back(0); m_assigned_since_gc.push_back(false); m_last_conflict.push_back(0); m_last_propagation.push_back(0); @@ -645,6 +653,17 @@ namespace sat { return 3*cls_allocator().get_allocation_size()/2 + memory::get_allocation_size() > memory::get_max_memory_size(); } + void solver::set_phase(literal l) { + if (l.var() >= num_vars()) + return; + bool value = !l.sign(); + if (m_phase[l.var()] != value) + m_phase_birthdate[l.var()] = m_stats.m_conflicts; + if (m_best_phase[l.var()] != value) + m_best_phase_birthdate[l.var()] = m_stats.m_conflicts; + m_best_phase[l.var()] = m_phase[l.var()] = value; + } + struct solver::cmp_activity { solver& s; cmp_activity(solver& s):s(s) {} @@ -896,6 +915,8 @@ namespace sat { m_assignment[(~l).index()] = l_false; bool_var v = l.var(); m_justification[v] = j; + if (m_phase[v] != !l.sign()) + m_phase_birthdate[v] = m_stats.m_conflicts; m_phase[v] = !l.sign(); m_assigned_since_gc[v] = true; m_trail.push_back(l); @@ -904,17 +925,17 @@ namespace sat { case BH_VSIDS: break; case BH_CHB: - m_last_propagation[v] = m_stats.m_conflict; + m_last_propagation[v] = m_stats.m_conflicts; break; } if (m_config.m_anti_exploration) { - uint64_t age = m_stats.m_conflict - m_canceled[v]; + uint64_t age = m_stats.m_conflicts - m_canceled[v]; if (age > 0) { double decay = pow(0.95, static_cast(age)); set_activity(v, static_cast(m_activity[v] * decay)); // NB. MapleSAT does not update canceled. - m_canceled[v] = m_stats.m_conflict; + m_canceled[v] = m_stats.m_conflicts; } } @@ -1378,8 +1399,12 @@ namespace sat { lbool r = m_local_search->check(_lits.size(), _lits.data(), nullptr); auto const& mdl = m_local_search->get_model(); if (mdl.size() == m_best_phase.size()) { - for (unsigned i = 0; i < m_best_phase.size(); ++i) - m_best_phase[i] = l_true == mdl[i]; + for (unsigned i = 0; i < m_best_phase.size(); ++i) { + bool is_true = l_true == mdl[i]; + if (m_best_phase[i] != is_true) + m_best_phase_birthdate[i] = m_stats.m_conflicts; + m_best_phase[i] = is_true; + } if (r == l_true) { m_conflicts_since_restart = 0; @@ -1671,12 +1696,12 @@ namespace sat { while (!m_case_split_queue.empty()) { if (m_config.m_anti_exploration) { next = m_case_split_queue.min_var(); - auto age = m_stats.m_conflict - m_canceled[next]; + auto age = m_stats.m_conflicts - m_canceled[next]; while (age > 0) { set_activity(next, static_cast(m_activity[next] * pow(0.95, static_cast(age)))); - m_canceled[next] = m_stats.m_conflict; + m_canceled[next] = m_stats.m_conflicts; next = m_case_split_queue.min_var(); - age = m_stats.m_conflict - m_canceled[next]; + age = m_stats.m_conflicts - m_canceled[next]; } } next = m_case_split_queue.next_var(); @@ -1714,6 +1739,32 @@ namespace sat { } } + uint64_t solver::get_preferred_phase_birthdate(bool_var v) const { + bool use_best = + m_config.m_phase == PS_FROZEN || + ((m_config.m_phase == PS_SAT_CACHING || m_config.m_phase == PS_LOCAL_SEARCH) && m_search_state == s_sat); + return use_best ? m_best_phase_birthdate[v] : m_phase_birthdate[v]; + } + + void solver::get_backbone_candidates(literal_vector& lits, unsigned max_num) { + struct candidate { + literal lit; + uint64_t age; + }; + svector cands; + uint64_t now = m_stats.m_conflicts; + for (bool_var v = 0; v < num_vars(); ++v) { + if (value(v) != l_undef || was_eliminated(v)) + continue; + bool is_pos = guess(v); + cands.push_back({ literal(v, !is_pos), now - get_preferred_phase_birthdate(v) }); + } + std::stable_sort(cands.begin(), cands.end(), + [](candidate const& a, candidate const& b) { return a.age > b.age; }); + for (unsigned i = 0; i < cands.size() && i < max_num; ++i) + lits.push_back(cands[i].lit); + } + bool solver::decide() { bool_var next; lbool phase = l_undef; @@ -2145,8 +2196,13 @@ namespace sat { for (bool_var v = 0; v < num; ++v) { if (!was_eliminated(v)) { m_model[v] = value(v); - m_phase[v] = value(v) == l_true; - m_best_phase[v] = value(v) == l_true; + bool is_true = value(v) == l_true; + if (m_phase[v] != is_true) + m_phase_birthdate[v] = m_stats.m_conflicts; + if (m_best_phase[v] != is_true) + m_best_phase_birthdate[v] = m_stats.m_conflicts; + m_phase[v] = is_true; + m_best_phase[v] = is_true; } } TRACE(sat_mc_bug, m_mc.display(tout);); @@ -2274,7 +2330,7 @@ namespace sat { m_restart_logs++; std::stringstream strm; - strm << "(sat.stats " << std::setw(6) << m_stats.m_conflict << " " + strm << "(sat.stats " << std::setw(6) << m_stats.m_conflicts << " " << std::setw(6) << m_stats.m_decision << " " << std::setw(4) << m_stats.m_restart << mk_stat(*this) @@ -2432,7 +2488,7 @@ namespace sat { m_conflicts_since_init++; m_conflicts_since_restart++; m_conflicts_since_gc++; - m_stats.m_conflict++; + m_stats.m_conflicts++; if (m_step_size > m_config.m_step_size_min) m_step_size -= m_config.m_step_size_dec; @@ -2564,7 +2620,7 @@ namespace sat { tout << "missed " << lit << "@" << lvl(lit) << "\n";); CTRACE(sat, idx == 0, display(tout);); if (idx == 0) - IF_VERBOSE(0, verbose_stream() << "num-conflicts: " << m_stats.m_conflict << "\n"); + IF_VERBOSE(0, verbose_stream() << "num-conflicts: " << m_stats.m_conflicts << "\n"); VERIFY(idx > 0); idx--; } @@ -2874,7 +2930,7 @@ namespace sat { inc_activity(var); break; case BH_CHB: - m_last_conflict[var] = m_stats.m_conflict; + m_last_conflict[var] = m_stats.m_conflicts; break; default: break; @@ -2915,13 +2971,18 @@ namespace sat { for (unsigned i = head; i < sz; ++i) { bool_var v = m_trail[i].var(); TRACE(forget_phase, tout << "forgetting phase of v" << v << "\n";); - m_phase[v] = m_rand() % 2 == 0; + bool value = m_rand() % 2 == 0; + if (m_phase[v] != value) + m_phase_birthdate[v] = m_stats.m_conflicts; + m_phase[v] = value; } if (is_sat_phase() && head >= m_best_phase_size) { m_best_phase_size = head; IF_VERBOSE(12, verbose_stream() << "sticky trail: " << head << "\n"); for (unsigned i = 0; i < head; ++i) { bool_var v = m_trail[i].var(); + if (m_best_phase[v] != m_phase[v]) + m_best_phase_birthdate[v] = m_stats.m_conflicts; m_best_phase[v] = m_phase[v]; } set_has_new_best_phase(true); @@ -2971,23 +3032,43 @@ namespace sat { void solver::do_rephase() { switch (m_config.m_phase) { case PS_ALWAYS_TRUE: - for (auto& p : m_phase) p = true; + for (unsigned i = 0; i < m_phase.size(); ++i) { + if (!m_phase[i]) + m_phase_birthdate[i] = m_stats.m_conflicts; + m_phase[i] = true; + } break; case PS_ALWAYS_FALSE: - for (auto& p : m_phase) p = false; + for (unsigned i = 0; i < m_phase.size(); ++i) { + if (m_phase[i]) + m_phase_birthdate[i] = m_stats.m_conflicts; + m_phase[i] = false; + } break; case PS_FROZEN: break; case PS_BASIC_CACHING: switch (m_rephase.count % 4) { case 0: - for (auto& p : m_phase) p = (m_rand() % 2) == 0; + for (unsigned i = 0; i < m_phase.size(); ++i) { + bool value = (m_rand() % 2) == 0; + if (m_phase[i] != value) + m_phase_birthdate[i] = m_stats.m_conflicts; + m_phase[i] = value; + } break; case 1: - for (auto& p : m_phase) p = false; + for (unsigned i = 0; i < m_phase.size(); ++i) { + if (m_phase[i]) + m_phase_birthdate[i] = m_stats.m_conflicts; + m_phase[i] = false; + } break; case 2: - for (auto& p : m_phase) p = !p; + for (unsigned i = 0; i < m_phase.size(); ++i) { + m_phase_birthdate[i] = m_stats.m_conflicts; + m_phase[i] = !m_phase[i]; + } break; default: break; @@ -2995,18 +3076,29 @@ namespace sat { break; case PS_SAT_CACHING: if (m_search_state == s_sat) - for (unsigned i = 0; i < m_phase.size(); ++i) - m_phase[i] = m_best_phase[i]; + for (unsigned i = 0; i < m_phase.size(); ++i) { + if (m_phase[i] != m_best_phase[i]) + m_phase_birthdate[i] = m_stats.m_conflicts; + m_phase[i] = m_best_phase[i]; + } break; case PS_RANDOM: - for (auto& p : m_phase) p = (m_rand() % 2) == 0; + for (unsigned i = 0; i < m_phase.size(); ++i) { + bool value = (m_rand() % 2) == 0; + if (m_phase[i] != value) + m_phase_birthdate[i] = m_stats.m_conflicts; + m_phase[i] = value; + } break; case PS_LOCAL_SEARCH: if (m_search_state == s_sat) { if (m_rand() % 2 == 0) bounded_local_search(); - for (unsigned i = 0; i < m_phase.size(); ++i) - m_phase[i] = m_best_phase[i]; + for (unsigned i = 0; i < m_phase.size(); ++i) { + if (m_phase[i] != m_best_phase[i]) + m_phase_birthdate[i] = m_stats.m_conflicts; + m_phase[i] = m_best_phase[i]; + } } break; @@ -3601,6 +3693,8 @@ namespace sat { m_phase.shrink(v); m_best_phase.shrink(v); m_prev_phase.shrink(v); + m_phase_birthdate.shrink(v); + m_best_phase_birthdate.shrink(v); m_assigned_since_gc.shrink(v); m_simplifier.reset_todos(); } @@ -3644,7 +3738,7 @@ namespace sat { SASSERT(value(v) == l_undef); m_case_split_queue.unassign_var_eh(v); if (m_config.m_anti_exploration) { - m_canceled[v] = m_stats.m_conflict; + m_canceled[v] = m_stats.m_conflicts; } } m_trail.shrink(old_sz); @@ -3812,7 +3906,7 @@ namespace sat { double multiplier = m_config.m_reward_offset * (is_sat ? m_config.m_reward_multiplier : 1.0); for (unsigned i = qhead; i < m_trail.size(); ++i) { auto v = m_trail[i].var(); - auto d = m_stats.m_conflict - m_last_conflict[v] + 1; + auto d = m_stats.m_conflicts - m_last_conflict[v] + 1; if (d == 0) d = 1; auto reward = multiplier / d; auto activity = m_activity[v]; @@ -4745,7 +4839,7 @@ namespace sat { st.update("sat mk var", m_mk_var); st.update("sat gc clause", m_gc_clause); st.update("sat del clause", m_del_clause); - st.update("sat conflicts", m_conflict); + st.update("sat conflicts", m_conflicts); st.update("sat decisions", m_decision); st.update("sat propagations 2ary", m_bin_propagate); st.update("sat propagations 3ary", m_ter_propagate); diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 9aa00ae47..d50ee9461 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -60,7 +60,7 @@ namespace sat { unsigned m_mk_bin_clause; unsigned m_mk_ter_clause; unsigned m_mk_clause; - unsigned m_conflict; + unsigned m_conflicts; unsigned m_propagate; unsigned m_bin_propagate; unsigned m_ter_propagate; @@ -148,6 +148,8 @@ namespace sat { bool_vector m_phase; bool_vector m_best_phase; bool_vector m_prev_phase; + svector m_phase_birthdate; + svector m_best_phase_birthdate; bool m_new_best_phase = false; svector m_assigned_since_gc; search_state m_search_state; @@ -373,12 +375,17 @@ namespace sat { bool was_eliminated(bool_var v) const { return m_eliminated[v]; } void set_eliminated(bool_var v, bool f) override; bool was_eliminated(literal l) const { return was_eliminated(l.var()); } - void set_phase(literal l) override { if (l.var() < num_vars()) m_best_phase[l.var()] = m_phase[l.var()] = !l.sign(); } + void set_phase(literal l) override; bool get_phase(bool_var b) { return m_phase.get(b, false); } bool get_best_phase(bool_var b) { return m_best_phase.get(b, false); } + uint64_t get_phase_birthdate(bool_var b) const { return m_phase_birthdate.get(b, 0); } + uint64_t get_best_phase_birthdate(bool_var b) const { return m_best_phase_birthdate.get(b, 0); } + uint64_t get_preferred_phase_birthdate(bool_var b) const; void set_has_new_best_phase(bool b) { m_new_best_phase = b; } bool has_new_best_phase() const { return m_new_best_phase; } void move_to_front(bool_var b); + unsigned get_activity(bool_var v) const { return m_activity[v]; } + void get_backbone_candidates(literal_vector& lits, unsigned max_num); unsigned scope_lvl() const { return m_scope_lvl; } unsigned search_lvl() const { return m_search_lvl; } bool at_search_lvl() const { return m_scope_lvl == m_search_lvl; } diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 2a98bc3ae..e8cd6d3fd 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -405,6 +405,50 @@ public: } } + unsigned get_assign_level(expr* e) const override { + expr* atom = e; + m.is_not(e, atom); + sat::bool_var bv = m_map.to_bool_var(atom); + return bv == sat::null_bool_var ? UINT_MAX : m_solver.lvl(bv); + } + + bool is_relevant(expr* e) const override { + expr* atom = e; + m.is_not(e, atom); + sat::bool_var bv = m_map.to_bool_var(atom); + if (bv == sat::null_bool_var) + return true; + auto* ext = dynamic_cast(m_solver.get_extension()); + return !ext || ext->is_relevant(bv); + } + + unsigned get_num_bool_vars() const override { + return m_solver.num_vars(); + } + + unsigned get_bool_var(expr* e) const override { + expr* atom = e; + m.is_not(e, atom); + sat::bool_var bv = m_map.to_bool_var(atom); + return bv == sat::null_bool_var ? UINT_MAX : bv; + } + + expr* bool_var2expr(unsigned v) const override { + return v < m_solver.num_vars() ? m_map.bool_var2expr(v) : nullptr; + } + + lbool get_assignment(unsigned v) const override { + return v < m_solver.num_vars() ? m_solver.value(v) : l_undef; + } + + double get_activity(unsigned v) const override { + return v < m_solver.num_vars() ? static_cast(m_solver.get_activity(v)) : 0.0; + } + + bool was_eliminated(unsigned v) const override { + return v < m_solver.num_vars() && m_solver.was_eliminated(v); + } + expr_ref_vector get_trail(unsigned max_level) override { expr_ref_vector result(m); unsigned sz = m_solver.trail_size(); @@ -451,8 +495,35 @@ public: vars.push_back(kv.m_value); } sat::literal_vector lits; - lbool result = m_solver.cube(vars, lits, backtrack_level); expr_ref_vector fmls(m); + if (!m_params.get_bool("cube.lookahead", false)) { + sat::bool_var best = sat::null_bool_var; + double best_activity = 0.0; + unsigned n = 0; + for (sat::bool_var v : vars) { + if (get_assignment(v) != l_undef || was_eliminated(v)) + continue; + double activity = get_activity(v); + if (best == sat::null_bool_var || activity > best_activity || (activity == best_activity && m_solver.rand()(++n) == 0)) { + best = v; + best_activity = activity; + } + } + if (best == sat::null_bool_var) + return expr_ref_vector(m); + expr* e = bool_var2expr(best); + SASSERT(e); + if (e) + fmls.push_back(e); + vs.reset(); + for (sat::bool_var v : vars) { + expr* x = bool_var2expr(v); + if (x) + vs.push_back(x); + } + return fmls; + } + lbool result = m_solver.cube(vars, lits, backtrack_level); expr_ref_vector lit2expr(m); lit2expr.resize(m_solver.num_vars() * 2); m_map.mk_inv(lit2expr); @@ -482,6 +553,27 @@ public: return fmls; } + void get_backbone_candidates(vector& candidates, unsigned max_num) override { + if (!is_internalized()) { + lbool r = internalize_formulas(); + if (r != l_true) + return; + } + convert_internalized(); + sat::literal_vector lits; + m_solver.get_backbone_candidates(lits, max_num); + expr_ref_vector lit2expr(m); + lit2expr.resize(m_solver.num_vars() * 2); + m_map.mk_inv(lit2expr); + uint64_t now = m_solver.get_stats().m_conflicts; + for (sat::literal lit : lits) { + expr* e = lit2expr.get(lit.index()); + if (!e) + continue; + candidates.push_back(scored_literal(m, e, static_cast(now - m_solver.get_phase_birthdate(lit.var())))); + } + } + expr* congruence_next(expr* e) override { return e; } expr* congruence_root(expr* e) override { return e; } expr_ref congruence_explain(expr* a, expr* b) override { return expr_ref(m.mk_eq(a, b), m); } diff --git a/src/sat/smt/atom2bool_var.cpp b/src/sat/smt/atom2bool_var.cpp index 68a263c85..b6760c943 100644 --- a/src/sat/smt/atom2bool_var.cpp +++ b/src/sat/smt/atom2bool_var.cpp @@ -49,6 +49,13 @@ sat::bool_var atom2bool_var::to_bool_var(expr * n) const { return m_mapping[idx].m_value; } +expr* atom2bool_var::bool_var2expr(sat::bool_var v) const { + for (auto const& kv : m_mapping) + if (kv.m_value == v) + return kv.m_key; + return nullptr; +} + struct collect_boolean_interface_proc { struct visitor { obj_hashtable & m_r; diff --git a/src/sat/smt/atom2bool_var.h b/src/sat/smt/atom2bool_var.h index 794429701..cee7a9882 100644 --- a/src/sat/smt/atom2bool_var.h +++ b/src/sat/smt/atom2bool_var.h @@ -29,6 +29,7 @@ public: atom2bool_var(ast_manager & m):expr2var(m) {} void insert(expr * n, sat::bool_var v) { expr2var::insert(n, v); } sat::bool_var to_bool_var(expr * n) const; + expr* bool_var2expr(sat::bool_var v) const; void mk_inv(expr_ref_vector & lit2expr) const; void mk_var_inv(expr_ref_vector & var2expr) const; // return true if the mapping contains uninterpreted atoms. diff --git a/src/sat/smt/bv_ackerman.cpp b/src/sat/smt/bv_ackerman.cpp index a709c16f3..1bb84bc09 100644 --- a/src/sat/smt/bv_ackerman.cpp +++ b/src/sat/smt/bv_ackerman.cpp @@ -155,7 +155,7 @@ namespace bv { void ackerman::propagate() { auto* n = m_queue; vv* k = nullptr; - unsigned num_prop = static_cast(s.s().get_stats().m_conflict * s.get_config().m_dack_factor); + unsigned num_prop = static_cast(s.s().get_stats().m_conflicts * s.get_config().m_dack_factor); num_prop = std::min(num_prop, m_table.size()); for (unsigned i = 0; i < num_prop; ++i, n = k) { k = n->next(); diff --git a/src/sat/smt/euf_ackerman.cpp b/src/sat/smt/euf_ackerman.cpp index 67a98b2f6..568df6034 100644 --- a/src/sat/smt/euf_ackerman.cpp +++ b/src/sat/smt/euf_ackerman.cpp @@ -171,7 +171,7 @@ namespace euf { SASSERT(ctx.s().at_base_lvl()); auto* n = m_queue; inference* k = nullptr; - unsigned num_prop = static_cast(ctx.s().get_stats().m_conflict * ctx.m_config.m_dack_factor); + unsigned num_prop = static_cast(ctx.s().get_stats().m_conflicts * ctx.m_config.m_dack_factor); num_prop = std::min(num_prop, m_table.size()); for (unsigned i = 0; i < num_prop; ++i, n = k) { k = n->next(); diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 098240fc9..f95b77b2d 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3652,6 +3652,13 @@ namespace smt { } } + void context::setup_for_parallel() { + // Native SMT parallel configures the parent context before cloning workers. + // context::copy then configures/internalizes each worker copy while + // preprocessing is still enabled. + setup_context(m_fparams.m_auto_config); + } + config_mode context::get_config_mode(bool use_static_features) const { if (!m_fparams.m_auto_config) return CFG_BASIC; diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 6a19ab5fd..193ef7705 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -64,6 +64,7 @@ namespace smt { class model_generator; class context; + class kernel; struct oom_exception : public z3_error { oom_exception() : z3_error(ERR_MEMOUT) {} @@ -85,6 +86,7 @@ namespace smt { friend class model_generator; friend class lookahead; friend class parallel; + friend class kernel; public: statistics m_stats; @@ -452,6 +454,8 @@ namespace smt { svector const & get_activity_vector() const { return m_activity; } double get_activity(bool_var v) const { return m_activity[v]; } + unsigned get_num_assignments() const { return m_stats.m_num_assignments; } + unsigned get_birthdate(bool_var v) const { return m_birthdate[v]; } void set_activity(bool_var v, double act) { m_activity[v] = act; } @@ -538,6 +542,8 @@ namespace smt { return m_scope_lvl == m_search_lvl; } + void pop_to_search_level() { pop_to_search_lvl(); } + bool tracking_assumptions() const { return !m_assumptions.empty() && m_search_lvl > m_base_lvl; } @@ -1697,6 +1703,8 @@ namespace smt { lbool setup_and_check(bool reset_cancel = true); + void setup_for_parallel(); + void reduce_assertions(); bool resource_limits_exceeded(); @@ -1914,4 +1922,3 @@ namespace smt { }; - diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp index a5ce0dcb7..fc2c87f5a 100644 --- a/src/smt/smt_kernel.cpp +++ b/src/smt/smt_kernel.cpp @@ -280,6 +280,22 @@ namespace smt { smt_params_helper::collect_param_descrs(d); } + void kernel::pop_to_base_level() { + m_imp->m_kernel.pop_to_base_lvl(); + } + + void kernel::set_preprocess(bool f) { + m_imp->m_kernel.get_fparams().m_preprocess = f; + } + + void kernel::reset_aux_statistics() { + m_imp->m_kernel.m_aux_stats.reset(); + } + + void kernel::add_aux_statistics(::statistics const& st) { + m_imp->m_kernel.m_aux_stats.copy(st); + } + context & kernel::get_context() { return m_imp->m_kernel; } diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h index 98b677213..a1b2bfc18 100644 --- a/src/smt/smt_kernel.h +++ b/src/smt/smt_kernel.h @@ -300,6 +300,14 @@ namespace smt { */ static void collect_param_descrs(param_descrs & d); + void pop_to_base_level(); + + void set_preprocess(bool f); + + void reset_aux_statistics(); + + void add_aux_statistics(::statistics const& st); + void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause); /** diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 64848d890..a7a1acf8a 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -626,7 +626,7 @@ namespace smt { ctx->set_logic(p.ctx.m_setup.get_logic()); context::copy(p.ctx, *ctx, true); ctx->pop_to_base_lvl(); - ctx->get_fparams().m_preprocess = false; + ctx->get_fparams().m_preprocess = false; // avoid preprocessing lemmas that are exchanged } void parallel::core_minimizer_worker::cancel() { @@ -887,6 +887,7 @@ namespace smt { ctx->pop_to_base_lvl(); m_shared_units_prefix = ctx->assigned_literals().size(); m_num_initial_atoms = ctx->get_num_bool_vars(); + ctx->get_fparams().m_preprocess = false; // avoid preprocessing lemmas that are exchanged smt_parallel_params pp(p.ctx.m_params); m_use_failed_literal_test = pp.num_global_bb_fl_threads() > 0; diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h index 64fcc1186..b98870e0c 100644 --- a/src/smt/smt_parallel.h +++ b/src/smt/smt_parallel.h @@ -32,6 +32,13 @@ namespace smt { struct cube_config { using literal = expr_ref; static bool literal_is_null(expr_ref const& l) { return l == nullptr; } + static bool same_atom(expr_ref const& a, expr_ref const& b) { + expr* atom_a = a.get(); + expr* atom_b = b.get(); + a.get_manager().is_not(atom_a, atom_a); + b.get_manager().is_not(atom_b, atom_b); + return atom_a == atom_b; + } static std::ostream& display_literal(std::ostream& out, expr_ref const& l) { return out << mk_bounded_pp(l, l.get_manager()); } }; diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index d1e5e5a6b..81391cb34 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -22,12 +22,15 @@ Notes: #include "ast/for_each_expr.h" #include "ast/ast_pp.h" #include "ast/func_decl_dependencies.h" +#include "smt/smt_context.h" #include "smt/smt_kernel.h" #include "params/smt_params.h" #include "params/smt_params_helper.hpp" #include "solver/solver_na2as.h" #include "solver/mus.h" +#include + namespace { class smt_solver : public solver_na2as { @@ -61,6 +64,7 @@ namespace { smt_params m_smt_params; smt::kernel m_context; cuber* m_cuber; + random_gen m_rand; symbol m_logic; bool m_minimizing_core; bool m_core_extend_patterns; @@ -86,14 +90,17 @@ namespace { solver * translate(ast_manager & m, params_ref const & p) override { ast_translation translator(get_manager(), m); + params_ref init; + init.copy(get_params()); + init.copy(p); - smt_solver * result = alloc(smt_solver, m, p, m_logic); + smt_solver* result = alloc(smt_solver, m, init, m_logic); smt::kernel::copy(m_context, result->m_context, true); - if (mc0()) + if (mc0()) result->set_model_converter(mc0()->translate(translator)); - for (auto & [k, v] : m_name2assertion) { + for (auto& [k, v] : m_name2assertion) { expr* val = translator(k); expr* key = translator(v); result->assert_expr(val, key); @@ -212,6 +219,112 @@ namespace { return m_context.get_trail(max_level); } + expr_ref_vector get_assigned_literals() override { + expr_ref_vector result(m); + auto& ctx = const_cast(m_context).get_context(); + for (auto lit : ctx.assigned_literals()) { + expr* atom = ctx.bool_var2expr(lit.var()); + if (!atom) + continue; + result.push_back(lit.sign() ? m.mk_not(atom) : atom); + } + return result; + } + + unsigned get_assign_level(expr* e) const override { + auto& ctx = const_cast(m_context).get_context(); + expr* atom = e; + get_manager().is_not(e, atom); + if (!ctx.b_internalized(atom)) + return UINT_MAX; + return ctx.get_assign_level(ctx.get_bool_var(atom)); + } + + bool is_relevant(expr* e) const override { + auto& ctx = const_cast(m_context).get_context(); + expr* atom = e; + get_manager().is_not(e, atom); + return ctx.b_internalized(atom) && ctx.is_relevant(atom); + } + + unsigned get_num_bool_vars() const override { + return const_cast(m_context).get_context().get_num_bool_vars(); + } + + unsigned get_bool_var(expr* e) const override { + auto& ctx = const_cast(m_context).get_context(); + expr* atom = e; + get_manager().is_not(e, atom); + return ctx.b_internalized(atom) ? ctx.get_bool_var(atom) : UINT_MAX; + } + + void pop_to_base_level() override { + m_context.pop_to_base_level(); + } + + void setup_for_parallel() override { + const_cast(m_context).get_context().setup_for_parallel(); + } + + void set_preprocess(bool f) override { + m_context.set_preprocess(f); + } + + void set_max_conflicts(unsigned max_conflicts) override { + auto& ctx = const_cast(m_context).get_context(); + ctx.get_fparams().m_max_conflicts = max_conflicts; + } + + unsigned get_max_conflicts() const override { + return const_cast(m_context).get_context().get_fparams().m_max_conflicts; + } + + void reset_parallel_statistics() override { + m_context.reset_aux_statistics(); + } + + void add_parallel_statistics(statistics const& st) override { + m_context.add_aux_statistics(st); + } + + void collect_parallel_statistics(statistics& st) const override { + m_context.collect_statistics(st); + } + + void get_backbone_candidates(vector& candidates, unsigned max_num) override { + ast_manager& m = get_manager(); + auto& ctx = m_context.get_context(); + unsigned curr_time = ctx.get_num_assignments(); + vector all; + + for (unsigned v = 0; v < ctx.get_num_bool_vars(); ++v) { + if (ctx.get_assignment(v) != l_undef && ctx.get_assign_level(v) == ctx.get_base_level()) + continue; + + expr* candidate = ctx.bool_var2expr(v); + if (!candidate) + continue; + + auto const& d = ctx.get_bdata(v); + if (d.m_phase_available && !d.m_phase) + candidate = m.mk_not(candidate); + + double age = static_cast(curr_time - ctx.get_birthdate(v)); + all.push_back(solver::scored_literal(m, candidate, age)); + } + + std::stable_sort( + all.begin(), + all.end(), + [](solver::scored_literal const& a, solver::scored_literal const& b) { + return a.score > b.score; + }); + + unsigned n = std::min(max_num, all.size()); + for (unsigned i = 0; i < n; ++i) + candidates.push_back(all[i]); + } + void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause) override { m_context.register_on_clause(ctx, on_clause); } @@ -347,6 +460,44 @@ namespace { expr_ref_vector cube(expr_ref_vector& vars, unsigned cutoff) override { ast_manager& m = get_manager(); + if (!get_params().get_bool("cube.lookahead", false)) { + auto& ctx = m_context.get_context(); + obj_hashtable selected_vars; + for (expr* v : vars) + selected_vars.insert(v); + expr_ref_vector candidates(m); + expr_ref result(m); + double score = 0.0; + unsigned n = 0; + + ctx.pop_to_search_level(); + for (unsigned v = 0; v < ctx.get_num_bool_vars(); ++v) { + if (ctx.get_assignment(v) != l_undef) + continue; + expr* e = ctx.bool_var2expr(v); + if (!e) + continue; + if (!selected_vars.empty() && !selected_vars.contains(e)) + continue; + candidates.push_back(e); + double new_score = ctx.get_activity(v); + // Match smt_parallel: cube split tie-breaking is independent + // of the per-worker SMT search seed. + if (new_score > score || !result || (new_score == score && m_rand(++n) == 0)) { + score = new_score; + result = e; + } + } + + vars.reset(); + vars.append(candidates); + + expr_ref_vector lits(m); + if (result) + lits.push_back(result); + return lits; + } + if (!m_cuber) { m_cuber = alloc(cuber, *this); // force propagation diff --git a/src/solver/parallel_params.pyg b/src/solver/parallel_params.pyg index 2aa2acf77..e577c58e8 100644 --- a/src/solver/parallel_params.pyg +++ b/src/solver/parallel_params.pyg @@ -6,6 +6,9 @@ def_module_params('parallel', ('enable', BOOL, False, 'enable parallel solver by default on selected tactics (for QF_BV)'), ('enable2', BOOL, False, 'enable (experimental) parallel solver by default on selected tactics (for QF_BV)'), ('threads.max', UINT, 10000, 'caps maximal number of threads below the number of processors'), + ('num_bb_threads', UINT, 2, 'run Janota-style chunking backbone worker threads; default is 2 (negative and positive mode), supported values are 0 (off), 1 (negative mode only) or 2 (negative and positive mode)'), + ('core_minimize', BOOL, True, 'minimize unsat cores used for parallel cube backtracking'), + ('cube.lookahead', BOOL, False, 'use lookahead cubing in the parallel solver; when false, use VSIDS activity to select one split literal'), ('conquer.batch_size', UINT, 100, 'number of cubes to batch together for fast conquer'), ('conquer.restart.max', UINT, 5, 'maximal number of restarts during conquer phase'), ('conquer.delay', UINT, 10, 'delay of cubes until applying conquer'), diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp index ebae4cb57..ae5b739f4 100644 --- a/src/solver/parallel_tactical2.cpp +++ b/src/solver/parallel_tactical2.cpp @@ -7,37 +7,7 @@ Module Name: Abstract: - Parallel portfolio solver using the solver API. - - Models the internals after smt/smt_parallel.cpp but operates on generic - solver objects (smt_solver, inc_sat_solver, etc.) via the solver interface - instead of accessing smt::context internals directly. - - Key features compared to parallel_tactical.cpp: - - Search tree for coordinated non-chronological backtracking (from smt_parallel). - - Shared clause pool: learned conflict clauses are broadcast to all workers. - - Shared backbone/unit pool: base-level units propagated by one worker are - asserted as facts on every other worker's solver. - - Workers reuse their solver state across multiple cube checks, accumulating - learned clauses (same pattern as smt_parallel workers). - - Key differences from smt_parallel: - - Uses the solver API throughout (translate, check_sat, get_trail, cube, - get_model, get_unsat_core, assert_expr, push, pop, updt_params, …) - rather than accessing smt::context members directly. - - Works with any conforming solver implementation. - - Cube path management follows the assumption-based pattern from smt_parallel: - - The worker's solver base assertion set is fixed at construction (the full - problem is translated into the worker's own ast_manager once). - - Shared clauses discovered by other workers are appended to the base set via - assert_expr at any time. - - The current cube path is passed as extra assumptions on every check_sat call, - so the solver can reuse learned clauses across different cube checks. - - Split atom selection is performed by temporarily pushing the cube path onto - the solver, calling solver::cube(), retrieving the first proposed literal, and - then popping, so that the base state is preserved. + Parallel tactical, portfolio loop specialized to the solver API. Author: @@ -55,14 +25,15 @@ Author: #include "solver/solver.h" #include "solver/parallel_tactical2.h" #include "solver/parallel_params.hpp" -#include "solver/solver_preprocess.h" #include "util/search_tree.h" #include "tactic/tactic.h" -#include "tactic/tactical.h" #include "solver/solver2tactic.h" +#include #include +#include #include +#include /* ------------------------------------------------------------------ */ /* Single-threaded stub */ @@ -91,6 +62,26 @@ tactic* mk_parallel_tactic2(solver* s, params_ref const& p) { #include #include +#define LOG_WORKER(lvl, s) IF_VERBOSE(lvl, verbose_stream() << "Worker " << id << s) +#define LOG_BB_WORKER(lvl, s) IF_VERBOSE(lvl, verbose_stream() << "Backbones Worker " << id << s) + +class bounded_pp_exprs { + expr_ref_vector const &es; + +public: + bounded_pp_exprs(expr_ref_vector const &es) : es(es) {} + + std::ostream &display(std::ostream &out) const { + for (auto e : es) + out << mk_bounded_pp(e, es.get_manager()) << "\n"; + return out; + } +}; + +inline std::ostream &operator<<(std::ostream &out, bounded_pp_exprs const &pp) { + return pp.display(out); +} + /* ------------------------------------------------------------------ */ /* Search-tree literal configuration */ /* ------------------------------------------------------------------ */ @@ -98,12 +89,23 @@ tactic* mk_parallel_tactic2(solver* s, params_ref const& p) { struct solver_cube_config { using literal = expr_ref; static bool literal_is_null(expr_ref const& l) { return l == nullptr; } + static bool same_atom(expr_ref const& a, expr_ref const& b) { + expr* atom_a = a.get(); + expr* atom_b = b.get(); + a.get_manager().is_not(atom_a, atom_a); + b.get_manager().is_not(atom_b, atom_b); + return atom_a == atom_b; + } static std::ostream& display_literal(std::ostream& out, expr_ref const& l) { if (l) return out << mk_bounded_pp(l, l.get_manager()); return out << "(null)"; } }; +static bool is_cancellation_exception(char const* msg) { + return msg && (strstr(msg, "canceled") != nullptr || strstr(msg, "cancelled") != nullptr); +} + /* ------------------------------------------------------------------ */ /* parallel_solver – the core portfolio engine */ /* ------------------------------------------------------------------ */ @@ -112,11 +114,21 @@ class parallel_solver { /* ---- forward declarations ---- */ class worker; + class core_minimizer_worker; + class backbones_worker; /* ---- node lease (mirrors smt_parallel) ---- */ struct node_lease { search_tree::node* leased_node = nullptr; + + // Cancellation generation counter for this node/subtree. + // Incremented when the node is closed; used to signal that all + // workers holding leases on this node (or its descendants) + // must abandon work immediately. unsigned cancel_epoch = 0; + + // Guards against multiple inc_cancel() calls for the same lease. + // Set when cancel_lease() is signaled; cleared when a new lease is assigned. bool cancel_signaled = false; }; @@ -126,11 +138,16 @@ class parallel_solver { expr_ref clause; }; - /* ================================================================ - * batch_manager - * Coordinates workers: distributes cubes, collects clauses/units, - * stores the final result (sat model / unsat core / exception). - * ================================================================ */ + struct bb_candidate { + expr_ref lit; + double age; + unsigned hits; // how many cubes reported it + bb_candidate(ast_manager& m, expr* e, double s, unsigned h) + : lit(e, m), age(s), hits(h) {} + }; + + using bb_candidates = vector; + class batch_manager { enum state { @@ -145,6 +162,19 @@ class parallel_solver { unsigned m_num_cubes = 0; unsigned m_max_cube_depth = 0; unsigned m_backbones_found = 0; + unsigned m_core_min_jobs_enqueued = 0; + unsigned m_core_min_jobs_published = 0; + unsigned m_core_min_jobs_skipped = 0; + unsigned m_core_min_global_unsat = 0; + unsigned m_bb_candidates_enqueued = 0; + unsigned m_bb_batches_issued = 0; + }; + + struct core_min_job { + search_tree::node* source = nullptr; + expr_ref_vector core; + core_min_job(ast_manager& m, search_tree::node* source) + : source(source), core(m) {} }; ast_manager& m; @@ -156,28 +186,49 @@ class parallel_solver { search_tree::tree m_search_tree; vector m_worker_leases; - /* shared clause pool (guarded by mux) */ - vector m_shared_clause_trail; - obj_hashtable m_shared_clause_set; + vector m_shared_clause_trail; // store all shared clauses with worker IDs + obj_hashtable m_shared_clause_set; // for duplicate filtering on per-thread clause expressions - /* shared backbone / unit pool (guarded by mux) */ obj_hashtable m_global_backbones; - /* result storage (guarded by mux) */ + bb_candidates m_bb_candidates; + unsigned m_max_global_bb_candidates = 100; + unsigned m_bb_batch_size = 150; + std::atomic m_bb_candidate_epoch = 0; + std::condition_variable m_bb_cv; + bb_candidates m_bb_current_batch; + unsigned m_bb_batch_id = 0; + unsigned m_num_bb_threads = 0; + unsigned_vector m_bb_last_batch_processed; + unsigned m_bb_cancel_epoch = 0; // When a backbone worker finishes early, it increments m_bb_cancel_epoch and notifies all + + // Core minimization job queue + std::condition_variable m_core_min_cv; + scoped_ptr_vector m_core_min_jobs; + unsigned m_exception_code = 0; std::string m_exception_msg; - model_ref m_model; /* sat model translated to m */ - expr_ref_vector m_unsat_core; /* unsat core translated to m */ + model_ref m_model; + expr_ref_vector m_unsat_core; - /* ---- cancellation helpers (called under mux) ---- */ + // called from batch manager to cancel other workers if we've reached a verdict void cancel_workers_unlocked() { - IF_VERBOSE(1, verbose_stream() << "par2: canceling workers\n"); + IF_VERBOSE(1, verbose_stream() << "Canceling workers\n"); for (auto* w : p.m_workers) w->cancel(); + if (p.m_core_minimizer_worker) { + p.m_core_minimizer_worker->cancel(); + m_core_min_cv.notify_all(); + } + if (!p.m_global_backbones_workers.empty()) + IF_VERBOSE(1, verbose_stream() << "Canceling backbones workers\n"); + for (auto* w : p.m_global_backbones_workers) + w->cancel(); + if (!p.m_global_backbones_workers.empty()) + m_bb_cv.notify_all(); } - void release_lease_unlocked(unsigned worker_id, - search_tree::node* n) { + void release_lease_unlocked(unsigned worker_id, search_tree::node* n) { if (worker_id >= m_worker_leases.size()) return; auto& lease = m_worker_leases[worker_id]; if (!lease.leased_node || lease.leased_node != n) return; @@ -198,9 +249,7 @@ class parallel_solver { } } - void collect_clause_unlocked(ast_translation& l2g, - unsigned source_worker_id, - expr* clause) { + void collect_clause_unlocked(ast_translation& l2g, unsigned source_worker_id, expr* clause) { expr* g_clause = l2g(clause); if (!m_shared_clause_set.contains(g_clause)) { m_shared_clause_set.insert(g_clause); @@ -209,12 +258,184 @@ class parallel_solver { } } - bool is_global_backbone_unlocked(ast_translation& l2g, - expr* bb_cand) { + // to avoid deadlock + bool is_global_backbone_unlocked(ast_translation& l2g, expr* bb_cand) { expr_ref cand(l2g(bb_cand), m); return m_global_backbones.contains(cand.get()); } + bool is_global_backbone_or_negation_unlocked(ast_translation& l2g, expr* bb_cand) { + expr_ref cand(l2g(bb_cand), m); + expr_ref neg_cand(mk_not(m, cand), m); + return m_global_backbones.contains(cand.get()) || + m_global_backbones.contains(neg_cand.get()); + } + + void collect_matching_targets_unlocked(search_tree::node* source, + expr* lit, + vector const& core, + vector& targets) { + targets.reset(); + if (!lit) + return; + + auto is_ancestor_of = [&](search_tree::node* ancestor, + search_tree::node* cur) { + if (!ancestor) + return false; + for (auto* p = cur; p; p = p->parent()) { + if (p == ancestor) + return true; + } + return false; + }; + + auto path_contains = [&](search_tree::node* cur, + solver_cube_config::literal const& lit0) { + for (auto* p = cur; p; p = p->parent()) { + if (p->get_literal() == lit0) + return true; + } + return false; + }; + + auto path_contains_core = [&](search_tree::node* cur) { + return all_of(core, [&](solver_cube_config::literal const& c) { + return path_contains(cur, c); + }); + }; + + ptr_vector> matches; + m_search_tree.find_nonclosed_nodes_with_literal(expr_ref(lit, m), matches); + for (auto* t : matches) { + if (!t || t == source) + continue; + if (m_search_tree.is_lease_canceled(t, t->get_cancel_epoch())) + continue; + + // When source is provided, keep only external matches. Nodes in the + // same branch are already closed by backtracking on the source node. + if (source && (is_ancestor_of(source, t) || is_ancestor_of(t, source))) + continue; + + // Reusing a conflict on another branch is sound only if that + // the path from that node->root contains every literal in the core. + // Matching on the closing literal alone is insufficient: F & a & l + // may be UNSAT while F & c & l is SAT. + if (!path_contains_core(t)) + continue; + + // Keep only highest matching nodes: closing an ancestor also closes + // all of its matching descendants. + bool is_highest_ancestor = true; + for (auto* p = t->parent(); p; p = p->parent()) { + if (any_of(targets, [&](node_lease const& target) { return target.leased_node == p; })) { + is_highest_ancestor = false; + break; + } + } + if (!is_highest_ancestor) + continue; + + targets.push_back({ t, t->get_cancel_epoch() }); + } + } + + // Given a newly closed node, source, and its core, find the lowest ancestor of source that + // contains a core literal, and return it as the source for the core minimization job + search_tree::node* find_core_source_unlocked( + ast_translation& l2g, search_tree::node* source, expr_ref_vector const& core) { + if (!source) + return nullptr; + + vector g_core; + for (expr* c : core) + g_core.push_back(expr_ref(l2g(c), m)); + + for (auto* cur = source; cur; cur = cur->parent()) { + if (solver_cube_config::literal_is_null(cur->get_literal())) + continue; + if (any_of(g_core, [&](solver_cube_config::literal const& lit) { return lit == cur->get_literal(); })) + return cur; + } + return nullptr; + } + + unsigned select_best_core_min_job_unlocked() const { + SASSERT(!m_core_min_jobs.empty()); + unsigned best_idx = 0; + auto* best_source = m_core_min_jobs[0]->source; + unsigned best_depth = best_source ? best_source->depth() : 0; + unsigned best_core_size = m_core_min_jobs[0]->core.size(); + + for (unsigned i = 1; i < m_core_min_jobs.size(); ++i) { + auto* job = m_core_min_jobs[i]; + auto* job_source = job->source; + unsigned job_depth = job_source ? job_source->depth() : 0; + unsigned job_core_size = job->core.size(); + + // rank first by core source node depth (deepest -> shallowest), then by core size (largest -> smallest) + if (job_depth > best_depth || + (job_depth == best_depth && job_core_size > best_core_size)) { + best_idx = i; + best_depth = job_depth; + best_core_size = job_core_size; + } + } + return best_idx; + } + + void backtrack_unlocked(ast_translation& l2g, unsigned worker_id, + expr_ref_vector const& core, + node_lease const* lease = nullptr, + vector const* targets = nullptr) { + if (m_state != state::is_running) + return; + + vector g_core; + for (expr* c : core) + g_core.push_back(expr_ref(l2g(c), m)); + + SASSERT(lease != nullptr || targets != nullptr); + bool did_backtrack = false; + + if (lease && !m_search_tree.is_lease_canceled(lease->leased_node, lease->cancel_epoch)) { + // we close/backtrack regardless of whether this lease is stale or not, as long as the lease isn't canceled + // i.e. worker 1 splits this node, but then worker 2 determines UNSAT --> worker 2 is stale but we still close this node and backtrack + did_backtrack = true; + release_lease_unlocked(worker_id, lease->leased_node); + m_search_tree.backtrack(lease->leased_node, g_core); + } + if (targets) { + for (auto const& target : *targets) { + if (m_search_tree.is_lease_canceled(target.leased_node, target.cancel_epoch)) + continue; + did_backtrack = true; + m_search_tree.backtrack(target.leased_node, g_core); + } + } + if (!did_backtrack) + return; + + // terminate on-demand the workers that are currently exploring the now-closed nodes + cancel_closed_leases_unlocked(worker_id); + + IF_VERBOSE(2, + for (expr* e : core) + verbose_stream() << mk_bounded_pp(e, core.get_manager()) << "\n"; + m_search_tree.display(verbose_stream() << "\n"); + ); + + if (m_search_tree.is_closed()) { + IF_VERBOSE(1, verbose_stream() << "Search tree closed, setting UNSAT\n"); + m_state = state::is_unsat; + SASSERT(m_unsat_core.empty()); + for (auto& e : m_search_tree.get_core_from_root()) + m_unsat_core.push_back(e.get()); + cancel_workers_unlocked(); + } + } + public: batch_manager(ast_manager& m, parallel_solver& p) @@ -222,25 +443,31 @@ class parallel_solver { m_search_tree(expr_ref(m)), m_unsat_core(m) {} - /* ---- initialisation ---- */ - void initialize(unsigned num_workers, - unsigned initial_max_thread_conflicts = 1000) { + void initialize(unsigned num_bb_threads, unsigned initial_max_thread_conflicts = 1000) { m_state = state::is_running; m_search_tree.reset(); m_search_tree.set_effort_unit(initial_max_thread_conflicts); m_worker_leases.reset(); - m_worker_leases.resize(num_workers); + m_worker_leases.resize(p.m_workers.size()); m_shared_clause_trail.reset(); m_shared_clause_set.reset(); m_global_backbones.reset(); + m_bb_candidates.reset(); + m_bb_current_batch.reset(); + m_bb_batch_id = 0; + m_num_bb_threads = num_bb_threads; + m_bb_last_batch_processed.reset(); + m_bb_last_batch_processed.resize(num_bb_threads); + m_bb_cancel_epoch = 0; + m_bb_candidate_epoch.store(0, std::memory_order_release); + m_core_min_jobs.reset(); m_model = nullptr; m_unsat_core.reset(); } - /* ---- result setters (called by workers, guarded by mux) ---- */ void set_sat(ast_translation& l2g, model& mdl) { std::scoped_lock lock(mux); - IF_VERBOSE(1, verbose_stream() << "par2: batch_manager SAT\n"); + IF_VERBOSE(1, verbose_stream() << "Batch manager setting SAT.\n"); if (m_state != state::is_running) return; m_state = state::is_sat; m_model = mdl.translate(l2g); @@ -250,7 +477,7 @@ class parallel_solver { void set_unsat(ast_translation& l2g, expr_ref_vector const& core) { std::scoped_lock lock(mux); - IF_VERBOSE(1, verbose_stream() << "par2: batch_manager UNSAT\n"); + IF_VERBOSE(1, verbose_stream() << "Batch manager setting UNSAT.\n"); if (m_state != state::is_running) return; m_state = state::is_unsat; SASSERT(m_unsat_core.empty()); @@ -261,7 +488,7 @@ class parallel_solver { void set_exception(std::string const& msg) { std::scoped_lock lock(mux); - IF_VERBOSE(1, verbose_stream() << "par2: batch_manager exception: " << msg << "\n"); + IF_VERBOSE(1, verbose_stream() << "Batch manager setting exception msg: " << msg << ".\n"); if (m_state != state::is_running) return; m_state = state::is_exception_msg; m_exception_msg = msg; @@ -270,13 +497,13 @@ class parallel_solver { void set_exception(unsigned error_code) { std::scoped_lock lock(mux); + IF_VERBOSE(1, verbose_stream() << "Batch manager setting exception code: " << error_code << ".\n"); if (m_state != state::is_running) return; m_state = state::is_exception_code; m_exception_code = error_code; cancel_workers_unlocked(); } - /* ---- cube distribution (called by workers) ---- */ bool get_cube(ast_translation& g2l, unsigned id, expr_ref_vector& cube, bool is_first_run, node_lease& lease) { @@ -296,7 +523,6 @@ class parallel_solver { m_worker_leases.resize(id + 1); m_worker_leases[id] = lease; - /* build cube from path root → t */ for (auto* cur = t; cur; cur = cur->parent()) { if (solver_cube_config::literal_is_null(cur->get_literal())) break; @@ -305,37 +531,139 @@ class parallel_solver { return true; } - /* ---- backtrack on conflict (called by workers) ---- */ void backtrack(ast_translation& l2g, unsigned worker_id, expr_ref_vector const& core, node_lease const& lease) { std::scoped_lock lock(mux); if (m_state != state::is_running) return; - vector g_core; - for (auto c : core) + for (expr* c : core) g_core.push_back(expr_ref(l2g(c), m)); - if (!m_search_tree.is_lease_canceled( - lease.leased_node, lease.cancel_epoch)) { - release_lease_unlocked(worker_id, lease.leased_node); - m_search_tree.backtrack(lease.leased_node, g_core); + vector targets; + expr* lit = lease.leased_node ? lease.leased_node->get_literal().get() : nullptr; + collect_matching_targets_unlocked(lease.leased_node, lit, g_core, targets); + backtrack_unlocked(l2g, worker_id, core, &lease, targets.empty() ? nullptr : &targets); + } + + void enqueue_core_minimization(ast_translation& l2g, + search_tree::node* source, + expr_ref_vector const& core) { + std::scoped_lock lock(mux); + if (m_state != state::is_running || !p.m_core_minimizer_worker || !source || core.empty()) + return; + if (core.size() <= 1) { + ++m_stats.m_core_min_jobs_skipped; + return; } - cancel_closed_leases_unlocked(worker_id); + source = find_core_source_unlocked(l2g, source, core); + if (!source) { + ++m_stats.m_core_min_jobs_skipped; + return; + } - IF_VERBOSE(2, m_search_tree.display(verbose_stream() << "\n");); + scoped_ptr job = alloc(core_min_job, m, source); + for (expr* c : core) + job->core.push_back(l2g(c)); + m_core_min_jobs.push_back(job.detach()); + ++m_stats.m_core_min_jobs_enqueued; + m_core_min_cv.notify_one(); + } - if (m_search_tree.is_closed()) { - IF_VERBOSE(1, verbose_stream() << "par2: search tree closed → UNSAT\n"); + bool wait_for_core_min_job(ast_translation& g2l, + search_tree::node*& source, + expr_ref_vector& core, + reslimit& lim) { + std::unique_lock lock(mux); + m_core_min_cv.wait(lock, [&]() { + return lim.is_canceled() || m_state != state::is_running || !m_core_min_jobs.empty(); + }); + + if (lim.is_canceled() || m_state != state::is_running) + return false; + + unsigned best_idx = select_best_core_min_job_unlocked(); + m_core_min_jobs.swap(best_idx, m_core_min_jobs.size() - 1); + core_min_job* job = m_core_min_jobs.detach_back(); + m_core_min_jobs.pop_back(); + SASSERT(job); + source = job->source; + core.reset(); + for (expr* c : job->core) + core.push_back(g2l(c)); + dealloc(job); + return source != nullptr; + } + + void publish_minimized_core(ast_translation& l2g, + expr_ref_vector const& asms, + search_tree::node* source, + unsigned original_core_size, + expr_ref_vector const& minimized_core) { + std::scoped_lock lock(mux); + if (m_state != state::is_running || !source || minimized_core.size() >= original_core_size) { + ++m_stats.m_core_min_jobs_skipped; + return; + } + + vector g_core; + for (expr* c : minimized_core) + g_core.push_back(expr_ref(l2g(c), m)); + + // don't publish a minimized core if the node already has an equal-or-smaller core by the time the minimizer thread finishes + // (e.g. from another thread or from backtracking resolution propagation) + if (source->get_core().size() <= g_core.size()) { + ++m_stats.m_core_min_jobs_skipped; + return; + } + + if (all_of(g_core, [&](solver_cube_config::literal const& lit) { return asms.contains(lit.get()); })) { + IF_VERBOSE(1, verbose_stream() << "Minimized core removed all path literals, setting UNSAT\n"); m_state = state::is_unsat; + SASSERT(m_unsat_core.empty()); + for (expr* e : minimized_core) + m_unsat_core.push_back(l2g(e)); + ++m_stats.m_core_min_jobs_published; + ++m_stats.m_core_min_global_unsat; + cancel_workers_unlocked(); + return; + } + + // do not backtrack through the batch manager since this only handles non-closed leases + // and the batch manager also tries to search for external matching targets in the tree + // which is a problem since we must backtrack only on the source node or the core is invalid + m_search_tree.backtrack(source, g_core); + + vector targets; + if (!g_core.empty()) { + collect_matching_targets_unlocked(source, g_core[0].get(), g_core, targets); + for (auto const& target : targets) { + if (!m_search_tree.is_lease_canceled(target.leased_node, target.cancel_epoch)) + m_search_tree.backtrack(target.leased_node, g_core); + } + } + + ++m_stats.m_core_min_jobs_published; + cancel_closed_leases_unlocked(UINT_MAX); + + IF_VERBOSE(1, verbose_stream() << "Batch manager publishing minimized core " + << original_core_size << " -> " << minimized_core.size() << "\n"); + IF_VERBOSE(2, + for (expr* e : minimized_core) + verbose_stream() << mk_bounded_pp(e, minimized_core.get_manager()) << "\n"; + m_search_tree.display(verbose_stream() << "\n"); + ); + if (m_search_tree.is_closed()) { + IF_VERBOSE(1, verbose_stream() << "Search tree closed by minimized core, setting UNSAT\n"); + m_state = state::is_unsat; + SASSERT(m_unsat_core.empty()); for (auto& e : m_search_tree.get_core_from_root()) m_unsat_core.push_back(e.get()); cancel_workers_unlocked(); } } - /* ---- try to split (called on undef) ---- */ void try_split(ast_translation& l2g, unsigned worker_id, node_lease const& lease, expr* atom, unsigned effort) { @@ -347,6 +675,8 @@ class parallel_solver { expr_ref lit(m), nlit(m); lit = l2g(atom); nlit = mk_not(m, lit); + VERIFY(!lease.leased_node->path_contains_atom(lit)); + VERIFY(!lease.leased_node->path_contains_atom(nlit)); bool did_split = m_search_tree.try_split( lease.leased_node, lease.cancel_epoch, @@ -359,8 +689,7 @@ class parallel_solver { m_stats.m_max_cube_depth = std::max( m_stats.m_max_cube_depth, lease.leased_node->depth() + 1); - IF_VERBOSE(1, verbose_stream() << "par2: split on " - << mk_bounded_pp(lit, m, 3) << "\n"); + IF_VERBOSE(1, verbose_stream() << "Batch manager splitting on literal: " << mk_bounded_pp(lit, m, 3) << "\n"); } } @@ -376,7 +705,6 @@ class parallel_solver { lease.leased_node, lease.cancel_epoch); } - /* ---- clause sharing ---- */ void collect_clause(ast_translation& l2g, unsigned source_worker_id, expr* clause) { @@ -384,41 +712,178 @@ class parallel_solver { collect_clause_unlocked(l2g, source_worker_id, clause); } - expr_ref_vector return_shared_clauses(ast_translation& g2l, - unsigned& worker_limit, - unsigned worker_id) { + expr_ref_vector return_shared_clauses(ast_translation& g2l, unsigned& worker_limit, unsigned worker_id) { std::scoped_lock lock(mux); expr_ref_vector result(g2l.to()); for (unsigned i = worker_limit; i < m_shared_clause_trail.size(); ++i) { if (m_shared_clause_trail[i].source_worker_id != worker_id) result.push_back(g2l(m_shared_clause_trail[i].clause.get())); } - worker_limit = m_shared_clause_trail.size(); + worker_limit = m_shared_clause_trail.size(); // update the worker limit to the end of the current trail return result; } - /* ---- backbone / unit sharing ---- */ - bool collect_global_backbone(ast_translation& l2g, - expr_ref const& backbone, - unsigned source_worker_id = UINT_MAX) { + bool collect_global_backbone(ast_translation& l2g, expr_ref const& backbone, unsigned source_worker_id = UINT_MAX) { std::scoped_lock lock(mux); + IF_VERBOSE(1, verbose_stream() << "collect-global-backbone\n"); if (is_global_backbone_unlocked(l2g, backbone.get())) return false; expr_ref g_bb(l2g(backbone.get()), m); m_global_backbones.insert(g_bb.get()); ++m_stats.m_backbones_found; - IF_VERBOSE(2, verbose_stream() << "par2: new backbone " - << mk_bounded_pp(g_bb, m, 3) << "\n"); - /* share it as a unit clause so other workers pick it up */ + IF_VERBOSE(1, verbose_stream() << " Found and sharing new global backbone: " << mk_bounded_pp(g_bb, m, 3) << "\n"); collect_clause_unlocked(l2g, source_worker_id, backbone.get()); + + expr_ref neg_g_bb(mk_not(m, g_bb), m); + vector g_core; + g_core.push_back(neg_g_bb); + vector targets; + collect_matching_targets_unlocked(nullptr, neg_g_bb, g_core, targets); + + if (!targets.empty()) { + IF_VERBOSE(1, verbose_stream() << " Closing negation of the new global backbone: " + << mk_bounded_pp(g_bb, m, 3) << "\n"); + expr_ref_vector l_core(l2g.from()); + l_core.push_back(mk_not(backbone)); + backtrack_unlocked(l2g, UINT_MAX, l_core, nullptr, &targets); + } + + return true; + } + + bool is_global_backbone_or_negation(ast_translation& l2g, expr* bb_cand) { + std::scoped_lock lock(mux); + return is_global_backbone_or_negation_unlocked(l2g, bb_cand); + } + + bool has_new_backbone_candidates(unsigned epoch) { + return m_bb_candidate_epoch.load(std::memory_order_acquire) != epoch; + } + + unsigned get_bb_candidate_epoch() const { + return m_bb_candidate_epoch.load(std::memory_order_acquire); + } + + void cancel_current_backbone_batch() { + std::scoped_lock lock(mux); + ++m_bb_cancel_epoch; + m_bb_cv.notify_all(); + } + + unsigned get_cancel_epoch() { + std::scoped_lock lock(mux); + return m_bb_cancel_epoch; + } + + expr_ref_vector get_global_backbones_snapshot(ast_translation& g2l) { + std::scoped_lock lock(mux); + expr_ref_vector snapshot(g2l.to()); + for (expr* gb : m_global_backbones) + snapshot.push_back(g2l(gb)); + return snapshot; + } + + void collect_backbone_candidates(ast_translation& l2g, + bb_candidates& bb_candidates) { + std::scoped_lock lock(mux); + bool changed = false; + + auto find_existing_candidate_idx = [&](expr* e) -> int { + for (unsigned i = 0; i < m_bb_candidates.size(); ++i) { + if (m_bb_candidates[i].lit.get() == e) + return i; + } + return -1; + }; + + auto rank_of = [&](bb_candidate const& c) { + return c.age * std::log2(2.0 + c.hits); + }; + + for (auto const& c : bb_candidates) { + expr_ref g_lit(l2g(c.lit.get()), m); + if (is_global_backbone_or_negation_unlocked(l2g, c.lit.get())) + continue; + + double age = c.age; + int idx = find_existing_candidate_idx(g_lit.get()); + if (idx >= 0) { + auto& existing = m_bb_candidates[idx]; + existing.age = (existing.age * existing.hits + age) / (existing.hits + 1); + existing.hits++; + continue; + } + + if (m_bb_candidates.size() < m_max_global_bb_candidates) { + m_bb_candidates.push_back(bb_candidate(m, g_lit.get(), age, 1)); + changed = true; + continue; + } + + bb_candidate incoming(m, g_lit.get(), age, 1); + auto worst_it = std::min_element( + m_bb_candidates.begin(), + m_bb_candidates.end(), + [&](bb_candidate const& a, bb_candidate const& b) { + return rank_of(a) < rank_of(b); + }); + if (worst_it != m_bb_candidates.end() && rank_of(incoming) > rank_of(*worst_it)) { + *worst_it = incoming; + changed = true; + } + } + + if (changed && !m_bb_candidates.empty()) { + m_bb_candidate_epoch.fetch_add(1, std::memory_order_release); + std::sort( + m_bb_candidates.begin(), + m_bb_candidates.end(), + [&](bb_candidate const& a, bb_candidate const& b) { + return rank_of(a) < rank_of(b); + }); + m_bb_cv.notify_all(); + } + } + + bool wait_for_backbone_job(unsigned bb_thread_id, ast_translation& g2l, + bb_candidates& out, reslimit& lim) { + out.reset(); + std::unique_lock lock(mux); + m_bb_cv.wait(lock, [&]() { + return lim.is_canceled() || + m_state != state::is_running || + m_bb_last_batch_processed[bb_thread_id] < m_bb_batch_id || + !m_bb_candidates.empty(); + }); + + if (lim.is_canceled() || m_state != state::is_running) + return false; + + if (m_bb_last_batch_processed[bb_thread_id] == m_bb_batch_id) { + unsigned n = std::min(m_bb_batch_size, m_bb_candidates.size()); + m_bb_current_batch.reset(); + for (unsigned i = 0; i < n; ++i) { + m_bb_current_batch.push_back(m_bb_candidates.back()); + m_bb_candidates.pop_back(); + } + ++m_bb_batch_id; + m_bb_cv.notify_all(); + } + + for (auto const& gc : m_bb_current_batch) { + expr_ref l_lit(g2l(gc.lit.get()), g2l.to()); + out.push_back(bb_candidate(g2l.to(), l_lit, gc.age, gc.hits)); + } + m_bb_last_batch_processed[bb_thread_id] = m_bb_batch_id; return true; } - /* ---- result accessors ---- */ lbool get_result() const { - if (m.limit().is_canceled()) return l_undef; + if (m.limit().is_canceled()) + return l_undef; // the main context was cancelled, so we return undef. switch (m_state) { - case state::is_running: + case state::is_running: // batch manager is still running, but all threads have processed their cubes, which + // means all cubes were unsat throw default_exception("par2: inconsistent end state"); case state::is_sat: return l_true; case state::is_unsat: return l_false; @@ -437,11 +902,15 @@ class parallel_solver { expr_ref_vector const& get_unsat_core() const { return m_unsat_core; } void collect_statistics(statistics& st) const { - st.update("par2-cubes", m_stats.m_num_cubes); - st.update("par2-cube-depth", m_stats.m_max_cube_depth); - st.update("par2-backbones", m_stats.m_backbones_found); + st.update("parallel-num_cubes", m_stats.m_num_cubes); + st.update("parallel-max-cube-size", m_stats.m_max_cube_depth); + st.update("bb-backbones-found", m_stats.m_backbones_found); + st.update("parallel-core-min-jobs-enqueued", m_stats.m_core_min_jobs_enqueued); + st.update("parallel-core-min-jobs-published", m_stats.m_core_min_jobs_published); + st.update("parallel-core-min-jobs-skipped", m_stats.m_core_min_jobs_skipped); + st.update("parallel-core-min-global-unsat", m_stats.m_core_min_global_unsat); } - }; // class batch_manager + }; /* ================================================================ * worker @@ -450,50 +919,48 @@ class parallel_solver { * batch_manager (mutex-protected). * ================================================================ */ class worker { - struct config { - unsigned m_threads_max_conflicts = 1000; - double m_max_conflict_mul = 1.5; - unsigned m_max_conflicts = UINT_MAX; - bool m_share_units = true; - bool m_share_conflicts = true; - unsigned m_max_cube_depth = 20; + struct config { + unsigned m_threads_max_conflicts = 1000; + double m_max_conflict_mul = 1.5; + unsigned m_max_conflicts = UINT_MAX; + bool m_share_units = true; + bool m_share_conflicts = true; + bool m_share_units_relevant_only = true; + bool m_share_units_initial_only = true; + bool m_core_minimize = false; + bool m_global_backbones = false; + unsigned m_max_cube_depth = 20; }; unsigned id; - parallel_solver& p; batch_manager& b; ast_manager m; /* worker-local manager */ ref s; /* translated solver copy */ expr_ref_vector asms; /* translated assumptions */ ast_translation m_g2l, m_l2g; /* global↔local translations */ config m_config; - expr_mark m_known_units; /* units already shared by this worker */ + uint_set m_known_units; /* bool vars already shared by this worker */ unsigned m_shared_clause_limit = 0; + unsigned m_shared_units_prefix = 0; + unsigned m_num_initial_atoms = 0; - void update_max_conflicts() { + void update_max_thread_conflicts() { m_config.m_threads_max_conflicts = static_cast( m_config.m_max_conflict_mul * m_config.m_threads_max_conflicts); - /* cap at the configured global maximum to prevent runaway cube checks */ - if (m_config.m_threads_max_conflicts > m_config.m_max_conflicts) - m_config.m_threads_max_conflicts = m_config.m_max_conflicts; } - /* Check the current cube (passed as additional assumptions). - * The solver's conflict budget is set via updt_params before - * each call so that long-running cubes are interrupted. */ lbool check_cube(expr_ref_vector const& cube) { - params_ref p; - p.set_uint("max_conflicts", - std::min(m_config.m_threads_max_conflicts, - m_config.m_max_conflicts)); - s->updt_params(p); + s->set_max_conflicts(std::min(m_config.m_threads_max_conflicts, m_config.m_max_conflicts)); expr_ref_vector combined(m); combined.append(asms); combined.append(cube); - IF_VERBOSE(2, verbose_stream() << "par2 worker " << id - << ": checking cube of size " << cube.size() << "\n"); + IF_VERBOSE(1, verbose_stream() << " Checking cube\n" + << bounded_pp_exprs(cube) + << "with max_conflicts: " + << std::min(m_config.m_threads_max_conflicts, m_config.m_max_conflicts) + << "\n";); lbool r = l_undef; try { r = s->check_sat(combined); @@ -503,94 +970,141 @@ class parallel_solver { b.set_exception(err.error_code()); } catch (z3_exception& ex) { - if (!m.limit().is_canceled()) + if (!m.limit().is_canceled() && !is_cancellation_exception(ex.what())) b.set_exception(ex.what()); } - IF_VERBOSE(2, verbose_stream() << "par2 worker " << id - << ": cube result " << r << "\n"); + LOG_WORKER(1, " DONE checking cube " << r << "\n";); return r; } - /* Assert shared clauses discovered by other workers into the - * base assertion set of this worker's solver. The solver - * automatically re-uses them on the next check_sat call. */ void collect_shared_clauses() { - expr_ref_vector nc = b.return_shared_clauses( - m_g2l, m_shared_clause_limit, id); + expr_ref_vector nc = b.return_shared_clauses(m_g2l, m_shared_clause_limit, id); for (expr* e : nc) { - IF_VERBOSE(4, verbose_stream() << "par2 worker " << id - << ": asserting shared clause " - << mk_bounded_pp(e, m, 3) << "\n"); + LOG_WORKER(4, " asserting shared clause: " << mk_bounded_pp(e, m, 3) << "\n"); s->assert_expr(e); } } - /* Propagate any new base-level units (backbone literals) this - * worker has learned to the shared backbone pool. - * - * Uses solver::get_trail(0) which returns all literals - * propagated at decision level 0. */ void share_units() { - if (!m_config.m_share_units) return; - expr_ref_vector trail = s->get_trail(0); - for (expr* e : trail) { - /* get_trail may include ground terms; skip complex ones */ + if (!m_config.m_share_units) + return; + expr_ref_vector trail = s->get_assigned_literals(); + unsigned sz = trail.size(); + unsigned prefix_sz = std::min(m_shared_units_prefix, sz); + bool at_prefix = true; + + for (unsigned i = m_shared_units_prefix; i < sz; ++i) { + expr* e = trail.get(i); + if (s->get_assign_level(e) > 0) { + at_prefix = false; + continue; + } + + if (at_prefix) + ++prefix_sz; + expr* atom = e; m.is_not(e, atom); - if (!is_uninterp_const(atom)) continue; - if (m_known_units.is_marked(e)) continue; - m_known_units.mark(e); + + if (m.is_and(atom) || m.is_or(atom) || m.is_ite(atom) || m.is_iff(atom)) + continue; + + unsigned v = s->get_bool_var(atom); + if (v == UINT_MAX) + continue; + if (m_known_units.contains(v)) + continue; + m_known_units.insert(v); + + if (m_config.m_share_units_relevant_only && !s->is_relevant(atom)) + continue; + if (m_config.m_share_units_initial_only && v >= m_num_initial_atoms) + continue; + expr_ref lit(e, m); b.collect_global_backbone(m_l2g, lit, id); } + m_shared_units_prefix = prefix_sz; } - /* Select a split atom using solver::cube() on a temporary - * solver state that includes the current cube path. - * - * We push the cube literals, call cube(), take the first - * literal, then pop to restore the base state. */ expr_ref get_split_atom(expr_ref_vector const& cube) { if (cube.size() >= m_config.m_max_cube_depth) return expr_ref(nullptr, m); - s->push(); - for (expr* c : cube) - s->assert_expr(c); - expr_ref_vector vars(m); - expr_ref_vector c = s->cube(vars, UINT_MAX); + obj_hashtable rejected_atoms; + while (true) { + expr_ref_vector cands = s->cube(vars, 1); + bool rejected = false; + for (expr* lit : cands) { + if (!lit) + continue; + if (m.is_true(lit) || m.is_false(lit)) + continue; + if (m_config.m_global_backbones && b.is_global_backbone_or_negation(m_l2g, lit)) { + expr* atom = lit; + m.is_not(lit, atom); + rejected_atoms.insert(atom); + rejected = true; + continue; + } + return expr_ref(lit, m); + } - s->pop(1); + if (!rejected || vars.empty()) + return expr_ref(nullptr, m); - /* solver::cube() convention: an empty result means done; a result - * whose last element is true means the problem is trivially sat; - * a result whose last element is false means unsat was detected. - * In all other cases every element (including index 0) is a - * valid literal that can serve as a split atom. */ - if (c.empty() || m.is_true(c.back()) || m.is_false(c.back())) - return expr_ref(nullptr, m); + expr_ref_vector next_vars(m); + for (expr* v : vars) { + expr* atom = v; + m.is_not(v, atom); + if (!rejected_atoms.contains(atom)) + next_vars.push_back(v); + } + if (next_vars.empty() || next_vars.size() == vars.size()) + return expr_ref(nullptr, m); + vars.reset(); + vars.append(next_vars); + } + } - return expr_ref(c.get(0), m); + bb_candidates find_backbone_candidates(expr_ref_vector const& cube, unsigned k = 10) { + bb_candidates result; + vector cands; + s->get_backbone_candidates(cands, s->get_num_bool_vars()); + + for (auto const& cand : cands) { + expr* lit = cand.lit.get(); + if (m_config.m_global_backbones && + b.is_global_backbone_or_negation(m_l2g, lit)) + continue; + result.push_back(bb_candidate(m, lit, cand.score, 1)); + if (result.size() >= k) + break; + } + return result; } public: - worker(unsigned id, parallel_solver& p, - solver& src, params_ref const& params, - expr_ref_vector const& src_asms) - : id(id), p(p), b(p.m_batch_manager), - asms(m), m_g2l(src.get_manager(), m), m_l2g(m, src.get_manager()) - { - /* create translated solver copy */ - s = src.translate(m, params); + worker(unsigned id, parallel_solver& p, solver& src, params_ref const& params, expr_ref_vector const& src_asms) + : id(id), b(p.m_batch_manager), asms(m), m_g2l(src.get_manager(), m), m_l2g(m, src.get_manager()) { + parallel_params pp(params); + m_config.m_core_minimize = pp.core_minimize(); + m_config.m_global_backbones = pp.num_bb_threads() > 0; + + s = src.translate(m, params); + // don't share initial units + s->pop_to_base_level(); + m_shared_units_prefix = s->get_assigned_literals().size(); + m_num_initial_atoms = s->get_num_bool_vars(); + // avoid preprocessing lemmas that are exchanged + s->set_preprocess(false); - /* translate assumptions */ for (expr* a : src_asms) asms.push_back(m_g2l(a)); - IF_VERBOSE(1, verbose_stream() << "par2: worker " << id - << " created (" << asms.size() << " assumptions)\n"); + LOG_WORKER(1, " created with " << asms.size() << " assumptions\n"); } void run() { @@ -600,19 +1114,23 @@ class parallel_solver { while (true) { if (!b.get_cube(m_g2l, id, cube, is_first_run, lease)) { - IF_VERBOSE(1, verbose_stream() << "par2 worker " << id - << ": no more cubes\n"); + LOG_WORKER(1, " no more cubes\n"); return; } is_first_run = false; - collect_shared_clauses(); - + check_cube_start: + LOG_WORKER(1, " CUBE SIZE IN MAIN LOOP: " << cube.size() << "\n"); + if (m_config.m_global_backbones) { + bb_candidates local_candidates = find_backbone_candidates(cube); + b.collect_backbone_candidates(m_l2g, local_candidates); + if (!m.inc()) + return; + } lbool r = check_cube(cube); if (b.lease_canceled(lease)) { - IF_VERBOSE(1, verbose_stream() << "par2 worker " << id - << ": lease canceled\n"); + LOG_WORKER(1, " abandoning canceled lease\n"); lease = {}; m.limit().dec_cancel(); continue; @@ -623,24 +1141,24 @@ class parallel_solver { switch (r) { case l_undef: { - update_max_conflicts(); - IF_VERBOSE(1, verbose_stream() << "par2 worker " << id - << ": undef – attempting split\n"); + update_max_thread_conflicts(); + LOG_WORKER(1, " found undef cube\n"); + if (m_config.m_max_cube_depth <= cube.size()) + goto check_cube_start; expr_ref atom = get_split_atom(cube); if (atom) { b.try_split(m_l2g, id, lease, atom.get(), m_config.m_threads_max_conflicts); + lease = {}; } else { - b.release_lease(id, lease); + goto check_cube_start; } - if (m_config.m_share_units) share_units(); break; } case l_true: { - IF_VERBOSE(1, verbose_stream() << "par2 worker " << id - << ": SAT\n"); + LOG_WORKER(1, " found sat cube\n"); model_ref mdl; s->get_model(mdl); if (mdl) @@ -649,49 +1167,43 @@ class parallel_solver { } case l_false: { - IF_VERBOSE(1, verbose_stream() << "par2 worker " << id - << ": UNSAT cube\n"); - expr_ref_vector core(m); - s->get_unsat_core(core); + expr_ref_vector unsat_core(m); + s->get_unsat_core(unsat_core); + LOG_WORKER(2, " unsat core:\n"; + for (auto c : unsat_core) verbose_stream() << mk_bounded_pp(c, m, 3) << "\n"); - /* Filter to only cube literals (exclude base assumptions). */ - expr_ref_vector cube_core(m); - for (expr* c : core) { - if (cube.contains(c)) - cube_core.push_back(c); - } - - /* If core contains none of the cube lits, the whole - * problem is UNSAT independent of the cube path. */ - if (cube_core.empty()) { - b.set_unsat(m_l2g, core); + if (all_of(unsat_core, [&](expr* e) { return asms.contains(e); })) { + LOG_WORKER(1, " determined formula unsat\n"); + b.set_unsat(m_l2g, unsat_core); return; } - b.backtrack(m_l2g, id, cube_core, lease); + LOG_WORKER(1, " found unsat cube\n"); + auto* source = lease.leased_node; + b.backtrack(m_l2g, id, unsat_core, lease); - if (m_config.m_share_conflicts) { - /* Share the negation of the cube-core conjunction - * as a learned clause: ¬(c₁ ∧ … ∧ cₙ) ≡ ¬c₁ ∨ … ∨ ¬cₙ */ - expr_ref_vector neg_lits(m); - for (expr* c : cube_core) - neg_lits.push_back(mk_not(expr_ref(c, m))); - expr_ref clause(mk_or(neg_lits), m); - b.collect_clause(m_l2g, id, clause.get()); - } - if (m_config.m_share_units) share_units(); + if (m_config.m_core_minimize) + b.enqueue_core_minimization(m_l2g, source, unsat_core); + lease = {}; + + if (m_config.m_share_conflicts) + b.collect_clause(m_l2g, id, mk_not(mk_and(unsat_core))); break; } - } // switch - } // while - } // run() + } + if (m_config.m_share_units) + share_units(); + } + } void cancel() { + LOG_WORKER(1, " canceling\n"); m.limit().cancel(); } void cancel_lease() { + LOG_WORKER(1, " canceling lease\n"); m.limit().inc_cancel(); } @@ -700,16 +1212,596 @@ class parallel_solver { } reslimit& limit() { return m.limit(); } - }; // class worker + }; + + class backbones_worker { + private: + struct stats { + unsigned m_batches_total = 0; + unsigned m_candidates_total = 0; + unsigned m_singleton_backbones = 0; + unsigned m_backbones_detected = 0; + unsigned m_internal_backbones_found = 0; + unsigned m_retry_backbones_found = 0; + unsigned m_bb_retries = 0; + unsigned m_fallback_singleton_checks = 0; + unsigned m_fallback_reason_chunk_exhausted = 0; + unsigned m_fallback_reason_undef = 0; + unsigned m_core_refinement_rounds = 0; + unsigned m_lits_removed_by_core = 0; + unsigned m_num_chunk_increases = 0; + }; + + unsigned id; + batch_manager& b; + ast_manager m; + ref s; + expr_ref_vector asms; + ast_translation m_g2l, m_l2g; + unsigned m_bb_chunk_size = 20; + unsigned m_bb_conflicts_per_chunk = 1000; + unsigned m_shared_clause_limit = 0; + stats m_stats; + unsigned m_shared_units_prefix = 0; + unsigned m_num_initial_atoms = 0; + bool m_positive_mode = false; + + void collect_shared_clauses() { + expr_ref_vector nc = b.return_shared_clauses(m_g2l, m_shared_clause_limit, UINT_MAX); + for (expr* e : nc) { + s->assert_expr(e); + LOG_BB_WORKER(4, " asserting shared clause: " << mk_bounded_pp(e, m, 3) << "\n"); + } + } + + bool try_get_unit_backbone(expr* candidate, expr_ref& backbone) { + expr_ref_vector trail = s->get_assigned_literals(); + expr* atom = candidate; + m.is_not(candidate, atom); + for (expr* e : trail) { + if (s->get_assign_level(e) > 0) + continue; + expr* trail_atom = e; + m.is_not(e, trail_atom); + if (trail_atom != atom) + continue; + backbone = expr_ref(e, m); + return true; + } + return false; + } + + lbool probe_literal(expr* e, bool is_retry) { + lbool r = l_undef; + try { + asms.push_back(e); + r = s->check_sat(asms); + asms.pop_back(); + } + catch (z3_error& err) { + asms.pop_back(); + if (!m.limit().is_canceled()) + b.set_exception(err.error_code()); + } + catch (z3_exception& ex) { + asms.pop_back(); + if (!m.limit().is_canceled() && !is_cancellation_exception(ex.what())) + b.set_exception(ex.what()); + } + + if (r == l_false) { + expr_ref_vector core(m); + s->get_unsat_core(core); + if (!core.contains(e)) { + b.set_unsat(m_l2g, core); + return l_false; + } + expr_ref bb(mk_not(m, e), m); + ++m_stats.m_backbones_detected; + if (b.collect_global_backbone(m_l2g, bb)) { + ++m_stats.m_internal_backbones_found; + if (is_retry) + ++m_stats.m_retry_backbones_found; + } + s->assert_expr(bb.get()); + return l_undef; + } + if (r == l_true) { + model_ref mdl; + s->get_model(mdl); + if (mdl) + b.set_sat(m_l2g, *mdl); + } + return r; + } + + void run_batch_mode() { + bb_candidates curr_batch; + + while (m.inc()) { + if (!b.wait_for_backbone_job(id, m_g2l, curr_batch, m.limit())) { + LOG_BB_WORKER(1, " BACKBONES WORKER cancelling\n"); + return; + } + + if (curr_batch.empty()) + continue; + + LOG_BB_WORKER(1, " received batch of " << curr_batch.size() << " candidates\n"); + collect_shared_clauses(); + + unsigned local_cancel_epoch = b.get_cancel_epoch(); + auto canceled = [&] { return local_cancel_epoch != b.get_cancel_epoch(); }; + unsigned bb_candidate_epoch = b.get_bb_candidate_epoch(); + + auto fallback_failed_literal_probe = + [&](expr_ref_vector const& chunk_lits, expr_ref_vector& bb_candidate_lits, bool is_retry = false) { + if (is_retry) + ++m_stats.m_bb_retries; + else + ++m_stats.m_fallback_singleton_checks; + + unsigned old_max_conflicts = s->get_max_conflicts(); + s->set_max_conflicts(10); + + for (expr* lit : chunk_lits) { + if (is_retry && b.has_new_backbone_candidates(bb_candidate_epoch)) { + s->set_max_conflicts(old_max_conflicts); + return; + } + if (!m.inc() || canceled()) { + s->set_max_conflicts(old_max_conflicts); + return; + } + if (!bb_candidate_lits.contains(lit)) + continue; + + expr_ref bb_ref(lit, m); + if (m_positive_mode) + bb_ref = mk_not(m, bb_ref); + + if (!b.is_global_backbone_or_negation(m_l2g, bb_ref.get())) { + expr_ref backbone(m); + if (try_get_unit_backbone(bb_ref.get(), backbone)) { + ++m_stats.m_backbones_detected; + if (b.collect_global_backbone(m_l2g, backbone)) { + ++m_stats.m_internal_backbones_found; + if (is_retry) + ++m_stats.m_retry_backbones_found; + } + LOG_BB_WORKER(1, " fallback found unit backbone: " << mk_bounded_pp(backbone.get(), m, 3) << "\n"); + } + else { + expr* atom = bb_ref.get(); + m.is_not(bb_ref.get(), atom); + if (s->get_bool_var(atom) != UINT_MAX) { + lbool terminal_result = probe_literal(mk_not(m, bb_ref), is_retry); + LOG_BB_WORKER(1, " RESULT: " << terminal_result << " FOR CANDIDATE: " << mk_bounded_pp(bb_ref.get(), m, 3) << "\n"); + if (terminal_result != l_undef) { + s->set_max_conflicts(old_max_conflicts); + return; + } + } + } + } + bb_candidate_lits.erase(lit); + } + + s->set_max_conflicts(old_max_conflicts); + }; + + ++m_stats.m_batches_total; + m_stats.m_candidates_total += curr_batch.size(); + + expr_ref_vector bb_candidate_lits(m); + for (auto const& c : curr_batch) + bb_candidate_lits.push_back(c.lit); + + unsigned chunk_delta = 1; + + while (!bb_candidate_lits.empty() && !canceled() && m.inc()) { + { + unsigned j = 0; + for (expr* lit : bb_candidate_lits) { + if (!b.is_global_backbone_or_negation(m_l2g, lit)) + bb_candidate_lits[j++] = lit; + } + bb_candidate_lits.shrink(j); + } + + { + unsigned j = 0; + for (expr* lit : bb_candidate_lits) { + expr_ref backbone(m); + if (try_get_unit_backbone(lit, backbone)) { + if (b.collect_global_backbone(m_l2g, backbone)) + ++m_stats.m_internal_backbones_found; + ++m_stats.m_backbones_detected; + continue; + } + bb_candidate_lits[j++] = lit; + } + bb_candidate_lits.shrink(j); + } + + unsigned chunk_size = std::min(m_bb_chunk_size * chunk_delta, bb_candidate_lits.size()); + expr_ref_vector chunk_lits(m); + expr_ref_vector negated_chunk_lits(m); + expr_mark chunk_atoms; + + for (unsigned i = 0; i < bb_candidate_lits.size() && chunk_lits.size() < chunk_size; ++i) { + expr* lit = bb_candidate_lits.get(i); + expr* atom = lit; + m.is_not(lit, atom); + if (chunk_atoms.is_marked(atom)) + continue; + chunk_atoms.mark(atom); + chunk_lits.push_back(lit); + negated_chunk_lits.push_back(mk_not(m, lit)); + } + + expr_ref_vector bb_asms(m); + if (!m_positive_mode) + bb_asms.append(negated_chunk_lits); + else + bb_asms.append(chunk_lits); + + collect_shared_clauses(); + + while (true) { + if (!m.inc()) + return; + if (canceled()) + break; + + ++m_stats.m_core_refinement_rounds; + unsigned base_asms_sz = asms.size(); + for (expr* a : bb_asms) + asms.push_back(a); + + s->set_max_conflicts(m_bb_conflicts_per_chunk); + lbool r = l_undef; + try { + r = s->check_sat(asms); + } + catch (z3_error& err) { + if (!m.limit().is_canceled()) + b.set_exception(err.error_code()); + } + catch (z3_exception& ex) { + if (!m.limit().is_canceled() && !is_cancellation_exception(ex.what())) + b.set_exception(ex.what()); + } + asms.shrink(base_asms_sz); + + if (!m.inc() || canceled()) + break; + + if (r == l_undef) { + LOG_BB_WORKER(1, " UNDEF at chunk_size=" << chunk_size << "\n"); + if (chunk_size < bb_candidate_lits.size()) { + ++chunk_delta; + ++m_stats.m_num_chunk_increases; + break; + } + + LOG_BB_WORKER(1, " UNDEF and max chunk -> fallback\n"); + fallback_failed_literal_probe(chunk_lits, bb_candidate_lits); + ++m_stats.m_fallback_reason_undef; + chunk_delta = 1; + break; + } + + if (r == l_true) { + LOG_BB_WORKER(1, " batch check returned SAT, thus entire formula is SAT\n"); + model_ref mdl; + s->get_model(mdl); + if (mdl) + b.set_sat(m_l2g, *mdl); + curr_batch.reset(); + return; + } + + expr_ref_vector bb_asms_in_core(m); + expr_ref_vector unsat_core(m); + s->get_unsat_core(unsat_core); + + for (expr* a : unsat_core) + if (bb_asms.contains(a)) + bb_asms_in_core.push_back(a); + + if (bb_asms_in_core.empty()) { + b.set_unsat(m_l2g, unsat_core); + return; + } + + if (bb_asms_in_core.size() == 1) { + expr* a = bb_asms_in_core.back(); + expr_ref backbone_lit(mk_not(m, a), m); + + ++m_stats.m_singleton_backbones; + ++m_stats.m_backbones_detected; + + if (b.collect_global_backbone(m_l2g, backbone_lit)) { + ++m_stats.m_internal_backbones_found; + s->assert_expr(backbone_lit.get()); + } + + expr* candidate_to_remove = + (!m_positive_mode) ? backbone_lit.get() : a; + bb_candidate_lits.erase(candidate_to_remove); + } + + unsigned sz_before = bb_asms.size(); + for (expr* a : bb_asms_in_core) + bb_asms.erase(a); + m_stats.m_lits_removed_by_core += sz_before - bb_asms.size(); + chunk_delta = 1; + + if (bb_asms.empty()) { + LOG_BB_WORKER(1, " no more negated chunk literals, fallback to individual checks\n"); + fallback_failed_literal_probe(chunk_lits, bb_candidate_lits); + ++m_stats.m_fallback_reason_chunk_exhausted; + break; + } + } + } + + while (!b.has_new_backbone_candidates(bb_candidate_epoch) && !canceled() && m.inc()) { + collect_shared_clauses(); + unsigned found_before = m_stats.m_internal_backbones_found; + + expr_ref_vector bb_snapshot = b.get_global_backbones_snapshot(m_g2l); + expr_mark bb_mark; + for (expr* e : bb_snapshot) { + bb_mark.mark(e); + bb_mark.mark(mk_not(m, e)); + } + bb_candidate_lits.reset(); + for (auto const& c : curr_batch) + if (!bb_mark.is_marked(c.lit.get())) + bb_candidate_lits.push_back(c.lit); + + if (bb_candidate_lits.empty()) + break; + + fallback_failed_literal_probe(bb_candidate_lits, bb_candidate_lits, true); + + if (m_stats.m_internal_backbones_found == found_before) + break; + } + + if (!canceled()) + b.cancel_current_backbone_batch(); + + curr_batch.reset(); + } + } + + public: + backbones_worker(unsigned id, parallel_solver& p, solver& src, params_ref const& params, + expr_ref_vector const& src_asms) + : id(id), b(p.m_batch_manager), + asms(m), m_g2l(src.get_manager(), m), m_l2g(m, src.get_manager()) { + s = src.translate(m, params); + s->set_max_conflicts(m_bb_conflicts_per_chunk); + s->pop_to_base_level(); + for (expr* a : src_asms) + asms.push_back(m_g2l(a)); + m_positive_mode = id != 0; + m_shared_units_prefix = s->get_assigned_literals().size(); + m_num_initial_atoms = s->get_num_bool_vars(); + IF_VERBOSE(1, verbose_stream() << "Initialized backbones thread " << id << "\n"); + } + + void run() { run_batch_mode(); } + + void cancel() { + LOG_BB_WORKER(1, " BACKBONES WORKER cancelling\n"); + m.limit().cancel(); + } + + void collect_statistics(statistics& st) const { + st.update("bb-batches-total", m_stats.m_batches_total); + st.update("bb-candidates-total", m_stats.m_candidates_total); + st.update("bb-backbones-detected", m_stats.m_backbones_detected); + st.update("bb-internal-backbones-found", m_stats.m_internal_backbones_found); + st.update("bb-retry-backbones-found", m_stats.m_retry_backbones_found); + st.update("bb-retries", m_stats.m_bb_retries); + st.update("bb-core-refinement-rounds", m_stats.m_core_refinement_rounds); + st.update("bb-singleton-backbones", m_stats.m_singleton_backbones); + st.update("bb-fallback-singleton-checks", m_stats.m_fallback_singleton_checks); + st.update("bb-fallback-chunk-exhausted", m_stats.m_fallback_reason_chunk_exhausted); + st.update("bb-fallback-undef", m_stats.m_fallback_reason_undef); + st.update("bb-literals-removed-by-core", m_stats.m_lits_removed_by_core); + st.update("bb-num-chunk-increases", m_stats.m_num_chunk_increases); + + auto safe_ratio = [](double num, double den) -> double { + return den > 0 ? num / den : 0.0; + }; + + st.update("bb-backbone-yield-pct", + 100.0 * safe_ratio(m_stats.m_internal_backbones_found, m_stats.m_candidates_total)); + st.update("bb-avg-backbones-per-batch", + safe_ratio(m_stats.m_internal_backbones_found, m_stats.m_batches_total)); + st.update("bb-core-refinement-rounds-per-batch", + safe_ratio(m_stats.m_core_refinement_rounds, m_stats.m_batches_total)); + st.update("bb-core-effectiveness-lit-removed-per-round", + safe_ratio(m_stats.m_lits_removed_by_core, m_stats.m_core_refinement_rounds)); + } + + reslimit& limit() { return m.limit(); } + }; + + class core_minimizer_worker { + batch_manager& b; + ast_manager m; + ref s; + expr_ref_vector asms; + ast_translation m_g2l, m_l2g; + unsigned m_num_core_minimize_calls = 0; + unsigned m_num_core_minimize_undef = 0; + unsigned m_num_core_minimize_refined = 0; + unsigned m_num_core_minimize_lits_removed = 0; + unsigned m_num_core_minimize_found_sat = 0; + unsigned m_core_minimize_conflict_budget = 5000; + unsigned m_shared_clause_limit = 0; + + void collect_shared_clauses() { + expr_ref_vector nc = b.return_shared_clauses(m_g2l, m_shared_clause_limit, UINT_MAX); + for (expr* e : nc) { + s->assert_expr(e); + IF_VERBOSE(4, verbose_stream() << "Core minimizer asserting shared clause: " + << mk_bounded_pp(e, m, 3) << "\n";); + } + } + + void minimize_unsat_core(expr_ref_vector& core) { + expr_ref_vector unknown(core), mus(m), trial(m); + unsigned original_size = core.size(); + ++m_num_core_minimize_calls; + + while (!unknown.empty()) { + if (!m.inc()) { + core.reset(); + core.append(mus); + core.append(unknown); + return; + } + + expr* lit = unknown.back(); + unknown.pop_back(); + expr_ref not_lit(mk_not(m, lit), m); + + trial.reset(); + trial.append(mus); + trial.append(unknown); + trial.push_back(not_lit); + + lbool r = l_undef; + try { + s->set_max_conflicts(m_core_minimize_conflict_budget); + r = s->check_sat(trial); + } + catch (z3_error&) { + r = l_undef; + } + catch (z3_exception&) { + r = l_undef; + } + + switch (r) { + case l_undef: + ++m_num_core_minimize_undef; + mus.push_back(lit); + break; + case l_true: { + if (!asms.empty()) { + mus.push_back(lit); + break; + } + ++m_num_core_minimize_found_sat; + model_ref mdl; + s->get_model(mdl); + if (mdl) + b.set_sat(m_l2g, *mdl); + return; + } + case l_false: { + expr_ref_vector unsat_core(m); + s->get_unsat_core(unsat_core); + if (!unsat_core.contains(not_lit)) { + ++m_num_core_minimize_refined; + unknown.reset(); + expr_ref_vector new_mus(m); + for (expr* c : unsat_core) { + if (mus.contains(c)) + new_mus.push_back(c); + else + unknown.push_back(c); + } + mus.reset(); + mus.append(new_mus); + } + break; + } + default: + UNREACHABLE(); + } + } + + core.reset(); + core.append(mus); + core.append(unknown); + if (core.size() < original_size) + m_num_core_minimize_lits_removed += original_size - core.size(); + } + + public: + core_minimizer_worker(parallel_solver& p, solver& src, params_ref const& params, + expr_ref_vector const& src_asms) + : b(p.m_batch_manager), + asms(m), m_g2l(src.get_manager(), m), m_l2g(m, src.get_manager()) { + s = src.translate(m, params); + s->pop_to_base_level(); + // avoid preprocessing lemmas that are exchanged + s->set_preprocess(false); + for (expr* a : src_asms) + asms.push_back(m_g2l(a)); + IF_VERBOSE(1, verbose_stream() << "Initialized core minimizer thread\n"); + } + + void run() { + while (m.inc()) { + search_tree::node* source = nullptr; + expr_ref_vector core(m); + if (!b.wait_for_core_min_job(m_g2l, source, core, m.limit())) + return; + + unsigned original_size = core.size(); + if (original_size <= 1) + continue; + + collect_shared_clauses(); + + expr_ref_vector minimized(m); + minimized.append(core); + + if (minimized.size() <= 1) + continue; + + minimize_unsat_core(minimized); + + if (minimized.size() < original_size) + b.publish_minimized_core(m_l2g, asms, source, original_size, minimized); + } + } + + void cancel() { + IF_VERBOSE(1, verbose_stream() << "Core minimizer cancelling\n"); + m.limit().cancel(); + } + + void collect_statistics(statistics& st) const { + st.update("parallel-core-minimize-calls", m_num_core_minimize_calls); + st.update("parallel-core-minimize-undef", m_num_core_minimize_undef); + st.update("parallel-core-minimize-refined", m_num_core_minimize_refined); + st.update("parallel-core-minimize-lits-removed", m_num_core_minimize_lits_removed); + st.update("parallel-core-minimize-found-sat", m_num_core_minimize_found_sat); + } + + reslimit& limit() { return m.limit(); } + }; /* ---- members ---- */ ref m_solver; ast_manager& m_manager; params_ref m_params; scoped_ptr_vector m_workers; + scoped_ptr m_core_minimizer_worker; + scoped_ptr_vector m_global_backbones_workers; batch_manager m_batch_manager; statistics m_stats; - public: parallel_solver(solver* s, params_ref const& p) @@ -718,6 +1810,16 @@ public: m_params(p), m_batch_manager(s->get_manager(), *this) {} + params_ref mk_worker_params(unsigned seed_offset) const { + params_ref p(m_params); + // Match smt_parallel's per-worker m_smt_params.m_random_seed += id. + // Generic solver workers receive the seed through translate params. + unsigned base_seed = m_params.get_uint("random_seed", 0); + p.set_uint("random_seed", base_seed + seed_offset); + p.set_uint("threads", 1); + return p; + } + /* Run the portfolio. Returns sat/unsat/undef. * * On sat: *mdl is populated (translated into m_manager). @@ -731,10 +1833,13 @@ public: unsigned num_threads = std::min( static_cast(std::thread::hardware_concurrency()), pp.threads_max()); - if (num_threads < 2) num_threads = 2; + bool core_minimize = pp.core_minimize(); + unsigned num_bb_threads = pp.num_bb_threads(); + if (num_bb_threads > 2) + throw default_exception("parallel.num_bb_threads must be 0, 1, or 2"); + unsigned total_threads = num_threads + (core_minimize ? 1 : 0) + num_bb_threads; - IF_VERBOSE(1, verbose_stream() << "par2: launching " << num_threads - << " threads\n"); + IF_VERBOSE(1, verbose_stream() << "Parallel tactical2 with " << total_threads << " threads\n";); if (m_manager.has_trace_stream()) throw default_exception( @@ -743,29 +1848,73 @@ public: /* Build workers – each gets a translated solver copy. */ m_workers.reset(); scoped_limits sl(m_manager.limit()); - params_ref worker_params(m_params); - worker_params.set_bool("override_incremental", true); + + // Set up the source before translating workers. SMT context copies + // then run initial internalization/preprocessing before workers disable + // preprocessing for exchanged lemmas. + m_solver->setup_for_parallel(); for (unsigned i = 0; i < num_threads; ++i) { + params_ref worker_params = mk_worker_params(i); auto* w = alloc(worker, i, *this, *m_solver, worker_params, asms); m_workers.push_back(w); sl.push_child(&(w->limit())); } - m_batch_manager.initialize(num_threads); + m_core_minimizer_worker = nullptr; + if (core_minimize) { + params_ref core_min_params = mk_worker_params(num_threads); + m_core_minimizer_worker = alloc(core_minimizer_worker, *this, *m_solver, core_min_params, asms); + sl.push_child(&(m_core_minimizer_worker->limit())); + } + m_global_backbones_workers.reset(); + for (unsigned i = 0; i < num_bb_threads; ++i) { + params_ref bb_params = mk_worker_params(num_threads + (core_minimize ? 1 : 0) + i); + auto* w = alloc(backbones_worker, i, *this, *m_solver, bb_params, asms); + m_global_backbones_workers.push_back(w); + sl.push_child(&(w->limit())); + } + IF_VERBOSE(1, verbose_stream() << "Launched " << m_workers.size() << " CDCL threads, " + << 0 << " SLS threads, " + << (m_core_minimizer_worker ? 1 : 0) << " core minimizer threads, " + << m_global_backbones_workers.size() << " global backbone threads.\n";); + + m_batch_manager.initialize(num_bb_threads); /* Launch threads. */ vector threads; for (auto* w : m_workers) threads.push_back(std::thread([w]() { w->run(); })); + if (m_core_minimizer_worker) + threads.push_back(std::thread([this]() { m_core_minimizer_worker->run(); })); + for (auto* w : m_global_backbones_workers) + threads.push_back(std::thread([w]() { w->run(); })); for (auto& t : threads) t.join(); - /* Collect per-worker statistics. */ - for (auto* w : m_workers) - w->collect_statistics(m_stats); - m_batch_manager.collect_statistics(m_stats); + m_solver->reset_parallel_statistics(); + statistics aux; + for (auto* w : m_workers) { + aux.reset(); + w->collect_statistics(aux); + m_solver->add_parallel_statistics(aux); + } + aux.reset(); + m_batch_manager.collect_statistics(aux); + m_solver->add_parallel_statistics(aux); + if (m_core_minimizer_worker) { + aux.reset(); + m_core_minimizer_worker->collect_statistics(aux); + m_solver->add_parallel_statistics(aux); + } + for (auto* w : m_global_backbones_workers) { + aux.reset(); + w->collect_statistics(aux); + m_solver->add_parallel_statistics(aux); + } + m_stats.reset(); + m_solver->collect_parallel_statistics(m_stats); m_manager.limit().reset_cancel(); @@ -779,7 +1928,10 @@ public: core.push_back(c); } + sl.reset(); m_workers.reset(); + m_core_minimizer_worker = nullptr; + m_global_backbones_workers.reset(); return result; } @@ -790,7 +1942,7 @@ public: void reset_statistics() { m_stats.reset(); } -}; // class parallel_solver +}; /* ------------------------------------------------------------------ */ /* parallel_tactic2 – wraps parallel_solver as a tactic */ @@ -824,8 +1976,7 @@ public: ptr_vector assumptions_raw; obj_map bool2dep; ref fmc; - extract_clauses_and_dependencies(g, clauses, assumptions_raw, - bool2dep, fmc); + extract_clauses_and_dependencies(g, clauses, assumptions_raw, bool2dep, fmc); for (expr* cl : clauses) s->assert_expr(cl); @@ -841,15 +1992,16 @@ public: ps.collect_statistics(m_stats); switch (is_sat) { - case l_true: - g->reset(); + case l_true: { if (g->models_enabled() && mdl) { - if (fmc) - g->add(concat(fmc.get(), model2model_converter(mdl.get()))); - else - g->add(model2model_converter(mdl.get())); + model_converter_ref mc = model2model_converter(mdl.get()); + mc = concat(fmc.get(), mc.get()); + mc = concat(s->mc0(), mc.get()); + g->add(mc.get()); } + g->reset(); break; + } case l_false: { SASSERT(!g->proofs_enabled()); @@ -875,9 +2027,7 @@ public: result.push_back(g.get()); } - void cleanup() override { - m_stats.reset(); - } + void cleanup() override {} tactic* translate(ast_manager& m) override { solver* s = m_solver->translate(m, m_params); @@ -895,10 +2045,10 @@ public: void reset_statistics() override { m_stats.reset(); } -}; // class parallel_tactic2 +}; tactic* mk_parallel_tactic2(solver* s, params_ref const& p) { return alloc(parallel_tactic2, s, p); } -#endif /* !SINGLE_THREAD */ +#endif diff --git a/src/solver/solver.h b/src/solver/solver.h index b45f4f347..d4118c4c2 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -57,7 +57,15 @@ solver* mk_smt2_solver(ast_manager& m, params_ref const& p, symbol const& logic class solver : public check_sat_result, public user_propagator::core { params_ref m_params; symbol m_cancel_backup_file; + statistics m_parallel_stats; public: + struct scored_literal { + expr_ref lit; + double score = 0.0; + scored_literal(ast_manager& m, expr* e, double s): lit(e, m), score(s) {} + scored_literal(expr_ref const& e, double s): lit(e), score(s) {} + }; + solver(ast_manager& m): check_sat_result(m) {} /** @@ -298,9 +306,47 @@ public: expr_ref_vector get_non_units(); virtual expr_ref_vector get_trail(unsigned max_level) = 0; // { return expr_ref_vector(get_manager()); } + virtual expr_ref_vector get_assigned_literals() { return get_trail(UINT_MAX); } + virtual unsigned get_assign_level(expr* e) const { return UINT_MAX; } + virtual bool is_relevant(expr* e) const { return true; } + virtual unsigned get_num_bool_vars() const { return UINT_MAX; } + virtual unsigned get_bool_var(expr* e) const { return UINT_MAX; } + virtual expr* bool_var2expr(unsigned) const { return nullptr; } + virtual lbool get_assignment(unsigned) const { return l_undef; } + virtual double get_activity(unsigned) const { return 0.0; } + virtual bool was_eliminated(unsigned) const { return false; } + + virtual void pop_to_base_level() {} + + virtual void setup_for_parallel() {} + + virtual void set_preprocess(bool) {} + + virtual void set_max_conflicts(unsigned max_conflicts) { + params_ref p; + p.set_uint("max_conflicts", max_conflicts); + updt_params(p); + } + + virtual unsigned get_max_conflicts() const { return UINT_MAX; } + + virtual void reset_parallel_statistics() { + m_parallel_stats.reset(); + } + + virtual void add_parallel_statistics(statistics const& st) { + m_parallel_stats.copy(st); + } + + virtual void collect_parallel_statistics(statistics& st) const { + st.copy(m_parallel_stats); + collect_statistics(st); + } virtual void get_levels(ptr_vector const& vars, unsigned_vector& depth) = 0; + virtual void get_backbone_candidates(vector&, unsigned) {} + class scoped_push { solver& s; bool m_nopop; diff --git a/src/solver/solver_pool.cpp b/src/solver/solver_pool.cpp index 3cf97ce3b..1463eecf8 100644 --- a/src/solver/solver_pool.cpp +++ b/src/solver/solver_pool.cpp @@ -127,6 +127,10 @@ public: m_base->get_levels(vars, depth); } + void get_backbone_candidates(vector& candidates, unsigned max_num) override { + m_base->get_backbone_candidates(candidates, max_num); + } + expr_ref_vector get_trail(unsigned max_level) override { return m_base->get_trail(max_level); } diff --git a/src/util/search_tree.h b/src/util/search_tree.h index 85294d550..701c2fe8d 100644 --- a/src/util/search_tree.h +++ b/src/util/search_tree.h @@ -68,9 +68,17 @@ namespace search_tree { literal const &get_literal() const { return m_literal; } + bool path_contains_atom(literal const& l) const { + for (node const* n = this; n; n = n->parent()) + if (!Config::literal_is_null(n->get_literal()) && Config::same_atom(n->get_literal(), l)) + return true; + return false; + } void split(literal const &a, literal const &b) { SASSERT(!Config::literal_is_null(a)); SASSERT(!Config::literal_is_null(b)); + VERIFY(!path_contains_atom(a)); + VERIFY(!path_contains_atom(b)); if (m_status != status::active) return; SASSERT(!m_left);