ICF.mod returns the wrong number of solutions

[JLiangWaterloo]

There still seems to be two issues with the current implementation in 3.3.1-SNAPSHOT develop branch. The following code will find many duplicate solutions.

public static void main(String[] args) {
    for (int i = 0; i < 1000; i++) {
        Solver s = new Solver();
        IntVar d = VF.enumerated("d", -4, 3, s);
        IntVar e = VF.enumerated("e", -1, 3, s);
        IntVar f = VF.enumerated("f", -1, 4, s);
        s.post(ICF.mod(d, e, f));
        s.set(ISF.random_value(s.retrieveIntVars(), System.currentTimeMillis()));
        Set<String> x = new HashSet<>();
        if (s.findSolution()) {
            do {
                String z = d.getValue() + " % " + e.getValue() + "  = " + f.getValue();
                if (!x.add(z)) {
                    System.out.println("Duplicate solution: " + z);
                }
            } while (s.nextSolution());
        }
    }
}

In the next example, the constraint is "(d % e = f) || (e = 0)". I expected at least one solution where "e = 0" but no solution is returned.

public static void main(String[] args) {
    Solver s = new Solver();
    IntVar d = VF.enumerated("d", new int[]{1, 2}, s);
    IntVar e = VF.enumerated("e", new int[]{0, 5}, s);
    IntVar f = VF.enumerated("f", new int[]{3, 4}, s);
    s.post(LCF.or(ICF.mod(d, e, f), ICF.arithm(e, "=", 0)));
    System.out.println(s.findSolution());
}

[jgFages]

Ok I see.

The problem is that "mod" introduces new variables (which lead to multiple identical solutions in your previous issue) and is propagated using several constraints.

My fix consisted in posting all constraints but one to ensure that the temporary variables are fixed whenever the original variables are. This includes posting an euclDiv. However such constraint imposes to a have a denominator different from zero...

I am on it!

[jgFages]

Hi,

I am sorry I forgot to answer this issue earlier. Actually, I find normal that even if the modulo constraint is reified the value 0 is removed from the domain of e, because modulo 0 is mathematically incorrect (as you cannot divide an integer by zero).

Reifying a constraint means that the relation encoded by the constraint may or may not be true (either d%e == f or d%e =/= f). It does not mean that the constraint may be undefined (d%e must be defined).

See this:
http://stackoverflow.com/questions/7370154/cant-mod-zero

[JLiangWaterloo]

Makes sense but it makes working with modulo very limited. As an alternative, would it be possible to add an optional feature to division/modulo to specify the result of division/modulo by 0?

i.e. Add the following method to ICF.

/**
 * if DIVISOR != 0 then ensures DIVIDEND / DIVISOR = RESULT, rounding towards 0
 * else if DIVISIOR = 0 then ensures RESULT = ZERO_DIVISOR_RESULT
 */
public static Constraint eucl_div(IntVar DIVIDEND, IntVar DIVISOR, IntVar RESULT, int ZERO_DIVISOR_RESULT) {
   ...
}

And likewise for modulo?

Given the circumstances, the above feature would be the optimal solution for the second problem in my original post.

Thanks.

[jgFages]

Are you sure your prefer :

"else if DIVISIOR = 0 then ensures RESULT = ZERO_DIVISOR_RESULT"

than

"else if DIVISIOR = 0 then nothing happens"

I ask because if ZERO_DIVISOR_RESULT is not in the domain of RESULT (because of filtering), then DIVISOR cannot be equal to 0...

[cprudhom]

I'm not sure we are trying to solve the right problem.
eucl_div and mod remove 0 from the divisor and there is nothing we can do about, since otherwise it is mathematically incorrect.
The main problem happens when those constraints are reified.
Actually, the constraints must override the makeOpposite() method from Constraint.

[JLiangWaterloo]

@jgFages

Are you sure your prefer :
"else if DIVISIOR = 0 then ensures RESULT = ZERO_DIVISOR_RESULT"
than
"else if DIVISIOR = 0 then nothing happens"

I would prefer option 2 but I could live with option 1 as well.

[jgFages]

I can do both ;-)

[JLiangWaterloo]

As an aside, in SMT solvers "a ÷ 0" is defined but not specified, i.e. it can return any real number which is essentially option 2 in @jgFages post. I don't know how other CSP solvers handle this case.

[jgFages]

Ok so after many discussions, we maintain the philosophy that constraints may have several restrictions (e.g. never divided by 0) whether it is reified or not. The reification process is related to the constraint semantic (the result is equal or not equal to the expected result).

So the existing eucl_div constraint will not change.

We do not want to add another constraint such as eucl_div_0_joker to choco because it would be endless. For scheduling constraints for instance, we assume we have tasks. We can reify these constraint in case a capacity is overloaded for instance but we do not want to allow the variables not to form tasks...

However, I can provide you the code so that you can use it:

