From e7b46b75c7f5fbaa1237188c5cf199a0c22ce306 Mon Sep 17 00:00:00 2001 From: Charles Prud'homme Date: Fri, 21 Aug 2026 12:22:17 +0200 Subject: [PATCH 01/12] MiniSat: new watch relies on circular approach + javadoc --- .../java/org/chocosolver/sat/ArrayClause.java | 20 ++++ .../java/org/chocosolver/sat/MiniSat.java | 101 +++++++++++++----- .../org/chocosolver/sat/SatDecorator.java | 2 +- 3 files changed, 97 insertions(+), 26 deletions(-) diff --git a/solver/src/main/java/org/chocosolver/sat/ArrayClause.java b/solver/src/main/java/org/chocosolver/sat/ArrayClause.java index 52e0cd2e46..af91e13e4c 100644 --- a/solver/src/main/java/org/chocosolver/sat/ArrayClause.java +++ b/solver/src/main/java/org/chocosolver/sat/ArrayClause.java @@ -41,6 +41,11 @@ public final class ArrayClause extends Clause { */ private final int id; + /** + * Position of the last scanned literal + */ + private int lastScannedLit = 1; + /** * Create a clause with a set of literals * @@ -166,4 +171,19 @@ public int _g(int i) { public void _s(int pos, int l) { literals_[pos] = l; } + + /** + * @return the position of the last scanned literal + */ + public int getLastScannedLit() { + return lastScannedLit; + } + + /** + * Set the position of the last scanned literal to lastScannedLit. + * @param lastScannedLit position to store + */ + public void setLastScannedLit(int lastScannedLit) { + this.lastScannedLit = lastScannedLit; + } } diff --git a/solver/src/main/java/org/chocosolver/sat/MiniSat.java b/solver/src/main/java/org/chocosolver/sat/MiniSat.java index 9d09f1f76b..940eea7814 100644 --- a/solver/src/main/java/org/chocosolver/sat/MiniSat.java +++ b/solver/src/main/java/org/chocosolver/sat/MiniSat.java @@ -99,7 +99,7 @@ public void resize(int j) { static final VarData VD_Undef = new VarData(R_Undef, -1, -1); public Clause confl = C_Undef; - public static final Clause C_Fail = new ArrayClause(new int[]{0, 0}); + public static final ArrayClause C_Fail = new ArrayClause(new int[]{0, 0}); static final ChannelInfo CI_Null = new ChannelInfo(null, 0, 0, 0); // If false, the constraints are already unsatisfiable. No part of @@ -254,7 +254,7 @@ public boolean addClause(TIntList ps) { propagate(); return (ok_ = (confl == C_Undef)); default: - Clause cr = new ArrayClause(ps); + ArrayClause cr = new ArrayClause(ps); clauses.add(cr); attachClause(cr); break; @@ -318,6 +318,7 @@ public void addLearnt(TIntList learnt_clause, boolean unforgettable) { uncheckedEnqueue(learnt_clause.get(0)); } else { Clause cr = new ArrayClause(learnt_clause, true); + ArrayClause cr = new ArrayClause(learnt_clause, true); learnts.add(cr); if (unforgettable) { // in the case of a solution, for instance. if (learnts.size() > 1) { @@ -490,7 +491,7 @@ private static boolean isAssertingClause(MiniSat sat, Clause c) { // Enqueue a literal. Assumes value of literal is undefined. public void uncheckedEnqueue(int l, Clause from) { assert valueLit(l) == lUndef : "l: " + printLit(l) + " from: " + from; - assert isAssertingClause(this, from.getConflict()) : "the reason " + showReason(from) + " is not valid because it is not unit"; + assert isAssertingClause(this, from.getConflict()) : "the reason " + showReason(from) + " is not asserting under propagation"; int v = var(l); if (assignment_.getQuick(v) == lUndef) { onLiteralPushed(l); @@ -527,9 +528,9 @@ public void uncheckedEnqueue(int l) { } public void cEnqueue(int l, Reason r) { - assert valueLit(l) != lTrue; + assert valueLit(l) != lTrue : l + " not true, reason is " + r; assert r != null : "reason is null for " + printLit(l); - assert isAssertingClause(this, r.getConflict()) : "the reason " + showReason(r) + " is not valid because it is not unit"; + assert isAssertingClause(this, r.getConflict()) : "the reason " + showReason(r) + " is not asserting under propagation"; int v = var(l); if (valueLit(l) == lFalse) { if (r == R_Undef) { @@ -560,7 +561,7 @@ public void cEnqueue(int l, Reason r) { } // Attach a clause to watcher lists. - void attachClause(Clause cr) { + void attachClause(ArrayClause cr) { assert cr.size() > 1; MinimaList l0 = watches_.get(neg(cr._g(0))); if (l0 == null) { @@ -625,7 +626,7 @@ private void propagateLit(int p) { } // Make sure the false literal is data[1]: - Clause cr = w.clause; + ArrayClause cr = w.clause; final int false_lit = neg(p); if (cr._g(0) == false_lit) { cr._s(0, cr._g(1)); @@ -645,7 +646,7 @@ private void propagateLit(int p) { continue; } - boolean cont = newWatch(cr, false_lit, w); + boolean cont = newWatchCircular(cr, false_lit, w); // Did not find watch -- clause is unit under assignment: if (!cont) { @@ -672,21 +673,73 @@ private void propagateLit(int p) { } } - private boolean newWatch(Clause cr, int false_lit, Watcher w) { + private void changeWatchedLiteral(ArrayClause cr, int false_lit, Watcher w, int k) { + // Swap: place the new literal in position 1 + cr._s(1, cr._g(k)); + cr._s(k, false_lit); + // Attach the watcher to the new position + MinimaList lw = watches_.get(neg(cr._g(1))); + if (lw == null) { + lw = new MinimaList<>(); + watches_.put(neg(cr._g(1)), lw); + } + lw.add(w); + } + + /** + * Implements the circular approach for finding a new watched literal in a clause. + * This method is based on the optimal implementation of watched literals as described in: + *

+ * Optimal Implementation of Watched Literals and More General Techniques + * by Ian P. Gent, Journal of Artificial Intelligence Research (JAIR), Volume 48, 2013. + *

+ *

+ * The circular approach maintains a pointer ({@code lastScannedLit}) to the last scanned position + * in the clause. When searching for a new acceptable literal (one that is not false), it starts + * from the position after the last scanned one, and wraps around to the beginning (position 2) + * when reaching the end of the clause. The search stops when it returns to the starting position, + * ensuring that each literal is checked at most twice per node in the search tree. + *

+ *

+ * This approach is proven to be big-O optimal when amortized across the entire search tree, + * with a worst-case constant factor of only 2. In contrast to the state restoration method, + * this approach is backtrack-stable: it does not require restoring the search position during + * backtracking, relying instead on the monotonicity property of acceptability (if a literal + * is unacceptable at a node, it remains unacceptable at all descendant nodes). + *

+ *

+ * Empirical results from the paper show a 29% speedup in unit propagation when using this + * circular approach in MiniSat, though this does not translate to a statistically significant + * improvement in overall solver runtime. + *

