From 1397dd12ffdbc848adedf28afd271146fa501bc3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 Aug 2025 15:42:16 -0700 Subject: [PATCH 01/12] change default Signed-off-by: Nikolaj Bjorner --- src/params/smt_parallel_params.pyg | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/params/smt_parallel_params.pyg b/src/params/smt_parallel_params.pyg index faaef6e82..91f7bce91 100644 --- a/src/params/smt_parallel_params.pyg +++ b/src/params/smt_parallel_params.pyg @@ -6,5 +6,5 @@ def_module_params('smt_parallel', ('share_conflicts', BOOL, True, 'share conflicts'), ('never_cube', BOOL, False, 'never cube'), ('frugal_cube_only', BOOL, False, 'only apply frugal cube strategy'), - ('relevant_units_only', BOOL, False, 'only share relvant units') + ('relevant_units_only', BOOL, True, 'only share relvant units') )) From df3d10a16f62ce8ffc6d793ddc64ee42934a3a0a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 16 Aug 2025 02:52:15 -0700 Subject: [PATCH 02/12] ensure memory safety Signed-off-by: Nikolaj Bjorner --- src/smt/smt_parallel.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 21e46a071..58d8a1c65 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -364,7 +364,9 @@ namespace smt { auto add_split_atom = [&](expr* atom, unsigned start) { unsigned stop = m_cubes.size(); for (unsigned i = start; i < stop; ++i) { - m_cubes.push_back(m_cubes[i]); + // copy the last cube so that expanding m_cubes doesn't invalidate reference. + auto cube = m_cubes[i]; + m_cubes.push_back(cube); m_cubes.back().push_back(m.mk_not(atom)); m_cubes[i].push_back(atom); } From 9bd7cd8577cf4374dd9f18f30b33ff10cd6693ac Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 16 Aug 2025 17:32:38 -0700 Subject: [PATCH 03/12] update readme file with notes about benchmarking Signed-off-by: Nikolaj Bjorner --- PARALLEL_PROJECT_NOTES.md | 48 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 48 insertions(+) diff --git a/PARALLEL_PROJECT_NOTES.md b/PARALLEL_PROJECT_NOTES.md index b60263e4e..bff187927 100644 --- a/PARALLEL_PROJECT_NOTES.md +++ b/PARALLEL_PROJECT_NOTES.md @@ -215,4 +215,52 @@ SMT parameters that could be tuned: seq.split_w_len (bool) (default: true) +# Benchmark setup + +## Prepare benchmark data + +Data +
+QF_LIA            - heavily skewed for selected benchmarks
+QF_NIA_small  
+
+Others we should try:
+
+Certora
+QF_ABV
+QF_UFBV
+QF_AUFBV (or whatever it is called)
+QF_UFLIA (might be too small)
+
+push more instances from smtlib.org benchmarks into z3-poly-testing/inputs or upload tgz files directly in setup.
+
+
+ +## Naming conventions and basic parameters + +The first rounds created a base-line where all features were turned off, then it created variants where one feature was turned off at a time. +The data-point where all but one feature is turned off could tell us something if a feature has a chance of being useful in isolation. +The following is a sample naming scheme. + +
+threads-1
+smt.threads=1 tactic.default_tactic=smt -T:30
+
+threads-4-none-unbounded
+smt.threads=4 tactic.default_tactic=smt smt_parallel.never_cube=true smt_parallel.share_conflicts=false smt_parallel.share_units=false smt.threads.max_conflicts=4294967295 -T:30
+
+threads-4-none
+smt.threads=4 tactic.default_tactic=smt smt_parallel.never_cube=true smt_parallel.share_conflicts=false smt_parallel.share_units=false -T:30
+
+threads-4-shareunits
+smt.threads=4 tactic.default_tactic=smt smt_parallel.never_cube=true smt_parallel.share_conflicts=false smt_parallel.share_units=true -T:30
+
+threads-4-shareconflicts
+smt.threads=4 tactic.default_tactic=smt smt_parallel.never_cube=true smt_parallel.share_conflicts=true smt_parallel.share_units=false -T:30
+
+threads-4-cube
+smt.threads=4 tactic.default_tactic=smt smt_parallel.never_cube=false smt_parallel.share_conflicts=false smt_parallel.share_units=false -T:30
+
+base-shareunits-nonrelevant
+
From b25a808dcbad9feb27b22345526b8d35b3de3047 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 16 Aug 2025 17:53:00 -0700 Subject: [PATCH 04/12] notes on parameters Signed-off-by: Nikolaj Bjorner --- PARALLEL_PROJECT_NOTES.md | 34 +++++++++++++++++++++++++--------- src/smt/smt_parallel.cpp | 4 ++-- 2 files changed, 27 insertions(+), 11 deletions(-) diff --git a/PARALLEL_PROJECT_NOTES.md b/PARALLEL_PROJECT_NOTES.md index bff187927..25116ac1e 100644 --- a/PARALLEL_PROJECT_NOTES.md +++ b/PARALLEL_PROJECT_NOTES.md @@ -240,27 +240,43 @@ push more instances from smtlib.org benchmarks into z3-poly-testing/inputs or up The first rounds created a base-line where all features were turned off, then it created variants where one feature was turned off at a time. The data-point where all but one feature is turned off could tell us something if a feature has a chance of being useful in isolation. -The following is a sample naming scheme. +The following is a sample naming scheme for associated settings. 
 threads-1
-smt.threads=1 tactic.default_tactic=smt -T:30
+-T:30 smt.threads=1 tactic.default_tactic=smt
 
 threads-4-none-unbounded
-smt.threads=4 tactic.default_tactic=smt smt_parallel.never_cube=true smt_parallel.share_conflicts=false smt_parallel.share_units=false smt.threads.max_conflicts=4294967295 -T:30
+-T:30 smt.threads=4 tactic.default_tactic=smt smt_parallel.never_cube=true smt_parallel.share_conflicts=false smt_parallel.share_units=false smt.threads.max_conflicts=4294967295
 
 threads-4-none
-smt.threads=4 tactic.default_tactic=smt smt_parallel.never_cube=true smt_parallel.share_conflicts=false smt_parallel.share_units=false -T:30
+-T:30 smt.threads=4 tactic.default_tactic=smt smt_parallel.never_cube=true smt_parallel.share_conflicts=false smt_parallel.share_units=false 
 
 threads-4-shareunits
-smt.threads=4 tactic.default_tactic=smt smt_parallel.never_cube=true smt_parallel.share_conflicts=false smt_parallel.share_units=true -T:30
+-T:30 smt.threads=4 tactic.default_tactic=smt smt_parallel.never_cube=true smt_parallel.share_conflicts=false smt_parallel.share_units=true 
 
 threads-4-shareconflicts
-smt.threads=4 tactic.default_tactic=smt smt_parallel.never_cube=true smt_parallel.share_conflicts=true smt_parallel.share_units=false -T:30
+-T:30 smt.threads=4 tactic.default_tactic=smt smt_parallel.never_cube=true smt_parallel.share_conflicts=true smt_parallel.share_units=false 
+
+threads-4-cube-frugal
+-T:30 smt.threads=4 tactic.default_tactic=smt smt_parallel.never_cube=false smt_parallel.frugal_cube_only=true smt_parallel.share_conflicts=false smt_parallel.share_units=false
+
+threads-4-shareunits-nonrelevant
+-T:30 smt.threads=4 tactic.default_tactic=smt smt_parallel.never_cube=true smt_parallel.share_conflicts=true smt_parallel.share_units=false smt_parallel.relevant_units_only=false 
 
 threads-4-cube
-smt.threads=4 tactic.default_tactic=smt smt_parallel.never_cube=false smt_parallel.share_conflicts=false smt_parallel.share_units=false -T:30
-
-base-shareunits-nonrelevant
+-T:30 smt.threads=4 tactic.default_tactic=smt smt_parallel.never_cube=false smt_parallel.frugal_cube_only=false smt_parallel.share_conflicts=false smt_parallel.share_units=false
+Ideas for other knobs that can be added: + + +
  • Only cube on literals that exist in initial formula. Don't cube on literals created during search (such as by theory lemmas). +
  • Only share units for literals that exist in the initial formula. + + +This requires collecting sub-expressions from the solver state at initialization time. It can be programmed by adding an expr_mark +structure and marking all expressions used in bool_vars after initialization as initial. +Then only initial bool_vars are shared as units. +A simpler approach is just to remember the initial number of bool_vars. +Fresh atoms are allocated with higher ordinals anyway. \ No newline at end of file diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 58d8a1c65..573e48107 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -89,7 +89,7 @@ namespace smt { // share with batch manager. // process next cube. expr_ref_vector const& unsat_core = ctx->unsat_core(); - IF_VERBOSE(1, verbose_stream() << "unsat core: " << unsat_core << "\n"); + IF_VERBOSE(2, verbose_stream() << "unsat core: " << unsat_core << "\n"); // If the unsat core only contains assumptions, // unsatisfiability does not depend on the current cube and the entire problem is unsat. if (all_of(unsat_core, [&](expr* e) { return asms.contains(e); })) { @@ -453,7 +453,7 @@ namespace smt { if (top_lits.size() >= k) break; } - IF_VERBOSE(2, verbose_stream() << "top literals " << top_lits << " head size " << ctx->m_pq_scores.size() << " num vars " << ctx->get_num_bool_vars() << "\n"); + IF_VERBOSE(3, verbose_stream() << "top literals " << top_lits << " head size " << ctx->m_pq_scores.size() << " num vars " << ctx->get_num_bool_vars() << "\n"); return top_lits; } From ca831bedcb994b8b3a54bb9338f74ab4f37244f6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 16 Aug 2025 18:24:03 -0700 Subject: [PATCH 05/12] move to config structure Signed-off-by: Nikolaj Bjorner --- src/smt/smt_parallel.cpp | 60 ++++++++++++++++++++++------------------ src/smt/smt_parallel.h | 15 +++++++--- 2 files changed, 44 insertions(+), 31 deletions(-) diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 573e48107..df0f23f4d 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -39,6 +39,8 @@ namespace smt { #include #include +#define LOG_WORKER(lvl, s) IF_VERBOSE(lvl, verbose_stream() << "Worker " << id << s) + namespace smt { void parallel::worker::run() { @@ -55,29 +57,31 @@ namespace smt { b.set_exception("context cancelled"); return; } - IF_VERBOSE(1, verbose_stream() << "Worker " << id << " checking cube: " << mk_bounded_pp(mk_and(cube), m, 3) << "\n"); + LOG_WORKER(1, " checking cube: " << mk_bounded_pp(mk_and(cube), m, 3) << "\n"); lbool r = check_cube(cube); if (m.limit().is_canceled()) { - IF_VERBOSE(1, verbose_stream() << "Worker " << id << " context cancelled\n"); + LOG_WORKER(1, " context cancelled\n"); return; } switch (r) { case l_undef: { if (m.limit().is_canceled()) break; - IF_VERBOSE(1, verbose_stream() << "Worker " << id << " found undef cube\n"); + LOG_WORKER(1, " found undef cube\n"); // return unprocessed cubes to the batch manager // add a split literal to the batch manager. // optionally process other cubes and delay sending back unprocessed cubes to batch manager. - vector returned_cubes; - returned_cubes.push_back(cube); - auto split_atoms = get_split_atoms(); - b.return_cubes(l2g, returned_cubes, split_atoms); + if (!m_config.m_never_cube) { + vector returned_cubes; + returned_cubes.push_back(cube); + auto split_atoms = get_split_atoms(); + b.return_cubes(l2g, returned_cubes, split_atoms); + } update_max_thread_conflicts(); break; } case l_true: { - IF_VERBOSE(1, verbose_stream() << "Worker " << id << " found sat cube\n"); + LOG_WORKER(1, " found sat cube\n"); model_ref mdl; ctx->get_model(mdl); b.set_sat(l2g, *mdl); @@ -89,11 +93,11 @@ namespace smt { // share with batch manager. // process next cube. expr_ref_vector const& unsat_core = ctx->unsat_core(); - IF_VERBOSE(2, verbose_stream() << "unsat core: " << unsat_core << "\n"); + LOG_WORKER(2, "unsat core: " << unsat_core << "\n"); // If the unsat core only contains assumptions, // unsatisfiability does not depend on the current cube and the entire problem is unsat. if (all_of(unsat_core, [&](expr* e) { return asms.contains(e); })) { - IF_VERBOSE(1, verbose_stream() << "Worker " << id << " determined formula unsat\n"); + LOG_WORKER(1, " determined formula unsat\n"); b.set_unsat(l2g, unsat_core); return; } @@ -101,14 +105,14 @@ namespace smt { if (asms.contains(e)) b.report_assumption_used(l2g, e); // report assumptions used in unsat core, so they can be used in final core - IF_VERBOSE(1, verbose_stream() << "Worker " << id << " found unsat cube\n"); - if (smt_parallel_params(p.ctx.m_params).share_conflicts()) + LOG_WORKER(1, " found unsat cube\n"); + if (m_config.m_share_conflicts) b.collect_clause(l2g, id, mk_not(mk_and(unsat_core))); break; } } } - if (smt_parallel_params(p.ctx.m_params).share_units()) + if (m_config.m_share_units) share_units(l2g); } } @@ -117,14 +121,19 @@ namespace smt { ast_translation g2l(p.ctx.m, m); for (auto e : _asms) asms.push_back(g2l(e)); - IF_VERBOSE(1, verbose_stream() << "Worker " << id << " created with " << asms.size() << " assumptions\n"); + LOG_WORKER(1, " created with " << asms.size() << " assumptions\n"); m_smt_params.m_preprocess = false; ctx = alloc(context, m, m_smt_params, p.ctx.get_params()); context::copy(p.ctx, *ctx, true); ctx->set_random_seed(id + m_smt_params.m_random_seed); - m_max_thread_conflicts = ctx->get_fparams().m_threads_max_conflicts; - m_max_conflicts = ctx->get_fparams().m_max_conflicts; + smt_parallel_params pp(p.ctx.m_params); + m_config.m_threads_max_conflicts = ctx->get_fparams().m_threads_max_conflicts; + m_config.m_max_conflicts = ctx->get_fparams().m_max_conflicts; + m_config.m_relevant_units_only = pp.relevant_units_only(); + m_config.m_never_cube = pp.never_cube(); + m_config.m_share_conflicts = pp.share_conflicts(); + m_config.m_share_units = pp.share_units(); } void parallel::worker::share_units(ast_translation& l2g) { @@ -133,15 +142,13 @@ namespace smt { unsigned sz = ctx->assigned_literals().size(); for (unsigned j = m_num_shared_units; j < sz; ++j) { // iterate only over new literals since last sync literal lit = ctx->assigned_literals()[j]; - if (!ctx->is_relevant(lit.var()) && smt_parallel_params(p.ctx.m_params).relevant_units_only()) { - // IF_VERBOSE(0, verbose_stream() << "non-relevant literal " << lit << "\n"); + if (!ctx->is_relevant(lit.var()) && m_config.m_relevant_units_only) continue; - } + expr_ref e(ctx->bool_var2expr(lit.var()), ctx->m); // turn literal into a Boolean expression - if (m.is_and(e) || m.is_or(e)) { - //IF_VERBOSE(0, verbose_stream() << "skip Boolean\n"); + if (m.is_and(e) || m.is_or(e)) continue; - } + if (lit.sign()) e = m.mk_not(e); // negate if literal is negative @@ -166,7 +173,7 @@ namespace smt { for (expr* e : new_clauses) { expr_ref local_clause(e, g2l.to()); // e was already translated to the local context in the batch manager!! ctx->assert_expr(local_clause); // assert the clause in the local context - IF_VERBOSE(2, verbose_stream() << "Worker " << id << " asserting shared clause: " << mk_bounded_pp(local_clause, m, 3) << "\n"); + LOG_WORKER(2, " asserting shared clause: " << mk_bounded_pp(local_clause, m, 3) << "\n"); } } @@ -188,7 +195,7 @@ namespace smt { asms.push_back(atom); lbool r = l_undef; - ctx->get_fparams().m_max_conflicts = std::min(m_max_thread_conflicts, m_max_conflicts); + ctx->get_fparams().m_max_conflicts = std::min(m_config.m_threads_max_conflicts, m_config.m_max_conflicts); try { r = ctx->check(asms.size(), asms.data()); } @@ -202,7 +209,7 @@ namespace smt { b.set_exception("unknown exception"); } asms.shrink(asms.size() - cube.size()); - IF_VERBOSE(1, verbose_stream() << "Worker " << id << " DONE checking cube " << r << "\n";); + LOG_WORKER(1, " DONE checking cube " << r << "\n";); return r; } @@ -354,8 +361,7 @@ namespace smt { // currenly, the code just implements the greedy strategy void parallel::batch_manager::return_cubes(ast_translation& l2g, vectorconst& C_worker, expr_ref_vector const& A_worker) { - if (smt_parallel_params(p.ctx.m_params).never_cube()) - return; // portfolio only + SASSERT(!smt_parallel_params(p.ctx.m_params).never_cube()); auto atom_in_cube = [&](expr_ref_vector const& cube, expr* atom) { return any_of(cube, [&](expr* e) { return e == atom || (m.is_not(e, e) && e == atom); }); diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h index b337d5e45..e6abc05ce 100644 --- a/src/smt/smt_parallel.h +++ b/src/smt/smt_parallel.h @@ -11,7 +11,7 @@ Abstract: Author: - nbjorner 2020-01-31 + Ilana 2025 Revision History: @@ -89,21 +89,28 @@ namespace smt { }; class worker { + struct config { + unsigned m_threads_max_conflicts = 1000; + unsigned m_max_conflicts = 10000000; + bool m_relevant_units_only = true; + bool m_never_cube = false; + bool m_share_conflicts = true; + bool m_share_units = true; + }; unsigned id; // unique identifier for the worker parallel& p; batch_manager& b; ast_manager m; expr_ref_vector asms; smt_params m_smt_params; + config m_config; scoped_ptr ctx; - unsigned m_max_conflicts = 800; // the global budget for all work this worker can do across cubes in the current run. - unsigned m_max_thread_conflicts = 100; // the per-cube limit for how many conflicts the worker can spend on a single cube before timing out on it and moving on unsigned m_num_shared_units = 0; unsigned m_shared_clause_limit = 0; // remembers the index into shared_clause_trail marking the boundary between "old" and "new" clauses to share void share_units(ast_translation& l2g); lbool check_cube(expr_ref_vector const& cube); void update_max_thread_conflicts() { - m_max_thread_conflicts *= 2; + m_config.m_threads_max_conflicts *= 2; } // allow for backoff scheme of conflicts within the thread for cube timeouts. public: worker(unsigned id, parallel& p, expr_ref_vector const& _asms); From c4607c2ba30662d9a84d5a77303ba549c34d04b8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 17 Aug 2025 09:49:24 -0700 Subject: [PATCH 06/12] update experiment notes Signed-off-by: Nikolaj Bjorner --- PARALLEL_PROJECT_NOTES.md | 10 +++++++--- src/smt/smt_parallel.cpp | 36 ++++++++++++++++++++++++++++++++++++ src/smt/smt_parallel.h | 8 ++++++++ 3 files changed, 51 insertions(+), 3 deletions(-) diff --git a/PARALLEL_PROJECT_NOTES.md b/PARALLEL_PROJECT_NOTES.md index 25116ac1e..e232ff78d 100644 --- a/PARALLEL_PROJECT_NOTES.md +++ b/PARALLEL_PROJECT_NOTES.md @@ -255,17 +255,21 @@ threads-4-none threads-4-shareunits -T:30 smt.threads=4 tactic.default_tactic=smt smt_parallel.never_cube=true smt_parallel.share_conflicts=false smt_parallel.share_units=true -threads-4-shareconflicts --T:30 smt.threads=4 tactic.default_tactic=smt smt_parallel.never_cube=true smt_parallel.share_conflicts=true smt_parallel.share_units=false - threads-4-cube-frugal -T:30 smt.threads=4 tactic.default_tactic=smt smt_parallel.never_cube=false smt_parallel.frugal_cube_only=true smt_parallel.share_conflicts=false smt_parallel.share_units=false +threads-4-cube-frugal-shareconflicts +-T:30 smt.threads=4 tactic.default_tactic=smt smt_parallel.never_cube=false smt_parallel.frugal_cube_only=true smt_parallel.share_conflicts=true smt_parallel.share_units=false + threads-4-shareunits-nonrelevant -T:30 smt.threads=4 tactic.default_tactic=smt smt_parallel.never_cube=true smt_parallel.share_conflicts=true smt_parallel.share_units=false smt_parallel.relevant_units_only=false threads-4-cube -T:30 smt.threads=4 tactic.default_tactic=smt smt_parallel.never_cube=false smt_parallel.frugal_cube_only=false smt_parallel.share_conflicts=false smt_parallel.share_units=false + +threads-4-cube-shareconflicts +-T:30 smt.threads=4 tactic.default_tactic=smt smt_parallel.never_cube=false smt_parallel.frugal_cube_only=false smt_parallel.share_conflicts=true smt_parallel.share_units=false + Ideas for other knobs that can be added: diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index df0f23f4d..2a0963e7c 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -157,6 +157,42 @@ namespace smt { m_num_shared_units = sz; } + void parallel::batch_manager::init_parameters_state() { + auto& smt_params = p.ctx.get_fparams(); + std::function(unsigned&)> inc = [](unsigned& v) { std::function clo = [&]() { ++v; }; return clo; }; + std::function(unsigned&)> dec = [](unsigned& v) { std::function clo = [&]() { if (v > 0) --v; }; return clo; }; + std::function(bool&)> incb = [](bool& v) { std::function clo = [&]() { v = true; }; return clo; }; + std::function(bool&)> decb = [](bool& v) { std::function clo = [&]() { v = false; }; return clo; }; + std::function unsigned_parameter = [&](unsigned& p) -> parameter_state { + return { { { p , 1.0}}, + { { 1.0, inc(p) }, { 1.0, dec(p) }} + }; + }; + std::function bool_parameter = [&](bool& p) -> parameter_state { + return { { { p , 1.0}}, + { { 1.0, incb(p) }, { 1.0, decb(p) }} + }; + }; + + + parameter_state s1 = unsigned_parameter(smt_params.m_arith_branch_cut_ratio); + parameter_state s2 = bool_parameter(smt_params.m_arith_eager_eq_axioms); + + + // arith.enable_hnf(bool) (default: true) + // arith.greatest_error_pivot(bool) (default: false) + // arith.int_eq_branch(bool) (default: false) + // arith.min(bool) (default: false) + // arith.nl.branching(bool) (default: true) + // arith.nl.cross_nested(bool) (default: true) + // arith.nl.delay(unsigned int) (default: 10) + // arith.nl.expensive_patching(bool) (default: false) + // arith.nl.expp(bool) (default: false) + // arith.nl.gr_q(unsigned int) (default: 10) + // arith.nl.grobner(bool) (default: true) + // arith.nl.grobner_cnfl_to_report(unsigned int) (default: 1) }; + } + void parallel::batch_manager::collect_clause(ast_translation& l2g, unsigned source_worker_id, expr* clause) { std::scoped_lock lock(mux); expr* g_clause = l2g(clause); diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h index e6abc05ce..1cbdb5ebe 100644 --- a/src/smt/smt_parallel.h +++ b/src/smt/smt_parallel.h @@ -32,6 +32,11 @@ namespace smt { expr_ref clause; }; + struct parameter_state { + std::vector> m_value_scores; // bounded number of values with scores. + std::vector>> m_weighted_moves; // possible moves weighted by how well they did + }; + class batch_manager { enum state { is_running, @@ -52,6 +57,7 @@ namespace smt { std::string m_exception_msg; vector shared_clause_trail; // store all shared clauses with worker IDs obj_hashtable shared_clause_set; // for duplicate filtering on per-thread clause expressions + vector m_parameters_state; // called from batch manager to cancel other workers if we've reached a verdict void cancel_workers() { @@ -60,6 +66,8 @@ namespace smt { w->cancel(); } + void init_parameters_state(); + public: batch_manager(ast_manager& m, parallel& p) : m(m), p(p), m_split_atoms(m) { } From d0d8e4d9f30163218bcd1045616a3afe3c4f16d3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 17 Aug 2025 11:30:02 -0700 Subject: [PATCH 07/12] move l2g and g2l to worker constructor to avoid race condition in ast_translation constructor Signed-off-by: Nikolaj Bjorner --- src/smt/smt_parallel.cpp | 40 ++++++++++++++++++++-------------------- src/smt/smt_parallel.h | 1 + 2 files changed, 21 insertions(+), 20 deletions(-) diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 2a0963e7c..cbf986baa 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -44,14 +44,12 @@ namespace smt { namespace smt { void parallel::worker::run() { - ast_translation g2l(p.ctx.m, m); // global to local context -- MUST USE p.ctx.m, not ctx->m, AS GLOBAL MANAGER!!! - ast_translation l2g(m, p.ctx.m); // local to global context while (m.inc()) { // inc: increase the limit and check if it is canceled, vs m.limit().is_canceled() is readonly. the .limit() is also not necessary (m.inc() etc provides a convenience wrapper) vector cubes; - b.get_cubes(g2l, cubes); + b.get_cubes(m_g2l, cubes); if (cubes.empty()) return; - collect_shared_clauses(g2l); + collect_shared_clauses(m_g2l); for (auto& cube : cubes) { if (!m.inc()) { b.set_exception("context cancelled"); @@ -75,7 +73,7 @@ namespace smt { vector returned_cubes; returned_cubes.push_back(cube); auto split_atoms = get_split_atoms(); - b.return_cubes(l2g, returned_cubes, split_atoms); + b.return_cubes(m_l2g, returned_cubes, split_atoms); } update_max_thread_conflicts(); break; @@ -84,7 +82,7 @@ namespace smt { LOG_WORKER(1, " found sat cube\n"); model_ref mdl; ctx->get_model(mdl); - b.set_sat(l2g, *mdl); + b.set_sat(m_l2g, *mdl); return; } case l_false: { @@ -98,29 +96,31 @@ namespace smt { // unsatisfiability does not depend on the current cube and the entire problem is unsat. if (all_of(unsat_core, [&](expr* e) { return asms.contains(e); })) { LOG_WORKER(1, " determined formula unsat\n"); - b.set_unsat(l2g, unsat_core); + b.set_unsat(m_l2g, unsat_core); return; } for (expr* e : unsat_core) if (asms.contains(e)) - b.report_assumption_used(l2g, e); // report assumptions used in unsat core, so they can be used in final core + b.report_assumption_used(m_l2g, e); // report assumptions used in unsat core, so they can be used in final core LOG_WORKER(1, " found unsat cube\n"); if (m_config.m_share_conflicts) - b.collect_clause(l2g, id, mk_not(mk_and(unsat_core))); + b.collect_clause(m_l2g, id, mk_not(mk_and(unsat_core))); break; } } } if (m_config.m_share_units) - share_units(l2g); + share_units(m_l2g); } } - parallel::worker::worker(unsigned id, parallel& p, expr_ref_vector const& _asms): id(id), p(p), b(p.m_batch_manager), m_smt_params(p.ctx.get_fparams()), asms(m) { - ast_translation g2l(p.ctx.m, m); + parallel::worker::worker(unsigned id, parallel& p, expr_ref_vector const& _asms): + id(id), p(p), b(p.m_batch_manager), m_smt_params(p.ctx.get_fparams()), asms(m), + m_g2l(p.ctx.m, m), + m_l2g(m, p.ctx.m) { for (auto e : _asms) - asms.push_back(g2l(e)); + asms.push_back(m_g2l(e)); LOG_WORKER(1, " created with " << asms.size() << " assumptions\n"); m_smt_params.m_preprocess = false; ctx = alloc(context, m, m_smt_params, p.ctx.get_params()); @@ -134,6 +134,8 @@ namespace smt { m_config.m_never_cube = pp.never_cube(); m_config.m_share_conflicts = pp.share_conflicts(); m_config.m_share_units = pp.share_units(); + + } void parallel::worker::share_units(ast_translation& l2g) { @@ -159,10 +161,10 @@ namespace smt { void parallel::batch_manager::init_parameters_state() { auto& smt_params = p.ctx.get_fparams(); - std::function(unsigned&)> inc = [](unsigned& v) { std::function clo = [&]() { ++v; }; return clo; }; - std::function(unsigned&)> dec = [](unsigned& v) { std::function clo = [&]() { if (v > 0) --v; }; return clo; }; - std::function(bool&)> incb = [](bool& v) { std::function clo = [&]() { v = true; }; return clo; }; - std::function(bool&)> decb = [](bool& v) { std::function clo = [&]() { v = false; }; return clo; }; + std::function(unsigned&)> inc = [](unsigned& v) { return [&]() -> void { ++v; }; }; + std::function(unsigned&)> dec = [](unsigned& v) { return [&]() -> void { if (v > 0) --v; }; }; + std::function(bool&)> incb = [](bool& v) { return [&]() -> void { v = true; }; }; + std::function(bool&)> decb = [](bool& v) { return [&]() -> void { v = false; }; }; std::function unsigned_parameter = [&](unsigned& p) -> parameter_state { return { { { p , 1.0}}, { { 1.0, inc(p) }, { 1.0, dec(p) }} @@ -174,10 +176,8 @@ namespace smt { }; }; - parameter_state s1 = unsigned_parameter(smt_params.m_arith_branch_cut_ratio); - parameter_state s2 = bool_parameter(smt_params.m_arith_eager_eq_axioms); - + parameter_state s2 = bool_parameter(smt_params.m_arith_eager_eq_axioms); // arith.enable_hnf(bool) (default: true) // arith.greatest_error_pivot(bool) (default: false) diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h index 1cbdb5ebe..6933eda30 100644 --- a/src/smt/smt_parallel.h +++ b/src/smt/smt_parallel.h @@ -113,6 +113,7 @@ namespace smt { smt_params m_smt_params; config m_config; scoped_ptr ctx; + ast_translation m_g2l, m_l2g; unsigned m_num_shared_units = 0; unsigned m_shared_clause_limit = 0; // remembers the index into shared_clause_trail marking the boundary between "old" and "new" clauses to share void share_units(ast_translation& l2g); From e76f9f2615d75f6bcccd105a4edfc0747f5901ec Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 17 Aug 2025 12:04:53 -0700 Subject: [PATCH 08/12] add more parameters, try to fix conflict timeout inside of nlsat solver Signed-off-by: Nikolaj Bjorner --- src/math/lp/lp_settings.cpp | 1 + src/math/lp/lp_settings.h | 5 ++++- src/math/lp/nla_core.cpp | 2 +- src/params/smt_parallel_params.pyg | 5 ++++- src/smt/smt_parallel.cpp | 9 ++++++++- src/smt/smt_parallel.h | 7 +++++-- 6 files changed, 23 insertions(+), 6 deletions(-) diff --git a/src/math/lp/lp_settings.cpp b/src/math/lp/lp_settings.cpp index 48b064567..c8e2cf862 100644 --- a/src/math/lp/lp_settings.cpp +++ b/src/math/lp/lp_settings.cpp @@ -41,4 +41,5 @@ void lp::lp_settings::updt_params(params_ref const& _p) { m_dio_ignore_big_nums = lp_p.dio_ignore_big_nums(); m_dio_calls_period = lp_p.dio_calls_period(); m_dio_run_gcd = lp_p.dio_run_gcd(); + m_max_conflicts = p.max_conflicts(); } diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index a7a2d96dd..e3ee2344d 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -137,6 +137,7 @@ struct statistics { unsigned m_bounds_tightening_conflicts = 0; unsigned m_bounds_tightenings = 0; unsigned m_nla_throttled_lemmas = 0; + ::statistics m_st = {}; void reset() { @@ -221,11 +222,13 @@ public: unsigned percent_of_entering_to_check = 5; // we try to find a profitable column in a percentage of the columns bool use_scaling = true; unsigned max_number_of_iterations_with_no_improvements = 2000000; - double time_limit; // the maximum time limit of the total run time in seconds + double time_limit; // the maximum time limit of the total run time in seconds // end of dual section bool m_bound_propagation = true; bool presolve_with_double_solver_for_lar = true; simplex_strategy_enum m_simplex_strategy; + + unsigned m_max_conflicts = 0; int report_frequency = 1000; bool print_statistics = false; diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 5a74f882f..585d605c3 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1595,7 +1595,7 @@ lbool core::bounded_nlsat() { scoped_rlimit sr(m_nra_lim, 100000); ret = m_nra.check(); } - p.set_uint("max_conflicts", UINT_MAX); + p.set_uint("max_conflicts", lp_settings().m_max_conflicts); m_nra.updt_params(p); lp_settings().stats().m_nra_calls++; if (ret == l_undef) diff --git a/src/params/smt_parallel_params.pyg b/src/params/smt_parallel_params.pyg index 91f7bce91..df7b1b189 100644 --- a/src/params/smt_parallel_params.pyg +++ b/src/params/smt_parallel_params.pyg @@ -6,5 +6,8 @@ def_module_params('smt_parallel', ('share_conflicts', BOOL, True, 'share conflicts'), ('never_cube', BOOL, False, 'never cube'), ('frugal_cube_only', BOOL, False, 'only apply frugal cube strategy'), - ('relevant_units_only', BOOL, True, 'only share relvant units') + ('relevant_units_only', BOOL, True, 'only share relvant units'), + ('max_conflict_mul', DOUBLE, 1.5, 'increment multiplier for max-conflicts'), + ('share_units_initial_only', BOOL, False, 'share only initial Boolean atoms as units'), + ('cube_initial_only', BOOL, False, 'cube only on initial Boolean atoms') )) diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index cbf986baa..51a3bb61d 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -55,7 +55,7 @@ namespace smt { b.set_exception("context cancelled"); return; } - LOG_WORKER(1, " checking cube: " << mk_bounded_pp(mk_and(cube), m, 3) << "\n"); + LOG_WORKER(1, " checking cube: " << mk_bounded_pp(mk_and(cube), m, 3) << " max-conflicts " << m_config.m_threads_max_conflicts << "\n"); lbool r = check_cube(cube); if (m.limit().is_canceled()) { LOG_WORKER(1, " context cancelled\n"); @@ -134,8 +134,15 @@ namespace smt { m_config.m_never_cube = pp.never_cube(); m_config.m_share_conflicts = pp.share_conflicts(); m_config.m_share_units = pp.share_units(); + m_config.m_share_units_initial_only = pp.share_units_initial_only(); + m_config.m_cube_initial_only = pp.cube_initial_only(); + m_config.m_max_conflict_mul = pp.max_conflict_mul(); + // don't share initial units + ctx->pop_to_base_lvl(); + m_num_shared_units = ctx->assigned_literals().size(); + m_num_initial_atoms = ctx->get_num_bool_vars(); } void parallel::worker::share_units(ast_translation& l2g) { diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h index 6933eda30..24e920f57 100644 --- a/src/smt/smt_parallel.h +++ b/src/smt/smt_parallel.h @@ -104,6 +104,9 @@ namespace smt { bool m_never_cube = false; bool m_share_conflicts = true; bool m_share_units = true; + double m_max_conflict_mul = 1.5; + bool m_share_units_initial_only = false; + bool m_cube_initial_only = false; }; unsigned id; // unique identifier for the worker parallel& p; @@ -115,11 +118,12 @@ namespace smt { scoped_ptr ctx; ast_translation m_g2l, m_l2g; unsigned m_num_shared_units = 0; + unsigned m_num_initial_atoms = 0; unsigned m_shared_clause_limit = 0; // remembers the index into shared_clause_trail marking the boundary between "old" and "new" clauses to share void share_units(ast_translation& l2g); lbool check_cube(expr_ref_vector const& cube); void update_max_thread_conflicts() { - m_config.m_threads_max_conflicts *= 2; + m_config.m_threads_max_conflicts = (unsigned)(m_config.m_max_conflict_mul * m_config.m_threads_max_conflicts); } // allow for backoff scheme of conflicts within the thread for cube timeouts. public: worker(unsigned id, parallel& p, expr_ref_vector const& _asms); @@ -132,7 +136,6 @@ namespace smt { m.limit().cancel(); } void collect_statistics(::statistics& st) const { - IF_VERBOSE(1, verbose_stream() << "Collecting statistics for worker " << id << "\n"); ctx->collect_statistics(st); } reslimit& limit() { From f486617f81e2b826845a82a442c13abd310a00da Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 17 Aug 2025 13:58:31 -0700 Subject: [PATCH 09/12] ensure that max-conflicts is propagated to nra-solver --- src/math/lp/nla_core.cpp | 5 ++++- src/smt/theory_lra.cpp | 2 ++ 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 585d605c3..9a28363d7 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -38,7 +38,7 @@ core::core(lp::lar_solver& s, params_ref const& p, reslimit & lim) : m_grobner(this), m_emons(m_evars), m_use_nra_model(false), - m_nra(s, m_nra_lim, *this), + m_nra(s, m_nra_lim, *this, p), m_throttle(lra.trail(), lra.settings().stats()) { m_nlsat_delay_bound = lp_settings().nlsat_delay(); @@ -1561,6 +1561,9 @@ lbool core::check() { if (no_effect() && params().arith_nl_nra()) { scoped_limits sl(m_reslim); sl.push_child(&m_nra_lim); + params_ref p; + p.set_uint("max_conflicts", lp_settings().m_max_conflicts); + m_nra.updt_params(p); ret = m_nra.check(); lp_settings().stats().m_nra_calls++; } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index f3d9a5169..4b544fc20 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1427,6 +1427,8 @@ public: void init_search_eh() { m_arith_eq_adapter.init_search_eh(); m_num_conflicts = 0; + if (m_solver) + lp().settings().m_max_conflicts = ctx().get_fparams().m_max_conflicts; } bool can_get_value(theory_var v) const { From 242eaa9ce88647e1cdd78a96f68b056c6ea7a689 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 17 Aug 2025 14:02:32 -0700 Subject: [PATCH 10/12] change logging of unsat core to use bounded pp Signed-off-by: Nikolaj Bjorner --- src/smt/smt_parallel.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 51a3bb61d..f71825f17 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -91,7 +91,7 @@ namespace smt { // share with batch manager. // process next cube. expr_ref_vector const& unsat_core = ctx->unsat_core(); - LOG_WORKER(2, "unsat core: " << unsat_core << "\n"); + LOG_WORKER(2, " unsat core:\n"; for (auto c : unsat_core) verbose_stream() << mk_bounded_pp(c, m, 3) << "\n"); // If the unsat core only contains assumptions, // unsatisfiability does not depend on the current cube and the entire problem is unsat. if (all_of(unsat_core, [&](expr* e) { return asms.contains(e); })) { From 19bc9aa1325c691ae2d3def875d991a344e50e73 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 17 Aug 2025 14:11:45 -0700 Subject: [PATCH 11/12] add handling for option to not share or cube non-initial atoms Signed-off-by: Nikolaj Bjorner --- src/smt/smt_parallel.cpp | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index f71825f17..cb46725a0 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -153,6 +153,11 @@ namespace smt { literal lit = ctx->assigned_literals()[j]; if (!ctx->is_relevant(lit.var()) && m_config.m_relevant_units_only) continue; + + if (m_config.m_share_units_initial_only && lit.var() >= m_num_initial_atoms) { + LOG_WORKER(2, " Skipping non-initial unit: " << lit.var() << "\n"); + continue; // skip non-iniial atoms if configured to do so + } expr_ref e(ctx->bool_var2expr(lit.var()), ctx->m); // turn literal into a Boolean expression if (m.is_and(e) || m.is_or(e)) @@ -491,9 +496,15 @@ namespace smt { expr_ref_vector top_lits(m); for (const auto& node: candidates) { + if (ctx->get_assignment(node.key) != l_undef) continue; + if (m_config.m_cube_initial_only && node.key >= m_num_initial_atoms) { + LOG_WORKER(2, " Skipping non-initial atom from cube: " << node.key << "\n"); + continue; // skip non-initial atoms if configured to do so + } + expr* e = ctx->bool_var2expr(node.key); if (!e) continue; From 97d7723c447eb2c0a5ecad07b92facaccec54019 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 17 Aug 2025 15:50:53 -0700 Subject: [PATCH 12/12] update notes Signed-off-by: Nikolaj Bjorner --- PARALLEL_PROJECT_NOTES.md | 20 ++++++++++++++------ 1 file changed, 14 insertions(+), 6 deletions(-) diff --git a/PARALLEL_PROJECT_NOTES.md b/PARALLEL_PROJECT_NOTES.md index e232ff78d..00ec087b4 100644 --- a/PARALLEL_PROJECT_NOTES.md +++ b/PARALLEL_PROJECT_NOTES.md @@ -272,15 +272,23 @@ threads-4-cube-shareconflicts -Ideas for other knobs that can be added: +Ideas for other knobs that can be tested
  • Only cube on literals that exist in initial formula. Don't cube on literals created during search (such as by theory lemmas).
  • Only share units for literals that exist in the initial formula. +
  • Vary the backoff scheme for max_conflict_mul from 1.5 to lower and higher. +
  • Vary smt.threads.max_conflicts +
  • Replace backoff scheme by a geometric scheme: add conflict_inc (a new parameter) every time and increment conflict_inc -This requires collecting sub-expressions from the solver state at initialization time. It can be programmed by adding an expr_mark -structure and marking all expressions used in bool_vars after initialization as initial. -Then only initial bool_vars are shared as units. -A simpler approach is just to remember the initial number of bool_vars. -Fresh atoms are allocated with higher ordinals anyway. \ No newline at end of file +
    +  cube_initial_only (bool) (default: false)          only useful when never_cube=false
+  frugal_cube_only (bool) (default: false)           only useful when never_cube=false
+  max_conflict_mul (double) (default: 1.5)
+  never_cube (bool) (default: false)
+  relevant_units_only (bool) (default: true)         only useful when share_units=true
+  share_conflicts (bool) (default: true)             only useful when never_cube=false
+  share_units (bool) (default: true)
+  share_units_initial_only (bool) (default: false)   only useful when share_units=true
+