feat: implement extended nogood propagation and CPIP nogood learning

[ImkoMarijnissen]

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

[ImkoMarijnissen]

After discussion with @maartenflippo:

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

[EmirDe]

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

[ImkoMarijnissen]

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.

[EmirDe]

I had a look. This is quite a complicated PR, so I think we need to discuss how to approach it.

The nogood propagator is heavily parameterised (PropagationMode x AnalysisMode) and we are handling all these cases in one file, so looking at the code can be a bit difficult. CPIP has additional requirements that standard unit propagation does not have, so it makes things complicated for both.

Another point is that in my experience, the nogood propagator is quite delicate, in the sense that anything we add to it can impact performance. Say if we run 1UIP with this code, I would expect that it may be slower than the previous version.

I am not sure what the best way forward is, but we can discuss. My current impression is that it may be too much to pack everything into one propagator (but maybe it is the best, we can see). On the other hand, some functionality is the same amongst the nogood propagators, so it makes sense to reuse.

I am wondering if we can separate the code by use case, but handle things at compile time to avoid performance loss and make it look nicer.

Overall, let us discuss in person!

Some other comments (a bit messy, sorry!):

Comments in resolution_resolver.rs need to be updated throughout the file -> part of it seems to refer to only the "old" version (without CPIP), so it can be a bit confusing (it simply misses CPIP).

We sometimes use "1UIP" and sometimes "OneUIP", could standardise.

We refer to the unique implication point, but for CPIPs, I think we are doing "first propagation point".

(perhaps unrelated, but very surprising) I noticed we renamed "decision_level" as "checkpoint". Why? The trail has a "checkpoint" and predicates have "checkpoints". It seems odd given that we have not used that terminology in our papers.

to discuss: to_process_heap -> totally not clear in the "should_continue_resolving"

There is a todo:
// TODO: compute this incrementally -> how important is this? Looks intense. A new data structure that is like a map with a counter would work.

// We wait until there are only elements over a single variable left. -> what is element, predicate?

// Firstly, there should be only elements over a single element. -> what is element, predicate?

todo discuss (I do not fully follow what is going on) -> AnalysisMode::BoundsCPIP => {
todo discuss (I do not fully follow the comments) -> WatcherProcessingStatus

let inference_code = &self.inference_codes[self.nogood_predicates.get_nogood_index(&watcher.nogood_id)]; -> why is this being fetched at this point, whereas it might not even be used, and in the code, its usage appears 150 lines later?

We need to state the invariants for extended nogoods, that we are maintaining, in the code.

// If there is a falsified predicate over the same variable as the 0th predicate, then we need to replace it. -> do we need to? Could we simply take a new domain id?

// Similarly, we need to keep the invariant for lazy unit propagation explanations that the propagated predicate is at the 0th position. -> for CPIP, no, right, since multiple predicates can be propagated?

Above we use "variable", later we use "domain" in "process_potential_watcher". Probably should use just domain id.

[EmirDe]

I have done a new pass! It would be best to discuss in person (will reach out separately for scheduling). Until then, a few high-level comments.

[1]

I now understand what my problem was. Even though I understand the methods individually, when presented with code that uses enums to switch between variants, it becomes hard to parse, since you need to consider all variants at once. This is both for the propagator and conflict analysis. And AnalysisMode is an enum will quite some elaborate methods.

It is true that many of the variants share the same code so that also makes sense to make it this way. But I am still wondering if we can do something to make this clearer. This is best in person to discuss also with Maarten.

Concretely, I am curious if we can define traits, and then have every variant implement their version of the functions for each trait. This way we can keep the high-level structure of the analysis and propagation procedure, and have a clearer way to fill in the differences. This would effectively remove the match cases for the difference mode (AnalysisMode and PropagationMode). Some code might still be duplicated, but not much, and maybe there are also solutions there.

[2]

The other issue is that when we are finding new watchers, for CPIP, we seem to be doing some replacements on the fly. However, some replacements may be redundant. I think we need to do the linear scan, and only do one replacement at the very end. For example, WatcherProcessingStatus::FoundNewWatchButContinue keeps replacing, but if we end up finding a predicate with a different variable, then we would use that predicate and stop with finding other watchers, and at this point, any changes done by WatcherProcessingStatus::FoundNewWatchButContinue will be irrelevant.

[EmirDe]

Maarten and I discussed this PR on Thursday. Here is a quick summary to discuss next week.

(@maartenflippo we added comments to the code, but I do not see them now. Can you check if you made the comments visible by adding the review?)

Overall, we have tried to understand why it is difficult to parse some parts of the code. We concluded that it has something to do with the enums, because at any given time when looking at the code, we mentally need to evaluate multiple propagation/learning schemes simultaneously.

1. Extended nogood propagation is very similar to standard unit propagation. The main difference is the definition of a watcher. When searching for a new watcher, unit propagation simply looks for a nonsatisfied predicate.

In contrast, extended nogood propagation looks for a 1) nonsatisfied predicate (as before), plus 2) the new watcher has a different domain_id compared to the other watcher. Here we see that the difference is simply one more criteria.

