[Choco-users] Mixing linear and boolean constraints...

[Sylvain B. <syl...@ce...>]

Hello all,

Choco, version 1.2.04, seems to have some problems to handle boolean 
constraints of linear constraints correctly (or do I misuse Choco ?).

Just consider the following example:

Problem p = new Problem();
IntDomainVar[][]  v = p.makeEnumIntVarArray("v", 3, 2, 0, 1);
Constraint[] tab = {p.eq(p.sum(v[0]), 2), p.eq(p.sum(v[1]), 2), 
p.eq(p.sum(v[2]), 2)};
Constraint c = p.or(tab);
p.post(c);
if (p.solve().booleanValue()) {
     System.out.print("v[0] = [" + v[0][0].getVal() + ", " + 
v[0][1].getVal() + "] / ");
     System.out.print("v[1] = [" + v[1][0].getVal() + ", " + 
v[1][1].getVal() + "] / ");
     System.out.print("v[2] = [" + v[2][0].getVal() + ", " + 
v[2][1].getVal() + "] - > c");
     System.out.println(c.isSatisfied() ? " satisfied." : " not 
satisfied!!!");
}
while (p.nextSolution().booleanValue()) {
     System.out.print("v[0] = [" + v[0][0].getVal() + ", " + 
"[0][1].getVal() + "] / ");
	    System.out.print("v[1] = [" + v[1][0].getVal() + ", " + 
v[1][1].getVal() + "] / ");
	    System.out.print("v[2] = [" + v[2][0].getVal() + ", " + 
v[2][1].getVal() + "] - > c");
	    System.out.println(c.isSatisfied() ? " satisfied." : " not 
satisfied!!!");
}

It produces the following output:
v[0] = [0, 0] / v[1] = [0, 0] / v[2] = [0, 0] - > c not satisfied!!!
v[0] = [0, 0] / v[1] = [0, 0] / v[2] = [0, 1] - > c not satisfied!!!
v[0] = [0, 0] / v[1] = [0, 0] / v[2] = [1, 0] - > c not satisfied!!!
v[0] = [0, 0] / v[1] = [0, 0] / v[2] = [1, 1] - > c satisfied.
...

(Solving the problem leaves some constraints obviously unsatisfied.)

However, replacing in the previous example the array tab by:
Constraint[] tab = {p.and(p.eq(v[0][0], 1), p.eq(v[0][1], 1)), 
p.and(p.eq(v[1][0], 1), p.eq(v[1][1], 1)), p.and(p.eq(v[2][0], 1), 
p.eq(v[2][1], 1))};
(which is semantically equivalent), produces the right output.

Do you have an idea about where the problem can come from ?

Just another little problem with boolean binary constraints. The 
following code:
Constraint c = p.or(tab[0], tab[1]);
System.out.println(" " + c.isSatisfied());

produces a NullPointerException at 
choco.bool.BinDisjunction.isSatisfied(BinDisjunction.java:186).

Thanks for any help!
Sylvain Bouveret.