+ * + * @param cr the clause in which to find a new watched literal + * @param false_lit the literal that has become false (the negated watched literal) + * @param w the watcher associated with this clause + * @return {@code true} if a new acceptable literal was found and set as the new watched literal, + * {@code false} if no acceptable literal exists in the clause + * @see JAIR Paper DOI + */ + private boolean newWatchCircular(ArrayClause cr, int false_lit, Watcher w) { + int last = cr.getLastScannedLit(); + int lastCache = last; + int n = cr.size(); // Look for new watch: - for (int k = 2; k < cr.size(); k++) { - if (valueLit(cr._g(k)) != lFalse) { - cr._s(1, cr._g(k)); - cr._s(k, false_lit); - MinimaList lw = watches_.get(neg(cr._g(1))); - if (lw == null) { - lw = new MinimaList<>(); - watches_.put(neg(cr._g(1)), lw); - } - lw.add(w); + do { + last++; + // If we return to the starting position, there are no valid literals + if (last == n) { + // By convention, the false literal is at 1 before calling this method + last = 1; + } + // Checks whether the literal at position k is valid + if (valueLit(cr._g(last)) != lFalse) { + changeWatchedLiteral(cr, false_lit, w, last); + // Updates the latest search position + cr.setLastScannedLit(last); return true; } - } + } while (lastCache != last); return false; } @@ -1084,8 +1137,6 @@ public void deleteAllLearnedClauses() { public void doReduceDB() { int i, j; - double extra_lim = cla_inc / learnts.size(); // Remove any clause below this activity - learnts.subList(learnt_first_removable, learnts.size()) // only removable clauses .sort(comp); // Don't delete binary or locked clauses or unforgettable clauses. @@ -1268,10 +1319,10 @@ private String showReason(Reason r) { */ private static final class Watcher { - final Clause clause; - int blocker; + private final ArrayClause clause; + private int blocker; - Watcher(final Clause cr, int l) { + Watcher(final ArrayClause cr, int l) { this.clause = cr; this.blocker = l; } diff --git a/solver/src/main/java/org/chocosolver/sat/SatDecorator.java b/solver/src/main/java/org/chocosolver/sat/SatDecorator.java index 5777cd297a..63a977d476 100644 --- a/solver/src/main/java/org/chocosolver/sat/SatDecorator.java +++ b/solver/src/main/java/org/chocosolver/sat/SatDecorator.java @@ -82,7 +82,7 @@ public void learnClause(int... ps) { ok_ = (confl == C_Undef); return; default: - Clause cr = new ArrayClause(ps); + ArrayClause cr = new ArrayClause(ps); //removeDominated(cr); learnts.add(cr); attachClause(cr); From 1694a1e46b3a8eb62a3341194af5a6b138d19149 Mon Sep 17 00:00:00 2001 From: Charles Prud'homme Date: Fri, 21 Aug 2026 12:24:52 +0200 Subject: [PATCH 02/12] MiniSat: move the highest decision literal to position 1 in the learned clauses --- .../java/org/chocosolver/sat/MiniSat.java | 43 ++++++++++++++++++- 1 file changed, 42 insertions(+), 1 deletion(-) diff --git a/solver/src/main/java/org/chocosolver/sat/MiniSat.java b/solver/src/main/java/org/chocosolver/sat/MiniSat.java index 940eea7814..0241c4cd1d 100644 --- a/solver/src/main/java/org/chocosolver/sat/MiniSat.java +++ b/solver/src/main/java/org/chocosolver/sat/MiniSat.java @@ -305,6 +305,47 @@ public boolean addClause(int p, int q, int r) { return addClause(temporary_add_vector_); } + /** + * Moves the literal with the highest decision level to position 1 in the clause. + * This ensures that the second watched literal (at position 1) is the one with the highest + * decision level, which can improve propagation efficiency. + * The literal at position 0 (the asserting literal) is left unchanged. + * + * The method performs an early exit if a literal at the current decision level is found, + * as no literal can have a higher level than the current one. + * + * @param cr the clause to reorganize + */ + private void moveHighestDecisionLitToPos1(ArrayClause cr) { + if (cr.size() <= 2) { + return; // Nothing to do for binary clauses + } + + int currentLevel = trailMarker(); + int highestPos = 1; + int highestLevel = level(var(cr._g(1))); + + // Find the literal with the highest decision level (excluding position 0) + for (int i = 2; i < cr.size(); i++) { + int litLevel = level(var(cr._g(i))); + if (litLevel > highestLevel) { + highestLevel = litLevel; + highestPos = i; + // Early exit: if we found a literal at the current level, no need to continue + if (highestLevel == currentLevel) { + break; + } + } + } + + // If a literal with higher level was found, swap it with position 1 + if (highestPos != 1) { + int temp = cr._g(1); + cr._s(1, cr._g(highestPos)); + cr._s(highestPos, temp); + } + } + /** * Add a learnt clause to the solver. * If the param unforgettable is true, the clause will not be removed during {@link #doReduceDB()}. @@ -317,8 +358,8 @@ public void addLearnt(TIntList learnt_clause, boolean unforgettable) { if (learnt_clause.size() == 1) { uncheckedEnqueue(learnt_clause.get(0)); } else { - Clause cr = new ArrayClause(learnt_clause, true); ArrayClause cr = new ArrayClause(learnt_clause, true); + moveHighestDecisionLitToPos1(cr); learnts.add(cr); if (unforgettable) { // in the case of a solution, for instance. if (learnts.size() > 1) { From 50436a67bf325064e67524beafbb555268612ec6 Mon Sep 17 00:00:00 2001 From: Charles Prud'homme Date: Fri, 21 Aug 2026 12:25:41 +0200 Subject: [PATCH 03/12] LCG: move calls to doReduceDB as first step of the `forget` method --- .../solver/search/loop/learn/LazyClauseGeneration.java | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/solver/src/main/java/org/chocosolver/solver/search/loop/learn/LazyClauseGeneration.java b/solver/src/main/java/org/chocosolver/solver/search/loop/learn/LazyClauseGeneration.java index 23c2fd0c56..f7bfb3f1e9 100644 --- a/solver/src/main/java/org/chocosolver/solver/search/loop/learn/LazyClauseGeneration.java +++ b/solver/src/main/java/org/chocosolver/solver/search/loop/learn/LazyClauseGeneration.java @@ -69,7 +69,7 @@ public class LazyClauseGeneration implements Learn { private final long reduceBase; private final long reduceFactor; private int reductions = 0; - private boolean extractFromVariablesOnSolution; + private final boolean extractFromVariablesOnSolution; /** * A temporary storage for learnt clauses. */ @@ -106,6 +106,10 @@ public boolean record() { @Override public void forget() { // required because MoveBinaryDFS add a useless decision level on refutation + if (mSat.nLearnts() >= max_learnts || mSolver.getFailCount() > nextReductionCall) { + mSat.doReduceDB(); + nextReductionCall += reduceBase + reduceFactor * (++reductions); + } if (nbRestarts == mSolver.getRestartCount()) { mSolver.cancelTrail(); mSolver.getDecisionPath().synchronize(true, learnt_clause.size() > 1); @@ -118,10 +122,6 @@ public void forget() { } else { nbRestarts = mSolver.getRestartCount(); } - if (mSat.nLearnts() >= max_learnts || mSolver.getFailCount() > nextReductionCall) { - mSat.doReduceDB(); - nextReductionCall += reduceBase + reduceFactor * (++reductions); - } } private void onFailure() { From cef9526c19c5c8254c15f7aebeaf0a6bbe97b983 Mon Sep 17 00:00:00 2001 From: Charles Prud'homme Date: Fri, 21 Aug 2026 12:29:45 +0200 Subject: [PATCH 04/12] Cumulative: calculate the tasks involved in the profile in a lazy manner when LCG is enabled --- .../constraints/nary/cumulative/Profile.java | 30 ++++++++++++------- .../nary/cumulative/PropagatorCumulative.java | 2 +- 2 files changed, 20 insertions(+), 12 deletions(-) diff --git a/solver/src/main/java/org/chocosolver/solver/constraints/nary/cumulative/Profile.java b/solver/src/main/java/org/chocosolver/solver/constraints/nary/cumulative/Profile.java index 0fbb6b3a2b..c0c3157e4a 100644 --- a/solver/src/main/java/org/chocosolver/solver/constraints/nary/cumulative/Profile.java +++ b/solver/src/main/java/org/chocosolver/solver/constraints/nary/cumulative/Profile.java @@ -32,6 +32,10 @@ public class Profile { private int min; private int max; + private final int[] copyLST; + private final int[] copyECT; + private final BitSet computed = new BitSet(); + /** * Instantiates a new Profile. * @@ -48,6 +52,8 @@ public Profile(final int nbTasks) { eventPointSeries = new EventPointSeries(nbTasks); list = new BitSet(nbTasks); time = new int[31]; + this.copyLST = new int[nbTasks]; + this.copyECT = new int[nbTasks]; } /** @@ -112,6 +118,8 @@ public void buildProfile(final Task[] tasks, final IntVar[] tasksHeights, final min = Integer.MAX_VALUE; max = Integer.MIN_VALUE; for (int i = activeTasks.nextSetBit(0); i != -1; i = activeTasks.nextSetBit(i + 1)) { + copyLST[i] = tasks[i].getLst(); + copyECT[i] = tasks[i].getEct(); min = Math.min(min, tasks[i].getEst()); max = Math.max(max, tasks[i].getLct()); } @@ -119,6 +127,7 @@ public void buildProfile(final Task[] tasks, final IntVar[] tasksHeights, final && max - min < activeTasks.cardinality() * activeTasks.cardinality()) { buildProfileNaive(tasks, tasksHeights, activeTasks); } else { + computed.clear(); buildProfileSweep(tasks, tasksHeights, activeTasks); } timePoints[idx] = Integer.MAX_VALUE; @@ -144,23 +153,14 @@ private void buildProfileSweep(final Task[] tasks, final IntVar[] tasksHeights, while (!eventPointSeries.isEmpty() && eventPointSeries.getTimeFirstEvent() == timePoints[idx]) { Event event = eventPointSeries.removeFirstEvent(); if (event.getType() == Event.SCP) { - if (lcg) { - list.set(event.getIndexTask()); - } h += tasksHeights[event.getIndexTask()].getLB(); } else { - if (lcg) { - list.clear(event.getIndexTask()); - } h -= tasksHeights[event.getIndexTask()].getLB(); } } if (lcg || h != heights[idx - 1]) { heights[idx] = h; - if (lcg) { - indexesTask[idx].clear(); - if (!list.isEmpty()) indexesTask[idx].or(list); - } + indexesTask[idx].clear(); idx++; } assert h >= 0; @@ -224,7 +224,15 @@ private void fillTime(final Task[] tasks, final IntVar[] tasksHeights, final ISt * * @return the list of indexes of tasks contributing to the rectangle k */ - public BitSet fillList(int k) { + public BitSet fillList(int k, final IStateBitSet activeTasks) { + if (!computed.get(k)) { + for (int i = activeTasks.nextSetBit(0); i != -1; i = activeTasks.nextSetBit(i + 1)) { + if (copyLST[i] <= getStartRectangle(k) && getEndRectangle(k) <= copyECT[i]) { + indexesTask[k].set(i); + } + } + computed.set(k); + } return indexesTask[k]; } diff --git a/solver/src/main/java/org/chocosolver/solver/constraints/nary/cumulative/PropagatorCumulative.java b/solver/src/main/java/org/chocosolver/solver/constraints/nary/cumulative/PropagatorCumulative.java index 791bdd6448..b7e7e7d8e6 100644 --- a/solver/src/main/java/org/chocosolver/solver/constraints/nary/cumulative/PropagatorCumulative.java +++ b/solver/src/main/java/org/chocosolver/solver/constraints/nary/cumulative/PropagatorCumulative.java @@ -369,7 +369,7 @@ private void addLiteralsTasks( final int j, final int begin, final int end) { - BitSet indexesTask = profile.fillList(j); + BitSet indexesTask = profile.fillList(j, activeTasks); for (int i = indexesTask.nextSetBit(0); i >= 0; i = indexesTask.nextSetBit(i + 1)) { literals.add(getNegGeqLit(tasks[i].getEnd(), end)); literals.add(getNegLeqLit(tasks[i].getStart(), begin)); From 46df07ff6733a4c9d10addcd8ac21b60f0337081 Mon Sep 17 00:00:00 2001 From: Charles Prud'homme Date: Fri, 21 Aug 2026 14:00:40 +0200 Subject: [PATCH 05/12] Fix #1233 --- .../constraints/binary/PropAbsolute.java | 153 +++++++++++++----- .../constraints/binary/PropAbsoluteLight.java | 69 ++++---- .../constraints/binary/AbsoluteLightTest.java | 26 +++ .../constraints/binary/AbsoluteTest.java | 81 ++++++++++ .../binary/AbstractBinaryTest.java | 33 ++++ 5 files changed, 277 insertions(+), 85 deletions(-) create mode 100644 solver/src/test/java/org/chocosolver/solver/constraints/binary/AbsoluteLightTest.java create mode 100644 solver/src/test/java/org/chocosolver/solver/constraints/binary/AbsoluteTest.java diff --git a/solver/src/main/java/org/chocosolver/solver/constraints/binary/PropAbsolute.java b/solver/src/main/java/org/chocosolver/solver/constraints/binary/PropAbsolute.java index 87e2671bca..add5576c36 100644 --- a/solver/src/main/java/org/chocosolver/solver/constraints/binary/PropAbsolute.java +++ b/solver/src/main/java/org/chocosolver/solver/constraints/binary/PropAbsolute.java @@ -17,8 +17,19 @@ import org.chocosolver.util.tools.ArrayUtils; /** - * Enforces X = |Y| - *
+ * A propagator to enforce the constraint absY = |Y|, where + * absY is a variable representing the absolute value of Y. + *

+ * This propagator ensures that: + *

    + *
  • absY is always non-negative,
    • + *
  • the domain of Y is restricted to [-absY.getUB(), absY.getUB()],
    • + *
  • the domain of absY is restricted to [0, max(|Y.getLB()|, |Y.getUB()|)].
    • + *
+ *

+ * If both variables have enumerated domains, additional filtering is applied to ensure + * that for every value v in the domain of absY, either v or -v + * is in the domain of Y, and vice versa. * * @author Charles Prud'homme * @author Jean-Guillaume Fages @@ -27,20 +38,47 @@ @Explained public class PropAbsolute extends Propagator { - private final IntVar X; - private final IntVar Y; + /** + * Variable representing the absolute value, i.e., absY = |Y|. + */ + final IntVar absY; + /** + * Variable whose absolute value is computed. + */ + final IntVar Y; + /** + * Indicates whether both variables have unfixed enumerated domains. + */ private final boolean bothEnumerated; + /** + * Creates a propagator to enforce X = |Y|. + * + * @param X variable representing the absolute value + * @param Y variable whose absolute value is computed + */ public PropAbsolute(IntVar X, IntVar Y) { - super(ArrayUtils.toArray(X, Y), PropagatorPriority.BINARY, true); - this.X = vars[0]; + this(X, Y, true); + } + + /** + * Creates a propagator to enforce X = |Y|. + * + * @param X variable representing the absolute value + * @param Y variable whose absolute value is computed + * @param react if true, the propagator is initially active + */ + public PropAbsolute(IntVar X, IntVar Y, boolean react) { + super(ArrayUtils.toArray(X, Y), PropagatorPriority.BINARY, react); + this.absY = vars[0]; this.Y = vars[1]; bothEnumerated = X.hasUnfixedEnumeratedDomain() && Y.hasUnfixedEnumeratedDomain(); } @Override public int getPropagationConditions(int vIdx) { - if (vars[0].hasEnumeratedDomain() && vars[1].hasEnumeratedDomain()) { + // Full propagation for enumerated domains, bound and instantiation events otherwise + if (absY.hasEnumeratedDomain() && Y.hasEnumeratedDomain()) { return IntEventType.all(); } else { return IntEventType.boundAndInst(); @@ -49,17 +87,41 @@ public int getPropagationConditions(int vIdx) { @Override public ESat isEntailed() { - if (vars[0].getUB() < 0) { + // If the upper bound of absY is negative, the constraint is always false (absY = |Y| >= 0) + if (absY.getUB() < 0) { return ESat.FALSE; - } else if (vars[0].isInstantiated()) { - if (vars[1].isInstantiated()) { - return ESat.eval(vars[0].getValue() == Math.abs(vars[1].getValue())); - } else if (vars[1].getDomainSize() == 2 && - vars[1].contains(vars[0].getValue()) && - vars[1].contains(-vars[0].getValue())) { - return ESat.TRUE; - } else if (!vars[1].contains(vars[0].getValue()) && - !vars[1].contains(-vars[0].getValue())) { + } else if (absY.isInstantiated()) { + int absVal = absY.getValue(); + if (Y.isInstantiated()) { + // Both variables are instantiated: check if absY.getValue() == |Y.getValue()| + return ESat.eval(absVal == Math.abs(Y.getValue())); + } else { + if (absVal == 0) { + // |Y| = 0 ⇔ Y = 0 + if (Y.getDomainSize() == 1 && Y.contains(0)) { + return ESat.TRUE; // Y can only be 0 + } else if (!Y.contains(0)) { + return ESat.FALSE; // Y cannot be 0 + } else { + return ESat.UNDEFINED; // Y may or may not be 0 + } + } else { + // |Y| = absVal ⇔ Y ∈ {absVal, -absVal} + if (Y.getDomainSize() == 2 && + Y.contains(absVal) && + Y.contains(-absVal)) { + return ESat.TRUE; // Y can only be absVal or -absVal + } else if (!Y.contains(absVal) && !Y.contains(-absVal)) { + return ESat.FALSE; // Y can be neither absVal nor -absVal + } else { + return ESat.UNDEFINED; + } + } + } + } else if (Y.isInstantiated()) { + // Y is instantiated, absY is not: check if |Y.getValue()| is in absY's domain + int absYVal = Math.abs(Y.getValue()); + if (!absY.contains(absYVal)) { return ESat.FALSE; } else { return ESat.UNDEFINED; @@ -71,7 +133,7 @@ public ESat isEntailed() { @Override public String toString() { - return String.format("%s = |%s|", vars[0].toString(), vars[1].toString()); + return String.format("%s = |%s|", absY.toString(), Y.toString()); } //*********************************************************************************** @@ -80,7 +142,8 @@ public String toString() { @Override public void propagate(int evtmask) throws ContradictionException { - X.updateLowerBound(0, this, Reason.undef()); + // Initial propagation: ensure absY is non-negative and apply bounds filtering + absY.updateLowerBound(0, this, Reason.undef()); setBounds(); if (bothEnumerated) { enumeratedFiltering(); @@ -91,15 +154,17 @@ public void propagate(int evtmask) throws ContradictionException { public void propagate(int varIdx, int mask) throws ContradictionException { if (IntEventType.isInstantiate(mask)) { if (varIdx == 1) { - X.instantiateTo(Math.abs(Y.getValue()), this, lcg() ? this.r(Y.getValLit()) : Reason.undef()); + // Y is instantiated: set absY to |Y| + absY.instantiateTo(Math.abs(Y.getValue()), this, lcg() ? this.r(Y.getValLit()) : Reason.undef()); setPassive(); } else if (Y.hasEnumeratedDomain()) { - int val = X.getValue(); - Y.updateLowerBound(-val, this, lcg() ? this.r(X.getValLit()) : Reason.undef()); - Y.updateUpperBound(val, this, lcg() ? this.r(X.getValLit()) : Reason.undef()); + // absY is instantiated: restrict Y to [-absY, absY] and remove (0, absY) if needed + int val = absY.getValue(); + Y.updateLowerBound(-val, this, lcg() ? this.r(absY.getValLit()) : Reason.undef()); + Y.updateUpperBound(val, this, lcg() ? this.r(absY.getValLit()) : Reason.undef()); val--; if (val >= 0) { - removeInterval(Y, -val, val, lcg() ? this.r(X.getValLit()) : Reason.undef()); + removeInterval(Y, -val, val, lcg() ? this.r(absY.getValLit()) : Reason.undef()); } setPassive(); } else { @@ -117,55 +182,55 @@ public void propagate(int varIdx, int mask) throws ContradictionException { private void setBounds() throws ContradictionException { // X = |Y| - int max = X.getUB(); - int min = X.getLB(); - Y.updateLowerBound(-max, this, lcg() ? this.r(X.getMaxLit()) : Reason.undef()); - Y.updateUpperBound(max, this, lcg() ? this.r(X.getMaxLit()) : Reason.undef()); + int max = absY.getUB(); + int min = absY.getLB(); + Y.updateLowerBound(-max, this, lcg() ? this.r(absY.getMaxLit()) : Reason.undef()); + Y.updateUpperBound(max, this, lcg() ? this.r(absY.getMaxLit()) : Reason.undef()); if (1 - min <= min -1) { - removeInterval(Y, 1 - min, min - 1, lcg() ? this.r(X.getMinLit()) : Reason.undef()); + removeInterval(Y, 1 - min, min - 1, lcg() ? this.r(absY.getMinLit()) : Reason.undef()); } ///////////////////////////////////////////////// - int prevLB = X.getLB(); - int prevUB = X.getUB(); + int prevLB = absY.getLB(); + int prevUB = absY.getUB(); min = Y.getLB(); max = Y.getUB(); if (max <= 0) { - X.updateLowerBound(-max, this, + absY.updateLowerBound(-max, this, lcg() ? this.r(Y.getMaxLit()) : Reason.undef()); - X.updateUpperBound(-min, this, + absY.updateUpperBound(-min, this, lcg() ? this.r(Y.getMinLit(), Y.getMaxLit()) : Reason.undef()); } else if (min >= 0) { - X.updateLowerBound(min, this, + absY.updateLowerBound(min, this, lcg() ? this.r(Y.getMinLit()) : Reason.undef()); - X.updateUpperBound(max, this, + absY.updateUpperBound(max, this, lcg() ? this.r(Y.getMinLit(), Y.getMaxLit()) : Reason.undef()); } else { if (Y.hasEnumeratedDomain() && !lcg()) { int mP = Y.nextValue(-1); int mN = -Y.previousValue(1); - X.updateLowerBound(Math.min(mP, mN), this); + absY.updateLowerBound(Math.min(mP, mN), this); } - X.updateUpperBound(Math.max(-min, max), this, + absY.updateUpperBound(Math.max(-min, max), this, lcg() ? this.r(Y.getMinLit(), Y.getMaxLit()) : Reason.undef()); } - if (prevLB != X.getLB() || prevUB != X.getUB()) setBounds(); + if (prevLB != absY.getLB() || prevUB != absY.getUB()) setBounds(); } private void enumeratedFiltering() throws ContradictionException { - int min = X.getLB(); - int max = X.getUB(); - for (int v = min; v <= max; v = X.nextValue(v)) { + int min = absY.getLB(); + int max = absY.getUB(); + for (int v = min; v <= max; v = absY.nextValue(v)) { if (!(Y.contains(v) || Y.contains(-v))) { - X.removeValue(v, this, + absY.removeValue(v, this, lcg() ? this.r(Y.getLit(v, IntVar.LR_EQ), Y.getLit(-v, IntVar.LR_EQ)) : Reason.undef()); } } min = Y.getLB(); max = Y.getUB(); for (int v = min; v <= max; v = Y.nextValue(v)) { - if (!(X.contains(Math.abs(v)))) { + if (!(absY.contains(Math.abs(v)))) { Y.removeValue(v, this, - lcg() ? this.r(X.getLit(Math.abs(v), IntVar.LR_EQ)) : Reason.undef()); + lcg() ? this.r(absY.getLit(Math.abs(v), IntVar.LR_EQ)) : Reason.undef()); } } } diff --git a/solver/src/main/java/org/chocosolver/solver/constraints/binary/PropAbsoluteLight.java b/solver/src/main/java/org/chocosolver/solver/constraints/binary/PropAbsoluteLight.java index ff6e6be8a5..a29bec3796 100644 --- a/solver/src/main/java/org/chocosolver/solver/constraints/binary/PropAbsoluteLight.java +++ b/solver/src/main/java/org/chocosolver/solver/constraints/binary/PropAbsoluteLight.java @@ -8,35 +8,43 @@ import org.chocosolver.sat.Reason; import org.chocosolver.solver.constraints.Explained; -import org.chocosolver.solver.constraints.Propagator; -import org.chocosolver.solver.constraints.PropagatorPriority; import org.chocosolver.solver.exception.ContradictionException; import org.chocosolver.solver.variables.IntVar; import org.chocosolver.solver.variables.events.IntEventType; -import org.chocosolver.util.ESat; -import org.chocosolver.util.tools.ArrayUtils; /** - * Enforces X = |Y| - *
+ * A light propagator to enforce the constraint absY = |Y|. + *

+ * This is a simplified version of {@link PropAbsolute} that only performs + * bounds-based filtering (no enumerated domain filtering). It is more efficient + * for problems where variables have large domains or when full domain filtering is not required. + *

+ * The propagator is created with react = false, meaning it is not initially active + * in the propagation engine. It only reacts to bound and instantiation events. * * @author Charles Prud'homme * @since 04/07/2025 + * @see PropAbsolute */ @Explained -public class PropAbsoluteLight extends Propagator { - - private final IntVar absY; - private final IntVar Y; +public class PropAbsoluteLight extends PropAbsolute { + /** + * Creates a light propagator to enforce X = |Y|. + *

+ * Note: This propagator is created with react = false. + * + * @param X variable representing the absolute value + * @param Y variable whose absolute value is computed + */ public PropAbsoluteLight(IntVar X, IntVar Y) { - super(ArrayUtils.toArray(X, Y), PropagatorPriority.BINARY, false); - this.absY = vars[0]; - this.Y = vars[1]; + super(X, Y, false); } @Override public int getPropagationConditions(int vIdx) { + // For absY (vIdx=0): only react to upper bound and instantiation events + // For Y (vIdx=1): react to all bound and instantiation events if (vIdx == 0) { return IntEventType.upperBoundAndInst(); } else { @@ -44,58 +52,37 @@ public int getPropagationConditions(int vIdx) { } } - @Override - public ESat isEntailed() { - if (vars[0].getUB() < 0) { - return ESat.FALSE; - } else if (vars[0].isInstantiated()) { - if (vars[1].isInstantiated()) { - return ESat.eval(vars[0].getValue() == Math.abs(vars[1].getValue())); - } else if (vars[1].getDomainSize() == 2 && - vars[1].contains(vars[0].getValue()) && - vars[1].contains(-vars[0].getValue())) { - return ESat.TRUE; - } else if (!vars[1].contains(vars[0].getValue()) && - !vars[1].contains(-vars[0].getValue())) { - return ESat.FALSE; - } else { - return ESat.UNDEFINED; - } - } else { - return ESat.UNDEFINED; - } - } - - @Override - public String toString() { - return String.format("%s = |%s|", vars[0].toString(), vars[1].toString()); - } - //*********************************************************************************** // FILTERING //*********************************************************************************** @Override public void propagate(int evtmask) throws ContradictionException { + // Ensure absY is non-negative absY.updateLowerBound(0, this, Reason.undef()); boolean loop; do { int l = Y.getLB(); int u = Y.getUB(); + // Update absY bounds based on Y's domain if (l >= 0) { + // Y is non-negative: absY ∈ [l, u] absY.updateLowerBound(l, this, lcg() ? this.r(Y.getMinLit()) : Reason.undef()); absY.updateUpperBound(u, this, lcg() ? this.r(Y.getMinLit(), Y.getMaxLit()) : Reason.undef()); } else if (u <= 0) { + // Y is non-positive: absY ∈ [-u, -l] absY.updateLowerBound(-u, this, lcg() ? this.r(Y.getMaxLit()) : Reason.undef()); absY.updateUpperBound(-l, this, lcg() ? this.r(Y.getMaxLit(), Y.getMinLit()) : Reason.undef()); } else { + // Y spans zero: absY ∈ [0, max(-l, u)] int t = Math.max(-l, u); absY.updateUpperBound(t, this, lcg() ? this.r(Y.getMaxLit(), Y.getMinLit()) : Reason.undef()); } + // Update Y bounds based on absY's upper bound int au = absY.getUB(); loop = Y.updateUpperBound(au, this, lcg() ? this.r(absY.getMaxLit()) : Reason.undef()); loop |= Y.updateLowerBound(-au, this, lcg() ? this.r(absY.getMaxLit()) : Reason.undef()); - }while(loop); + } while (loop); } } diff --git a/solver/src/test/java/org/chocosolver/solver/constraints/binary/AbsoluteLightTest.java b/solver/src/test/java/org/chocosolver/solver/constraints/binary/AbsoluteLightTest.java new file mode 100644 index 0000000000..0111e5d703 --- /dev/null +++ b/solver/src/test/java/org/chocosolver/solver/constraints/binary/AbsoluteLightTest.java @@ -0,0 +1,26 @@ +/* + * This file is part of choco-solver, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.solver.constraints.binary; + +import org.chocosolver.solver.Model; +import org.chocosolver.solver.constraints.Constraint; +import org.chocosolver.solver.constraints.ConstraintsName; +import org.chocosolver.solver.variables.IntVar; + +/** + *
+ * + * @author Charles Prud'homme + * @since 21/08/2026 + */ +public class AbsoluteLightTest extends AbsoluteTest { + + @Override + protected Constraint make(IntVar[] vars, Model model) { + return new Constraint(ConstraintsName.ABSOLUTE, new PropAbsoluteLight(vars[0], vars[1])); + } +} diff --git a/solver/src/test/java/org/chocosolver/solver/constraints/binary/AbsoluteTest.java b/solver/src/test/java/org/chocosolver/solver/constraints/binary/AbsoluteTest.java new file mode 100644 index 0000000000..c45dac6af1 --- /dev/null +++ b/solver/src/test/java/org/chocosolver/solver/constraints/binary/AbsoluteTest.java @@ -0,0 +1,81 @@ +/* + * This file is part of choco-solver, http://choco-solver.org/ + * Copyright (c) 1999, IMT Atlantique. + * SPDX-License-Identifier: BSD-3-Clause. + * See LICENSE file in the project root for full license information. + */ +package org.chocosolver.solver.constraints.binary; + +import org.chocosolver.solver.Model; +import org.chocosolver.solver.Providers; +import org.chocosolver.solver.constraints.Constraint; +import org.chocosolver.solver.constraints.ConstraintsName; +import org.chocosolver.solver.search.strategy.strategy.FullyRandom; +import org.chocosolver.solver.variables.BoolVar; +import org.chocosolver.solver.variables.IntVar; +import org.chocosolver.util.ESat; +import org.testng.Assert; +import org.testng.annotations.DataProvider; +import org.testng.annotations.Test; + +/** + *
+ * + * @author Charles Prud'homme + * @since 21/08/2026 + */ +public class AbsoluteTest extends AbstractBinaryTest { + + @Override + protected int validTuple(int vx, int vy) { + return Math.abs(vy) == vx ? 1 : 0; + } + + @Override + protected Constraint make(IntVar[] vars, Model model) { + return new Constraint(ConstraintsName.ABSOLUTE, new PropAbsolute(vars[0], vars[1])); + } + + @Test(groups = "1s", timeOut = 30_000, dataProviderClass = Providers.class, dataProvider = "random") + @Providers.Arguments(values = {"1", "50", "1"}) + public void testReification(int seed) { + Model model = new Model(); + + IntVar base = model.intVar("base", new int[]{-2, 0}); + IntVar result = model.intVar("result", new int[]{0, 1}); + BoolVar truth = make(new IntVar[]{result, base}, model).reify(); + + // Make the issue deterministic and independent of the default search strategy. + model.getSolver().setSearch( + new FullyRandom(new IntVar[]{base, result, truth}, seed) + ); + + while (model.getSolver().solve()) { + Assert.assertTrue(check(base.getValue(), result.getValue(), truth.getValue())); + } + Assert.assertEquals(model.getSolver().getSolutionCount(), 4); + } + + private boolean check(int b, int r, int t) { + return (Math.abs(b) == r) == (t == 1); + } + + @DataProvider + public Object[][] combinations(){ + return new Object[][]{ + {new int[]{0,1}, ESat.UNDEFINED}, + {new int[]{0}, ESat.TRUE}, + {new int[]{1, 2}, ESat.FALSE}, + }; + } + + @Test(groups = "1s", dataProvider = "combinations") + public void testXY(int[] dom, ESat expected){ + Model model = new Model(); + + IntVar X = model.intVar("X", 0); + IntVar Y = model.intVar("result", dom); + Constraint c = make(new IntVar[]{X, Y}, model); + Assert.assertEquals(c.getPropagator(0).isEntailed(), expected); + } +} diff --git a/solver/src/test/java/org/chocosolver/solver/constraints/binary/AbstractBinaryTest.java b/solver/src/test/java/org/chocosolver/solver/constraints/binary/AbstractBinaryTest.java index e61925de95..7ad627bc11 100644 --- a/solver/src/test/java/org/chocosolver/solver/constraints/binary/AbstractBinaryTest.java +++ b/solver/src/test/java/org/chocosolver/solver/constraints/binary/AbstractBinaryTest.java @@ -133,4 +133,37 @@ public void test2() { Assert.assertEquals(cp, base, seed +" >> found: " + cp + " solutions, while " + base + " are expected (" + seed + ")"); } } + + @Test(groups="10s", timeOut=60000) + public void testReified() { + boolean bounded; // true if domains are bounded, false if they are enumerated + Random rand = new Random(0); + for (int k = 0; k < 20000; k++) { + long seed = System.currentTimeMillis(); + if(k==0){ + seed = 1410851231099L; + } + rand.setSeed(seed); + bounded = rand.nextBoolean(); + int size = 5; // domain size + int range = 15; // value range + int[][] domains; + if (bounded) { + domains = DomainBuilder.buildFullDomains(2, size, range, rand); + } else { + domains = DomainBuilder.buildFullDomains2(2, size, range, rand, rand.nextDouble(), rand.nextBoolean()); + } + // total number of solutions: brut force algorithm + long base = brutForceTest(domains, bounded); + Model s = modeler(domains, bounded, seed); + try { + while (s.getSolver().solve()) ; + } catch (AssertionError ae) { + System.err.printf("seed: %d\n", seed); + throw ae; + } + long cp = s.getSolver().getSolutionCount(); + Assert.assertEquals(cp, base, "found: " + cp + " solutions, while " + base + " are expected (" + seed + ")"); + } + } } From a66c60ecc5b4eeb088dedc785cea509093011d11 Mon Sep 17 00:00:00 2001 From: Charles Prud'homme Date: Fri, 21 Aug 2026 14:41:50 +0200 Subject: [PATCH 06/12] Rename tests --- .../parser/{T_annotation.java => AnnotationTest.java} | 2 +- .../parser/{T_annotations.java => AnnotationsTest.java} | 2 +- .../flatzinc/parser/{T_bool_const.java => BoolConstTest.java} | 2 +- .../parser/{T_constraint.java => ConstraintTest.java} | 4 ++-- .../parser/flatzinc/parser/{T_expr.java => ExprTest.java} | 2 +- .../parser/{T_flatzinc_model.java => FlatzincModelTest.java} | 2 +- .../flatzinc/parser/{T_index_set.java => IndexSetTest.java} | 2 +- .../flatzinc/parser/{T_par_type.java => ParTypeTest.java} | 2 +- .../flatzinc/parser/{T_par_type_u.java => ParTypeUTest.java} | 2 +- .../flatzinc/parser/{T_param_decl.java => ParamDeclTest.java} | 2 +- .../flatzinc/parser/{T_solve_goal.java => SolveGoalTest.java} | 2 +- .../flatzinc/parser/{T_var_decl.java => VarDeclTest.java} | 2 +- .../flatzinc/parser/{T_var_type.java => VarTypeTest.java} | 2 +- .../flatzinc/parser/{T_var_type_u.java => VarTypeUTest.java} | 2 +- 14 files changed, 15 insertions(+), 15 deletions(-) rename parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/{T_annotation.java => AnnotationTest.java} (96%) rename parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/{T_annotations.java => AnnotationsTest.java} (98%) rename parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/{T_bool_const.java => BoolConstTest.java} (94%) rename parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/{T_constraint.java => ConstraintTest.java} (95%) rename parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/{T_expr.java => ExprTest.java} (98%) rename parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/{T_flatzinc_model.java => FlatzincModelTest.java} (99%) rename parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/{T_index_set.java => IndexSetTest.java} (96%) rename parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/{T_par_type.java => ParTypeTest.java} (98%) rename parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/{T_par_type_u.java => ParTypeUTest.java} (97%) rename parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/{T_param_decl.java => ParamDeclTest.java} (97%) rename parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/{T_solve_goal.java => SolveGoalTest.java} (98%) rename parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/{T_var_decl.java => VarDeclTest.java} (99%) rename parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/{T_var_type.java => VarTypeTest.java} (99%) rename parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/{T_var_type_u.java => VarTypeUTest.java} (98%) diff --git a/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_annotation.java b/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/AnnotationTest.java similarity index 96% rename from parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_annotation.java rename to parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/AnnotationTest.java index 28f607ce0a..cbb7404f85 100644 --- a/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_annotation.java +++ b/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/AnnotationTest.java @@ -20,7 +20,7 @@ * @author Charles Prud'homme * @since 18/10/12 */ -public class T_annotation extends GrammarTest { +public class AnnotationTest extends GrammarTest { @Test(groups = "1s") public void test1() throws IOException, RecognitionException { diff --git a/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_annotations.java b/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/AnnotationsTest.java similarity index 98% rename from parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_annotations.java rename to parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/AnnotationsTest.java index 77dd76812e..a7b5185596 100644 --- a/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_annotations.java +++ b/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/AnnotationsTest.java @@ -21,7 +21,7 @@ * @author Charles Prud'homme * @since 18/10/12 */ -public class T_annotations extends GrammarTest { +public class AnnotationsTest extends GrammarTest { @Test(groups = "1s") public void test0() throws IOException, RecognitionException { diff --git a/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_bool_const.java b/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/BoolConstTest.java similarity index 94% rename from parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_bool_const.java rename to parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/BoolConstTest.java index 28bd817981..29038840a5 100644 --- a/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_bool_const.java +++ b/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/BoolConstTest.java @@ -18,7 +18,7 @@ * @author Charles Prud'homme * @since 18/10/12 */ -public class T_bool_const extends GrammarTest { +public class BoolConstTest extends GrammarTest { @Test(groups = "1s") diff --git a/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_constraint.java b/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/ConstraintTest.java similarity index 95% rename from parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_constraint.java rename to parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/ConstraintTest.java index 0d89327e63..d2da135ce8 100644 --- a/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_constraint.java +++ b/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/ConstraintTest.java @@ -23,7 +23,7 @@ * @author Charles Prud'homme * @since 18/10/12 */ -public class T_constraint extends GrammarTest { +public class ConstraintTest extends GrammarTest { Model mSolver; Datas map; @@ -37,7 +37,7 @@ public void before() { @Test(groups = "1s") public void test1() throws IOException { map.register("x", mSolver.intVar("x", 0, 2, true)); - Flatzinc4Parser fp = parser("constraint int_le(0,x); % 0<= x\n", mSolver, map); + Flatzinc4Parser fp = parser("constraint int_le(1,x); % 0<= x\n", mSolver, map); fp.constraint(); Assert.assertEquals(mSolver.getCstrs().length, 1); Constraint c = mSolver.getCstrs()[0]; diff --git a/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_expr.java b/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/ExprTest.java similarity index 98% rename from parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_expr.java rename to parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/ExprTest.java index 6c95d4f650..03a72bb067 100644 --- a/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_expr.java +++ b/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/ExprTest.java @@ -22,7 +22,7 @@ * @author Charles Prud'homme * @since 18/10/12 */ -public class T_expr extends GrammarTest { +public class ExprTest extends GrammarTest { @Test(groups = "1s") public void test1() throws IOException, RecognitionException { diff --git a/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_flatzinc_model.java b/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/FlatzincModelTest.java similarity index 99% rename from parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_flatzinc_model.java rename to parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/FlatzincModelTest.java index 590c4f45ea..836a53f9f8 100644 --- a/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_flatzinc_model.java +++ b/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/FlatzincModelTest.java @@ -22,7 +22,7 @@ * @author Charles Prud'homme * @since 19/10/12 */ -public class T_flatzinc_model extends GrammarTest { +public class FlatzincModelTest extends GrammarTest { Model mSolver; Datas datas; diff --git a/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_index_set.java b/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/IndexSetTest.java similarity index 96% rename from parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_index_set.java rename to parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/IndexSetTest.java index 6ff00ae48d..866a29c770 100644 --- a/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_index_set.java +++ b/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/IndexSetTest.java @@ -22,7 +22,7 @@ * @author Charles Prud'homme * @since 18/10/12 */ -public class T_index_set extends GrammarTest { +public class IndexSetTest extends GrammarTest { @Test(groups = "1s") public void test1() throws IOException, RecognitionException { diff --git a/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_par_type.java b/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/ParTypeTest.java similarity index 98% rename from parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_par_type.java rename to parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/ParTypeTest.java index fc3024caac..435aa33632 100644 --- a/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_par_type.java +++ b/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/ParTypeTest.java @@ -20,7 +20,7 @@ * @author Charles Prud'homme * @since 18/10/12 */ -public class T_par_type extends GrammarTest { +public class ParTypeTest extends GrammarTest { @Test(groups = "1s") public void test1() throws IOException, RecognitionException { diff --git a/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_par_type_u.java b/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/ParTypeUTest.java similarity index 97% rename from parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_par_type_u.java rename to parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/ParTypeUTest.java index f6caad86eb..58f221fe08 100644 --- a/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_par_type_u.java +++ b/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/ParTypeUTest.java @@ -20,7 +20,7 @@ * @author Charles Prud'homme * @since 18/10/12 */ -public class T_par_type_u extends GrammarTest { +public class ParTypeUTest extends GrammarTest { @Test(groups = "1s") public void test1() throws IOException, RecognitionException { diff --git a/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_param_decl.java b/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/ParamDeclTest.java similarity index 97% rename from parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_param_decl.java rename to parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/ParamDeclTest.java index 2827b24000..7cf1b615ec 100644 --- a/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_param_decl.java +++ b/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/ParamDeclTest.java @@ -19,7 +19,7 @@ * @author Charles Prud'homme * @since 18/10/12 */ -public class T_param_decl extends GrammarTest { +public class ParamDeclTest extends GrammarTest { @Test(groups = "1s") public void test1() throws IOException { diff --git a/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_solve_goal.java b/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/SolveGoalTest.java similarity index 98% rename from parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_solve_goal.java rename to parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/SolveGoalTest.java index 62f31f3a81..f9fda97038 100644 --- a/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_solve_goal.java +++ b/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/SolveGoalTest.java @@ -20,7 +20,7 @@ * @author Charles Prud'homme * @since 18/10/12 */ -public class T_solve_goal extends GrammarTest { +public class SolveGoalTest extends GrammarTest { Model mSolver; Datas datas; diff --git a/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_var_decl.java b/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/VarDeclTest.java similarity index 99% rename from parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_var_decl.java rename to parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/VarDeclTest.java index 075b424265..08bc333d16 100644 --- a/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_var_decl.java +++ b/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/VarDeclTest.java @@ -26,7 +26,7 @@ * @author Charles Prud'homme * @since 18/10/12 */ -public class T_var_decl extends GrammarTest { +public class VarDeclTest extends GrammarTest { Model mSolver; Datas datas; diff --git a/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_var_type.java b/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/VarTypeTest.java similarity index 99% rename from parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_var_type.java rename to parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/VarTypeTest.java index 0cafa1685b..50d05bac95 100644 --- a/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_var_type.java +++ b/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/VarTypeTest.java @@ -20,7 +20,7 @@ * @author Charles Prud'homme * @since 18/10/12 */ -public class T_var_type extends GrammarTest { +public class VarTypeTest extends GrammarTest { @Test(groups = "1s") public void test1() throws IOException, RecognitionException { diff --git a/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_var_type_u.java b/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/VarTypeUTest.java similarity index 98% rename from parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_var_type_u.java rename to parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/VarTypeUTest.java index ad548b997c..a1e24ebe12 100644 --- a/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/T_var_type_u.java +++ b/parsers/src/test/java/org/chocosolver/parser/flatzinc/parser/VarTypeUTest.java @@ -20,7 +20,7 @@ * @author Charles Prud'homme * @since 18/10/12 */ -public class T_var_type_u extends GrammarTest { +public class VarTypeUTest extends GrammarTest { @Test(groups = "1s") public void test1() throws IOException, RecognitionException { From f9570e4eab462d5c9e1dc57e3886374ee89b9926 Mon Sep 17 00:00:00 2001 From: Charles Prud'homme Date: Mon, 31 Aug 2026 10:33:46 +0200 Subject: [PATCH 07/12] Fix error in ReversePropagationGuidedNeighborhood + update Javadoc --- .../PropagationGuidedNeighborhood.java | 118 ++++++++++++++---- .../ReversePropagationGuidedNeighborhood.java | 118 ++++++++++++++---- .../solver/search/loop/LNSTest.java | 9 +- 3 files changed, 195 insertions(+), 50 deletions(-) diff --git a/solver/src/main/java/org/chocosolver/solver/search/loop/lns/neighbors/PropagationGuidedNeighborhood.java b/solver/src/main/java/org/chocosolver/solver/search/loop/lns/neighbors/PropagationGuidedNeighborhood.java index 34a5d825a6..ce8b31a84f 100644 --- a/solver/src/main/java/org/chocosolver/solver/search/loop/lns/neighbors/PropagationGuidedNeighborhood.java +++ b/solver/src/main/java/org/chocosolver/solver/search/loop/lns/neighbors/PropagationGuidedNeighborhood.java @@ -17,10 +17,22 @@ import java.util.stream.IntStream; /** - * A Propagation Guided LNS + * A Propagation Guided Large Neighborhood Search (LNS) neighbor. *

* Based on "Propagation Guided Large Neighborhood Search", Perron et al. CP2004. - *
+ *

+ * This implementation selects variables to be part of the fragment (to be frozen) based on + * the impact of constraint propagation. The algorithm maintains a fragment of variables + * that are frozen to their current values. It iteratively selects variables to add to the + * fragment, prioritizing those that cause the most domain reduction when frozen. + *

+ * Variables that cause significant domain reduction in other variables through propagation + * are considered most influential and are prioritized for inclusion in the fragment. + * This creates a dynamic neighborhood that adapts based on constraint propagation effects. + *

+ * This strategy is particularly effective when the constraint propagation provides + * strong guidance on which variables are most influential in reducing the search space. + * For a reverse approach, see {@link ReversePropagationGuidedNeighborhood}. * * @author Charles Prud'homme * @since 08/04/13 @@ -29,61 +41,79 @@ public class PropagationGuidedNeighborhood extends IntNeighbor { /** - * Number of variables + * Number of variables in the neighborhood */ protected final int n; /** - * Domain size of each variable in {@link #variables} + * Current domain size of each variable in {@link #variables} */ protected int[] curDoms; /** - * Domain size of each variable in {@link #variables} before propagation + * Domain size of each variable in {@link #variables} before the current propagation step. + * Used to compute the domain reduction caused by freezing a variable. */ protected int[] befDoms; /** - * Store the modified variables + * Stores the domain reduction (in absolute values) for each variable, + * used to rank variables by their impact on propagation */ protected int[] all; /** - * For randomness + * Random number generator for random variable selection */ protected Random rd; /** - * Intial size of the fragment + * Desired size of the fragment (target logarithmic sum of domain sizes) */ final double desiredSize; /** - * Current size of the fragment + * Current size of the fragment. + * This is dynamically adjusted by {@link #restrictLess()} to increase the neighborhood size + * over time (size *= 1.01 each call). */ double size; /** - * Number of variables modified through propagation to consider while computing the neighbor + * Maximum number of candidate variables to store and consider. + * Only the top listSize variables with the highest domain reduction impact + * are kept as candidates for the next selection. */ int listSize; /** - * Logarithmic cardinality of domains + * Current logarithmic sum of domain sizes of variables in the fragment. + * Used to track progress toward the desired fragment size. + * The loop in {@link #update()} continues while logSum > size. */ double logSum = 0.; /** - * Store the variable elligible for propagation + * List of candidate variable indices eligible for selection. + * Contains variables from the fragment that caused domain reduction when frozen, + * sorted by their impact (highest first) and limited to {@link #listSize} entries. */ List candidates; /** - * Indicate which variables are selected in a fragment + * BitSet indicating which variables are currently in the fragment (to be frozen). + * A bit set to 1 means the variable is in the fragment and will be frozen. */ protected BitSet fragment; /** - * Reference to the model + * Reference to the model containing the variables and constraints */ protected Model mModel; /** - * Create a propagation-guided neighbor for LNS + * Constructs a Propagation Guided LNS neighbor. + *

+ * This neighbor selects variables to be part of the fragment (to be frozen) based on + * the impact of constraint propagation. Variables that cause the most domain reduction + * when frozen are prioritized. * - * @param vars set of variables to consider - * @param desiredSize desired size of the fragment - * @param listSize number of modified variable to store while propagating - * @param seed for randomness + * @param vars the integer variables to consider for the neighborhood + * @param desiredSize the desired size of the fragment (logarithmic sum of domain sizes). + * Note: this is a double value representing a target sum, not a count of variables. + * @param listSize the number of modified variables to store and consider while propagating. + * Variables are ranked by their impact (domain reduction caused) and only the + * top listSize are kept as candidates for the next selection. + * @param seed the seed for the random number generator used when no candidates are available */ public PropagationGuidedNeighborhood(IntVar[] vars, double desiredSize, int listSize, long seed) { super(vars); @@ -97,6 +127,14 @@ public PropagationGuidedNeighborhood(IntVar[] vars, double desiredSize, int list this.fragment = new BitSet(n); } + /** + * Creates a fragment by freezing variables based on propagation guidance. + * Initially computes the logarithmic sum of all variable domain sizes and copies + * current domain sizes to {@link #befDoms}. All variables start in the fragment. + * Then calls {@link #update()} to iteratively select and freeze variables. + * + * @throws ContradictionException if the fragment is trivially infeasible + */ @Override public void fixSomeVariables() throws ContradictionException { logSum = Arrays.stream(variables).mapToDouble(v -> MathUtils.log2(v.getDomainSize())).sum(); @@ -106,9 +144,19 @@ public void fixSomeVariables() throws ContradictionException { } /** - * Create the fragment + * Creates the fragment by iteratively selecting and freezing variables. + * For each selected variable, it freezes the variable to its solution value, + * propagates constraints, and measures the impact on other variables' domains. + * Variables that cause significant domain reduction in others are prioritized for + * inclusion in the fragment. + *

+ * The method stops when either: + *

    + *
  • The logarithmic sum of domain sizes falls below the target size
    • + *
  • No more variables are left in the fragment
    • + *
* - * @throws ContradictionException if the fragment is trivially infeasible + * @throws ContradictionException if propagating the freezing of a variable leads to a contradiction */ protected void update() throws ContradictionException { while (logSum > size && fragment.cardinality() > 0) { @@ -148,7 +196,12 @@ protected void update() throws ContradictionException { } /** - * @return a variable id in {@link #variables} to be part of the fragment + * Selects the next variable to process from the fragment. + * If there are candidate variables (those that caused significant domain reduction when + * frozen), it prioritizes them (selecting from the head of the list). + * Otherwise, it selects a variable randomly from the remaining variables in the fragment. + * + * @return the index of the selected variable in {@link #variables} */ int selectVariable() { int id; @@ -163,23 +216,44 @@ int selectVariable() { return id; } + /** + * Loads the neighborhood state from a solution. + * Resets the current size to the desired size. + * + * @param solution the solution to load from + */ @Override public void loadFromSolution(Solution solution) { super.loadFromSolution(solution); size = desiredSize; } + /** + * Records the current solution. + * Resets the current size to the desired size after recording. + */ @Override public void recordSolution() { super.recordSolution(); size = desiredSize; } + /** + * Restricts the neighborhood less by increasing the fragment size. + * Multiplies the current size by 1.01, allowing the neighborhood to grow + * over time and explore larger fragments. + */ @Override public void restrictLess() { size *= 1.01; } + /** + * Initializes the neighborhood by recording the initial domain sizes of all variables. + * This is called once at the beginning of the search to establish baseline domain sizes + * in {@link #curDoms} and {@link #befDoms} that are used to measure the impact of + * freezing variables during the neighborhood exploration. + */ @Override public void init() { this.curDoms = new int[n]; diff --git a/solver/src/main/java/org/chocosolver/solver/search/loop/lns/neighbors/ReversePropagationGuidedNeighborhood.java b/solver/src/main/java/org/chocosolver/solver/search/loop/lns/neighbors/ReversePropagationGuidedNeighborhood.java index 440f1a9ee3..6f6661229f 100644 --- a/solver/src/main/java/org/chocosolver/solver/search/loop/lns/neighbors/ReversePropagationGuidedNeighborhood.java +++ b/solver/src/main/java/org/chocosolver/solver/search/loop/lns/neighbors/ReversePropagationGuidedNeighborhood.java @@ -17,71 +17,100 @@ import java.util.stream.IntStream; /** - * A Propagation Guided LNS - *

- * Based on "Propagation Guided Large Neighborhood Search", Perron et al. CP2004. - *
+ * A Reverse Propagation Guided Large Neighborhood Search (LNS) neighbor. + *

+ * This implementation works in reverse compared to {@link PropagationGuidedNeighborhood}: + * instead of selecting variables to be part of the fragment (to be frozen), it selects + * variables to NOT be part of the fragment (to be relaxed). The approach is based on + * "Propagation Guided Large Neighborhood Search", Perron et al. CP2004. + *

+ * The algorithm maintains a fragment of variables that are frozen to their current values. + * It iteratively selects variables to remove from the fragment (unfreeze) based on the + * impact of propagation. Variables that cause the most domain reduction when frozen are + * prioritized for removal, creating a dynamic neighborhood that adapts based on constraint + * propagation effects. + *

+ * This strategy can be particularly effective when the constraint propagation provides + * strong guidance on which variables are most influential in reducing the search space. * * @author Charles Prud'homme * @since 08/04/13 */ -public class ReversePropagationGuidedNeighborhood extends IntNeighbor{ +public class ReversePropagationGuidedNeighborhood extends IntNeighbor { /** - * Number of variables + * Number of variables in the neighborhood */ protected final int n; /** - * Domain size of each variable in {@link #variables} + * Initial domain size of each variable in {@link #variables}, + * recorded during initialization */ protected int[] domSiz; /** - * Store the modified variables + * Stores the domain reduction percentage for each variable, + * used to rank variables by their impact on propagation */ protected int[] all; /** - * For randomness + * Random number generator for random variable selection */ protected Random rd; /** - * Intial size of the fragment + * Desired size of the fragment (target logarithmic sum of domain sizes) */ final double desiredSize; /** - * Goal size of the fragment + * Current target size of the fragment (adjusted by epsilon) */ double size; /** - * Number of variables modified through propagation to consider while computing the neighbor + * Maximum number of candidate variables to store and consider. + * Only the top listSize variables with the highest domain reduction impact + * are kept as candidates for the next selection. */ int listSize; /** - * Logarithmic cardinality of domains + * Current logarithmic sum of domain sizes of frozen variables. + * Used to track progress toward the desired fragment size. */ double logSum = 0.; /** - * Restriction parameter + * Adaptive restriction parameter that adjusts the fragment size dynamically. + * It is updated after each call to {@link #fixSomeVariables()} based on the + * actual log-sum achieved, allowing the algorithm to adapt to the problem structure. + * A value greater than 1.0 increases the fragment size, while a value less than 1.0 decreases it. */ private double epsilon = 1.; /** - * Store the variable elligible for propagation + * List of candidate variable indices eligible for selection. + * Contains variables from the fragment that caused domain reduction when frozen, + * sorted by their impact (highest first) and limited to {@link #listSize} entries. */ List candidates; /** - * Indicate which variables are selected in a fragment + * BitSet indicating which variables are currently in the fragment (frozen). + * A bit set to 1 means the variable is frozen to its solution value. */ protected BitSet fragment; /** - * Reference to the model + * Reference to the model containing the variables and constraints */ protected Model mModel; /** - * Create a reverse adaptive neighbor for LNS based on PGLNS, which selects variables to not be part of a fragment - * @param vars variables to consider - * @param desiredSize desired size of the fragment - * @param listSize number of modified variable to store while propagating - * @param seed for randomness + * Constructs a Reverse Propagation Guided LNS neighbor. + *

+ * This neighbor selects variables to NOT be part of the fragment (i.e., to relax/freeze). + * The selection is guided by the impact of constraint propagation: variables that cause + * the most domain reduction when frozen are prioritized. + * + * @param vars the integer variables to consider for the neighborhood + * @param desiredSize the desired size of the fragment (number of variables to freeze) + * @param listSize the number of modified variables to store and consider while propagating. + * Variables are ranked by their impact (domain reduction caused) and only the + * top listSize are kept as candidates for the next selection. + * @param seed the seed for the random number generator used when no candidates are available */ public ReversePropagationGuidedNeighborhood(IntVar[] vars, int desiredSize, int listSize, long seed) { super(vars); @@ -96,6 +125,17 @@ public ReversePropagationGuidedNeighborhood(IntVar[] vars, int desiredSize, int this.fragment = new BitSet(n); } + /** + * Creates a fragment by freezing variables based on reverse propagation guidance. + * Initially, all variables are considered frozen (part of the fragment). + * The method iteratively removes variables from the fragment until the desired size + * is reached or a contradiction is detected. + *

+ * The epsilon parameter is adaptively adjusted based on the actual log-sum of domain + * sizes encountered during the process, allowing the neighborhood size to adapt over time. + * + * @throws ContradictionException if fixing variables leads to a contradiction + */ @Override public void fixSomeVariables() throws ContradictionException { logSum = 0; @@ -104,12 +144,27 @@ public void fixSomeVariables() throws ContradictionException { try { update(); epsilon = (.95 * epsilon) + (.05 * (logSum / size)); - }catch (ContradictionException ce){ + } catch (ContradictionException ce) { epsilon = (.95 * epsilon) + (.05 / size); throw ce; } } + /** + * Updates the fragment by iteratively selecting and removing variables. + * For each selected variable, it temporarily freezes the variable to its solution value, + * propagates constraints, and measures the impact on other variables' domains. + * Variables that cause significant domain reduction in others are prioritized for removal + * from the fragment in subsequent iterations. + *

+ * The method stops when either: + *

    + *
  • The logarithmic sum of domain sizes reaches or exceeds the target size
    • + *
  • No more variables are left in the fragment
    • + *
+ * + * @throws ContradictionException if propagating the freezing of a variable leads to a contradiction + */ protected void update() throws ContradictionException { while (logSum < size && fragment.cardinality() > 0) { // 1. pick a variable @@ -121,7 +176,10 @@ protected void update() throws ContradictionException { mModel.getSolver().pushTrail(); variables[id].instantiateTo(values[id], Cause.Null); - mModel.getSolver().propagate(); + try { + mModel.getSolver().propagate(); + } catch (ContradictionException ignored) { + } fragment.clear(id); for (int i = 0; i < n; i++) { @@ -156,7 +214,12 @@ protected void update() throws ContradictionException { } /** - * @return a variable id in {@link #variables} to be part of the fragment + * Selects the next variable to process from the fragment. + * If there are candidate variables (those that caused significant domain reduction when + * frozen), it prioritizes them. Otherwise, it selects a variable randomly from the + * remaining variables in the fragment. + * + * @return the index of the selected variable in {@link #variables} */ int selectVariable() { int id; @@ -171,6 +234,11 @@ int selectVariable() { return id; } + /** + * Initializes the neighborhood by recording the initial domain sizes of all variables. + * This is called once at the beginning of the search to establish baseline domain sizes + * that are used to measure the impact of freezing variables during the neighborhood exploration. + */ @Override public void init() { this.domSiz = new int[n]; diff --git a/solver/src/test/java/org/chocosolver/solver/search/loop/LNSTest.java b/solver/src/test/java/org/chocosolver/solver/search/loop/LNSTest.java index e12a50668d..604eae8329 100644 --- a/solver/src/test/java/org/chocosolver/solver/search/loop/LNSTest.java +++ b/solver/src/test/java/org/chocosolver/solver/search/loop/LNSTest.java @@ -30,6 +30,8 @@ import org.testng.annotations.DataProvider; import org.testng.annotations.Test; +import java.util.Arrays; + import static java.lang.Math.ceil; import static org.chocosolver.solver.search.strategy.Search.domOverWDegSearch; import static org.chocosolver.solver.search.strategy.Search.lastConflict; @@ -62,7 +64,8 @@ private void knapsack20(final int lns) { Solver r = model.getSolver(); r.setSearch(lastConflict(domOverWDegSearch(objects))); - r.limitTime(900); +// r.limitTime(900); + r.limitNode(3000); switch (lns) { case 0: break; @@ -103,7 +106,7 @@ private void knapsack20(final int lns) { // So, the least we can do is to check that a solution is found Assert.assertTrue(r.getSolutionCount() > 0, "No solution found with LNS=" + lns); // We can also check that the weight is not that bad - Assert.assertTrue(bp >= 7900, "Power is too low with LNS=" + lns); + Assert.assertTrue(bp >= 7900, "Power is too low "+bp+" with LNS=" + lns); Assert.assertTrue(bw >= 1090, "Weight is too low with LNS=" + lns); } @@ -301,7 +304,7 @@ public void testPN1() { } int[] coeffs = new int[nodes]; - for (int i = 0; i < nodes; i++) coeffs[i] = 1; + Arrays.fill(coeffs, 1); model.scalar(costmaxs, coeffs, "=", optVar).post(); model.setObjective(Model.MINIMIZE, optVar); From dfa93b53018db8b3e21f73fc84ddd33965064451 Mon Sep 17 00:00:00 2001 From: Charles Prud'homme Date: Mon, 31 Aug 2026 19:01:12 +0200 Subject: [PATCH 08/12] ReifiedTest: add new tests --- .../constraints/reification/ReifiedTest.java | 306 ++++++++++++++++++ 1 file changed, 306 insertions(+) diff --git a/solver/src/test/java/org/chocosolver/solver/constraints/reification/ReifiedTest.java b/solver/src/test/java/org/chocosolver/solver/constraints/reification/ReifiedTest.java index ce8f849195..2a4a4fd8aa 100644 --- a/solver/src/test/java/org/chocosolver/solver/constraints/reification/ReifiedTest.java +++ b/solver/src/test/java/org/chocosolver/solver/constraints/reification/ReifiedTest.java @@ -505,4 +505,310 @@ public void testofir1() { } solver2.printShortStatistics(); } + + // ======================================================================== + // Tests for issue #1240: Unsound reified variable disequality on bounded domains + // ======================================================================== + + /** + * MWE from issue #1240: reifyXeqY with bounded domains and b=0 should not accept x==y + * Expected: 2 solutions (y=-1 and y=1) + * Bug: 3 solutions including invalid x=0, y=0, equal=0 + */ + @Test(groups = "1s", timeOut = 60000) + public void testIssue1240_reifyXeqY() { + Model model = new Model(); + IntVar x = model.intVar("x", 0, 1, true); + IntVar y = model.intVar("y", -1, 1, true); + BoolVar equal = model.boolVar("equal"); + + model.reifyXeqY(x, y, equal); + model.arithm(x, "=", 0).post(); + model.arithm(equal, "=", 0).post(); + System.out.println(model); + while (model.getSolver().solve()) { + // With x=0 and equal=0, y must not be 0 + assertEquals(x.getValue(), 0, "x should be 0"); + assertEquals(equal.getValue(), 0, "equal should be 0"); + assert x.getValue() != y.getValue() : + String.format("Invalid solution: x=%d, y=%d, equal=%d", + x.getValue(), y.getValue(), equal.getValue()); + } + assertEquals(model.getSolver().getSolutionCount(), 2, "Expected 2 solutions, got " + model.getSolver().getSolutionCount()); + } + + /** + * Variant using reifyXneY with bounded domains and b=1 + * Expected: 2 solutions (y=-1 and y=1) + * Bug: 3 solutions including invalid x=0, y=0, notEqual=1 + */ + @Test(groups = "1s", timeOut = 60000) + public void testIssue1240_reifyXneY() { + Model model = new Model(); + IntVar x = model.intVar("x", 0, 1, true); + IntVar y = model.intVar("y", -1, 1, true); + BoolVar notEqual = model.boolVar("notEqual"); + + model.reifyXneY(x, y, notEqual); + model.arithm(x, "=", 0).post(); + model.arithm(notEqual, "=", 1).post(); + + while (model.getSolver().solve()) { + // With x=0 and notEqual=1, y must not be 0 + assertEquals(x.getValue(), 0, "x should be 0"); + assertEquals(notEqual.getValue(), 1, "notEqual should be 1"); + assert x.getValue() != y.getValue() : + String.format("Invalid solution: x=%d, y=%d, notEqual=%d", + x.getValue(), y.getValue(), notEqual.getValue()); + } + assertEquals(model.getSolver().getSolutionCount(), 2, "Expected 2 solutions, got " + model.getSolver().getSolutionCount()); + } + + /** + * Variant using reifyXeqYC with offset c=0 + * reifyXeqYC(x, y, c, b) means: b = (x == y + c) + * With x=0, c=0, b=0: 0 != y+0, so y != 0 + * y in [-1,1], so solutions are y=-1 and y=1 + */ + @Test(groups = "1s", timeOut = 60000) + public void testIssue1240_reifyXeqYC() { + Model model = new Model(); + IntVar x = model.intVar("x", 0, 1, true); + IntVar y = model.intVar("y", -1, 1, true); + BoolVar equal = model.boolVar("equal"); + + model.reifyXeqYC(x, y, 0, equal); + model.arithm(x, "=", 0).post(); + model.arithm(equal, "=", 0).post(); + + while (model.getSolver().solve()) { + // With x=0, c=0, equal=0: x != y+0 => 0 != y + assert x.getValue() != y.getValue() : + String.format("Invalid solution: x=%d, y=%d, equal=%d", + x.getValue(), y.getValue(), equal.getValue()); + } + assertEquals(model.getSolver().getSolutionCount(), 2, "Expected 2 solutions, got " + model.getSolver().getSolutionCount()); + } + + /** + * Variant using reifyXneYC with offset c=0 + * This should reproduce the issue with the interior value problem + */ + @Test(groups = "1s", timeOut = 60000) + public void testIssue1240_reifyXneYC() { + Model model = new Model(); + IntVar x = model.intVar("x", 0, 1, true); + IntVar y = model.intVar("y", -1, 1, true); + BoolVar notEqual = model.boolVar("notEqual"); + + model.reifyXneYC(x, y, 0, notEqual); + model.arithm(x, "=", 0).post(); + model.arithm(notEqual, "=", 1).post(); + + while (model.getSolver().solve()) { + // With x=0, c=0, notEqual=1: x != y+0 => 0 != y + assert x.getValue() != y.getValue() : + String.format("Invalid solution: x=%d, y=%d, notEqual=%d", + x.getValue(), y.getValue(), notEqual.getValue()); + } + assertEquals(model.getSolver().getSolutionCount(), 2, "Expected 2 solutions, got " + model.getSolver().getSolutionCount()); + } + + /** + * Variant using reifXrelYC with "=" + */ + @Test(groups = "1s", timeOut = 60000) + public void testIssue1240_reifXrelYC_eq() { + Model model = new Model(); + IntVar x = model.intVar("x", 0, 1, true); + IntVar y = model.intVar("y", -1, 1, true); + BoolVar equal = model.boolVar("equal"); + + model.reifXrelYC(x, "=", y, 0, equal); + model.arithm(x, "=", 0).post(); + model.arithm(equal, "=", 0).post(); + + while (model.getSolver().solve()) { + assert x.getValue() != y.getValue() : + String.format("Invalid solution: x=%d, y=%d, equal=%d", + x.getValue(), y.getValue(), equal.getValue()); + } + assertEquals(model.getSolver().getSolutionCount(), 2, "Expected 2 solutions, got " + model.getSolver().getSolutionCount()); + } + + /** + * Variant using reifXrelYC with "!=" + */ + @Test(groups = "1s", timeOut = 60000) + public void testIssue1240_reifXrelYC_ne() { + Model model = new Model(); + IntVar x = model.intVar("x", 0, 1, true); + IntVar y = model.intVar("y", -1, 1, true); + BoolVar notEqual = model.boolVar("notEqual"); + + model.reifXrelYC(x, "!=", y, 0, notEqual); + model.arithm(x, "=", 0).post(); + model.arithm(notEqual, "=", 1).post(); + + while (model.getSolver().solve()) { + assert x.getValue() != y.getValue() : + String.format("Invalid solution: x=%d, y=%d, notEqual=%d", + x.getValue(), y.getValue(), notEqual.getValue()); + } + assertEquals(model.getSolver().getSolutionCount(), 2, "Expected 2 solutions, got " + model.getSolver().getSolutionCount()); + } + + /** + * Variant using impXrelYC with "!=" + */ + @Test(groups = "1s", timeOut = 60000) + public void testIssue1240_impXrelYC() { + Model model = new Model(); + IntVar x = model.intVar("x", 0, 1, true); + IntVar y = model.intVar("y", -1, 1, true); + BoolVar b = model.boolVar("b", true); + + model.impXrelYC(x, "!=", y, 0, b); + model.arithm(x, "=", 0).post(); + + while (model.getSolver().solve()) { + // With b=true (instantiated), we should have x != y + assert x.getValue() != y.getValue() : + String.format("Invalid solution: x=%d, y=%d, b=%d", + x.getValue(), y.getValue(), b.getValue()); + } + assertEquals(model.getSolver().getSolutionCount(), 2, "Expected 2 solutions, got " + model.getSolver().getSolutionCount()); + } + + /** + * Variant using x.eq(y).boolVar() forced to false + */ + @Test(groups = "1s", timeOut = 60000) + public void testIssue1240_eqBoolVar() { + Model model = new Model(); + IntVar x = model.intVar("x", 0, 1, true); + IntVar y = model.intVar("y", -1, 1, true); + BoolVar equal = x.eq(y).boolVar(); + + model.arithm(x, "=", 0).post(); + model.arithm(equal, "=", 0).post(); + + while (model.getSolver().solve()) { + assert x.getValue() != y.getValue() : + String.format("Invalid solution: x=%d, y=%d, equal=%d", + x.getValue(), y.getValue(), equal.getValue()); + } + assertEquals(model.getSolver().getSolutionCount(), 2, "Expected 2 solutions, got " + model.getSolver().getSolutionCount()); + } + + /** + * Variant using x.ne(y).boolVar() forced to true + */ + @Test(groups = "1s", timeOut = 60000) + public void testIssue1240_neBoolVar() { + Model model = new Model(); + IntVar x = model.intVar("x", 0, 1, true); + IntVar y = model.intVar("y", -1, 1, true); + BoolVar notEqual = x.ne(y).boolVar(); + + model.arithm(x, "=", 0).post(); + model.arithm(notEqual, "=", 1).post(); + + while (model.getSolver().solve()) { + assert x.getValue() != y.getValue() : + String.format("Invalid solution: x=%d, y=%d, notEqual=%d", + x.getValue(), y.getValue(), notEqual.getValue()); + } + assertEquals(model.getSolver().getSolutionCount(), 2, "Expected 2 solutions, got " + model.getSolver().getSolutionCount()); + } + + /** + * Variant using x.in(y).boolVar() with single IntVar operand, forced to false + */ + @Test(groups = "1s", timeOut = 60000) + public void testIssue1240_inBoolVar() { + Model model = new Model(); + IntVar x = model.intVar("x", 0, 1, true); + IntVar y = model.intVar("y", -1, 1, true); + BoolVar in = x.in(y).boolVar(); + + model.arithm(x, "=", 0).post(); + model.arithm(in, "=", 0).post(); + + while (model.getSolver().solve()) { + // in=0 means x not in y, so x != y + assert x.getValue() != y.getValue() : + String.format("Invalid solution: x=%d, y=%d, in=%d", + x.getValue(), y.getValue(), in.getValue()); + } + assertEquals(model.getSolver().getSolutionCount(), 2, "Expected 2 solutions, got " + model.getSolver().getSolutionCount()); + } + + /** + * Variant using x.notin(y).boolVar() with single IntVar operand, forced to true + */ + @Test(groups = "1s", timeOut = 60000) + public void testIssue1240_notinBoolVar() { + Model model = new Model(); + IntVar x = model.intVar("x", 0, 1, true); + IntVar y = model.intVar("y", -1, 1, true); + BoolVar notin = x.notin(y).boolVar(); + + model.arithm(x, "=", 0).post(); + model.arithm(notin, "=", 1).post(); + + while (model.getSolver().solve()) { + // notin=1 means x not in y, so x != y + assert x.getValue() != y.getValue() : + String.format("Invalid solution: x=%d, y=%d, notin=%d", + x.getValue(), y.getValue(), notin.getValue()); + } + assertEquals(model.getSolver().getSolutionCount(), 2, "Expected 2 solutions, got " + model.getSolver().getSolutionCount()); + } + + /** + * Test with different domain configurations to ensure the issue is caught + */ + @Test(groups = "1s", timeOut = 60000) + public void testIssue1240_variousDomains() { + // Test with x in [1,2], y in [0,2], equal=0 + Model model = new Model(); + IntVar x = model.intVar("x", 1, 2, true); + IntVar y = model.intVar("y", 0, 2, true); + BoolVar equal = model.boolVar("equal"); + + model.reifyXeqY(x, y, equal); + model.arithm(x, "=", 1).post(); + model.arithm(equal, "=", 0).post(); + + while (model.getSolver().solve()) { + assert x.getValue() != y.getValue() : + String.format("Invalid solution: x=%d, y=%d, equal=%d", + x.getValue(), y.getValue(), equal.getValue()); + } + assertEquals(model.getSolver().getSolutionCount(), 2, "Expected 2 solutions, got " + model.getSolver().getSolutionCount()); + } + + /** + * Test with a different interior value configuration + */ + @Test(groups = "1s", timeOut = 60000) + public void testIssue1240_anotherInteriorValue() { + Model model = new Model(); + IntVar x = model.intVar("x", 5, 10, true); + IntVar y = model.intVar("y", 0, 10, true); + BoolVar equal = model.boolVar("equal"); + + model.reifyXeqY(x, y, equal); + model.arithm(x, "=", 5).post(); + model.arithm(equal, "=", 0).post(); + + while (model.getSolver().solve()) { + assert x.getValue() != y.getValue() : + String.format("Invalid solution: x=%d, y=%d, equal=%d", + x.getValue(), y.getValue(), equal.getValue()); + } + // y can be 0,1,2,3,4,6,7,8,9,10 = 10 values + assertEquals(model.getSolver().getSolutionCount(), 10, "Expected 10 solutions, got " + model.getSolver().getSolutionCount()); + } } \ No newline at end of file From 7e7f42ff13a6553365c5ed390ddc8f123e076115 Mon Sep 17 00:00:00 2001 From: Charles Prud'homme Date: Mon, 31 Aug 2026 19:01:30 +0200 Subject: [PATCH 09/12] PropXneYHalfReif: fix issue #1240 --- .../reification/PropXneYHalfReif.java | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/solver/src/main/java/org/chocosolver/solver/constraints/reification/PropXneYHalfReif.java b/solver/src/main/java/org/chocosolver/solver/constraints/reification/PropXneYHalfReif.java index 762b04e953..8a6272ff30 100644 --- a/solver/src/main/java/org/chocosolver/solver/constraints/reification/PropXneYHalfReif.java +++ b/solver/src/main/java/org/chocosolver/solver/constraints/reification/PropXneYHalfReif.java @@ -51,13 +51,17 @@ public void propagate(int evtmask) throws ContradictionException { } else if (b.isInstantiatedTo(1)) { // if b is true, then x and y must be different if (x.isInstantiated()) { - y.removeValue(x.getValue(), this, - lcg() ? this.r(x.getValLit(), b.getValLit()) : Reason.undef()); - setPassive(); + if(y.removeValue(x.getValue(), this, + lcg() ? this.r(x.getValLit(), b.getValLit()) : Reason.undef()) + || !y.contains(x.getValue())){ + setPassive(); + } }else if (y.isInstantiated()) { - x.removeValue(y.getValue(), this, - lcg() ? this.r(y.getValLit(), b.getValLit()) : Reason.undef()); - setPassive(); + if(x.removeValue(y.getValue(), this, + lcg() ? this.r(y.getValLit(), b.getValLit()) : Reason.undef()) + || !x.contains(y.getValue())){ + setPassive(); + } } } else if (x.isInstantiated() && y.isInstantiated() && x.getValue() == y.getValue()) { // if x and y are instantiated and equal, then b must be false From 85e6fff3189d1cd2a6639af9901ae601fef55ae6 Mon Sep 17 00:00:00 2001 From: Charles Prud'homme Date: Tue, 1 Sep 2026 10:26:43 +0200 Subject: [PATCH 10/12] PropXneYHalfReif and PropXeqYHalfReif: update Javadoc --- .../reification/PropXeqYHalfReif.java | 13 +++++++++++-- .../reification/PropXneYHalfReif.java | 16 ++++++++++++++-- 2 files changed, 25 insertions(+), 4 deletions(-) diff --git a/solver/src/main/java/org/chocosolver/solver/constraints/reification/PropXeqYHalfReif.java b/solver/src/main/java/org/chocosolver/solver/constraints/reification/PropXeqYHalfReif.java index 5aec80d78b..0747029a2b 100644 --- a/solver/src/main/java/org/chocosolver/solver/constraints/reification/PropXeqYHalfReif.java +++ b/solver/src/main/java/org/chocosolver/solver/constraints/reification/PropXeqYHalfReif.java @@ -17,8 +17,17 @@ import org.chocosolver.util.ESat; /** - * A propagator dedicated to express b ⇒ x == y - *
+ * A propagator dedicated to express b ⇒ x == y. + *

+ * This propagator ensures that if b is true, then x and y must be equal. + * When b is false, no filtering is required. + *

+ *

+ * This propagator handles both enumerated and bounded domains. For bounded domains, + * it performs bounds consistency by synchronizing the lower and upper bounds of x and y. + * If both variables have enumerated domains and their combined size is below a threshold, + * it also removes values from one variable that are not in the other's domain. + *

* * @author Charles Prud'homme * @since 08/02/2024 diff --git a/solver/src/main/java/org/chocosolver/solver/constraints/reification/PropXneYHalfReif.java b/solver/src/main/java/org/chocosolver/solver/constraints/reification/PropXneYHalfReif.java index 8a6272ff30..c8b33c7335 100644 --- a/solver/src/main/java/org/chocosolver/solver/constraints/reification/PropXneYHalfReif.java +++ b/solver/src/main/java/org/chocosolver/solver/constraints/reification/PropXneYHalfReif.java @@ -17,8 +17,20 @@ import org.chocosolver.util.ESat; /** - * A propagator dedicated to express b ⇒ x != y - *
+ * A propagator dedicated to express b ⇒ x != y. + *

+ * This propagator ensures that if b is true, then x and y must be different. + * When b is false, no filtering is required. + *

+ *

+ * Important note on bounded domains: + * When x (or y) is instantiated and y (or x) has a bounded domain, attempting to remove + * a value that is interior to the domain (not on a bound) will not change the domain + * representation. However, the propagator must not passivate unconditionally after + * calling {@code removeValue}, as this would fail to check the constraint when search + * later narrows the domain to that value. The propagator checks whether the value was + * actually removed or is no longer in the domain before passivating. + *

* * @author Charles Prud'homme * @since 08/02/2024 From 81962569502e893d907ef2f24c9414e477bbe921 Mon Sep 17 00:00:00 2001 From: Charles Prud'homme Date: Fri, 21 Aug 2026 14:24:11 +0200 Subject: [PATCH 11/12] PR #1234: update tests metrics --- parsers/src/test/resources/xcsp/instances.csv | 34 +++++++++---------- 1 file changed, 17 insertions(+), 17 deletions(-) diff --git a/parsers/src/test/resources/xcsp/instances.csv b/parsers/src/test/resources/xcsp/instances.csv index 6587bfff75..2f3932fd9a 100644 --- a/parsers/src/test/resources/xcsp/instances.csv +++ b/parsers/src/test/resources/xcsp/instances.csv @@ -3,14 +3,14 @@ basics;Allergy.xml.lzma;1;_;1;0 basics;AllInterval-005.xml.lzma;1;_;9;4 basics;Auction-cnt-example_c18.xml.lzma;3;54;9;4 basics;Auction-sum-example_c18.xml.lzma;3;54;9;4 -basics;Bacp-m1-06_c18.xml.lzma;6;10;88170;76399 -basics;Bacp-m2-06_c18.xml.lzma;6;10;268585;223729 +basics;Bacp-m1-06_c18.xml.lzma;6;10;84254;72918 +basics;Bacp-m2-06_c18.xml.lzma;6;10;290531;242205 basics;Bibd-sc-06-050-25-03-10.xml.lzma;1;_;2840;1719 basics;Bibd-sum-06-050-25-03-10.xml.lzma;1;_;1261;849 basics;Blackhole-04-3-00.xml.lzma;1;_;7;0 basics;BusScheduling-cnt-t1.xml.lzma;1;7;204;191 basics;CarSequencing-dingbas.xml.lzma;1;_;14;10 -basics;ChessboardColoration-07-07.xml.lzma;24;2;12039;10363 +basics;ChessboardColoration-07-07.xml.lzma;24;2;9011;7666 basics;ColouredQueens-07.xml.lzma;1;_;37;28 basics;CostasArray-12.xml.lzma;1;_;1116;998 basics;Crossword-lex-vg-5-6.xml.lzma;1;_;11348;10395 @@ -25,41 +25,41 @@ basics;FlexibleJobshop-easy01.xml.lzma;39;253;294;188 basics;FlexibleJobshop-easy02.xml.lzma;60;11;5792;2402 basics;Furniture.xml.lzma;1;603;33;32 basics;GracefulGraph-K02-P04.xml.lzma;1;_;48;44 -basics;GraphColoring-3-fullins-4.xml.lzma;11;6;95931;75505 +basics;GraphColoring-3-fullins-4.xml.lzma;11;6;85960;69074 basics;GraphColoring-qwhdec-o5-h10-1.xml.lzma;1;4;1;0 basics;Hanoi-05.xml.lzma;1;_;31;0 basics;Kakuro-easy-000-ext.xml.lzma;1;_;1;0 basics;Kakuro-easy-000-sumdiff.xml.lzma;1;_;9;7 -basics;Knapsack-30-100-00.xml.lzma;42;709;42195;34412 +basics;Knapsack-30-100-00.xml.lzma;42;709;46578;38254 basics;KnightTour-06-ext03.xml.lzma;1;_;407;337 basics;KnightTour-06-int.xml.lzma;1;_;7561;6362 basics;Langford-3-10.xml.lzma;1;_;38;33 basics;LangfordBin-08.xml.lzma;1;_;585;518 -basics;LowAutocorrelation-015.xml.lzma;17;15;49762;37874 +basics;LowAutocorrelation-015.xml.lzma;17;15;45882;34893 basics;MagicSequence-008-ca.xml.lzma;1;_;6;4 basics;MagicSequence-008-co.xml.lzma;1;_;6;4 basics;MagicSquare-4-table.xml.lzma;1;_;9;3 basics;MagicSquare-6-mdd.xml.lzma;1;_;838;633 basics;MagicSquare-6-sum.xml.lzma;1;_;2871;2150 basics;Mapping-full2x2_mp3.xml.lzma;12;1100;7267;5109 -basics;Mario-easy-4.xml.lzma;13;545;5485;5074 +basics;Mario-easy-4.xml.lzma;13;545;11178;10378 #basics;MarketSplit-01.xml.lzma;0;_;1113575;919484 basics;MSPSP-easy_01.xml.lzma;14;26;1789;800 -basics;MSPSP-hard_01.xml.lzma;4;35;610;510 +basics;MSPSP-hard_01.xml.lzma;4;35;611;510 basics;MultiKnapsack-1-0_X2.xml.lzma;1;_;3;1 basics;MultiKnapsack-1-01.xml.lzma;1;_;3;1 basics;NFC-12_2_10.xml.lzma;31;848;173;108 basics;NFC-12_2_5.xml.lzma;14;1074;76;49 basics;Nonogram-001-regular.xml.lzma;1;_;82;63 basics;Nonogram-001-table.xml.lzma;1;_;82;63 -basics;NurseRostering-00_c18.xml.lzma;14;1202;101768;83362 +basics;NurseRostering-00_c18.xml.lzma;14;1202;116448;95750 basics;Opd-07-007-003.xml.lzma;3;1;98;81 basics;Ortholatin-005.xml.lzma;1;_;94;83 basics;Pb-gr-05.xml.lzma;3;11;221;207 basics;Pb-robin08.xml.lzma;1;_;2984;938 -basics;PeacableArmies-m1-05_c18.xml.lzma;5;4;6302;5013 -basics;PeacableArmies-m2-05_c18.xml.lzma;5;4;2503;2162 -basics;PizzaVoucher-10a_c18.xml.lzma;15;210;10696;9686 +basics;PeacableArmies-m1-05_c18.xml.lzma;5;4;6149;4917 +basics;PeacableArmies-m2-05_c18.xml.lzma;5;4;2525;2179 +basics;PizzaVoucher-10a_c18.xml.lzma;15;210;10835;9815 basics;Primes-15-20-2-1.xml.lzma;1;_;16;10 basics;PrizeCollecting-15-3-5-0.xml.lzma;7;20;1868;1702 basics;qcp-15-120-00_X2.xml.lzma;1;_;415;278 @@ -70,7 +70,7 @@ basics;QuasiGroup-7-09.xml.lzma;1;_;343;294 basics;QueenAttacking-06.xml.lzma;5;0;3882;3136 basics;Queens-0008-m1.xml.lzma;1;_;23;20 basics;RadarSurveillance-8-24-3-2-00.xml.lzma;1;_;92;22 -basics;Ramsey-12.xml.lzma;54;2;55014;31654 +basics;Ramsey-12.xml.lzma;54;2;57445;33115 basics;Rcpsp-j30-01-01_c18.xml.lzma;7;43;199;162 basics;Rlfap-graph-04-opt_c18.xml.lzma;10;394;2651;1656 basics;RoomMate-sr0050-int.xml.lzma;1;_;2;0 @@ -85,10 +85,10 @@ basics;StillLife-wastage-03.xml.lzma;3;6;23;18 basics;StripPacking-C1P1.xml.lzma;1;_;630917;493619 basics;Subisomorphism-A-10.xml.lzma;1;_;30;28 basics;Sudoku-s01a-alldiff.xml.lzma;1;_;1;0 -basics;SumColoring-myciel4_c18.xml.lzma;4;22;42734;39554 -basics;Taillard-os-04-04-0.xml.lzma;28;193;13435;12022 +basics;SumColoring-myciel4_c18.xml.lzma;4;22;45161;41768 +basics;Taillard-os-04-04-0.xml.lzma;28;193;13175;11782 basics;Tal-01_c18.xml.lzma;2;6;11;8 -basics;TeamAssignment-data1_4_6.xml.lzma;19;2948;10776;9744 +basics;TeamAssignment-data1_4_6.xml.lzma;19;2948;11612;10607 basics;TemplateDesign-m1-1_c18.xml.lzma;2;2;133;129 basics;TemplateDesign-m1s-1_c18.xml.lzma;1;2;10;9 basics;TemplateDesign-m2-1_c18.xml.lzma;2;2;167;161 @@ -99,6 +99,6 @@ basics;testObjective1.xml.lzma;2;11;8;5 basics;testPrimitive.xml.lzma;1;_;3;1 #basics;TestSchedulingM18-t30m10r3-15.xml.lzma;93;4149;3450;2650 basics;Tpp-3-3-20-1.xml.lzma;9;126;273;217 -basics;TravelingTournament-a3-galaxy04_c18.xml.lzma;6;416;4160;3792 +basics;TravelingTournament-a3-galaxy04_c18.xml.lzma;6;416;3765;3425 basics;Warehouse-opl.xml.lzma;19;383;130;90 basics;Zebra.xml.lzma;1;_;9;2 \ No newline at end of file From e2ac568422ba21c3396e0aca97a20da90e159a97 Mon Sep 17 00:00:00 2001 From: Charles Prud'homme Date: Wed, 2 Sep 2026 14:59:13 +0200 Subject: [PATCH 12/12] AbsoluteLight: update Javadoc --- .../solver/constraints/IIntConstraintFactory.java | 6 ++++++ .../solver/constraints/binary/PropAbsoluteLight.java | 5 +++++ 2 files changed, 11 insertions(+) diff --git a/solver/src/main/java/org/chocosolver/solver/constraints/IIntConstraintFactory.java b/solver/src/main/java/org/chocosolver/solver/constraints/IIntConstraintFactory.java index 1d2b32bf35..89cdf91fbd 100644 --- a/solver/src/main/java/org/chocosolver/solver/constraints/IIntConstraintFactory.java +++ b/solver/src/main/java/org/chocosolver/solver/constraints/IIntConstraintFactory.java @@ -251,6 +251,12 @@ default Constraint notMember(IntVar var, IntIterableRangeSet set) { /** * Creates an absolute value constraint: var1 = |var2| + *

+ * When LCG (Lazy Clause Generation) is enabled, this uses {@link PropAbsoluteLight} which + * performs bounds-based filtering only and does not propagate holes from var2 to var1. + * For example, if var1 = [0,3] and var2 = [-3, -2, 2, 3], + * the hole -1 in var2 (which would imply 1 is missing in var1) + * is not propagated when using {@link PropAbsoluteLight}. */ default Constraint absolute(IntVar var1, IntVar var2) { assert var1.getModel() == var2.getModel(); diff --git a/solver/src/main/java/org/chocosolver/solver/constraints/binary/PropAbsoluteLight.java b/solver/src/main/java/org/chocosolver/solver/constraints/binary/PropAbsoluteLight.java index a29bec3796..ee3a342dbe 100644 --- a/solver/src/main/java/org/chocosolver/solver/constraints/binary/PropAbsoluteLight.java +++ b/solver/src/main/java/org/chocosolver/solver/constraints/binary/PropAbsoluteLight.java @@ -21,6 +21,11 @@ *

* The propagator is created with react = false, meaning it is not initially active * in the propagation engine. It only reacts to bound and instantiation events. + *

+ * Note: This propagator does not propagate holes that could be made from Y to absY. + * For example, if absY = [0,3] and Y = {-3, -2, 2, 3}, + * the hole {-1, 0, 1} in Y (which would imply 0,1 are missing in absY) + * is not propagated. * * @author Charles Prud'homme * @since 04/07/2025