From 868b5eeaa750cf48f13c1e1c053bcc46afa7f300 Mon Sep 17 00:00:00 2001 From: Ilana Shapiro Date: Sat, 20 Jun 2026 22:06:00 -0700 Subject: [PATCH] some bugfixes: Avoid updating max_conflicts through params in the parallel tactic path. Expose direct conflict-limit setters on solver wrappers and use them for SMT and incremental SAT solvers. Also restore single-candidate non-lookahead cube selection to match the parallel split heuristic, specifically do the filtering for invalid atoms during split atom selection. this requires new params so we have a separate get_split_atoms function for now. --- src/sat/sat_solver.h | 2 + src/sat/sat_solver/inc_sat_solver.cpp | 41 +++++++-------- src/smt/smt_solver.cpp | 52 +++++++++---------- src/solver/parallel_tactical2.cpp | 74 ++++++++++++++++----------- src/solver/solver.h | 8 +++ 5 files changed, 102 insertions(+), 75 deletions(-) diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 622e551bb..c7ddd22f0 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -449,6 +449,8 @@ namespace sat { void set_par(parallel* p, unsigned id); bool canceled() { return !m_rlimit.inc(); } config const& get_config() const { return m_config; } + void set_max_conflicts(unsigned n) { m_config.m_max_conflicts = n; } + unsigned get_max_conflicts() const { return m_config.m_max_conflicts; } void set_drat(bool d) { m_config.m_drat = d; } drat& get_drat() { return m_drat; } drat* get_drat_ptr() { return &m_drat; } diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 08e17039f..95664a4fe 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -391,6 +391,15 @@ public: if (m_preprocess) m_preprocess->collect_statistics(st); m_solver.collect_statistics(st); } + + void set_max_conflicts(unsigned max_conflicts) override { + m_solver.set_max_conflicts(max_conflicts); + } + + unsigned get_max_conflicts() const override { + return m_solver.get_max_conflicts(); + } + void get_unsat_core(expr_ref_vector & r) override { r.reset(); r.append(m_core.size(), m_core.data()); @@ -495,6 +504,9 @@ public: parallel_params pp(m_params); if (!pp.cube_lookahead()) { sat::bool_var_vector candidates; + sat::bool_var result = sat::null_bool_var; + double score = 0.0; + unsigned n = 0; unsigned search_lvl = m_solver.search_lvl(); for (sat::bool_var v : vars) { if (was_eliminated(v)) @@ -502,32 +514,21 @@ public: if (get_assignment(v) != l_undef && m_solver.lvl(v) <= search_lvl) continue; candidates.push_back(v); + double new_score = get_activity(v); + if (new_score > score || result == sat::null_bool_var || (new_score == score && m_solver.rand()(++n) == 0)) { + score = new_score; + result = v; + } } - std::sort(candidates.begin(), candidates.end(), [&](sat::bool_var a, sat::bool_var b) { - return get_activity(a) > get_activity(b); - }); - // shuffle sub-sequences with equal activity - unsigned i = 0; - while (i < candidates.size()) { - unsigned j = i + 1; - double act = get_activity(candidates[i]); - while (j < candidates.size() && get_activity(candidates[j]) == act) - ++j; - if (j - i > 1) - shuffle(j - i, candidates.data() + i, m_solver.rand()); - i = j; - } - if (candidates.empty()) - return expr_ref_vector(m); vs.reset(); for (sat::bool_var v : candidates) { expr* e = bool_var2expr(v); - if (e) { - if (fmls.size() < backtrack_level) - fmls.push_back(e); + if (e) vs.push_back(e); - } } + expr* e = result == sat::null_bool_var ? nullptr : bool_var2expr(result); + if (e) + fmls.push_back(e); return fmls; } lbool result = m_solver.cube(vars, lits, backtrack_level); diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 3ebbbfb81..fb9edfdcb 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -268,6 +268,15 @@ namespace { m_context.set_preprocess(f); } + void set_max_conflicts(unsigned max_conflicts) override { + auto& ctx = m_context.get_context(); + ctx.get_fparams().m_max_conflicts = max_conflicts; + } + + unsigned get_max_conflicts() const override { + return m_context.get_context().get_fparams().m_max_conflicts; + } + void get_backbone_candidates(vector& candidates, unsigned max_num) override { ast_manager& m = get_manager(); auto& ctx = m_context.get_context(); @@ -440,14 +449,13 @@ namespace { parallel_params pp(get_params()); if (!pp.cube_lookahead()) { auto& ctx = m_context.get_context(); - expr_mark selected_vars; + obj_hashtable selected_vars; for (expr* v : vars) - selected_vars.mark(v); - struct candidate { - expr* e; - double score; - }; - vector candidates; + 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) { @@ -456,30 +464,22 @@ namespace { expr* e = ctx.bool_var2expr(v); if (!e) continue; - if (!vars.empty() && !selected_vars.is_marked(e)) + if (!selected_vars.empty() && !selected_vars.contains(e)) continue; - candidates.push_back({ e, ctx.get_activity(v) }); - } - - std::stable_sort(candidates.begin(), candidates.end(), - [](candidate const& a, candidate const& b) { - return a.score > b.score; - }); - for (unsigned i = 0, j = 0; i < candidates.size(); i = j) { - j = i + 1; - while (j < candidates.size() && candidates[i].score == candidates[j].score) - ++j; - if (j > i + 1) - shuffle(j - i, candidates.data() + i, m_rand); + candidates.push_back(e); + double new_score = ctx.get_activity(v); + if (new_score > score || !result || (new_score == score && m_rand(++n) == 0)) { + score = new_score; + result = e; + } } vars.reset(); - expr_ref_vector lits(m); - for (auto const &c : candidates) { - vars.push_back(c.e); - lits.push_back(c.e); - } + vars.append(candidates); + expr_ref_vector lits(m); + if (result) + lits.push_back(result); return lits; } diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp index eeb79c83d..4e96594cf 100644 --- a/src/solver/parallel_tactical2.cpp +++ b/src/solver/parallel_tactical2.cpp @@ -106,12 +106,6 @@ static bool is_cancellation_exception(char const* msg) { return msg && (strstr(msg, "canceled") != nullptr || strstr(msg, "cancelled") != nullptr); } -static void set_max_conflicts(solver_ref& s, unsigned max_conflicts) { - params_ref p(s->get_params()); - p.set_uint("max_conflicts", max_conflicts); - s->updt_params(p); -} - /* ------------------------------------------------------------------ */ /* parallel_solver – the core portfolio engine */ /* ------------------------------------------------------------------ */ @@ -1026,7 +1020,7 @@ class parallel_solver { } lbool check_cube(expr_ref_vector const& cube) { - set_max_conflicts(s, std::min(m_config.m_threads_max_conflicts, m_config.m_max_conflicts)); + 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); @@ -1112,20 +1106,42 @@ class parallel_solver { if (cube.size() >= m_config.m_max_cube_depth) return result; - expr_ref_vector placeholder_noop(m); + expr_ref_vector vars(m); + obj_hashtable rejected_atoms; try { - expr_ref_vector cands = s->cube(placeholder_noop); - for (expr* lit : cands) { - if (!lit) - continue; - if (m.is_true(lit) || m.is_false(lit)) - continue; - if (b.path_contains_atom(m_l2g, lease, lit)) - continue; - if (m_config.m_global_backbones && b.is_global_backbone_or_negation(m_l2g, lit)) - continue; - result = lit; - return result; + 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; + } + result = lit; + return result; + } + + if (!rejected || vars.empty()) + return result; + + 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 result; + vars.reset(); + vars.append(next_vars); } } catch (...) { @@ -1428,16 +1444,16 @@ class parallel_solver { else ++m_stats.m_fallback_singleton_checks; - unsigned old_max_conflicts = s->get_params().get_uint("max_conflicts", UINT_MAX); - set_max_conflicts(s, 10); + 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)) { - set_max_conflicts(s, old_max_conflicts); + s->set_max_conflicts(old_max_conflicts); return; } if (!m.inc() || canceled()) { - set_max_conflicts(s, old_max_conflicts); + s->set_max_conflicts(old_max_conflicts); return; } if (!bb_candidate_lits.contains(lit)) @@ -1465,7 +1481,7 @@ class parallel_solver { 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) { - set_max_conflicts(s,old_max_conflicts); + s->set_max_conflicts(old_max_conflicts); return; } } @@ -1474,7 +1490,7 @@ class parallel_solver { bb_candidate_lits.erase(lit); } - set_max_conflicts(s, old_max_conflicts); + s->set_max_conflicts(old_max_conflicts); }; ++m_stats.m_batches_total; @@ -1548,7 +1564,7 @@ class parallel_solver { for (expr* a : bb_asms) asms.push_back(a); - set_max_conflicts(s,m_bb_conflicts_per_chunk); + s->set_max_conflicts(m_bb_conflicts_per_chunk); lbool r = l_undef; try { r = s->check_sat(asms); @@ -1673,7 +1689,7 @@ class parallel_solver { : 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); - set_max_conflicts(s, m_bb_conflicts_per_chunk); + 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)); @@ -1769,7 +1785,7 @@ class parallel_solver { lbool r = l_undef; try { - set_max_conflicts(s, m_core_minimize_conflict_budget); + s->set_max_conflicts(m_core_minimize_conflict_budget); r = s->check_sat(trial); } catch (z3_error&) { diff --git a/src/solver/solver.h b/src/solver/solver.h index 733b95d2a..df0d11711 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -321,6 +321,14 @@ public: 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 get_levels(ptr_vector const& vars, unsigned_vector& depth) = 0;