MiniZinc: égalité Trivial insatisfiables

Question

je le modèle MiniZinc suivant:

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; 

Le modèle devrait avoir la solution triviale 0 = A_1_1 = A_2_1 = A_3_1. Cependant, Gecode et d'autres solveurs rapportent ceci comme insatisfiable.

Qu'est-ce que je néglige?

Answer 1

Il semble y avoir un bug dans MiniZinc quand il traduit le modèle au format FlatZinc. Le message donné est de MiniZinc:

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

Le fichier généré contient FlatZinc ceci:

constraint bool_eq(false,true); 
solve satisfy; 

et c'est pourquoi les solveurs FlatZinc donnent insatisfiables.

Fait intéressant, les travaux de modèles suivants, en utilisant une variable de décision temporaire, 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; 

Le modèle alors donné l'ensemble des 10 solutions avec A_1_1 est affecté des valeurs de 0 à 9, A_2_1 = A_3_1 = 0, et T est affecté à la même valeur que A_1_1.

Cependant, si T est initialisé avec A_1_1 puis UNSAT est jeté à nouveau:

var 0..9: T = A_1_1;

Mise à jour: On peut noter que la contrainte suivante fonctionne, à savoir 2 * A_1_1 sur le côté droit:

constraint A_3_1 + A_2_1 + A_1_1 = 2 * A_1_1; 

Answer 2

Votre contrainte semble essayer d'utiliser l'opérateur d'affectation, mais l'opération maynot soit valide. Vous pouvez essayer a = b + c mais b + c = a peut ne pas être autorisé. Alternativement, vous pouvez essayer d'utiliser l'égalité == opérateur pour définir votre contrainte qui devrait fonctionner. Je n'ai pas de programme installé pour valider, mais j'espère que cela vous donnera un peu plus d'informations sur le problème. Je ne serais pas surpris s'il y a un bug aussi, je serais ravi de le savoir.