Changes made in preparation for the XCSP3 and MiniZinc competitions #1167

cprudhom · 2025-08-19T07:27:41Z

These changes include the following:

Change to the default strategy for XCSP3
Conditional transformation of expressions into constraints in extensions and detection of some classic expressions (see #embody() method)
Implementation of a cache for the XCSP3 parser
addition of a configurable RoundRobin strategy
improvement and correction of DomOverWDeg and its variants
improvement of structures for CompactTable
creation of a class dedicated to preprocessing algorithms
addition of flexibility in ParallelPortfolio
other improvements and bug fixes

… in XCSP (+ to fzn)

The degree of the XCSP variable should be different from 0 to be really created in the choco model.

…return this

…ation" of a failure is too big (=all variables)

… Expression (XCSP3)

…ory footprint when using PropSTR2+

…rint

…laration (for RoundRobin mainly)

…ico order for breaking ties

…arch

+add model and decision path to AbstractStrategy

+ delete ValueSortedMap.java

Can be used to map double to Identity-based objects

jgFages · 2025-08-19T08:25:46Z

solver/src/main/java/org/chocosolver/solver/constraints/IDecompositionFactory.java

+     * @param vars   array of integer variables
+     * @param except array of values that can be excluded from the allDifferent constraint
+     */
+    default void allDifferentExceptDec2(IntVar[] vars, int[] except) {


Maybe rename as "allDifferentExceptGCCDec" ?

Why GCC?
allDifferentExceptManyDec ?

because the decomposition is based on GCC, so I would understand it as a "GCC based decomposition"
but I admit that reading "ExceptGCC" might be confusing, so perhaps allDifferentExceptDecGCC would be better.
We can also stay with the allDifferentExceptDec2

What about "allDifferentExceptDecBasedOnGCC" ? Or "allDifferentExceptDecByGCC" ?

jgFages · 2025-08-19T08:36:42Z

solver/src/main/java/org/chocosolver/solver/constraints/reification/PropXgeCHalfReif.java

            return IntEventType.DECUPP.getMask();
        }
-        return IntEventType.INCLOW.getMask();
+        return IntEventType.INSTANTIATE.getMask();


change made to trigger the setPassive ?

jgFages · 2025-08-19T08:43:19Z

...r/src/main/java/org/chocosolver/solver/search/strategy/selectors/values/IntDomainSticky.java

+ *
+ * @author Charles Prud'homme
+ */
+public final class IntDomainSticky implements IntValueSelector, Function<IntVar, OptionalInt>, IVariableMonitor<IntVar> {


not used in round robin?

Should be. I'll change that

Actually, it is already usable in RoundRobin

… to MiniSat#doReduceDB(). This is done by storing separately failure clauses and prohibiting-solution ones in MiniSat#learnts

…ents generated by propagateSat() can be lost because of `onPropagatorExecution` not placed correctly + fix typo in IntCircularQueue#toString

…les). See 2025/hitori with 5.1.dzn

See https://gist.github.com/cprudhom/b94a841728ccf9ee24b2efcfb683115c for details

…d of CT + add new option 'maxSizeInMBToUseCompactTable' in Settings + STR2+ now manages tuples without ISet (IStateInt + int[] instead)

+ correction of few propagators which were incorrect + correction of false literal declaration (init of MiniSat) + correction of assertion message and showReason

jgFages · 2025-09-12T14:26:06Z

solver/src/main/java/org/chocosolver/sat/Clause.java

+    /**
+     * Indicates if all literals but one are false in the clause.
+     * By implication, the remaining literal is the asserting literal.
+     * By contract, the literal at index 0 is the asserting literal and should not be considered.


I find the combination of "literal at index 0 ... should not be considered" and "allFalseButOne" confusing.
My first understanding is that were are checking that all literals but one are false, starting from position 1, whereas the code check that they are all false. If the code is correct, I would rephrase the doc :
"By contract, the literal at index 0 is the asserting literal and always true."

Your first understanding is correct: we are checking that all literals but one are false, starting from position 1.
The loop starts at 1 (not 0) and if a literal is not false, the loop is broken and false is returned.

Then, the contract is not that the literal at 0 is always true.
In its current usage (for assertion only), it should be undefined, otherwise there is a problem somewhere (indeed, the current cannot explain an event that already occurs).

Note that if this method is called somewhere else in the code, the assertion can be wrong, though, since it must be true only when a literal is satisfied or falsified.

Its easier (from a conception perspective) to keep the method in the Clause class, but I agree that it can be renamed for clarity.

solver/src/main/java/org/chocosolver/sat/MiniSat.java

ArthurGodet · 2025-09-12T15:38:28Z

solver/src/main/java/org/chocosolver/solver/constraints/IDecompositionFactory.java

+     * @param vars   array of integer variables
+     * @param except array of values that can be excluded from the allDifferent constraint
+     */
+    default void allDifferentExceptDec2(IntVar[] vars, int[] except) {


What about "allDifferentExceptDecBasedOnGCC" ? Or "allDifferentExceptDecByGCC" ?

solver/src/main/java/org/chocosolver/solver/constraints/IDecompositionFactory.java

ArthurGodet · 2025-09-12T15:45:52Z

solver/src/main/java/org/chocosolver/solver/constraints/IDecompositionFactory.java

+     * If a task is optional, it can be performed with a duration of 0 and the other mandatory tasks can overlap it.
+     * Otherwise, the task must be performed and cannot be overlapped by any other task even if it has a duration of 0.


This is not clear to me. I don't see, from the code, where the optionality of a task does intervene ? And shouldn't the optional tasks that are performed be considered as mandatory tasks ?

Following the MiniZinc definition (for which this decomposition has been written) a task with 0-duration is considered as optional, and can be overlapped.
But, if strict is set to true, a 0-duration task cannot be overlapped.

Ok this is clearer for the definition and I agree on the documentation.

I still would precise that optionality is treated as the possibility of the task to have a null-duration (as it is the only criteria taken into account in the code wrt optionality of tasks)

solver/src/main/java/org/chocosolver/solver/constraints/IIntConstraintFactory.java

ArthurGodet · 2025-09-12T15:57:29Z

solver/src/main/java/org/chocosolver/solver/constraints/binary/PropAbsoluteLight.java

+            int u = Y.getUB();
+            if (l >= 0) {
+                absY.updateLowerBound(l, this, lcg() ? Reason.r(Y.getMinLit()) : Reason.undef());
+                absY.updateUpperBound(u, this, lcg() ? Reason.r(Y.getMinLit(), Y.getMaxLit()) : Reason.undef());


Why is there Y.getMinLit() in the explanation ?

Because l (Y.getLB()) is >=0, which could happen due to filtering of Y lower bound.

Consider the case where Y = [-10, 5], then |Y| = [0,10]
If an event set Y to [2,5], then |Y| = [2,5] and the modification of |Y| upper bound is due to the current upper bound of Y and the fact the lower bound of Y changes (to a value >= 0)

I would have expected the explanation to therefore be Reason.r(Y.getLELit(-1), Y.getMaxLit()) but it would only work for enumerated-domains' variables. Maybe we could rely on the getNegGeqLit and getNegLeqLit functions I used in PropagatorCumulative (by making them static functions in Reason ?)

solver/src/main/java/org/chocosolver/solver/constraints/binary/PropAbsoluteLight.java

+ taking PR comments into account

…of TimeTabling and OverloadChecking (#1165) and fixes #1114

cprudhom and others added 30 commits March 13, 2025 13:45

Add decomposition of AllDifferentExcept0 and AllDifferentExceptValues…

6ea8118

… in XCSP (+ to fzn)

Fix error in XCSP groups declaration.

18e0976

The degree of the XCSP variable should be different from 0 to be really created in the choco model.

Reduce the extension fallback threshold to 100_000 instead of 2147483

8e13668

Add new lzma files

b6e5bc2

Add seed as new parameter in PickOnDom and PickOnFil

ff9a26a

Update BlackBoxConfigurator#setRefinedPartialAssignmentGeneration to …

90562c8

…return this

Add MetaStrategy abstract class

3f7f551

Remove PropSat from failure-based search strategy because the "explan…

473c313

…ation" of a failure is too big (=all variables)

Fix error when getting the group of variables and some are null (XCSP3)

5077bce

Change conditions for choosing between extension or decomposition for…

279b868

… Expression (XCSP3)

Simplify PropSTR2 to avoid storing the Tuples object

cc8f328

Cache matrix (using SoftReference) in the Tuples object to reduce mem…

089a9cc

…ory footprint when using PropSTR2+

Cache tuples (using WeakHashMap) in XCSPParser to reduce memory footp…

dde2edd

…rint

Add a RoundRobin strategy based on Group

d300c5a

Remove assert k > 0 for LastConflict to allow dummy meta strategy dec…

9e01cc5

…laration (for RoundRobin mainly)

AbstractCriterionBasedVariableSelector now interpert seed = -1 as lex…

1bac37a

…ico order for breaking ties

Add NextModuloN policy for MAB (= round robin)

a1aa164

Update Search#roundRobinSearch and create Search#adaptiveRoundRobinSe…

595ca4a

…arch

Fix java compatibility

db8cb2d

Define a default search strategy for XCSP3

0f7298e

support regular with negative values

898291e

faster isInScope method + bugfix conflictOrderingSearch

69d1e6b

+add model and decision path to AbstractStrategy

search simplification

4a5d207

update changes.md

1c62aeb

fix tests

e5b5b44

fix test

3504d0f

Add Javadoc

6349fd1

support regular with negative values

7ca5d1c

Move MapVal and ArrayVal to IVal inner classes.

44b4b6c

+ delete ValueSortedMap.java

Create Weightable class and its two inner classes.

d8e4d0d

Can be used to map double to Identity-based objects

cprudhom added 3 commits August 18, 2025 18:00

Expr : fix seed in sampling for conversion to extensional constraint

62bc705

XCCSP: update tests wrt to changes related to competition preparation

68b61f4

Table: fix test wrt commuit #e86270e7

e92e588

cprudhom added this to the 5.0.0 milestone Aug 19, 2025

cprudhom self-assigned this Aug 19, 2025

cprudhom added bug feature java Pull requests that update java code labels Aug 19, 2025

jgFages reviewed Aug 19, 2025

View reviewed changes

jgFages approved these changes Aug 19, 2025

View reviewed changes

cprudhom added 10 commits August 19, 2025 12:13

Merge branch 'develop' into xcsp

280c584

fix commit #280c5848 (merge manually on github)

5f78220

LCG: prevent prohibiting-solution clauses from being removed on calls…

8505628

… to MiniSat#doReduceDB(). This is done by storing separately failure clauses and prohibiting-solution ones in MiniSat#learnts

LCG: fix a bug that occurs when some constraints are reified. Some ev…

7d94505

…ents generated by propagateSat() can be lost because of `onPropagatorExecution` not placed correctly + fix typo in IntCircularQueue#toString

CPProfiler: display modifications

6c7d05f

Flatzinc: set complementary search by default (not only output variab…

b3ecbd8

…les). See 2025/hitori with 5.1.dzn

X+Y=Z: removal of PropXplusYeqZ, fall back propagator is PropSum

839c644

See https://gist.github.com/cprudhom/b94a841728ccf9ee24b2efcfb683115c for details

Table: when the memory estimation is too big STR2+ is selected instea…

d8faa17

…d of CT + add new option 'maxSizeInMBToUseCompactTable' in Settings + STR2+ now manages tuples without ISet (IStateInt + int[] instead)

LCG : constants are now managed as a specific case of IntVarEagerLit

12f6c52

LCG : add new assertion when enqueuing literal in MiniSat

55e0c1d

+ correction of few propagators which were incorrect + correction of false literal declaration (init of MiniSat) + correction of assertion message and showReason

jgFages reviewed Sep 12, 2025

View reviewed changes

MiniSat: move Clause#allFalseButOne to MiniSat#isAssertingClause

ca30903

ArthurGodet requested changes Sep 12, 2025

View reviewed changes

cprudhom and others added 5 commits September 16, 2025 17:55

Javadoc : update

674e0e4

+ taking PR comments into account

Replace Cumulative implementation by state-of-the-art implementation …

89c999d

…of TimeTabling and OverloadChecking (#1165) and fixes #1114

Update CHANGES.md

f29f80f

Explained Bimodal AllDifferent (#1173)

422901b

IntVar no longer extends Iterable (#1177)

f77428e

		* If a task is optional, it can be performed with a duration of 0 and the other mandatory tasks can overlap it.
		* Otherwise, the task must be performed and cannot be overlapped by any other task even if it has a duration of 0.

Changes made in preparation for the XCSP3 and MiniZinc competitions #1167

Are you sure you want to change the base?

Changes made in preparation for the XCSP3 and MiniZinc competitions #1167

Uh oh!

Conversation

cprudhom commented Aug 19, 2025

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!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

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!

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!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants