feat: Add a new nogood management scheme, replacing the tiered system by Hubert1913 · Pull Request #455 · ConSol-Lab/Pumpkin

Hubert1913 · 2026-05-25T13:53:36Z

Replaces the tiered nogood management system with one that follows the scheme of "sort all nogoods using a heuristic and remove the worse half". During reductions, it keeps nogoods that have either relatively low LBD or high activity, while trying to give these metrics equal priority - half of the retained nogoods are chosen because they had low LBD and the other half because they had high activity.

The behaviour can be controlled via three parameters:

--learning-initial-max-num-nogoods - specifies the number of nogoods at which the first database reduction occurs. Default:40_000
--learning-max-num-nogoods-increment - specifies the factor by which the maximal number of nogoods is increased after each reduction. Default: 1.1 (meaning it grows by 10%, e.g. 40000 -> 44000 after the first reduction)
--learning-num-nogoods-upper-limit - specifies the upper limit for the database size (the size is not increased above this limit). Default: 1_000_000_000 (meaning that this limit is not applied in practice). It might be beneficial to lower this limit in some cases, especially when solving satisfaction instances.

ImkoMarijnissen · 2026-05-27T09:23:56Z

I evaluated on MiniZic instances and got the following results:

Overall

main:

{'ERROR': 44,
 'OPTIMAL': 103,
 'SATISFIABLE': 147,
 'UNKNOWN': 94,
 'UNSATISFIABLE': 5}

new-nogood-management-scheme:

{'ERROR': 34,
 'OPTIMAL': 108,
 'SATISFIABLE': 152,
 'UNKNOWN': 94,
 'UNSATISFIABLE': 5}

MiniZinc Scoring

{
    'main': 130.94
    'new-nogood-management-scheme': 140.06, 
}

Average Primal Integral

{
    'main': 46.04
    'new-nogood-management-scheme': 33.93, 
}

Conclusions

The new management strategy appears to work better than what we currently have. The overall results indicate that most of the advancement comes from instances for which we used to run out of memory (falling in the ERROR class). Both the MiniZinc scoring and primal integral indicate that it indeed performs better!

If I remember correctly, then @maartenflippo did/was planning to review the code.

ImkoMarijnissen

Overall, this looks good, thank you for making the PR!

I have some questions and potential requests for changes.

ImkoMarijnissen · 2026-05-27T09:36:00Z

+    /// The factor by which the maximum number of nogoods is increased after each database
+    /// reduction
+    pub max_num_nogoods_increment: f32,


It would be good to add the text that you added in the PR here, explaining hwo it is used

ImkoMarijnissen · 2026-05-27T09:36:48Z

+            current_max_num_nogoods: 40000,
+            num_nogoods_upper_limit: 1_000_000_000,
+            max_num_nogoods_increment: 1.1,


Is there any reasoning for these numbers? Especially num_nogoods_upper_limit seems to be significantly higher than the maximum number of nogoods that we allowed previously