However in the code, the difference is rather substantial. We think this is because the propagation algorithm, in addition to simply propagating, also tries to eagerly rearrange the predicate in a way that is convenient for explanations.

The question is whether that is necessary, can we simplify the propagation algorithm, and then shift the explanation logic to a different place? I think this could make this cleaner, but potentially also more efficient (see previous comment above).

2. We considered whether replacing enums with traits makes sense. This would make the different variants something the compiler can do at compile-time, and potentially make the code cleaner. However we concluded that probably this is not a good idea, since this signals that there will be future extensions through traits which is unlikely, and we do not get that much over enums.

3. Changing enum functions to concrete types might be better. Some of the enum functions are only applicable to CPIP and receive as input a hashmap (if I recall correctly) that only matters for that type. Also, CPIP and the bounds version behave the same in a lot of cases. The question is whether this can be improved (to be discussed).

[ImkoMarijnissen]

Overall, we have tried to understand why it is difficult to parse some parts of the code. We concluded that it has something to do with the enums, because at any given time when looking at the code, we mentally need to evaluate multiple propagation/learning schemes simultaneously.

1. Extended nogood propagation is very similar to standard unit propagation. The main difference is the definition of a watcher. When searching for a new watcher, unit propagation simply looks for a nonsatisfied predicate.

In contrast, extended nogood propagation looks for a 1) nonsatisfied predicate (as before), plus 2) the new watcher has a different domain_id compared to the other watcher. Here we see that the difference is simply one more criteria.

However in the code, the difference is rather substantial. We think this is because the propagation algorithm, in addition to simply propagating, also tries to eagerly rearrange the predicate in a way that is convenient for explanations.

This is indeed correct. In the current code, we make an assumption when performing unit propagation (the propagated atomic constraint is at position 0). In an attempt to make the changes less intrusive, I ensured that extended nogood propagation also adhered to these invariants.

The question is whether that is necessary, can we simplify the propagation algorithm, and then shift the explanation logic to a different place? I think this could make this cleaner, but potentially also more efficient (see previous comment above).

I am not sure about it being more efficient. We are looking for a replacement of the watcher at position 1, but in the case of FoundNewWatchButContinue, we replace the watcher at position 0 to ensure the aforementioned invariants. We can move this logic (e.g., to the lazy_explanation method), but this would introduce overhead there instead (we could avoid this overhead for 1UIP nogoods, but then we would need to check the enum variant there).

If you had something else in mind, then please let me know!

2. We considered whether replacing enums with traits makes sense. This would make the different variants something the compiler can do at compile-time, and potentially make the code cleaner. However we concluded that probably this is not a good idea, since this signals that there will be future extensions through traits which is unlikely, and we do not get that much over enums.

Fair enough, thank you for letting me know!

3. Changing enum functions to concrete types might be better. Some of the enum functions are only applicable to CPIP and receive as input a hashmap (if I recall correctly) that only matters for that type. Also, CPIP and the bounds version behave the same in a lot of cases. The question is whether this can be improved (to be discussed).

To me, it is not entirely clear what this would look like without traits. It would be great to discuss!