Three-tier nogood management system #213

EmirDe · 2025-06-24T16:11:21Z

I drafted a new nogood management strategy. The previous version was a "temporary" solution that stayed for too long; this version is supposed to be better.

There are a few changes:

This version implements the three-tier system for nogoods, this is the main change. This means that nogoods are partitioned into three categories (low-, mid-, and high-lbd), and the solver keeps them around for a different amount of time. Low-lbd are typically kept longer (most likely forever), high-lbd tier is temporary (similar to what we had before), whereas now there is also a mid-tier with lbds in between high and low, which is the main change compared to before.
The values for low-lbd is now 3, and high-lbd is 7 or greater. We might need to try out different values to see if there is any difference for CP benchmarks.
We now also delete some nogoods falsified at the root level. When cleaning up nogoods, if we happen to encounter a nogood falsified at the root level (one of its watchers is falsified at the root, or its cached predicate is falsified), then we will also remove that nogood. It could very well be the case that some nogoods are falsified, but we do not detect them in this pass (if we encounter that nogood later, its watchers will be updated so it will get removed later). We also do not simplify nogoods by removing true predicates, which could come later.

Can you please have a detailed look at the code, to see if something looks strange, e.g., does the code follow the comments?

In particular, there is an issue that surprises me, and where the tests fail. Have a look at the function are_watched_predicates_falsified_at_root_level. For some reason, when running the tests, getting a decision level for a predicate that is assigned fails - how is that possible?

ImkoMarijnissen · 2025-06-25T10:04:03Z

In particular, there is an issue that surprises me, and where the tests fail. Have a look at the function are_watched_predicates_falsified_at_root_level. For some reason, when running the tests, getting a decision level for a predicate that is assigned fails - how is that possible?

Currently, the function get_decision_level_for_predicate only returns the decision level of satisfied predicates; negating the falsified predicates before retrieving the decision level fixes the issue with the test cases

ImkoMarijnissen · 2025-06-25T10:18:23Z

pumpkin-solver/src/propagators/nogoods/nogood_propagator.rs

+                    .high_lbd
+                    .iter()
+                    .chain(self.learned_nogood_ids.mid_lbd.iter())
+                    .chain(self.learned_nogood_ids.low_lbd.iter())


The comments above states that low-lbd nogoods do not get their activities updated. Should it be rescaled here then?

good catch, I removed the iterator over low_lbd nogoods.

ImkoMarijnissen · 2025-06-25T11:03:48Z

pumpkin-solver/src/propagators/nogoods/nogood_propagator.rs

+    /// Learned nogoods are partitioned into three categories: high-, mid-, and low-lbd nogoods.
+    /// Each tier has a predefined limit on the number of nogoods it may store.
+    /// If a tier has more nogoods than the limit prescribes, roughly half of the nogoods from the
+    /// tier are removed. High- and mid-tier nogoods remove the least active nogoods, whereas


Is the sorting of low-tier nogoods based on the paper(s) or is this a design choice?

It is based on the paper listed right before this comment block. I tried to make this clear with the comments, can you have a look and let me know what was the issue?

ImkoMarijnissen · 2025-06-25T11:04:32Z

pumpkin-solver/src/propagators/nogoods/nogood_propagator.rs

+        context.is_predicate_falsified(watcher1)
+            && context
+                .assignments
+                .get_decision_level_for_predicate(&watcher1)


As stated in the comments, get_decision_level_for_predicate only works for satisfied predicates

Thank you, fixed!

p.s. "As stated in the comments" -> which comments? For me, there were no comments for get_decision_level_for_predicate for the propagation context. I did add a comment now.

ImkoMarijnissen · 2025-06-25T11:05:17Z

pumpkin-solver/src/propagators/nogoods/nogood_propagator.rs

