feat: implement extended nogood propagation and CPIP nogood learning by ImkoMarijnissen · Pull Request #454 · ConSol-Lab/Pumpkin

ImkoMarijnissen · 2026-05-21T10:20:53Z

Based on the paper "From Literals to Atomic Constraints: Generalising Conflict-Driven Clause Learning for Constraint Programming - Imko Marijnissen, Maarten Flippo, and Emir Demirović" (to appear at CP'26), I have implemented the extended nogood propagation and CPIP nogood learning.

Overview

The PR consists of the following:

Adjusting the ResolutionResolver to be able to produce CPIP nogoods; this involves updating the stopping criterion for resolving and the structure LearnedNogood to ensure certain invariants.
Adjusting the NogoodPropagator in several ways:
When adding a(n) (asserting) nogood, the watchers need to be placed on atomic constraints over different variables, and the detection of propagation, which can take place at the root level, is adjusted.
When propagating, the watcher structure is different between the two approaches so this has been adjusted
I implemented extended nogood propagation based on the algorithm described in the paper.

This supersedes the branch feat/extended-conflict-analysis in several ways:

It now uses lazy explanations for the propagation
It also performs nogood database management; this is based on the original (SAT-based) strategy. This could be adjusted in the future since LBD could be uninformative.

Feedback

The main point I would like feedback on is whether it makes sense to keep the 1UIP + unit propagation and CPIP + extended nogood propagation approaches merged or whether it would be preferable to be separated into their own structs. I have kept it this way to be able to clearly see the differences between the two, but I can imagine that this does not make the code clearer.

Additionally, do we want to include testing this feature in the CI or is that unnecessary?

@maartenflippo I ran into the issue that retrieving from unit_nogood_inference_codes when using CPIP + extended nogood propagation led to some issues. I have resolved this in a way but it would be good to hear your opinion on this!

Experimentation

I tested the extended nogood propagation + CPIP learning using different priority schemes. The (Updated) instances are the ones where incremental stopping condition calculation is included.

Overall Results

1UIP + High Priority:

{'ERROR': 42,
 'OPTIMAL': 100,
 'SATISFIABLE': 153,
 'UNKNOWN': 93,
 'UNSATISFIABLE': 5}

CPIP with Extended Nogood Propagation + High Priority:

{'ERROR': 43,
 'OPTIMAL': 95,
 'SATISFIABLE': 156,
 'UNKNOWN': 94,
 'UNSATISFIABLE': 5}

CPIP with Extended Nogood Propagation + High Priority (Updated):

{'ERROR': 48,
 'OPTIMAL': 101,
 'SATISFIABLE': 146,
 'UNKNOWN': 93,
 'UNSATISFIABLE': 5}

1UIP + Very Low Priority:

{'ERROR': 43,
 'OPTIMAL': 101,
 'SATISFIABLE': 151,
 'UNKNOWN': 93,
 'UNSATISFIABLE': 5}

CPIP with Extended Nogood Propagation + Very Low Priority:

{'ERROR': 43,
 'OPTIMAL': 97,
 'SATISFIABLE': 154,
 'UNKNOWN': 94,
 'UNSATISFIABLE': 5}

CPIP with Extended Nogood Propagation + Very Low Priority (Updated):

{'ERROR': 32,
 'OPTIMAL': 99,
 'SATISFIABLE': 167,
 'UNKNOWN': 90,
 'UNSATISFIABLE': 5}

MiniZinc Scoring

{
    '1UIP + High Priority': 641.0,
    'CPIP + High Priority': 670.71,
    'CPIP + High Priority (Updated)': 653.61,
    '1UIP + Very Low Priority': 652.35,
    'CPIP + Very Low Priority': 698.09,
    'CPIP + Very Low Priority (Updated)': 708.24,
}

Average Primal Integral

{
    '1UIP + High Priority': 63.18,
    'CPIP + High Priority': 64.09,
    'CPIP + High Priority (Updated)': 69.13,
    '1UIP + Very Low Priority': 68.44,
    'CPIP + Very Low Priority': 63.37,
    'CPIP + Very Low Priority (Updated)': 46.45,
}

Overall Conclusions

In terms of the number of instances solved, 1UIP with a Very Low Priority appears to be best. However, looking at the MiniZinc scoring, both of the CPIP approaches outperform their 1UIP counterparts, with CPIP + Very Low priority performing the best. For the primal integral, the results are more mixed, with CPIP + Very Low Priority having the best anytime performance. This appears to indicate that CPIP has some better anytime performance compared to 1UIP learning (when using a very low priority of the nogood propagator). I think it would be better to keep the 1UIP as the default since I would expect 1UIP to outperform when using free search.

After Update: It appears that while 1UIP + Very Low Priority is generally the best at proving optimality, CPIP + Very Low Priority (Updated) proves optimality on a similar number of instances while providing solutions on 16 more. Additionally, the MiniZinc score of this approach is significantly higher, and the primal integral is significantly lower.

TODO

Rerun the experimentation to determine the impact of the changes
Calculate the stopping condition for learning CPIP nogoods incrementally rather than recalculating from scratch in every iteration

…ed UIP + adding some small docs

…docs

…ysis

…xplanations

This reverts commit c434a87.

maartenflippo

I started doing an in-depth review but got lost, so I am pausing here for a moment.

My overall impression of this PR so far is that it is incredibly hard to understand what is going on. Both in the propagator and the resolver. This is because two very different analysis and propagation routines are merged into one. I understand that there would be a lot of duplication, but this is almost impossible to understand in a code review.

The main point I would like feedback on is whether it makes sense to keep the 1UIP + unit propagation and CPIP + extended nogood propagation approaches merged or whether it would be preferable to be separated into their own structs. I have kept it this way to be able to clearly see the differences between the two, but I can imagine that this does not make the code clearer.

Depending on the results of the experiment, I think we may simply want to remove the one we do not use... However, if we want to keep everything, we definitely want to find a different way to structure it. Perhaps we can do a zoom meeting at some point to talk about how we can do this?

Additionally, do we want to include testing this feature in the CI or is that unnecessary?

Yes, we do. Now we are not running it so I cannot see whether this works or not. I expect it to fail at least on test cases where we run the solver + processor + checker, as the new propagation rule is not covered by our unit propagation inference rule in the proof.

@maartenflippo I ran into the issue that retrieving from unit_nogood_inference_codes when using CPIP + extended nogood propagation led to some issues. I have resolved this in a way but it would be good to hear your opinion on this!

I think I found the place you talk about here. I left a comment, there as well, but I think it is not right. Yet, running with proof logging should clarify a lot.

maartenflippo · 2026-05-22T01:22:07Z

-#[derive(Debug, Clone, Copy, Default)]
-/// Determines which type of learning is performed by the [`ResolutionResolver`].
-pub enum AnalysisMode {
-    #[default]
-    /// Standard conflict analysis which returns as soon as the first unit implication point is
-    /// found (i.e. when a nogood is created which only contains a single predicate from the
-    /// current decision level)
-    OneUIP,
-    /// An alternative to 1-UIP which stops as soon as the learned nogood only creates decision
-    /// predicates.
-    AllDecision,
-}


This I don't want to remove. The ConflictResolverType may have a bunch of other variants that have nothing to do with the resolution resolver (e.g. no-learning or the hypercube linear resolver).

maartenflippo · 2026-05-22T01:24:56Z

@@ -179,8 +177,87 @@ impl ResolutionResolver {
        // level, and both will be decisions. This is accounted for below.
        while {
            match self.mode {


... can we not? 😅 Please, extract this into its own function or something...

On a serious note: Keeping the AnalysisMode here would be a good idea. We can give it an associated function keep_resolving(...) -> bool.

maartenflippo · 2026-05-22T01:27:18Z

+            | ConflictResolverType::BoundsExtendedCPIP => dec_level == context.get_checkpoint(),
+            ConflictResolverType::AllDecision => !context.is_decision_predicate(predicate),
+            ConflictResolverType::NoLearning => unreachable!(),
        } {


This could also be a function on AnalysisMode

maartenflippo · 2026-05-22T01:36:58Z

+    #[allow(unused, reason = "Will be reintroduced with database management")]
    handle: PropagatorHandle<NogoodPropagator>,
+
+    analysis_mode: ConflictResolverType,


I feel this should be a separate type here. Make it specific to what the variants are that this propagator supports, and remove any unreachable branches.

maartenflippo · 2026-05-22T01:38:17Z

+impl Eq for Watcher {}
+
+impl PartialEq for Watcher {
+    fn eq(&self, other: &Self) -> bool {
+        self.nogood_id.eq(&other.nogood_id)
+    }
+}


I am afraid this could shoot us in the foot later on. In case we want to write e.g. tests around this, the equality behavior is not what we expect. Instead perhaps we can introduce a method on the Wathcer that tests for this type of equality instead?

maartenflippo · 2026-05-22T01:40:09Z

        code: u64,
        mut context: ExplanationContext,
    ) -> LazyExplanation<'_> {
+        if (code >> 32) > 0 {


What is going on here? Can we make use of a bitstruct (like e.g. the element propagator) if we are packing fields into a u64?

maartenflippo · 2026-05-22T01:41:45Z

+        for predicate in nogood.iter().filter_map(|&predicate_id| {
+            // First, we filter out all of the predicates which are currently satisfied and
+            // which are not concerning the propagated domain id
+            let predicate = context.get_predicate(predicate_id);
+
+            is_falsified |= context.is_predicate_id_falsified(predicate_id);
+
+            pumpkin_assert_moderate!(
+                predicate.get_domain() == propagated_domain
+                    || context.is_predicate_id_satisfied(predicate_id),
+                "Expected {predicate} to be unassigned with {propagated_domain:?}; nogood: {:?}",
+                nogood
+                    .iter()
+                    .map(|predicate_id| {
+                        let predicate = context.get_predicate(*predicate_id);
+
+                        (
+                            predicate,
+                            context.lower_bound(&predicate.get_domain()),
+                            context.upper_bound(&predicate.get_domain()),
+                        )
+                    })
+                    .collect::<Vec<_>>()
+            );
+
+            (!context.is_predicate_id_satisfied(predicate_id)
+                && predicate.get_domain() == propagated_domain)
+                .then_some(predicate)
+        }) {


Please pull this out into a named binding

maartenflippo · 2026-05-22T01:48:08Z

+                let unit_ic = unit_nogood_inference_codes.get(&predicate).or_else(|| {
+                    // It could be the case that we attempt to get the reason for the predicate
+                    // [x >= v] but that the corresponding unit nogood idea is the one for the
+                    // predicate [x == v]
+                    let domain_id = predicate.get_domain();
+                    let right_hand_side = predicate.get_right_hand_side();
+
+                    unit_nogood_inference_codes.get(&predicate!(domain_id == right_hand_side))
+                });
+
+                if let Some(unit_ic) = unit_ic {
+                    let _ = proof_log.log_inference(
+                        &mut state.constraint_tags,
+                        unit_ic.clone(),
+                        [],
+                        Some(predicate),
+                        &state.variable_names,
+                        &state.assignments,
+                    );
+                } else {
+                    // Otherwise we log the inference which was used to derive the nogood
+                    let _ = proof_log.log_inference(
+                        &mut state.constraint_tags,
+                        ic.clone(),
+                        reason_buffer.as_ref().iter().copied(),
+                        Some(predicate),
+                        &state.variable_names,
+                        &state.assignments,
+                    );
+                }


I doubt whether this is correct, but running with proof checking on should make that obvious.

Interestingly, running the test suite with the extended nogood propagation and CPIP passes all test cases after this change; any idea what could be going wrong? Should I try to create the proof and process it manually?

…ion can take place

…d for calculating info about domain

ImkoMarijnissen · 2026-05-27T08:03:40Z

After discussion with @maartenflippo:

Remove ExtendedOneUIP
Separate propagation and learning enum (keep original enum in solver flags)

… extended nogood propagation

EmirDe · 2026-05-28T06:58:45Z

What is the status of this, is it ready for review/finalised?

ImkoMarijnissen · 2026-05-28T07:12:08Z

What is the status of this, is it ready for review/finalised?

@EmirDe It should indeed be ready to be reviewed. I need to discuss with Maarten how this interacts with proof logging, but the functionality should be there.

ImkoMarijnissen added 30 commits December 17, 2025 11:21

feat: first version of extended propagation

b724421

Merge branch 'main' into feat/extended-conflict-analysis

e96b8bd

docs: add explanation to propagation approach for posterity

9dd1140

feat: adding initial simple version of extended UIP

349d5e9

feat: adding differentation between full extended UIP and half extend…

8fc657c

…ed UIP + adding some small docs

refactor: remove database management from both approaches + updating …

f31e485

…docs

refactor: use pattern matching for analysis mode in nogood propagator

02d6e96

feat: adding bounds-propagation only option to extended conflict anal…

45e9f08

…ysis

refactor: update backup brancher to be more deterministic

b127aa7

feat: more statistics about propagation

0a1c069

feat: include more statistics

5120112

feat: more statistics

a3c8934

fix: improper setting of bounds

add92c2

refactor: update to take into account semantic and unit propagation

5cd87aa

feat: first attempt at two-watcher scheme

571bb03

chore: cleanup + adding docs

46f0058

fix: always semantically minimise when adding a permanent nogood

1a48a66

fix: issue with watchers + adding propagate from scratch + optimise e…

07d5618

…xplanations

Merge branch 'main' into feat/extended-conflict-analysis

0b9e032

fix: incorrect explanations for bound propagations

182e1f7

Merge branch 'main' into feat/generalising-conflict-analysis

9f903e4

refactor: moving boolean away and passing enum directly

d8bba6c

refactor: simplifying while-loop guard constraints

1146bed

refactor: adding more statistics + adding docs

a22941f

fix: do not unnecessarily recalculate the decision level

c434a87

chore: put back variable in logging of statistics

6b5d16b

chore: simplification of if-statement

e857ffa

refactor: begin to unify the propagation algorithms

dd6073e

refactor: further unification of propagation algorithms

97d1038

refactor: even further unification of propagation algorithms

e1d1558

ImkoMarijnissen requested review from EmirDe and maartenflippo May 21, 2026 10:20

ImkoMarijnissen added 3 commits May 21, 2026 13:05

Revert "fix: do not unnecessarily recalculate the decision level"

dd13971

This reverts commit c434a87.

fix: proof logging unit propagations

b144667

fix: revert autonomous search changes

f977de9

maartenflippo requested changes May 22, 2026

View reviewed changes

maartenflippo reviewed May 22, 2026

View reviewed changes

ImkoMarijnissen added 9 commits May 22, 2026 11:12

refactor: reintroduce AnalysisMode and add methods to the enum

aab47df

refactor: reintroduce AnalysisMode and add methods to the enum

f8d204e

fix: use proper import in main

8c78a1d

refactor: move processing watcher to analysis mode

a0bb253

refactor: add method for determining whether extended nogood propagat…

89c67d5

…ion can take place

refactor: also factor out propagation method

fc27571

refactor: move out the removing and replacing of watchers

edc7321

refactor: unify adding asserting nogood

af354aa

docs: adding documentation to analysis mode

ffa7475

ImkoMarijnissen requested a review from maartenflippo May 26, 2026 11:36

ImkoMarijnissen added 2 commits May 26, 2026 13:39

chore: remove PartialEq for Watcher

196e0f4

refactor: use bitfield for lazy nogood explanation + factor out metho…

9c6a82a

…d for calculating info about domain

ImkoMarijnissen added 2 commits May 27, 2026 15:08

refactor: separate propagation and learning method + remove 1uip with…

0506de5

… extended nogood propagation

fix: nogood with flags

596978e

ImkoMarijnissen marked this pull request as ready for review May 28, 2026 06:22

fix: use input nogood when using flag

aedfd6d

ImkoMarijnissen added 4 commits May 28, 2026 10:03

docs: add documentation to fields

fbc32b4

test: add nogood priority argument for testing

781bbec

feat: incrementally compute loop condition CPIP

1195d79

docs: adding documentation

812cc17

Conversation

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

Uh oh!

Overview

Feedback

Experimentation

Overall Results

MiniZinc Scoring

Average Primal Integral

Overall Conclusions

TODO

Uh oh!

maartenflippo left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

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!

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

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ImkoMarijnissen commented May 27, 2026

Uh oh!

EmirDe commented May 28, 2026

Uh oh!

ImkoMarijnissen commented May 28, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

ImkoMarijnissen commented May 21, 2026 •

edited

Loading

maartenflippo left a comment •

edited

Loading

ImkoMarijnissen May 26, 2026 •

edited

Loading