Initially, I chose these values as a blend of parameters used in several solvers. The fact that num_nogoods_upper_limit is so high is just a workaround to let the database grow without any limits (as we definitely won't hit a billion stored nogoods).

I also did a quick comparison of performance using different parameters:

The naming here corresponds to {current_max_num_nogoods}_{max_num_nogoods_increment}_{num_nogoods_upper_limit}

It turned out that the initial values were quite good. Potentially lowering current_max_num_nogoods to 10_000 (first row in the table) could be better, as it solved more instances. However, it had more conflicts, both when using the arithmetic mean in the table above, and when comparing versions on a per-instance basis and combining using the geometric mean:

At the same time, this increase in conflicts is expected, as the lower current_max_num_nogoods means we perform reductions earlier, so we likely have to "re-learn" more nogoods at the beginning of solving. So I am not entirely sure which of these is better, given the fluctuating runtime on DelftBlue.

ImkoMarijnissen · 2026-05-27T09:40:44Z

+        // However, it could also happen that the same nogood is retained because of its activity
+        // before it is considered for LBD (depending on values of other nogoods). So it is likely
+        // that the order in which LBD and activity are considered does not have much influence.


Has this been empirically evaluated or is this an intuition? It seems like this could have a noticeable influence on the budget for the different metrics.

It is an intuition. In theory, I think one metric could get more "priority" in a given reduction, for example, suppose that we reduce when having 8 nogoods, then the 4 nogoods we might end up with could be ranked 1st, 8th, 2nd, 7th by LBD and 1st, 2nd, 3rd, 4th by activity (correspondingly), thus giving activity more "budget". However, it is equally easy to construct an example in which LBD gets an advantage.

These examples are also highly specific, so intuitively, I think that in practice, with a much bigger database, these differences in budget get evened out.

ImkoMarijnissen · 2026-05-27T09:46:59Z

+            // Sort learned nogoods increasingly based on LBD
+            self.learned_nogood_ids.sort_unstable_by(|id1, id2| {
+                let nogood1 = &self.nogood_info[self.nogood_predicates.get_nogood_index(id1)];
+                let nogood2 = &self.nogood_info[self.nogood_predicates.get_nogood_index(id2)];
+                nogood1.lbd.cmp(&nogood2.lbd)
+            });

-            // Sort the "mid" LBD nogood by activity
-            NogoodPropagator::sort_nogoods_by_decreasing_activity(
-                &mut self.learned_nogood_ids.mid_lbd,
-                &self.nogood_info,
-                &self.nogood_predicates,
-            );
+            // Clone the nogoods to sort them descendingly on activity
+            let mut sorted_on_activity = self.learned_nogood_ids.clone();
+            sorted_on_activity.sort_unstable_by(|id1, id2| {
+                let nogood1 = &self.nogood_info[self.nogood_predicates.get_nogood_index(id1)];
+                let nogood2 = &self.nogood_info[self.nogood_predicates.get_nogood_index(id2)];
+                nogood2.activity.partial_cmp(&nogood1.activity).unwrap()
+            });


Several points:

Could keep a temporary buffer to prevent reallocation (similar for nogoods_to_keep).

Is this better than sorting only once and doing tie-breaking based on a set preference (e.g., if we have two nogoods, one has lower LBD and the other has higher activity, then we tie-break based on the size of the nogood)?

I added a self.temp_nogood_ids - I hope that's what you meant (btw, I'm open to suggestions if you have an idea for a better name). nogoods_to_keep got dropped (as mentioned in one of the other comments).

I'm not sure if I understand what you mean. Are you proposing a scheme where Nogood A is 'better' than Nogood B if it has both lower LBD and higher activity, and when these metrics don't agree, then we use a third one to tie-break?
If so, then my scheme is doing something slightly different - it doesn't necessarily choose nogoods that are 'good' according to both metrics, e.g. a nogood might be kept if it has poor LBD but exceptionally high activity. Instead, we are looking for nogoods that are 'very good' in at least one of the metrics.
I did test a similar scheme to what you proposed. It wasn't exactly the same, as I flipped the notion of keep nogoods that are good in both metrics into remove nogoods that are poor in at least one of the metrics (so I still sorted the list twice, and didn't use any third metric for tie-breaking). This scheme performed worse, solving fewer instances, with more conflicts.

ImkoMarijnissen · 2026-05-27T09:49:06Z

+                // First we find a nogood to keep according to LBD
+                // Skip all nogoods that are already retained
+                while lbd_index < num_all_nogoods
+                    && nogoods_to_keep.contains(&self.learned_nogood_ids[lbd_index])


Could set this as a flag in nogood_info (and then reset at the beginning since you are already going through all nogood ids anyways); this way, you do not need to store nogoods_to_keep and you do not need to keep doing hash lookups.

I thought about adding a is_kept flag, but decided that using a HashSet would be cleaner to understand.

Now I realised that this can be done with just the is_deleted flag - setting it to true for all nogoods at the beginning and then resetting to false for the retained ones.

ImkoMarijnissen · 2026-05-27T09:52:04Z

+        for nogood_id in self.learned_nogood_ids.iter().skip(lbd_index) {
+            if !nogoods_to_keep.contains(nogood_id) {
+                self.nogood_info[self.nogood_predicates.get_nogood_index(nogood_id)].is_deleted =
+                    true;
+            }
        }


