From e76f9f2615d75f6bcccd105a4edfc0747f5901ec Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 17 Aug 2025 12:04:53 -0700 Subject: [PATCH] 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() {