all_different with free integer variables: chuffed cannot find all solutions

[odow]

In this issue opened in our Julia interface, jump-dev/MiniZinc.jl#84, solving n-queens with [email protected] returns 52 solutions instead of the expected 92.

I assume this is related to #10 and #108

I tried to simplify the example, but I don't really know what I'm doing. All the trivial examples I wrote seemed to return the correct number of solutions.

Example

The .mzn file we wrote is (Note the unbounded var int: x9;):

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";

Chuffed

The output with Chuffed is:

oscar@Oscars-MBP MiniZinc % /Applications/MiniZincIDE.app/Contents/Resources/minizinc /tmp/nqueens.mzn --num-solutions 100 --solver org.chuffed.chuffed -s -o /tmp/output
% Generated FlatZinc statistics:
%%%mzn-stat: paths=0
%%%mzn-stat: flatIntVars=24
%%%mzn-stat: flatIntConstraints=19
%%%mzn-stat: method="satisfy"
%%%mzn-stat: flatTime=0.0763033
%%%mzn-stat-end
%%%mzn-stat: nSolutions=52
%%%mzn-stat-end

Gecode

The output with Gecode is:

oscar@Oscars-MBP MiniZinc % /Applications/MiniZincIDE.app/Contents/Resources/minizinc /tmp/nqueens.mzn --num-solutions 100 --solver org.gecode.gecode -s -o /tmp/output
% Generated FlatZinc statistics:
%%%mzn-stat: paths=0
%%%mzn-stat: flatIntVars=24
%%%mzn-stat: flatIntConstraints=19
%%%mzn-stat: method="satisfy"
%%%mzn-stat: flatTime=0.0857667
%%%mzn-stat-end
%%%mzn-stat: nSolutions=92
%%%mzn-stat-end