Can we not remove them directly here? What is the reason for keeping this in two separate loops?

I think I didn't want to remove elements while iterating through the vector, or maybe I just didn't connect the dots.

Either way, the removal of to_keep means this loop is gone as well.

ImkoMarijnissen · 2026-05-27T09:53:34Z

+        if self.parameters.current_max_num_nogoods > self.parameters.num_nogoods_upper_limit {
+            self.parameters.current_max_num_nogoods = self.parameters.num_nogoods_upper_limit;
+        }


I would suggest self.parameters.current_max_num_nogoods = self.parameters.current_max_num_nogoods.min(self.parameters.num_nogoods_upper_limit)

ImkoMarijnissen · 2026-05-27T09:54:50Z

-    ///
-    /// Learned nogoods are kept based on the tiered system introduced in "Improving
-    /// SAT Solvers by Exploiting Empirical Characteristics of CDCL - Chanseok Oh (2016)".
+    /// The initial max number of learned nogoods that are initially kept in the database


Double usage of initial

ImkoMarijnissen · 2026-05-27T09:55:50Z

+    /// The initial max number of learned nogoods that are initially kept in the database
    ///
    /// Possible values: usize
    #[arg(
-        long = "learning-max-num-high-lbd-nogoods",
-        default_value_t = 20_000,
+        long = "learning-initial-max-num-nogoods",
+        default_value_t = 40_000,
        verbatim_doc_comment
    )]
-    learning_max_num_high_lbd_nogoods: usize,
+    learning_initial_max_num_nogoods: usize,

-    /// The number of mid-lbd learned nogoods that are kept in the database.
-    ///
-    /// This is based on the variation of the three-tiered system proposed in
-    /// "Improving Implementation of SAT Competitions 2017–2019 Winners".
+    /// The factor with which the max number of stored nogoods is multiplied
+    /// after each database reduction
    ///
-    /// Possible values: usize
+    /// Possible values: f32
    #[arg(
-        long = "learning-max-num-mid-lbd-nogoods",
-        default_value_t = 7000,
+        long = "learning-max-num-nogoods-increment",
+        default_value_t = 1.1,
        verbatim_doc_comment
    )]
-    learning_max_num_mid_lbd_nogoods: usize,
+    learning_max_num_nogoods_increment: f32,

-    /// The number of low-lbd learned nogoods that are kept in the database.
-    ///
-    /// This is based on the variation of the three-tiered system proposed in
-    /// "Improving Implementation of SAT Competitions 2017–2019 Winners".
+    /// The upper limit for the nogoods database size (growth stops at this value)


Pet peeve: please put a . at the end of sentences in documentation.

Hubert1913 · 2026-05-31T23:16:59Z

@ImkoMarijnissen Thanks for the review and performance comparison!

The overall results indicate that most of the advancement comes from instances for which we used to run out of memory

Are the out-of-memory errors because ArenaAllocator doesn't actually remove nogoods from memory? Because my version definitely keeps more nogoods in self.learned_nogood_ids on bigger instances than the tiered system. So this would mean that the current scheme removes nogoods too aggressively, and needs to re-learn many of them (potentially several times), cluttering the memory, right?

feat: add a new nogood management scheme, replacing the tiered system

569fbbf

ImkoMarijnissen requested changes May 27, 2026

View reviewed changes

Hubert1913 added 3 commits May 31, 2026 20:24

Improve documentation based on PR feedback

4d1f420

Simplify way of marking which nogoods are retained

6da2a05

Move nogoods sorted on activity to a temporary buffer

46efb60

Conversation

Hubert1913 commented May 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ImkoMarijnissen commented May 27, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Overall

MiniZinc Scoring

Average Primal Integral

Conclusions

Uh oh!

ImkoMarijnissen left a comment

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!

Choose a reason for hiding this comment

Uh oh!

Hubert1913 commented May 31, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Hubert1913 commented May 25, 2026 •

edited

Loading

ImkoMarijnissen commented May 27, 2026 •

edited

Loading