<< Page principale

4. Le solveur Minizinc

4.1. Introduction

Minizinc se définit comme un langage de modélisation de contraintes Libre et Open-Source.

Les contraintes sont ensuite traduites en un langage bas niveau nommé FlatZinc qui permet une interface avec des solveurs tel Gecode.

L'intérêt de Minizinc et qu'il permet de définir des CSP et des CSP avec optimisation et de les résoudre en faisant appel à un solveur. Il existe une interface avec Python qui permet d'appeler Minizinc et de récupérer les solutions.

La documentation de Minizinc est disponible à partir de cette page.

Le reste de cette page consiste en une introduction très succinte de Minizinc.

4.2. Installation

4.2.1. Ubuntu et python

Je ne suis pas parvenu à installer minizinc avec Anaconda, j'ai donc utilisé le python disponible par défaut sous Linux Ubuntu 20.04.2 :

richer@zentopia:\$ conda deactivate
richer@zentopia:\$ pip3 install minizinc
richer@zentopia:\$ sudo snap install minizinc --classic

La première ligne désactive Anaconda (il n'est donc pas nécessaire de la saisir si vous n'avez pas installé Anaconda) afin d'utiliser le Python par défaut (version 3.8.5).

4.2.2. Interface graphique

Il est possible d'utiliser Minizinc sous forme d'une interface graphique :

MiniZinc IDE

Pour cela, il faut se rendre sur la page Software et télécharger le programme 64 bit Windows Installer ou 64 bit Linux AppImage.

Si vous avez réalisé l'installation avec snap (Ubuntu), il faut lancer minizinc_ide .

4.3. Utilisation avec Python

Pour communiquer avec Python, il faut :

Voici un exemple simple qui reprend les étapes précédentes :

minizinc_python.py

  1. import minizinc
  2.  
  3. # description du problème en Minizinc
  4. model = minizinc.Model()
  5. model.add_string("""
  6. include "globals.mzn";
  7. var 3..9 : x;
  8. var 0..9 : y;
  9. constraint 2 * x + y < 10;
  10. solve satisfy;
  11. """)
  12.  
  13. # recherche d'un solveur
  14. gecode = minizinc.Solver.lookup("gecode")
  15.  
  16. # création du problème
  17. problem = minizinc.Instance(gecode, model)
  18.  
  19. # résolution et obtention des solutions
  20. solutions = problem.solve(all_solutions=True)
  21.  
  22. print(solutions)
  23.  
  24. for solution in solutions:
  25.     print(solution.x, solution.y)
  26.  
  27.  

On obtient en résultat la variable solutions qui est le résultat renvoyé par le solveur. Puis on affiche chaque couple (x,y) de chaque solution :

richer@zentopia:\$ python3 minizinc_python.py

[Solution(x=3, y=0, _output_item='', _checker=''), Solution(x=3, y=1, _output_item='', _checker=''), Solution(x=3, y=2, _output_item='', _checker=''), Solution(x=3, y=3, _output_item='', _checker=''), Solution(x=4, y=0, _output_item='', _checker=''), Solution(x=4, y=1, _output_item='', _checker='')]
3 0
3 1
3 2
3 3
4 0
4 1

4.4. Modélisation des problèmes

On pourra se référer au MiniZinc Handbook pour de plus amples informations.

4.4.1. Déclaration des constantes

Les paramètres (ou constantes) sont déclarés comme suit et on doit leur attribuer une valeur:

decl_cst.mzn

  1. % N est une constante entière qui vaut 10
  2. int: N = 10;
  3.  
  4. % weight est un tableau de constantes entières
  5. array[1..N] of int: weight;
  6.  
  7. % définition des valeurs de weight
  8. weight = [95,4,60,32,23,72,80,62,65,46] ;
  9.  

On peut déclarer des entiers (int), des réels (float), des booléens (bool) et des chaînes de caractères (string).

4.4.2. Déclaration de variables

Les variables (appelées variables de décision) n'ont pas de valeur initiale. C'est le solveur qui se chargera de leur attribuer une valeur :

decl_var.mzn

  1. % déclare une variable entière qui prend ses valeurs
  2. % dans l'intervalle [0,9]
  3. var  0..9: S;
  4.  
  5. # variable entière M
  6. var int: M;
  7.  
  8. % déclare un tableau de N variables entières qui prennent
  9. % leurs valeurs dans l'intervalle [0,1]
  10. array[1..N] of var 0..1: x;
  11.  

4.4.3. Déclaration de Contraintes

4.4.3.a  Contraintes simples

Les contraintes sont introduites par le mot clé constraint :

