[upstream] wrong number of solutions

[blegat]

CP experts told le during the presentation thatvthis should be 92, not 52. They checked writing the problem directly in MiniZinc and using Chuffed and they got 92 so it seems to be a problem in the minizinc writer here

MiniZinc.jl/test/examples/nqueens_solveall.jl

Line 27 in 5e9241b

actual_count = 52,

[odow]

I changed this when I updated to a newer version of Chuffed:
d3fef25

Let me take a look

[odow]

The .mzn file is correct:

shell> cat test.mzn
var 1 .. 8: x1;
var 1 .. 8: x2;
var 1 .. 8: x3;
var 1 .. 8: x4;
var 1 .. 8: x5;
var 1 .. 8: x6;
var 1 .. 8: x7;
var 1 .. 8: x8;
var int: x9;
var int: x10;
var int: x11;
var int: x12;
var int: x13;
var int: x14;
var int: x15;
var int: x16;
var int: x17;
var int: x18;
var int: x19;
var int: x20;
var int: x21;
var int: x22;
var int: x23;
var int: x24;
constraint 1*x1 + -1*x9 = -1;
constraint 1*x2 + -1*x10 = -2;
constraint 1*x3 + -1*x11 = -3;
constraint 1*x4 + -1*x12 = -4;
constraint 1*x5 + -1*x13 = -5;
constraint 1*x6 + -1*x14 = -6;
constraint 1*x7 + -1*x15 = -7;
constraint 1*x8 + -1*x16 = -8;
constraint 1*x1 + -1*x17 = 1;
constraint 1*x2 + -1*x18 = 2;
constraint 1*x3 + -1*x19 = 3;
constraint 1*x4 + -1*x20 = 4;
constraint 1*x5 + -1*x21 = 5;
constraint 1*x6 + -1*x22 = 6;
constraint 1*x7 + -1*x23 = 7;
constraint 1*x8 + -1*x24 = 8;
constraint alldifferent([x1, x2, x3, x4, x5, x6, x7, x8]);
constraint alldifferent([x9, x10, x11, x12, x13, x14, x15, x16]);
constraint alldifferent([x17, x18, x19, x20, x21, x22, x23, x24]);
solve satisfy;
include "alldifferent.mzn";

and if I solve with Chuffed 0.13 in minizincIDE it also finds 52 solutions. So this is not a bug in MiniZinc.jl

[blegat]

The issue seems to be that var int: sets a lower bound of 0 by default while the slack variables should be allowed to be negative

[odow]

I don't think that is true:

[odow]

We updated in a big jump: chuffed/chuffed@0.10.4...0.13.2

I haven't bisected, but a scan of the issues shows:

• Chuffed ignores alldifferent on unconstrained variables in FlatZinc chuffed/chuffed#10

and then this temporary fix:

• Temporarily fix for #10 by enforcing usage of the bounds propagator. chuffed/chuffed#108

I'll open an issue and discuss with them.

[odow]

I've opened an issue in Chuffed: chuffed/chuffed#200. This is their bug. With the same .mzn file, other solvers like Gecode can find the correct number of solutions.