Sujet de thèse au LERIA

Étude des mécanismes de transformation de modèles CSP / SAT

Encadrants

BARICHARD, Vincent – Laboratoire : LERIA (UPRES EA 2645)

Affiliation : Université d’Angers

E-mail : vincent.barichard@univ-angers.fr

LARDEUX, Frédéric – Laboratoire : LERIA (UPRES EA 2645)

Affiliation : Université d’Angers

E-mail : frederic.lardeux@univ-angers.fr

Un CSP (Constraint Satisfaction Problem) est un formalisme permettant de modéliser la plupart des problèmes avec contraintes. Un CSP est défini par un ensemble de variables ainsi qu’un ensemble de contraintes liant les variables entre elles. Résoudre un CSP consiste à trouver une affectation des variables qui satisfasse toutes les contraintes du problème. L’une des principales forces des CSP est son langage déclaratif de haut niveau.

L’utilisateur modélise son problème dans ce langage, mais n’implémente pas l’algorithme pour le résoudre (la résolution est laissée à la charge d’un solveur). Le formalisme CSP est riche, il comprend différents types de domaines pour les variables : domaines énumérés, intervalles d’entiers ou de flottants, ensembles. Il intègre également une large bibliothèque de contraintes prédéfinies : contraintes booléennes et arithmétiques, contraintes non linéaires, contraintes ensemblistes, contraintes globales . . . La communauté a porté une attention particulière à la définition et l’implémentation de contraintes globales comme alldifferent (qui force toutes les variables d’une liste à avoir des valeurs différentes) ou cumulative (qui est utilisé dans l’ordonnancement de tâches partageant des ressources). Ces contraintes globales améliorent la résolution mais augmentent aussi la puissance du langage.

D’un autre côté, le problème de satisfiabilité en logique propositionnelle (SAT) est moins riche car il ne comprend que des variables booléennes et des formules propositionnelles. Cependant, les solveurs SAT sont maintenant très puissants et capables de manipuler des instances de très grande taille (de plusieurs millions de variables). Depuis plusieurs années, beaucoup d’efforts ont été fournis pour améliorer les solveurs SAT si bien qu’aujourd’hui ils intègrent des techniques de résolution plus évoluées que les solveurs CSP. Pour pouvoir mettre à profit cette puissance, mais à partir d’un formalisme plus riche comme CSP, il est naturel de vouloir convertir un problème CSP en problème SAT.

Transformer manuellement un problème CSP en SAT est une tâche fastidieuse source d’erreurs. Transformer automatiquement de manière naïve un problème CSP en SAT ne donne pas non plus satisfaction car les problèmes obtenus explosent en termes de nombre de variables et clauses et sont de plus totalement illisibles. Des premiers travaux [5, 3, 4] ont été réalisés sur la transformation plus astucieuse de CSP ensemblistes vers SAT. L’approche de transformation choisie est basée sur un encodage automatique des contraintes en SAT. Le codage se fait par règles, chaque règle encodant une contrainte particulière (e.g., intersection, union, appartenance, cardinalité) par des variables booléennes et clauses correspondantes.

L’objectif de cette thèse est double (pratique et théorique). Du côté

pratique, elle permettra d’enrichir le système de transformation actuel avec

de nouvelles règles pour augmenter la bibliothèque de contraintes traitées

(e.g. contraintes arithmétiques, certaines contraintes globales). Afin de

rendre accessible et utilisable par tous l’approche proposée, il faudra

également brancher le moteur de règles et le solveur SAT à des langages de

modélisation CSP normalisés et reconnus comme Minizinc [1] et XCSP3 [2]. Cela

permettra de comparer l’approche par transformation aux solveurs CSP actuels

comme Gecode [6] mais aussi de rendre la conversion du problème en SAT

transparente pour l’utilisateur. Du côté théorique, une étude sur les

différents mécanismes de simplification sera menée. Le premier point de cette

étude concernera la comparaison des mécanismes de réduction SAT et CSP. En

effet, la modélisation naïve d’un problème en CSP est rarement la plus concise

en termes de contraintes et de variables. En CSP, deux approches

complémentaires sont souvent utilisées pour réduire la taille de ces instances

la détection de symétries et l’application de règles de réduction. Casser les symétries d’un problème diminue énormément sa taille mais supprime des solutions ce qui peut rendre l’instance plus difficile à résoudre. Au contraire, réduire l’instance à l’aide de règles de réduction conserve toutes les solutions, mais la réduction est souvent moindre. Dans la communauté SAT, les travaux sur les symétries sont assez peu nombreux. Par contre, la réduction est très utilisée et se fait principalement grâce à la propagation unitaire. D’autres mécanismes tels que la subsomption sont aussi utilisés mais peu de travaux y font référence. Comment contrôler les réductions CSP et SAT de manière à obtenir une instance plus facile à résoudre tout en restant lisible est une question ouverte.

Le deuxième point de l’étude théorique concernera la mise en évidence de propriétés cachées apparaissant uniquement lors de l’utilisation combinée de certaines contraintes. Les contraintes globales peuvent être vues comme des boîtes noires intégrant un algorithme efficace de traitement. Même si ce cadre étanche permet facilement d’ajouter des nouvelles contraintes globales à un solveur, il ne permet pas de raisonner sur l’ensemble des contraintes (des boîtes noires). Nous croyons que la transformation de modèles permettra de découvrir certaines de ces propriétés cachées. En effet, en travaillant avec un langage intermédiaire de modélisation, ici le langage SAT, l’information est disponible.

Tout le travail d’analyse qui s’en suivra devrait permettre de mettre en évidence ces propriétés afin d’en faire profiter le solveur SAT.

Références

[1] Minizinc. http ://www.minizinc.org/.

[2] Frédéric Boussemart, Christophe Lecoutre, Cédric Piette, and Vincent Perradin.

XCSP3 an integrated format for benchmarking combinatorial constrained problems.

http ://www.xcsp.org/.

[3] Frédéric Lardeux and Eric Monfroy. From declarative set constraint models to “good”

SAT instances. In Artificial Intelligence and Symbolic Computation - 12th Internatio-

nal Conference, AISC 2014, Seville, Spain, December 11-13, 2014. Proceedings, pages

76–87, 2014.

[4] Frédéric Lardeux and Eric Monfroy. Expressively modeling the social golfer problem

in SAT. In Proceedings of the International Conference on Computational Science,

ICCS 2015, Computational Science at the Gates of Nature, Reykjavík, Iceland, 1-3

June, 2015, 2014, pages 336–345, 2015.

[5] Frédéric Lardeux, Eric Monfroy, Broderick Crawford, and Ricardo Soto. Set constraint

model and automated encoding into SAT : application to the social golfer problem.

Annals OR, 235(1) :423–452, 2015.

[6] Christian Schulte. http ://www.gecode.org. Contributions to Gecode were made by

Vincent Barichard, including float variables and float constraints.