<< 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 :

importer minizinc
créer un Model, c'est à dire exprimer le problème dans le langage Minizinc
rechercher un Solver capable de résoudre le problème
créer une instance du problème composée du Model et du Solver
puis appeler la méthode solve sur le problème

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

minizinc_python.py

import minizinc
 
# description du problème en Minizinc
model = minizinc.Model()
model.add_string("""
include "globals.mzn";
var 3..9 : x;
var 0..9 : y;
constraint 2 * x + y < 10;
solve satisfy;
""")
 
# recherche d'un solveur
gecode = minizinc.Solver.lookup("gecode")
 
# création du problème
problem = minizinc.Instance(gecode, model)
 
# résolution et obtention des solutions
solutions = problem.solve(all_solutions=True)
 
print(solutions)
 
for solution in solutions:
    print(solution.x, solution.y)
 
 

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

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

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

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

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

% contrainte entre x1 et x2
constraint x1 + 2 * x2 <= x3;
 
% contrainte SEND + MORE = MONEY
constraint R3+S+M=O+10*R4;

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

%
% SEND + MORE = MONEY
%
array[1..8] of var int : all = [S,E,N,D,M,O,R,Y];
constraint all_different(all);
 
%
% N Reines
%
int: N = 8;
% colonnes ou sont placées les reines
array[1..N] of var 1..N: queens;
 
constraint alldifferent(queens);
% diagonales gauches et droites
constraint alldifferent([ queens[i] + i | i in 1..N]); 
constraint alldifferent([ queens[i] - i | i in 1..N]); 
 
 

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

%
% Ramsey
%
 
int: N = 10;
 
array[1..N,1..N] of var 0..1 : R;
array[1..N,1..N] of var 0..1 : G;
array[1..N,1..N] of var 0..1 : B;
 
% on colorie un arc en Rouge, Vert ou Bleu
constraint forall(i in 1..N-1) (
  forall(j in i+1..N) (
      R[i,j] + G[i,j] + B[i,j] = 1
    )
);
 

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

%
% Voyageur de commerce
%
array[1 .. N] of var 1..N: chemin; 
int: min_val = min([distances[i,j] | i,j in 1..N where distances[i,j] > 0]);
int: max_val = max([distances[i,j] | i,j in 1..N]);
array[1..N] of var min_val .. max_val : d;
 
constraint alldifferent(chemin);
constraint circuit(chemin);
constraint forall(i in 1..N) (
      distances[i,chemin[i]] = d[i]
    );
 
 

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

%
% SEND + MORE = MONEY
%
solve satisfy;
 
%
% Voyageur de commerce
%
var int: distance = sum(d);
solve :: int_search(d, max_regret, indomain_split, complete) minimize distance; 
 
%
% Sac à dos
%
var int: gain = sum(i in 1..N)(profit[i] * x[i]); 
solve  :: int_search(x, max_regret,indomain_split, complete) maximize  gain;
 
 

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

input_order : suivant l'ordre donné par <variables>
first_fail : choix de la variable avec le domaine de plus petite taille
smallest : choix de la variable avec la plus petite valeur dans son domaine.

4.4.4.b Contraintes sur le choix

indomain_min : affecter à une variable sa plus petite valeur dans le domaine
indomain_median : affecter la valeur médiane
indomain_random : affecter aléatoirement

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.

Page de Jean-Michel Richer