decl_ctr.mzn

  1. % contrainte entre x1 et x2
  2. constraint x1 + 2 * x2 <= x3;
  3.  
  4. % contrainte SEND + MORE = MONEY
  5. constraint R3+S+M=O+10*R4;
  6.  
  7.  

4.4.3.b  Contraintes de type alldifferent

Les contraintes de type alldifferent expriment le fait qu'un ensemble de variables prennent des valeurs différentes, ou autrement dit, que deux variables ne peuvent avoir la même valeur :

decl_ctr_all_diff.mzn

  1. %
  2. % SEND + MORE = MONEY
  3. %
  4. array[1..8] of var int : all = [S,E,N,D,M,O,R,Y];
  5. constraint all_different(all);
  6.  
  7. %
  8. % N Reines
  9. %
  10. int: N = 8;
  11. % colonnes ou sont placées les reines
  12. array[1..N] of var 1..N: queens;
  13.  
  14. constraint alldifferent(queens);
  15. % diagonales gauches et droites
  16. constraint alldifferent([ queens[i] + i | i in 1..N]);
  17. constraint alldifferent([ queens[i] - i | i in 1..N]);
  18.  
  19.  

4.4.3.c  Contraintes utilisant forall

Le mot clé forall permet de réaliser l'enumération sur une variable de boucle :

decl_ctr_forall.mzn

  1. %
  2. % Ramsey
  3. %
  4.  
  5. int: N = 10;
  6.  
  7. array[1..N,1..N] of var 0..1 : R;
  8. array[1..N,1..N] of var 0..1 : G;
  9. array[1..N,1..N] of var 0..1 : B;
  10.  
  11. % on colorie un arc en Rouge, Vert ou Bleu
  12. constraint forall(i in 1..N-1) (
  13.   forall(j in i+1..N) (
  14.       R[i,j] + G[i,j] + B[i,j] = 1
  15.     )
  16. );
  17.  

4.4.3.d  Contraintes complexes

Dans le cas du voyageur de commerce, il faut exprimer le fait que l'on passe d'une ville à l'autre en définissant un tableau $d$ (en plus du tableau $x$ qui indique l'ordre de passage) sur lequel on exprime les distances parcourues :

decl_ctr_complexe.mzn

  1. %
  2. % Voyageur de commerce
  3. %
  4. array[1 .. N] of var 1..N: chemin;
  5. int: min_val = min([distances[i,j] | i,j in 1..N where distances[i,j] > 0]);
  6. int: max_val = max([distances[i,j] | i,j in 1..N]);
  7. array[1..N] of var min_val .. max_val : d;
  8.  
  9. constraint alldifferent(chemin);
  10. constraint circuit(chemin);
  11. constraint forall(i in 1..N) (
  12.       distances[i,chemin[i]] = d[i]
  13.     );
  14.  
  15.  

La contrainte circuit(x) force les éléments de $x$ à définir un circuit où $x [ i ] = j$ signifie que $j$ est le successeur de $i$.

4.4.4. Déclaration de la résolution

La déclaration de la résolution utilise souvent solve satisfy, mais dans d'autres cas comme celui du voyageur de commerce ou du sac à dos, il faut minimiser ou maximiser une quantité.

Il peut aussi être intéressant de contrôler la recherche (cf N Reines). C'est ce que permet de faire int_search et autres bool_search, float_search , seq_search :

decl_resol.mzn

  1. %
  2. % SEND + MORE = MONEY
  3. %
  4. solve satisfy;
  5.  
  6. %
  7. % Voyageur de commerce
  8. %
  9. var int: distance = sum(d);
  10. solve :: int_search(d, max_regret, indomain_split, complete) minimize distance;
  11.  
  12. %
  13. % Sac à dos
  14. %
  15. var int: gain = sum(i in 1..N)(profit[i] * x[i]);
  16. solve  :: int_search(x, max_regret,indomain_split, complete) maximize  gain;
  17.  
  18.  

Le contrôle qu' autorise int_search( <variables>, <varchoice>, <constrainchoice> ) permet de définir les variables à prendre en considération, la stratégie de choix de variables et la stratégie de choix de contraintes sur les variables. On pourra consulter cette page pour voir l'ensemble des possibilités offertes. Voici quelques exemples :

4.4.4.a  Stratégie de choix des variables

4.4.4.b  Contraintes sur le choix

4.5. Exemples de problèmes

4.6. Exercices

Exercice 4.1

En se basant sur la représentation du problème SEND + MORE = MONEY, résoudre les problèmes suivants :

  • $HUIT + HUIT = SEIZE$
  • $UN + UN + NEUF = ONZE$
  • $MARS + SATURNE + NEPTUNE = PLANETES$
  • $MOI + TOI + LUI + ELLE = NOUS$

Vous trouverez d'autres exemples sur cette page.