[BUG] IsEntailed for InverseChanneling not working with negative bounds

[IgnaceBleukx]

Hi,

I am trying to post a reification of the inverse_channeling constraint. However, when one of the variables in the forward array has a lowerbound which is negative, I get an ArrayOutOfBounds exception while the solver is checking for entailment of the channeling constraint:

ava.lang.ArrayIndexOutOfBoundsException: Index -5 out of bounds for length 3
    at org.chocosolver.solver.constraints.nary.channeling.PropInverseChannelAC.isEntailed(PropInverseChannelAC.java:131)
    at org.chocosolver.solver.constraints.Constraint.isSatisfied(Constraint.java:160)
    at org.chocosolver.solver.constraints.reification.PropOpposite.propagate(PropOpposite.java:41)
    at org.chocosolver.solver.propagation.PropagationEngine.propagateEvents(PropagationEngine.java:215)
    at org.chocosolver.solver.propagation.PropagationEngine.propagate(PropagationEngine.java:199)
    at org.chocosolver.solver.Solver.doPropagate(Solver.java:481)
    at org.chocosolver.solver.Solver.propagate(Solver.java:493)
    at org.chocosolver.solver.Solver.searchLoop(Solver.java:338)
    at org.chocosolver.solver.Solver.solve(Solver.java:306)
    at org.chocosolver.solver.search.IResolutionHelper.findSolution(IResolutionHelper.java:102)

Kind regards, Ignace

[cprudhom]

This is the expected behavior.

The first API is inverseChanneling(IntVar[] X, IntVar[] Y), it ensures that: so indices must be greater or equal to 0.

If you want to have negative values, you need to use the second API inverseChanneling(IntVar[] X, IntVar[] Y, int o1, int o2) where o1 and o2 can be negative.

You should use the second method with the correctly defined offsets.

Hope that helps

[IgnaceBleukx]

Hi, thanks for the quick answer. I'm not sure the offset-version of the constraint is really what I want, I do not want a solution where the mapping is offset, but rather the reification of the channeling constraint.

This is the exact situation in which the bug occurs: I have an array $X = [x_0, x_1, x_2]$ with domain $D(x_i) = [-5..5]$.

I also have an array of variables $Y = [y_0, y_1, y_2]$ where each domain $D(y_i) = {i}$, so only a single value.

Modelling the constraint $InverseChanneling(X, [y_0, y_1, y_2]) \Leftrightarrow b \wedge \neg b$ triggers the out-of bounds exception.

However, the constraint $InverseChanneling(X, [y_2, y_1, y_0]) \Leftrightarrow b \wedge \neg b$ runs fine and yields a correct solution $X = [-5,-5,-5]$

[IgnaceBleukx]

Hi, Is there any update on this issue? I managed to construct a minimal example in Java as well:

Model model = new Model();

// int lb = 0; // this lowerbound works fine
int lb = -1; // this lowerbound raises the array-out-of-bounds error

IntVar[] fwd = model.intVarArray(3, lb, 2);
IntVar[] rev = model.intVarArray(3, lb, 2);

Constraint cons = model.inverseChanneling(fwd, rev);
BoolVar bv = cons.reify();
model.arithm(bv, "<=", 0).post();

Solver solver = model.getSolver();
solver.findSolution();

The inverse constraint has 6 solutions:

fwd      ,  rev
[0, 1, 2], [0, 1, 2]
[0, 2, 1], [0, 2, 1]
[1, 0, 2], [1, 0, 2]
[1, 2, 0], [2, 0, 1]
[2, 0, 1], [1, 2, 0]
[2, 1, 0], [2, 1, 0]

So, when the reification variable is False, I believe any of the remaining 3810 assignments are a solution to the reification, including those with negative bounds, e.g., [-1,2,2],[0,0,0].

Is my reasoning correct here? Kind regards, Ignace

[dimitri-justeau]

Hi @IgnaceBleukx , I think confirmation of @cprudhom will be necessary, but from what I understand the behavior you get is not what you expect because inverseChanneling(IntVar[] X, IntVar[] Y) expects the domains of variables in X and Y to be in [0, |X|-1] , unless you use the offset version to allow negative values: https://javadoc.io/static/org.choco-solver/choco-solver/4.10.14/org.chocosolver.solver/org/chocosolver/solver/constraints/IIntConstraintFactory.html#inverseChanneling(org.chocosolver.solver.variables.IntVar[],org.chocosolver.solver.variables.IntVar[],int,int)

I guess that the we could expect Choco to check for X and Y domains before starting the search, and throw an exception if requirements are not satisfied.

[jgFages]

Hi all, Actually, I do not think it should throw an exception, it should filter the domain to [offset, n-1+offset] The expected behavior is to have "no solution" if the model is infeasible, not a java exception. Furthermore, if should be possible to declare domains wider than necessary (e.g. [-1000,1000] for a 10-size array). It may not be the smartest domain definition but yet it does include the solution space

[dimitri-justeau]

Well, regardless of the chosen behavior, I think that the most important is that it remains coherent with the documentation. Currently it says that "|X| = |Y|" and that "the variables should take their values in [0,|X|-1]". So if I rely on this, [-1000, 1000] when |X| = 10 does not respect the constraint's requirements. If we decide that the constraint should filter the domain to [offset, n-1+offset], it should be explicitly stated in the documentation, otherwise there is a possibility that users will get behaviors that they don't expect or understand. If we decide that the constraint should not filter the domains, the solver should not accept a setting that does not satisfy the constraint's requirements.

[cprudhom]

The error comes from the isEntailed method of PropInverseChannelAC. Indeed, the test suppose that (ignoring offsets for readability) when X[i] is instantiated to j (resp. Y[j] = i), then -1<j<n (resp. -1<i<n). These conditions should be added.

if (X[i].isInstantiated() && !Y[X[i].getValue() - minX].contains(i + minY)) {
  return ESat.FALSE;

should be turned into:

if (X[i].isInstantiated()) {
    int x = X[i].getValue() - minX;
    if (x < 0 || x >= n || !Y[x].isInstantiated() || Y[x].getValue() != i + minY) {
        return ESat.FALSE;
    }
}

and the same goes for Y. Doing so, the constraint should be reified properly.

[cprudhom]

Correction:

if (X[i].isInstantiated()) {
    int x = X[i].getValue() - minX;
    if (x < 0 || x >= n) return ESat.FALSE;
    if (!Y[x].contains(i + minY) && Y[x].isInstantiated()) return ESat.FALSE;
}