/**
* if DIVISOR != 0 then ensures DIVIDEND / DIVISOR = RESULT, rounding towards 0
* else if DIVISIOR = 0 then nothing happens
*
* @param DIVIDEND
* @param DIVISOR
* @param RESULT
*/
public static Constraint eucl_div_0(IntVar DIVIDEND, IntVar DIVISOR, IntVar RESULT) {
if(!DIVISOR.contains(0)){
return eucl_div(DIVIDEND,DIVISOR,RESULT);
}else if(DIVISOR.isInstantiatedTo(0)){
return RESULT.getSolver().TRUE;
}else {
Solver s = DIVISOR.getSolver();
int dlb = Math.min(1, DIVISOR.getLB());
int dub = Math.max(1, DIVISOR.getUB());
IntVar div2 = VF.integer(StringUtils.randomName(), dlb, dub, s);
int rlb = Math.min(RESULT.getLB(), DIVIDEND.getLB());
int rub = Math.max(RESULT.getUB(), DIVIDEND.getUB());
IntVar res2 = VF.integer(StringUtils.randomName(), rlb, rub, s);
s.post(eucl_div(DIVIDEND, div2, res2));
return LCF.or(
// usual division
LCF.and(arithm(DIVISOR, "=", div2), arithm(RESULT, "=", res2)),
// division by 0
LCF.and(arithm(DIVISOR, "=", 0), arithm(div2, "=", 1) // avoids multiple identical solutions
)
);
}
}

/**
* Modulo constraint (extended)
* if Y != 0 then ensures X % Y = RESULT
* else if Y = 0 then nothing happens
*
* @param X
* @param Y
* @param RESULT
*/
public static Constraint mod_0(IntVar X, IntVar Y, IntVar RESULT) {
if(!Y.contains(0)){
return mod(X, Y, RESULT);
}else if(Y.isInstantiatedTo(0)){
return RESULT.getSolver().TRUE;
}else {
Solver s = Y.getSolver();
int ylb = Math.min(1, Y.getLB());
int yub = Math.max(1, Y.getUB());
IntVar mod2 = VF.integer(StringUtils.randomName(), ylb, yub, s);
int rlb = Math.min(RESULT.getLB(), 0);
int rub = Math.max(RESULT.getUB(), 0);
IntVar res2 = VF.integer(StringUtils.randomName(), rlb, rub, s);
s.post(mod(X, mod2, res2));
return LCF.or(
// usual modulo
LCF.and(arithm(Y, "=", mod2), arithm(RESULT, "=", res2)),
// modulo 0
LCF.and(arithm(Y, "=", 0), arithm(mod2, "=", 1) // avoids multiple identical solutions
)
);
}
}

Is that ok for you?

[jgFages]

May I close the issue?

[JLiangWaterloo]

There's still the issue with duplicate solutions as outlined in my original post, i.e., the following code finds a lot of duplicate solutions:

public static void main(String[] args) {
    for (int i = 0; i < 1000; i++) {
        Solver s = new Solver();
        IntVar d = VF.enumerated("d", -4, 3, s);
        IntVar e = VF.enumerated("e", -1, 3, s);
        IntVar f = VF.enumerated("f", -1, 4, s);
        s.post(ICF.mod(d, e, f));
        s.set(ISF.random_value(s.retrieveIntVars(), System.currentTimeMillis()));
        Set<String> x = new HashSet<>();
        if (s.findSolution()) {
            do {
                String z = d.getValue() + " % " + e.getValue() + "  = " + f.getValue();
                if (!x.add(z)) {
                    System.out.println("Duplicate solution: " + z);
                }
            } while (s.nextSolution());
        }
    }
}

[jgFages]

Ok I see, I have tested my code using a branching heuristic on d,e,f (which works).
However, I am surprised that branching on automatically-created variables leads to duplicate solutions.
I dig...

[jgFages]

Although this is not satisfactory, a helpful patch is to add nogoods on solutions:

SMF.nogoodRecordingOnSolution(s.retrieveIntVars());

Keep digging ...

[jgFages]

Ok I get it, this has nothing to do with mod (except the fact that some bounded vars are created).

It is incorrect to use the random_value heuristic for assignments on bounded vars (and s.retrieveIntVars() may included bounded vars). The reason is that after backtracking over a decision let say x=42, it will remove value 42 from the domain of x, but if the domain is bounded (e.g. [10, 56]), then that information will be lost. This is why you have many same solutions. It can also lead to exploring many times the same search space that has no solution in it...

Anyway, this raises the fact that the above point was not clear.
I see two options:

1. Raise a java exception if some variables are bounded when calling ISF.random_value.
   => bonus: The user learns
   => minus: The user has to change his heuristic (to random_bound for instance)
2. Create a random_valueOrBound value selector if you see what I mean. I insist it would be one even more value selector because random_value does make sense for bounded variables in case domain split decisions are computed (instead of assignments).
   => bonus: The user does not have to change the heuristic
   => minus: What the solver does is not really what the user thinks

Any preference? I prefer to raise an exception...

[JLiangWaterloo]

Perhaps both? Quite often I want to find random solutions and the most convenient way for me to do it is "ISF.random_value(s.retrieveIntVars(), System.currentTimeMillis())" (or random_valueOrBound if implemented). I don't want to be surprised by unknown bound variables that the library created behind the scenes without my knowledge. A random_valueOrBound would be very convenient.

[jgFages]

done!

[JLiangWaterloo]

Looks good to me. Thanks!