From 0076e3bf977b9581585c50d0e3bf8b42c7123cbf Mon Sep 17 00:00:00 2001 From: Ilana Shapiro Date: Sat, 13 Dec 2025 04:06:56 -0800 Subject: [PATCH] Search tree core resolution optimization (#8066) * Add cube tree optimization about resolving cores recursively up the path, to prune. Also integrate asms into the tree so they're not tracked separately (#7960) * draft attempt at optimizing cube tree with resolvents. have not tested/ran yet * adding comments * fix bug about needing to bubble resolvent upwards to highest ancestor * fix bug where we need to cover the whole resolvent in the path when bubbling up * clean up comments * close entire tree when sibling resolvent is empty * integrate asms directly into cube tree, remove separate tracking * try to fix bug about redundant resolutions, merging close and try_resolve_upwards into once function * separate the logic again to avoid mutual recursion * Refactor search tree closure and resolution logic Refactor close_with_core to simplify logic and remove unnecessary parameters. Update sibling resolvent computation and try_resolve_upwards for clarity. * apply formatting Signed-off-by: Nikolaj Bjorner * Refactor close_with_core to use current node in lambda * Fix formatting issues in search_tree.h * fix build issues Signed-off-by: Nikolaj Bjorner * Update smt_parallel.cpp * Change loop variable type in unsat core processing * Change method to retrieve unsat core from root --------- Signed-off-by: Nikolaj Bjorner Co-authored-by: Nikolaj Bjorner --- src/smt/smt_parallel.cpp | 30 +----- src/smt/smt_parallel.h | 7 -- src/util/search_tree.h | 202 +++++++++++++++++++++++++-------------- 3 files changed, 135 insertions(+), 104 deletions(-) diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 8d639628c..c4ece1ad7 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -115,10 +115,6 @@ namespace smt { b.set_unsat(m_l2g, unsat_core); return; } - // report assumptions used in unsat core, so they can be used in final core - for (expr *e : unsat_core) - if (asms.contains(e)) - b.report_assumption_used(m_l2g, e); LOG_WORKER(1, " found unsat cube\n"); b.backtrack(m_l2g, unsat_core, node); @@ -262,14 +258,16 @@ namespace smt { vector g_core; for (auto c : core) { expr_ref g_c(l2g(c), m); - if (!is_assumption(g_c)) - g_core.push_back(expr_ref(l2g(c), m)); + g_core.push_back(expr_ref(l2g(c), m)); } m_search_tree.backtrack(node, g_core); IF_VERBOSE(1, m_search_tree.display(verbose_stream() << bounded_pp_exprs(core) << "\n");); if (m_search_tree.is_closed()) { m_state = state::is_unsat; + SASSERT(p.ctx.m_unsat_core.empty()); + for (auto e : m_search_tree.get_core_from_root()) + p.ctx.m_unsat_core.push_back(e); cancel_workers(); } } @@ -415,27 +413,13 @@ namespace smt { cancel_workers(); } - void parallel::batch_manager::report_assumption_used(ast_translation &l2g, expr *assumption) { - std::scoped_lock lock(mux); - p.m_assumptions_used.insert(l2g(assumption)); - } - lbool parallel::batch_manager::get_result() const { if (m.limit().is_canceled()) 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_search_tree.is_closed()) - 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 - SASSERT(p.ctx.m_unsat_core.empty()); - for (auto a : p.m_assumptions_used) - p.ctx.m_unsat_core.push_back(a); - } - return l_false; + throw default_exception("inconsistent end state"); case state::is_unsat: return l_false; case state::is_sat: @@ -500,16 +484,12 @@ namespace smt { scoped_clear(parallel &p) : p(p) {} ~scoped_clear() { p.m_workers.reset(); - p.m_assumptions_used.reset(); - p.m_assumptions.reset(); } }; scoped_clear clear(*this); m_batch_manager.initialize(); m_workers.reset(); - for (auto e : asms) - m_assumptions.insert(e); scoped_limits sl(m.limit()); flet _nt(ctx.m_fparams.m_threads, 1); SASSERT(num_threads > 1); diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h index 5851835b7..3c47d818d 100644 --- a/src/smt/smt_parallel.h +++ b/src/smt/smt_parallel.h @@ -79,10 +79,6 @@ namespace smt { void init_parameters_state(); - bool is_assumption(expr* e) const { - return p.m_assumptions.contains(e); - } - public: batch_manager(ast_manager& m, parallel& p) : m(m), p(p), m_search_tree(expr_ref(m)) { } @@ -98,7 +94,6 @@ namespace smt { void backtrack(ast_translation& l2g, expr_ref_vector const& core, node* n); void split(ast_translation& l2g, unsigned id, node* n, expr* atom); - void report_assumption_used(ast_translation& l2g, expr* assumption); void collect_clause(ast_translation& l2g, unsigned source_worker_id, expr* clause); expr_ref_vector return_shared_clauses(ast_translation& g2l, unsigned& worker_limit, unsigned worker_id); @@ -162,8 +157,6 @@ namespace smt { }; - obj_hashtable m_assumptions_used; // assumptions used in unsat cores, to be used in final core - obj_hashtable m_assumptions; // all assumptions batch_manager m_batch_manager; scoped_ptr_vector m_workers; diff --git a/src/util/search_tree.h b/src/util/search_tree.h index 29b021906..ae70bd675 100644 --- a/src/util/search_tree.h +++ b/src/util/search_tree.h @@ -14,7 +14,7 @@ Abstract: - Closed nodes are fully explored (both children are closed). - Active nodes have no children and are currently being explored. - Open nodes either have children that are open or are leaves. - + A node can be split if it is active. After splitting, it becomes open and has two open children. Backtracking on a conflict closes all nodes below the last node whose atom is in the conflict set. @@ -35,25 +35,33 @@ namespace search_tree { enum class status { open, closed, active }; - template - class node { + template class node { typedef typename Config::literal literal; literal m_literal; - node* m_left = nullptr, * m_right = nullptr, * m_parent = nullptr; + node *m_left = nullptr, *m_right = nullptr, *m_parent = nullptr; status m_status; + vector m_core; + public: - node(literal const& l, node* parent) : - m_literal(l), m_parent(parent), m_status(status::open) {} + node(literal const &l, node *parent) : m_literal(l), m_parent(parent), m_status(status::open) {} ~node() { dealloc(m_left); dealloc(m_right); } - status get_status() const { return m_status; } - void set_status(status s) { m_status = s; } - literal const& get_literal() const { return m_literal; } - bool literal_is_null() const { return Config::is_null(m_literal); } - void split(literal const& a, literal const& b) { + status get_status() const { + return m_status; + } + void set_status(status s) { + m_status = s; + } + literal const &get_literal() const { + return m_literal; + } + bool literal_is_null() const { + return Config::is_null(m_literal); + } + void split(literal const &a, literal const &b) { SASSERT(!Config::literal_is_null(a)); SASSERT(!Config::literal_is_null(b)); if (m_status != status::active) @@ -78,12 +86,12 @@ namespace search_tree { return d; } - node* find_active_node() { + node *find_active_node() { if (m_status == status::active) return this; if (m_status != status::open) return nullptr; - node* nodes[2] = { m_left, m_right }; + node *nodes[2] = {m_left, m_right}; for (unsigned i = 0; i < 2; ++i) { auto res = nodes[i] ? nodes[i]->find_active_node() : nullptr; if (res) @@ -94,7 +102,7 @@ namespace search_tree { return nullptr; } - void display(std::ostream& out, unsigned indent) const { + void display(std::ostream &out, unsigned indent) const { for (unsigned i = 0; i < indent; ++i) out << " "; Config::display_literal(out, m_literal); @@ -105,10 +113,19 @@ namespace search_tree { if (m_right) m_right->display(out, indent + 2); } + + void set_core(vector const &core) { + m_core = core; + } + vector const &get_core() const { + return m_core; + } + void clear_core() { + m_core.clear(); + } }; - template - class tree { + template class tree { typedef typename Config::literal literal; scoped_ptr> m_root = nullptr; literal m_null_literal; @@ -116,7 +133,7 @@ namespace search_tree { // return an active node in the subtree rooted at n, or nullptr if there is none // close nodes that are fully explored (whose children are all closed) - node* activate_from_root(node* n) { + node *activate_from_root(node *n) { if (!n) return nullptr; if (n->get_status() != status::open) @@ -127,7 +144,7 @@ namespace search_tree { n->set_status(status::active); return n; } - node* nodes[2] = { left, right }; + node *nodes[2] = {left, right}; unsigned index = m_rand(2); auto child = activate_from_root(nodes[index]); if (child) @@ -135,37 +152,75 @@ namespace search_tree { child = activate_from_root(nodes[1 - index]); if (child) return child; - if (left && right && left->get_status() == status::closed && right->get_status() == status::closed) - n->set_status(status::closed); + if (left && right && left->get_status() == status::closed && right->get_status() == status::closed) + n->set_status(status::closed); return nullptr; } - void close_node(node* n) { - if (!n) - return; - if (n->get_status() == status::closed) + void close(node *n) { + if (!n || n->get_status() == status::closed) return; n->set_status(status::closed); - close_node(n->left()); - close_node(n->right()); - while (n) { - auto p = n->parent(); - if (!p) - return; - if (p->get_status() != status::open) - return; - if (p->left()->get_status() != status::closed) - return; - if (p->right()->get_status() != status::closed) - return; - p->set_status(status::closed); - n = p; + close(n->left()); + close(n->right()); + } + + // Invariants: + // Cores labeling nodes are subsets of the literals on the path to the node and the (external) assumption + // literals. If a parent is open, then the one of the children is open. + void close_with_core(node *n, vector const &C) { + if (!n || n->get_status() == status::closed) + return; + node *p = n->parent(); + if (p && all_of(C, [n](auto const &l) { return l != n->get_literal(); })) { + close_with_core(p, C); + return; } + close(n->left()); + close(n->right()); + n->set_core(C); + n->set_status(status::closed); + + if (!p) + return; + auto left = p->left(); + auto right = p->right(); + if (!left || !right) + return; + + // only attempt when both children are closed and each has a core + if (left->get_status() != status::closed || right->get_status() != status::closed) + return; + + auto resolvent = compute_sibling_resolvent(left, right); + close_with_core(p, resolvent); + } + + // Given complementary sibling nodes for literals x and ¬x, sibling resolvent = (core_left ∪ core_right) \ {x, + // ¬x} + vector compute_sibling_resolvent(node *left, node *right) { + vector res; + + auto &core_l = left->get_core(); + auto &core_r = right->get_core(); + + if (core_l.empty() || core_r.empty() || left->parent() != right->parent()) + return res; + + auto lit_l = left->get_literal(); + auto lit_r = right->get_literal(); + + for (auto const &lit : core_l) + if (lit != lit_l && !res.contains(lit)) + res.push_back(lit); + for (auto const &lit : core_r) + if (lit != lit_r && !res.contains(lit)) + res.push_back(lit); + return res; } public: - - tree(literal const& null_literal) : m_null_literal(null_literal) { + tree(literal const &null_literal) : m_null_literal(null_literal) { reset(); } @@ -177,51 +232,51 @@ namespace search_tree { m_root = alloc(node, m_null_literal, nullptr); m_root->set_status(status::active); } - + // Split current node if it is active. // After the call, n is open and has two children. - void split(node* n, literal const& a, literal const& b) { + void split(node *n, literal const &a, literal const &b) { n->split(a, b); } // conflict is given by a set of literals. - // they are a subset of literals on the path from root to n - void backtrack(node* n, vector const& conflict) { + // they are subsets of the literals on the path from root to n AND the external assumption literals + void backtrack(node *n, vector const &conflict) { if (conflict.empty()) { - close_node(m_root.get()); - m_root->set_status(status::closed); + close_with_core(m_root.get(), conflict); return; - } + } SASSERT(n != m_root.get()); // all literals in conflict are on the path from root to n // remove assumptions from conflict to ensure this. - DEBUG_CODE( - auto on_path = [&](literal const& a) { - node* p = n; - while (p) { - if (p->get_literal() == a) - return true; - p = p->parent(); - } - return false; - }; - SASSERT(all_of(conflict, [&](auto const& a) { return on_path(a); })); - ); - + DEBUG_CODE(auto on_path = + [&](literal const &a) { + node *p = n; + while (p) { + if (p->get_literal() == a) + return true; + p = p->parent(); + } + return false; + }; + SASSERT(all_of(conflict, [&](auto const &a) { return on_path(a); }));); + while (n) { - if (any_of(conflict, [&](auto const& a) { return a == n->get_literal(); })) { - close_node(n); + if (any_of(conflict, [&](auto const &a) { return a == n->get_literal(); })) { + // close the subtree under n (preserves core attached to n), and attempt to resolve upwards + close_with_core(n, conflict); return; } + n = n->parent(); } UNREACHABLE(); } // return an active node in the tree, or nullptr if there is none - // first check if there is a node to activate under n, + // first check if there is a node to activate under n, // if not, go up the tree and try to activate a sibling subtree - node* activate_node(node* n) { + node *activate_node(node *n) { if (!n) { if (m_root->get_status() == status::active) return m_root.get(); @@ -233,10 +288,10 @@ namespace search_tree { auto p = n->parent(); while (p) { - if (p->left() && p->left()->get_status() == status::closed && - p->right() && p->right()->get_status() == status::closed) { + if (p->left() && p->left()->get_status() == status::closed && p->right() && + p->right()->get_status() == status::closed) { p->set_status(status::closed); - n = p; + n = p; p = n->parent(); continue; } @@ -250,25 +305,28 @@ namespace search_tree { res = activate_from_root(p->left()); if (res) return res; - } + } n = p; p = n->parent(); } return nullptr; } - node* find_active_node() { + node *find_active_node() { return m_root->find_active_node(); } + vector const &get_core_from_root() const { + return m_root->get_core(); + } + bool is_closed() const { return m_root->get_status() == status::closed; } - std::ostream& display(std::ostream& out) const { + std::ostream &display(std::ostream &out) const { m_root->display(out, 0); return out; } - }; -} \ No newline at end of file +} // namespace search_tree