-            else {
-                self.learned_nogood_ids.low_lbd.push(*id);
-                false
+    fn are_watched_predicates_falsified_at_root_level(


The name could be a bit more clear to indicate that it checks whether one of the watchers is falsified at the root

Fixed. Now called has_a_watched_predicate_falsified_at_root_level.

ImkoMarijnissen · 2025-06-25T11:11:58Z

pumpkin-solver/src/propagators/nogoods/nogood_propagator.rs

+        // We maintain a flag that signals if the process below will require another pass.
+        // This can happen when the cached predicate is falsified at the root level.
+        // Note that each nogood is watched twice.
+        // Since we do not know if this is the first or second watcher with this nogood,


This could be clarified a bit; what is meant by 'this', and the first or second watcher is a bit unclear. Maybe something like:

When we encounter a watcher where its cached predicate is falsified at the root, we mark it as deleted. However, we could have encountered the other watcher (with a different cached predicate) attached to this nogood prior to encountering this watcher with a falsified cached predicate ; to ensure that we delete this other watcher as well, we require another pass

Thank you, I updated the comment.

ImkoMarijnissen · 2025-06-25T11:12:51Z

pumpkin-solver/src/propagators/nogoods/nogood_propagator.rs

+                        == 0
+                {
+                    // Mark that a nogood has been deleted due to the cached predicate.
+                    another_pass_needed = true;


As we can retrieve what Predicate is being watched by the other watcher, perhaps we can do a more targeted deletion if this turns out to be a hotspot?

Can you clarify? Here the nogood is deleted because of the cached predicate, and not a watched predicate.

Note that the first time we delete based on a watched predicate, the nogood gets marked as deleted, so it never tests its watched predicates again.

ImkoMarijnissen · 2025-06-25T11:15:05Z

pumpkin-solver/src/propagators/nogoods/nogood_propagator.rs

+    fn promote_mid_lbd_nogoods(&mut self) {
+        self.learned_nogood_ids.mid_lbd.retain(|id| {
+            // Still a mid-tier nogood?
+            if self.nogood_info[*id].lbd > self.parameters.lbd_low {


Why is this a > in this function but a >= in the promote_high_lbd_nogoods case?

I added a comment in the if block. In short, the nogood is a mid-lbd nogood, so it is enough to test if it became a low-lbd nogood, otherwise it stays in the mid-lbd range.

Review re-requested

… database was done

maartenflippo

I think it looks good, but I would suggest making a refactoring. Can we separate a NogoodDatabase from the NogoodPropagator and have the database be a field on the propagator? At the moment, everything is in the propagator and it is extremely confusing to discern what is concerned with propagation and what is concerned with database management.

maartenflippo · 2025-06-25T13:32:22Z

pumpkin-solver/src/propagators/nogoods/nogood_propagator.rs

+    /// Nogoods can move from higher tiers to lower tiers if the lbd drops sufficiently low, but
+    /// not the other way around. This is the main difference regarding this aspect from the paper
+    /// "Improving Implementation of SAT Competitions 2017–2019 Winners".


Why can't low lbd go to high tiers? For completeness of this description we might want to include that. Right now, it seems a bit mysterious.

…dicate

EmirDe added 2 commits June 24, 2025 17:48

initial implementation of the three-tier nogood management system

5f58a87

renamed function

d69f35e

EmirDe requested review from maartenflippo and ImkoMarijnissen June 24, 2025 16:11

ImkoMarijnissen previously requested changes Jun 25, 2025

View reviewed changes

applied suggestions by Imko

ad1a3d1

EmirDe requested a review from ImkoMarijnissen June 25, 2025 12:32

Emir Demirović added 2 commits June 25, 2025 14:40

small comment about efficiency

e979e41

added code to prevent updating watchers when no cleanup of the nogood…

ecadc61

… database was done

maartenflippo reviewed Jun 25, 2025

View reviewed changes

ImkoMarijnissen added 2 commits June 25, 2025 15:59

fix: missed negation when retrieving decision level of propagated pre…

19e0210

…dicate

fix: propagating nogoods being deleted

33b87c1

Three-tier nogood management system #213

Are you sure you want to change the base?

Three-tier nogood management system #213

Conversation

EmirDe commented Jun 24, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ImkoMarijnissen commented Jun 25, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

maartenflippo left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

EmirDe commented Jun 24, 2025 •

edited

Loading