mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-19 00:38:57 +00:00
Code Activity

Add core strengthening and non-chronological backtracking to parallel search tree (#8193)

Browse source 
* 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>
This commit is contained in:
Ilana Shapiro 2026-01-15 11:49:18 -08:00 • committed by GitHub
parent 7d4964a2f0
commit 1d1fc69be3
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 66 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

78
src/util/search_tree.h
View file

@ -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,