Skip to content

Fix 1233 #1236

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
cprudhom merged 14 commits into from
Sep 9, 2026
Merged

Fix 1233 #1236

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
e7b46b7
MiniSat: new watch relies on circular approach
cprudhom Aug 21, 2026
1694a1e
MiniSat: move the highest decision literal to position 1 in the learn…
cprudhom Aug 21, 2026
50436a6
LCG: move calls to doReduceDB as first step of the `forget` method
cprudhom Aug 21, 2026
cef9526
Cumulative: calculate the tasks involved in the profile in a lazy man…
cprudhom Aug 21, 2026
46df07f
Fix #1233
cprudhom Aug 21, 2026
a66c60e
Rename tests
cprudhom Aug 21, 2026
f9570e4
Fix error in ReversePropagationGuidedNeighborhood
cprudhom Aug 31, 2026
dfa93b5
ReifiedTest: add new tests
cprudhom Aug 31, 2026
7e7f42f
PropXneYHalfReif: fix issue #1240
cprudhom Aug 31, 2026
85e6fff
PropXneYHalfReif and PropXeqYHalfReif: update Javadoc
cprudhom Sep 1, 2026
8196256
PR #1234: update tests metrics
cprudhom Aug 21, 2026
b6ef6de
Merge branch 'develop' into fix_1233
cprudhom Sep 2, 2026
e2ac568
AbsoluteLight: update Javadoc
cprudhom Sep 2, 2026
1323506
Merge branch 'develop' into fix_1233
cprudhom Sep 9, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 6 additions & 0 deletions solver/src/main/java/org/chocosolver/solver/constraints/IIntConstraintFactory.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -251,6 +251,12 @@ default Constraint notMember(IntVar var, IntIterableRangeSet set) {

/**
* Creates an absolute value constraint: var1 = |var2|
* <p>
* 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 <code>var1 = [0,3]</code> and <code>var2 = [-3, -2, 2, 3]</code>,
* the hole <code>-1</code> in <code>var2</code> (which would imply <code>1</code> is missing in <code>var1</code>)
* is not propagated when using {@link PropAbsoluteLight}.
*/
default Constraint absolute(IntVar var1, IntVar var2) {
assert var1.getModel() == var2.getModel();
Expand Down
153 changes: 109 additions & 44 deletions solver/src/main/java/org/chocosolver/solver/constraints/binary/PropAbsolute.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,8 +17,19 @@
import org.chocosolver.util.tools.ArrayUtils;

/**
* Enforces X = |Y|
* <br/>
* A propagator to enforce the constraint <code>absY = |Y|</code>, where
* <code>absY</code> is a variable representing the absolute value of <code>Y</code>.
* <p>
* This propagator ensures that:
* <ul>
* <li><code>absY</code> is always non-negative,</li>
* <li>the domain of <code>Y</code> is restricted to <code>[-absY.getUB(), absY.getUB()]</code>,</li>
* <li>the domain of <code>absY</code> is restricted to <code>[0, max(|Y.getLB()|, |Y.getUB()|)]</code>.</li>
* </ul>
* <p>
* If both variables have enumerated domains, additional filtering is applied to ensure
* that for every value <code>v</code> in the domain of <code>absY</code>, either <code>v</code> or <code>-v</code>
* is in the domain of <code>Y</code>, and vice versa.
*
* @author Charles Prud'homme
* @author Jean-Guillaume Fages
Expand All @@ -27,20 +38,47 @@
@Explained
public class PropAbsolute extends Propagator<IntVar> {

private final IntVar X;
private final IntVar Y;
/**
* Variable representing the absolute value, i.e., <code>absY = |Y|</code>.
*/
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 <code>X = |Y|</code>.
*
* @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 <code>X = |Y|</code>.
*
* @param X variable representing the absolute value
* @param Y variable whose absolute value is computed
* @param react if <code>true</code>, 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();
Expand All @@ -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;
Expand All @@ -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());
}

//***********************************************************************************
Expand All @@ -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();
Expand All @@ -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 {
Expand All @@ -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());
}
}
}
Expand Down
74 changes: 33 additions & 41 deletions solver/src/main/java/org/chocosolver/solver/constraints/binary/PropAbsoluteLight.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,94 +8,86 @@

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|
* <br/>
* A light propagator to enforce the constraint <code>absY = |Y|</code>.
* <p>
* 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.
* <p>
* The propagator is created with <code>react = false</code>, meaning it is not initially active
* in the propagation engine. It only reacts to bound and instantiation events.
* <p>
* Note: This propagator does not propagate holes that could be made from Y to absY.
* For example, if <code>absY = [0,3]</code> and <code>Y = {-3, -2, 2, 3}</code>,
* the hole <code>{-1, 0, 1}</code> in <code>Y</code> (which would imply <code>0,1</code> are missing in <code>absY</code>)
* is not propagated.
*
* @author Charles Prud'homme
* @since 04/07/2025
* @see PropAbsolute
*/
@Explained
public class PropAbsoluteLight extends Propagator<IntVar> {

private final IntVar absY;
private final IntVar Y;
public class PropAbsoluteLight extends PropAbsolute {

/**
* Creates a light propagator to enforce <code>X = |Y|</code>.
* <p>
* Note: This propagator is created with <code>react = false</code>.
*
* @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 {
return IntEventType.boundAndInst();
}
}

@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);
}

}
Loading
Loading