CODEWITHSUNDEEP
constraintsminizincgecode
Martin
Martin

Reputation: 35

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?

Upvotes: 2

Views: 496

Answers (2)

SShrestha
SShrestha

Reputation: 19

Your constraint seems to be attempting to use assignment operator but the operation maynot be valid. You may try a = b+ c but b+c=a may not be allowed. Alternately you can try to use equality == operator to define your constraint which should work. I don't have program installed to validate but hope it gives you bit more insight to the issue. I would not be surprised if there is bug too, I would be keen to know.

Upvotes: -1

hakank
hakank

Reputation: 6854

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;

Upvotes: 2

Related Questions