From 20b9690b0189717f6ad971feb4d989294a861045 Mon Sep 17 00:00:00 2001 From: Ilana Shapiro Date: Wed, 23 Jul 2025 15:26:02 -0700 Subject: [PATCH 1/2] very basic setup (#7741) --- src/smt/smt_lookahead.h | 4 ++- src/smt/smt_parallel.cpp | 61 ++++++++++++++++++++++++++++++++++++---- 2 files changed, 58 insertions(+), 7 deletions(-) diff --git a/src/smt/smt_lookahead.h b/src/smt/smt_lookahead.h index 5deccad2c..d53af58e4 100644 --- a/src/smt/smt_lookahead.h +++ b/src/smt/smt_lookahead.h @@ -30,11 +30,13 @@ namespace smt { struct compare; - double get_score(); + // double get_score(); void choose_rec(expr_ref_vector& trail, expr_ref_vector& result, unsigned depth, unsigned budget); public: + double get_score(); + lookahead(context& ctx); expr_ref choose(unsigned budget = 2000); diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index c8958c61c..ac5a81979 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -92,16 +92,64 @@ namespace smt { sl.push_child(&(new_m->limit())); } - auto cube = [](context& ctx, expr_ref_vector& lasms, expr_ref& c) { - lookahead lh(ctx); - c = lh.choose(); - if (c) { + // auto cube = [](context& ctx, expr_ref_vector& lasms, expr_ref& c) { + // lookahead lh(ctx); + // c = lh.choose(); + // if (c) { + // if ((ctx.get_random_value() % 2) == 0) + // c = c.get_manager().mk_not(c); + // lasms.push_back(c); + // } + // }; + + auto cube = [&](context& ctx, expr_ref_vector& lasms, expr_ref& c) { + lookahead lh(ctx); // Create lookahead object to use get_score for evaluation + + std::vector> candidates; // List of candidate literals and their scores + unsigned budget = 10; // Maximum number of variables to sample for building the cubes + + // Loop through all Boolean variables in the context + for (bool_var v = 0; v < ctx.m_bool_var2expr.size(); ++v) { + if (ctx.get_assignment(v) != l_undef) continue; // Skip already assigned variables + + expr* e = ctx.bool_var2expr(v); // Get expression associated with variable + if (!e) continue; // Skip if not a valid variable + + literal lit(v, false); // Create literal for v = true + + ctx.push_scope(); // Save solver state + ctx.assign(lit, b_justification::mk_axiom(), true); // Assign v = true with axiom justification + ctx.propagate(); // Propagate consequences of assignment + + if (!ctx.inconsistent()) { // Only keep variable if assignment didn’t lead to conflict + double score = lh.get_score(); // Evaluate current state using lookahead scoring + candidates.emplace_back(expr_ref(e, ctx.get_manager()), score); // Store (expr, score) pair + } + + ctx.pop_scope(1); // Restore solver state + + if (candidates.size() >= budget) break; // Stop early if sample budget is exhausted + } + + // Sort candidates in descending order by score (higher score = better) + std::sort(candidates.begin(), candidates.end(), + [](auto& a, auto& b) { return a.second > b.second; }); + + unsigned cube_size = 2; // compute_cube_size_from_feedback(); // NEED TO IMPLEMENT: Decide how many literals to include (adaptive) + + // Select top-scoring literals to form the cube + for (unsigned i = 0; i < std::min(cube_size, (unsigned)candidates.size()); ++i) { + expr_ref lit = candidates[i].first; + + // Randomly flip polarity with 50% chance (introduces polarity diversity) if ((ctx.get_random_value() % 2) == 0) - c = c.get_manager().mk_not(c); - lasms.push_back(c); + lit = ctx.get_manager().mk_not(lit); + + lasms.push_back(lit); // Add literal as thread-local assumption } }; + obj_hashtable unit_set; expr_ref_vector unit_trail(ctx.m); unsigned_vector unit_lim; @@ -217,6 +265,7 @@ namespace smt { while (true) { vector threads(num_threads); for (unsigned i = 0; i < num_threads; ++i) { + // [&, i] is the lambda's capture clause: capture all variables by reference (&) except i, which is captured by value. threads[i] = std::thread([&, i]() { worker_thread(i); }); } for (auto & th : threads) { From ac857aaf727da71274d744862969502ed151a783 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 23 Jul 2025 15:32:49 -0700 Subject: [PATCH 2/2] add score access and reset Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.h | 8 ++++++++ src/smt/smt_internalizer.cpp | 11 +++++++++++ 2 files changed, 19 insertions(+) diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 3dbadc1cb..da6e92569 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -189,6 +189,7 @@ namespace smt { unsigned_vector m_lit_occs; //!< occurrence count of literals svector m_bdata; //!< mapping bool_var -> data svector m_activity; + svector m_scores; clause_vector m_aux_clauses; clause_vector m_lemmas; vector m_clauses_to_reinit; @@ -929,6 +930,13 @@ namespace smt { ast_pp_util m_lemma_visitor; void dump_lemma(unsigned n, literal const* lits); void dump_axiom(unsigned n, literal const* lits); + void add_scores(unsigned n, literal const* lits); + void reset_scores() { + for (auto& s : m_scores) s[0] = s[1] = 0.0; + } + double get_score(literal l) const { + return m_scores[l.var()][l.sign()]; + } public: void ensure_internalized(expr* e); diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index c15505ab0..faf7ea24d 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -928,6 +928,8 @@ namespace smt { set_bool_var(id, v); m_bdata.reserve(v+1); m_activity.reserve(v+1); + m_scores.reserve(v + 1); + m_scores[v][0] = m_scores[v][1] = 0.0; m_bool_var2expr.reserve(v+1); m_bool_var2expr[v] = n; literal l(v, false); @@ -1416,6 +1418,7 @@ namespace smt { break; case CLS_LEARNED: dump_lemma(num_lits, lits); + add_scores(num_lits, lits); break; default: break; @@ -1524,6 +1527,14 @@ namespace smt { }} } + void context::add_scores(unsigned n, literal const* lits) { + for (unsigned i = 0; i < n; ++i) { + auto lit = lits[i]; + unsigned v = lit.var(); + m_scores[v][lit.sign()] += 1.0 / n; + } + } + void context::dump_axiom(unsigned n, literal const* lits) { if (m_fparams.m_axioms2files) { literal_buffer tmp;