Search code examples
constraintsminizincgecode

Minizinc: Trivial equality unsatisfiable

I have the following minizinc model:

include "globals.mzn";
var 0..9: A_1_1;
var 0..9: A_2_1;
var 0..9: A_3_1;
constraint (A_3_1+A_2_1+A_1_1) = A_1_1;
solve satisfy;

The model should have the trivial solution 0=A_1_1=A_2_1=A_3_1. However, Gecode and other solvers report this as unsatisfiable.

What am I overlooking?

Solution

  • It seems to be a bug in MiniZinc when it translates the model to FlatZinc format. The message given is from MiniZinc: 

    WARNING: model inconsistency detected
test66.mzn:6:
in binary '=' operator expression

    The generated FlatZinc file contains just this:

    constraint bool_eq(false,true);
solve  satisfy;

    and that's why the FlatZinc solvers yield UNSATISFIABLE.

    Interestingly, the following model works, using a temporary decision variable, T:

    var 0..9: A_1_1;
var 0..9: A_2_1;
var 0..9: A_3_1;
var 0..9: T;

constraint
    T = A_3_1 + A_2_1 + A_1_1 /\
    T = A_1_1
; 
solve satisfy;

    The model then yield all 10 solutions with A_1_1 is assigned values from 0 to 9, A_2_1 = A_3_1 = 0, and T is assigned to same value as A_1_1.

    However, if T is initialized with A_1_1 then UNSAT is thrown again:

    var 0..9: T = A_1_1;

    Update: One can note that the following constraint works, i.e. 2 * A_1_1 at the right side:

    constraint A_3_1 + A_2_1 + A_1_1 = 2 * A_1_1;