Skip to content

feat: Add a new nogood management scheme, replacing the tiered system #455

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Hubert1913 wants to merge 4 commits into
base: main
Choose a base branch
from
Open

feat: Add a new nogood management scheme, replacing the tiered system #455

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
569fbbf
feat: add a new nogood management scheme, replacing the tiered system
Hubert1913 May 25, 2026
4d1f420
Improve documentation based on PR feedback
Hubert1913 May 31, 2026
6da2a05
Simplify way of marking which nogoods are retained
Hubert1913 May 31, 2026
46efb60
Move nogoods sorted on activity to a temporary buffer
Hubert1913 May 31, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
44 changes: 11 additions & 33 deletions pumpkin-crates/core/src/propagators/nogoods/learning_options.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,34 +6,14 @@ pub struct LearningOptions {
pub max_activity: f32,
/// Determines the factor by which the activities are divided when a conflict is found.
pub activity_decay_factor: f32,
/// The solver partitions the nogoods into three tiers.
///
/// This limit specifies how many nogoods can be stored in the "high" LBD tier.
pub max_num_high_lbd_nogoods: usize,
/// The solver partitions the nogoods into three tiers.
///
/// This limit specifies how many nogoods can be stored in the "mid" LBD tier.
pub max_num_mid_lbd_nogoods: usize,
/// The solver partitions the nogoods into three tiers.
///
/// This limit specifies how many nogoods can be stored in the "low" LBD tier.
pub max_num_low_lbd_nogoods: usize,
/// Used to determine which tier a nogood belongs in.
///
/// If the LBD of a nogood is higher than or equal to this threshold then it is considered to
/// be a "high" LBD nogood.
///
/// If the LBD of a nogood is between [`LearningOptions::lbd_threshold_high`] and
/// [`LearningOptions::lbd_threshold_low`] then it is considered a "mid" LBD nogood.
pub lbd_threshold_high: u32,
/// Used to determine which tier a nogood belongs in.
///
/// If the LBD of a nogood is lower than or equal to this value then it is considered to be a
/// "low" LBD nogood.
///
/// If the LBD of a nogood is between [`LearningOptions::lbd_threshold_high`] and
/// [`LearningOptions::lbd_threshold_low`] then it is considered a "mid" LBD nogood.
pub lbd_threshold_low: u32,
/// The maximum number of nogoods that the solver stores.
pub current_max_num_nogoods: usize,
/// The factor by which the maximum number of nogoods is increased after each database
/// reduction. For the database to grow, it should be greater than 1. For example, the
/// default value of 1.1 means the database grows by 10% (e.g. 40_000 -> 44_000).
pub max_num_nogoods_increment: f32,
Comment on lines +11 to +14

@ImkoMarijnissen ImkoMarijnissen May 27, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

/// The upper limit for the number of stored nogoods.
pub num_nogoods_upper_limit: usize,
/// Specifies by how much the activity is increased when a nogood is bumped.
pub activity_bump_increment: f32,
}
Expand All @@ -42,11 +22,9 @@ impl Default for LearningOptions {
Self {
max_activity: 1e20,
activity_decay_factor: 0.99,
max_num_high_lbd_nogoods: 20000,
max_num_mid_lbd_nogoods: 7000,
max_num_low_lbd_nogoods: 100000,
lbd_threshold_high: 7,
lbd_threshold_low: 3,
current_max_num_nogoods: 40000,
max_num_nogoods_increment: 1.1,
Comment on lines +25 to +26

@ImkoMarijnissen ImkoMarijnissen May 27, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

@Hubert1913 Hubert1913 May 31, 2026

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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:
image
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:
image
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.

num_nogoods_upper_limit: 1_000_000_000,
activity_bump_increment: 1.0,
}
}
Expand Down
Loading