Skip to content. | Skip to navigation

Emergences

Lettre d'information n° 42

Image emergences pour impression
Personal tools
You are here: Home 2016 Lettre d'information n° 42 Un solveur de contraintes en Java
Document Actions

Un solveur de contraintes en Java

Librairie Java de modélisation et de résolution de problèmes mathématiques basée sur la programmation par contraintes (PPC), Choco est devenu l'un des outils open source les plus performants dans son domaine. Co-responsable du développement et ingénieur de recherche dans l'équipe Tasc* à Nantes, Charles Prud'homme revient sur les raisons de ce succès et explique l'intérêt que présente un tel solveur pour l'industrie.

Librairie Java de modélisation et de résolution de problèmes mathématiques basée sur la programmation par contraintes (PPC), Choco est devenu l'un des outils open source les plus performants dans son domaine. Co-responsable du développement et ingénieur de recherche dans l'équipe Tasc* à Nantes, Charles Prud'homme revient sur  les raisons de ce succès et explique l'intérêt que présente un tel solveur pour l'industrie.

 

Tout d'abord, à quoi sert exactement cet outil ?

Choco est une librairie de modélisation et de résolution de problèmes mathématiques basée sur la PPC. Cette technologie traite de manière efficace des problèmes de planification, d'ordonnancement, de placement d’objet, etc. Parmi les projets traités par Choco, on peut citer l’affectation de conducteurs à des lignes de bus, la génération automatique de résumé vidéo, la génération automatique de tests, un configurateur de véhicule ou encore l’optimisation de placement de machines virtuelles sur des plateformes d’hébergement.


Qui sont ses utilisateurs ?

Nous avons un large panel qui va des étudiants aux industriels en passant par les laboratoires de recherche. À titre d’exemple, dans les cinq derniers mois, Choco a été téléchargé plus de 3500 fois.


La PPC est à la fois un langage de modélisation et une technique de résolution.

Oui. La modélisation consiste à définir quelles sont les inconnues, au sens mathématique, du problème traité et à les lier partiellement ou totalement entre elles avec des contraintes. Chaque contrainte porte une sémantique («  égale à » , « tous différents », « doit respecter une expression régulière », etc.) et exprime les conditions que doivent respecter ses variables dans une solution. Quant à la méthode de résolution, elle exploite les propriétés intrinsèques de contraintes en combinant une recherche avec de la propagation. La partie recherche consiste en un parcours de l’ensemble des combinaisons possibles, habituellement, en profondeur d’abord. Une recherche exhaustive est souvent impossible en pratique, elle est donc renforcée par une partie propagation. Chaque partie est équipée d’un algorithme de filtrage qui supprime du domaine des variables les valeurs qui ne peuvent pas satisfaire les conditions.


Et si on comparait avec des technologies plus connues comme la Programmation Linéaire (PL) ou la Satisfaction de Problèmes Booléens (SAT)  ?

Celles-ci supportent uniquement des contrainte linéaires ou des formules booléennes. Certes, cette typologie favorise la résolution, mais elle complique la modélisation. Il faut réussir à traduire les « règles » utilisateurs. À l'inverse, la PPC gère des contraintes quelconques (linéaires ou non). Ce qui favorise la description des problèmes et bénéficie également au niveau des techniques de résolution. Seconde différence majeure : elle déduit des contraintes les valeurs impossibles du domaine des variables, filtrant des combinaisons et propageant ses déductions à l’ensemble du réseau de contraintes.


L’utilisateur ne doit donc se préoccuper que de décrire son problème, laissant à la librairie le soin de le résoudre ?

En pratique, c’est moins vrai. Il faut ajouter de la valeur au modèle en exprimant des éléments cachés : contraintes redondantes, zones prometteuses de recherche… Malgré tout, le pouvoir expressif de la technologie facilite la modélisation. Il donne plus la main à l’utilisateur et à sa maitrise du problème à résoudre. D’autre part, il est aisé de faire évoluer un modèle lorsque le cahier des charges change. Ce qui n’est pas toujours évident en PL. De plus, il est assez facile de l’interfacer avec d’autres technologies comme la SAT par exemple.


Dans le paysage des librairies open-source, Choco est l'un des solveurs les plus en vue. À quoi l'attribuez-vous ?

La librairie existe depuis bientôt 20 ans (1). Elle possède une bonne stabilité. C'est l’une des rares codées en Java. De plus, elle présente des spécificités intéressantes : des contraintes globales état-de-l’art, des résolutions multi-threadées, des explications supportées nativement, un code facilement modifiable. Enfin, c'est également l’une des plus efficaces.

-------
Notes :

* TASC est une équipe-projet Inria, École des Mines de Nantes et Université de Nantes, commune au Laboratoire d'Informatique de Nantes Atlantique.

(1) Choco est lancé en 1999 en langage Claire par François Laburthe et Narendra Jussien. Objectif initial : proposer une librairie open-source et libre pour la programmation par contraintes à destination principale de l’enseignement et la recherche. En 2003, deux doctorants, Hadrien Cambazard et Guillaume Rochart, portent le code en Java, un langage alors en forte progression et très prisé des industriels. En 2008, Charles Prud'homme est recruté au sein de Tasc pour donner de la stabilité à l'outil. En 2011, il engage une refonte de la librairie  en collaboration avec Xavier Lorca et en compagnie de Jean-Guillaume Fages, alors doctorant dans l'équipe.