From b1b7270686001932fecd19adb2de3a95faf3db3b Mon Sep 17 00:00:00 2001 From: Ilana Shapiro Date: Fri, 16 Jan 2026 10:41:13 -0800 Subject: [PATCH] Fix UNKNOWN bug in search tree about inconsistent end state (#8214) * restore more aggressive pruning in search tree * restore where we close children to be correct * add core strengthening check * fix recursion bug * less strict core propagation * old search tree version * restore search tree patch * remove flag * debugging inconsistent end state with search, some changes need to be made in search tree, only backtrack should be closing nodes, I think the bug is when we do find_highest_attach for nonchronological backjumping, you might get to a point where the sibling is closed, so then we need to resolve further up the tree * clean up code, fix deadlock * delete test files * clean up --------- Co-authored-by: Ilana Shapiro Co-authored-by: Ilana Shapiro Co-authored-by: Ilana Shapiro --- src/smt/smt_parallel.cpp | 1 + src/util/search_tree.h | 51 ++++++++++++++++++++++++++++++++++------ 2 files changed, 45 insertions(+), 7 deletions(-) diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 29915ce6d..178bbcf3d 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -276,6 +276,7 @@ namespace smt { IF_VERBOSE(1, m_search_tree.display(verbose_stream() << bounded_pp_exprs(core) << "\n");); if (m_search_tree.is_closed()) { + IF_VERBOSE(1, verbose_stream() << "Search tree closed, setting UNSAT\n"); m_state = state::is_unsat; SASSERT(p.ctx.m_unsat_core.empty()); for (auto e : m_search_tree.get_core_from_root()) diff --git a/src/util/search_tree.h b/src/util/search_tree.h index 449d77703..04a222066 100644 --- a/src/util/search_tree.h +++ b/src/util/search_tree.h @@ -89,7 +89,7 @@ namespace search_tree { node *find_active_node() { if (m_status == status::active) return this; - if (m_status != status::open) + if (m_status == status::closed) return nullptr; node *nodes[2] = {m_left, m_right}; for (unsigned i = 0; i < 2; ++i) { @@ -132,7 +132,6 @@ namespace search_tree { random_gen m_rand; // 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) { if (!n) return nullptr; @@ -152,8 +151,6 @@ 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); return nullptr; } @@ -190,6 +187,39 @@ namespace search_tree { return attach_here; } + // Propagate closure upward via sibling resolution starting at node `cur`. + // Returns true iff global UNSAT was detected. + bool propagate_closure_upward(node* cur) { + while (true) { + node* parent = cur->parent(); + if (!parent) + return false; + + auto left = parent->left(); + auto right = parent->right(); + if (!left || !right) + return false; + + if (left->get_status() != status::closed || + right->get_status() != status::closed) + return false; + + if (left->get_core().empty() || + right->get_core().empty()) + return false; + + auto res = compute_sibling_resolvent(left, right); + + if (res.empty()) { + close(m_root.get(), res); // global UNSAT + return true; + } + + close(parent, res); + cur = parent; // keep bubbling + } + } + void close(node *n, vector const &C) { if (!n || n->get_status() == status::closed) return; @@ -245,6 +275,11 @@ namespace search_tree { auto attach = find_highest_attach(p, resolvent); close(attach, resolvent); + + // try to propagate the highest attach node upward *with sibling resolution* + // this handles the case when non-chronological backjumping takes us to a node whose sibling was closed by another thread + node* cur = attach; + propagate_closure_upward(cur); } // Given complementary sibling nodes for literals x and ¬x, sibling resolvent = (core_left ∪ core_right) \ {x, @@ -312,6 +347,7 @@ namespace search_tree { }; SASSERT(all_of(conflict, [&](auto const &a) { return on_path(a); }));); + // Walk upward to find the nearest ancestor whose decision participates in the conflict while (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 @@ -339,9 +375,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) { - p->set_status(status::closed); + if (p->left() && p->left()->get_status() == status::closed && + p->right() && p->right()->get_status() == status::closed) { + if (p->get_status() != status::closed) + return nullptr; // inconsistent state n = p; p = n->parent(); continue;