From 9bf74b5d2b042898dbb7b56798a3494835b81506 Mon Sep 17 00:00:00 2001 From: Ilana Shapiro Date: Sun, 24 Aug 2025 17:24:44 -0700 Subject: [PATCH] add implementation and toggleable param for splitting frugal + choosing deepest cubes only --- src/params/smt_parallel_params.pyg | 3 + src/smt/smt_parallel.cpp | 96 +++++++++++++++++++++++++----- src/smt/smt_parallel.h | 5 ++ 3 files changed, 89 insertions(+), 15 deletions(-) diff --git a/src/params/smt_parallel_params.pyg b/src/params/smt_parallel_params.pyg index 53892b066..dde9efd4d 100644 --- a/src/params/smt_parallel_params.pyg +++ b/src/params/smt_parallel_params.pyg @@ -11,4 +11,7 @@ def_module_params('smt_parallel', ('share_units_initial_only', BOOL, False, 'share only initial Boolean atoms as units'), ('cube_initial_only', BOOL, False, 'cube only on initial Boolean atoms'), ('max_cube_size', UINT, 20, 'maximum size of a cube to share'), + ('max_greedy_cubes', UINT, 1000, 'maximum number of cube to greedily share before switching to frugal'), + ('num_split_lits', UINT, 2, 'how many literals, k, we split on to create 2^k cubes'), + ('frugal_deepest_cube_only', BOOL, False, 'only apply frugal cube strategy, and only on a deepest (biggest) cube from the batch manager'), )) diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 47c1a5fd2..2ca181e31 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -137,6 +137,8 @@ namespace smt { 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(); + m_config.m_max_greedy_cubes = pp.max_greedy_cubes(); + m_config.m_num_split_lits = pp.num_split_lits(); // don't share initial units ctx->pop_to_base_lvl(); @@ -272,20 +274,37 @@ namespace smt { void parallel::batch_manager::get_cubes(ast_translation& g2l, vector& cubes) { std::scoped_lock lock(mux); - if (m_cubes.size() == 1 && m_cubes[0].size() == 0) { + if (m_cubes.size() == 1 && m_cubes[0].empty()) { // special initialization: the first cube is emtpy, have the worker work on an empty cube. cubes.push_back(expr_ref_vector(g2l.to())); return; } for (unsigned i = 0; i < std::min(m_max_batch_size / p.num_threads, (unsigned)m_cubes.size()) && !m_cubes.empty(); ++i) { - auto& cube = m_cubes.back(); - expr_ref_vector l_cube(g2l.to()); - for (auto& e : cube) { - l_cube.push_back(g2l(e)); + if (m_config.m_frugal_deepest_cube_only) { + // get the deepest set of cubes + auto& deepest_cubes = m_cubes_depth_sets.rbegin()->second; + unsigned idx = rand() % deepest_cubes.size(); + auto& cube = deepest_cubes[idx]; // get a random cube from the deepest set + + expr_ref_vector l_cube(g2l.to()); + for (auto& e : cube) { + l_cube.push_back(g2l(e)); + } + cubes.push_back(l_cube); + + deepest_cubes.erase(deepest_cubes.begin() + idx); // remove the cube from the set + if (deepest_cubes.empty()) + m_cubes_depth_sets.erase(m_cubes_depth_sets.size() - 1); + } else { + auto& cube = m_cubes.back(); + expr_ref_vector l_cube(g2l.to()); + for (auto& e : cube) { + l_cube.push_back(g2l(e)); + } + cubes.push_back(l_cube); + m_cubes.pop_back(); } - cubes.push_back(l_cube); - m_cubes.pop_back(); } } @@ -341,7 +360,7 @@ namespace smt { return l_undef; // the main context was cancelled, so we return undef. switch (m_state) { case state::is_running: // batch manager is still running, but all threads have processed their cubes, which means all cubes were unsat - if (!m_cubes.empty()) + if (!m_cubes.empty() || (m_config.m_frugal_deepest_cube_only && !m_cubes_depth_sets.empty())) throw default_exception("inconsistent end state"); if (!p.m_assumptions_used.empty()) { // collect unsat core from assumptions used, if any --> case when all cubes were unsat, but depend on nonempty asms, so we need to add these asms to final unsat core @@ -439,9 +458,36 @@ namespace smt { } }; + // apply the frugal strategy to ALL incoming worker cubes, but save in the deepest cube data structure + auto add_split_atom_deepest_cubes = [&](expr* atom) { + for (auto& c : C_worker) { + expr_ref_vector g_cube(l2g.to()); + for (auto& atom : c) + g_cube.push_back(l2g(atom)); + if (g_cube.size() >= m_config.m_max_cube_size) // we already added this before!! we just need to add the splits now + continue; + + // add depth set d+1 if it doesn't exist yet + unsigned d = g_cube.size(); + if (m_cubes_depth_sets.find(d + 1) == m_cubes_depth_sets.end()) + m_cubes_depth_sets[d + 1] = vector(); + + // split on the negative atom + m_cubes_depth_sets[d + 1].push_back(g_cube); + m_cubes_depth_sets[d + 1].back().push_back(m.mk_not(atom)); + + // need to split on the positive atom too + g_cube.push_back(atom); + m_cubes_depth_sets[d + 1].push_back(g_cube); + + m_stats.m_num_cubes += 2; + m_stats.m_max_cube_size = std::max(m_stats.m_max_cube_size, d + 1); + } + }; + std::scoped_lock lock(mux); - unsigned max_cubes = 1000; - bool greedy_mode = (m_cubes.size() <= max_cubes) && !m_config.m_frugal_cube_only; + unsigned max_greedy_cubes = 1000; + bool greedy_mode = (m_cubes.size() <= max_greedy_cubes) && !m_config.m_frugal_cube_only && !m_config.m_frugal_deepest_cube_only; unsigned a_worker_start_idx = 0; // @@ -455,7 +501,7 @@ namespace smt { m_split_atoms.push_back(g_atom); add_split_atom(g_atom, 0); // split all *existing* cubes - if (m_cubes.size() > max_cubes) { + if (m_cubes.size() > max_greedy_cubes) { greedy_mode = false; ++a_worker_start_idx; // start frugal from here break; @@ -470,16 +516,26 @@ namespace smt { expr_ref_vector g_cube(l2g.to()); for (auto& atom : c) g_cube.push_back(l2g(atom)); - unsigned start = m_cubes.size(); // update start after adding each cube so we only process the current cube being added - m_cubes.push_back(g_cube); + + if (m_config.m_frugal_deepest_cube_only) { + // need to add the depth set if it doesn't exist yet + if (m_cubes_depth_sets.find(g_cube.size()) == m_cubes_depth_sets.end()) { + m_cubes_depth_sets[g_cube.size()] = vector(); + } + m_cubes_depth_sets[g_cube.size()].push_back(g_cube); + m_stats.m_num_cubes += 1; + m_stats.m_max_cube_size = std::max(m_stats.m_max_cube_size, g_cube.size()); + } else { + m_cubes.push_back(g_cube); + } if (greedy_mode) { // Split new cube on all existing m_split_atoms not in it for (auto g_atom : m_split_atoms) { if (!atom_in_cube(g_cube, g_atom)) { add_split_atom(g_atom, start); - if (m_cubes.size() > max_cubes) { + if (m_cubes.size() > max_greedy_cubes) { greedy_mode = false; break; } @@ -494,7 +550,11 @@ namespace smt { expr_ref g_atom(l2g(A_worker[i]), l2g.to()); if (!m_split_atoms.contains(g_atom)) m_split_atoms.push_back(g_atom); - add_split_atom(g_atom, initial_m_cubes_size); + if (m_config.m_frugal_deepest_cube_only) { + add_split_atom_deepest_cubes(g_atom); + } else { + add_split_atom(g_atom, initial_m_cubes_size); + } } } } @@ -548,11 +608,17 @@ namespace smt { m_state = state::is_running; m_cubes.reset(); m_cubes.push_back(expr_ref_vector(m)); // push empty cube + + if (m_config.m_frugal_deepest_cube_only) { + m_cubes_depth_sets.clear(); + } + m_split_atoms.reset(); smt_parallel_params sp(p.ctx.m_params); m_config.m_max_cube_size = sp.max_cube_size(); m_config.m_frugal_cube_only = sp.frugal_cube_only(); m_config.m_never_cube = sp.never_cube(); + m_config.m_frugal_deepest_cube_only = sp.frugal_deepest_cube_only(); } void parallel::batch_manager::collect_statistics(::statistics& st) const { diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h index dd9a15c82..ae084a65e 100644 --- a/src/smt/smt_parallel.h +++ b/src/smt/smt_parallel.h @@ -20,6 +20,7 @@ Revision History: #include "smt/smt_context.h" #include +#include namespace smt { @@ -49,6 +50,7 @@ namespace smt { unsigned m_max_cube_size = 20; bool m_frugal_cube_only = false; bool m_never_cube = false; + bool m_frugal_deepest_cube_only = false; }; struct stats { unsigned m_max_cube_size = 0; @@ -63,6 +65,7 @@ namespace smt { stats m_stats; expr_ref_vector m_split_atoms; // atoms to split on vector m_cubes; + std::map> m_cubes_depth_sets; // map> contains sets of cubes, key is depth/size of cubes in the set unsigned m_max_batch_size = 10; unsigned m_exception_code = 0; std::string m_exception_msg; @@ -120,6 +123,8 @@ namespace smt { double m_max_conflict_mul = 1.5; bool m_share_units_initial_only = false; bool m_cube_initial_only = false; + bool m_max_greedy_cubes = 1000; + unsigned m_num_split_lits = 2; }; unsigned id; // unique identifier for the worker