From f5fc7eb173ae09af2eb75cf7daab7d82f860ec51 Mon Sep 17 00:00:00 2001
From: Ilana Shapiro <ishapiro00@gmail.com>
Date: Thu, 15 Jan 2026 11:49:18 -0800
Subject: [PATCH] Add core strengthening and non-chronological backtracking to
 parallel search tree (#8193)

* 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

---------

Co-authored-by: Ilana Shapiro <ilanashapiro@Mac.localdomain>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MacBook-Pro.local>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MBP.lan1>
---
 src/util/search_tree.h | 78 +++++++++++++++++++++++++++++++++++-------
 1 file changed, 66 insertions(+), 12 deletions(-)

diff --git a/src/util/search_tree.h b/src/util/search_tree.h
index ae70bd675..0856e9e15 100644
--- a/src/util/search_tree.h
+++ b/src/util/search_tree.h
@@ -157,29 +157,77 @@ namespace search_tree {
             return nullptr;
         }
 
-        void close(node<Config> *n) {
+        // Bubble to the highest ancestor where ALL literals in the resolvent
+        // are present somewhere on the path from that ancestor to root
+        node<Config>* find_highest_attach(node<Config>* p, vector<literal> const& resolvent) {
+            node<Config>* candidate = p;
+            node<Config>* attach_here = p;
+
+            while (candidate) {
+                bool all_found = true;
+
+                for (auto const& r : resolvent) {
+                    bool found = false;
+                    for (node<Config>* q = candidate; q; q = q->parent()) {
+                        if (q->get_literal() == r) {
+                            found = true;
+                            break;
+                        }
+                    }
+                    if (!found) {
+                        all_found = false;
+                        break;
+                    }
+                }
+
+                if (all_found) {
+                    attach_here = candidate;  // bubble up to this node
+                }
+
+                candidate = candidate->parent();
+            }
+
+            return attach_here;
+        }
+
+        void close(node<Config> *n, vector<literal> const &C) {
             if (!n || n->get_status() == status::closed)
                 return;
             n->set_status(status::closed);
-            close(n->left());
-            close(n->right());
+            n->set_core(C);
+            close(n->left(), C);
+            close(n->right(), C);
         }
 
         // 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<Config> *n, vector<literal> const &C) {
-            if (!n || n->get_status() == status::closed)
+            if (!n)
                 return;
+
+            // If the node is closed AND has a stronger or equal core, we are done. 
+            // Otherwise, closed nodes may still accept a different (stronger) core to enable pruning/resolution higher in the tree.
+            auto subseteq = [](vector<literal> const& A, vector<literal> const& B) {
+                for (auto const& a : A)
+                    if (!B.contains(a))
+                        return false;
+                return true;
+            };
+            if (n->get_status() == status::closed && subseteq(n->get_core(), C))
+                return;
+
             node<Config> *p = n->parent();
+
+            // The conflict does NOT depend on the decision literal at node n, so n’s split literal is irrelevant to this conflict
+            // thus the entire subtree under n is closed regardless of the split, so the conflict should be attached higher, at the nearest ancestor that does participate
             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);
+            
+            // Close descendants WITHOUT resolving
+            close(n, C);
 
             if (!p)
                 return;
@@ -188,12 +236,18 @@ namespace search_tree {
             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;
+            // only attempt when both children are closed and each has a *non-empty* core
+            if (left->get_status() != status::closed || right->get_status() != status::closed) return;
+            if (left->get_core().empty() || right->get_core().empty()) return;
 
             auto resolvent = compute_sibling_resolvent(left, right);
-            close_with_core(p, resolvent);
+            if (resolvent.empty()) { // empty resolvent => global UNSAT
+                close(m_root.get(), resolvent);
+                return;
+            }
+
+            auto attach = find_highest_attach(p, resolvent);
+            close(attach, resolvent);
         }
 
         // Given complementary sibling nodes for literals x and ¬x, sibling resolvent = (core_left ∪ core_right) \ {x,