Enhance MiniSat and LCG with improved reason management and optimizations#1185
Merged
Enhance MiniSat and LCG with improved reason management and optimizations#1185
Conversation
… variable for end-variables of cumulative when undeclared in FZN.
…ing and limits/reduces GC. MiniSat: missing import related to introduction of MinimaList
+ MiniSat: DB reduction now relies on LBD
+ clean up code
… int-array during resolution and reduce GC. From dev pov, any propagator can now declare a reason with `this.r(...)` + correction/improvement in Profile and PropCumulative when LCG is activated
jgFages
reviewed
Mar 27, 2026
| hasFiltered |= updateMinDuration(end.getLB() - start.getUB(), this); | ||
| hasFiltered |= updateMaxDuration(end.getUB() - start.getLB(), this); | ||
| } | ||
| // TODO : add filtering for enumerated domains |
Member
Author
There was a problem hiding this comment.
I didn't add the TODO in the first place, but I think that achieving AC on Task when domains are enumerated can really be costly. If that's a need, I suggest the user to explicitly add a constraint. @ArthurGodet what do you think ?
Collaborator
There was a problem hiding this comment.
I agree on removing this TODO, as filtering algorithms on Tasks (the ones for Cumulative and Disjunctive constraints) always filter on bounds (and never on values inside the domain), and Tasks are designed to be used for these two constraints.
jgFages
approved these changes
Mar 27, 2026
ArthurGodet
requested changes
Mar 28, 2026
...r/src/main/java/org/chocosolver/solver/constraints/nary/cumulative/PropagatorCumulative.java
Show resolved
Hide resolved
...r/src/main/java/org/chocosolver/solver/constraints/nary/cumulative/PropagatorCumulative.java
Show resolved
Hide resolved
ArthurGodet
approved these changes
Mar 30, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This appears to be a big PR because all explained propagators have been modified but the main modifications are in the
satpackage.The way reasons are managed has been deeply modified to reduce GC by default (n-ary reasons are recycled) even if it is still manageable to use the previous version.
In addition, Literal Block Distance has been implemented and is used when the clause store needs to be reduced to better select the ones to keep.
Also, the way tasks involved in the profile of the cumulative constraint are stored has changed too are (when LCG is activated).