Les problèmes de satisfaction de contraintes (CSPs) fournissent un cadre puissant permettant de représenter et résoudre de nombreux problèmes de nature combinatoire (ex. planification, ordonnancement, configuration, …). Ils sont souvent modélisés à l’aide de variables discrètes combinées par des contraintes. Ces contraintes sont généralement de trois types : les contraintes tables, les contraintes en intentions et les contraintes globales [11]. Nous obtenons alors des instances du problème de satisfaction de contraintes qui sont représentées formellement par des réseaux de contraintes. L’un des principaux avantages de ce formalisme réside dans le pouvoir d’expressivité des contraintes utilisées. Cependant, cette expressivité a un coût puisqu’il est généralement difficile d’extraire efficacement de l’information relative aux situations d’échecs pouvant être rencontrés durant le processus de recherche d’une solution.
Une restriction au formalisme CSP consiste à considérer uniquement des variables dont les domaines sont binaires et des contraintes sur ces variables qui sont des clauses. Le langage de représentation ainsi considéré n’est autre que le langage CNF (qui est souvent appelé par abus de langage SAT). Le fait que ce langage soit « pauvre » permet d’utiliser des mécanismes d’analyse de conflits qui permettent d’expliquer finement le pourquoi d’une situation conflictuelle et donc de ne pas explorer inutilement des espaces de recherche qui ne peuvent contenir de solution [4,2].
Bien qu’il soit indéniable que le langage SAT soit moins expressif que le langage CSP, la théorie nous dit que ces problèmes sont « similaires » – ils sont tous les deux NP-complets. Cette proximité est largement utilisée en pratique car de nombreuses transformations ont été proposées dans la littérature afin de transformer une instance de problème CSP en SAT [13, 14, 1, 10, 6, 7]. Bien que de manière générale les formules générées via l’utilisation de ces encodages soient très grandes, une approche pratique s’appuyant sur ces transformations et utilisant un solveur SAT comme boîte noire permet pour de nombreuses instances d’obtenir des résultats sensiblement plus efficaces que des approches dédiées à la résolution de problèmes CSP. Néanmoins, il existe de nombreuses situations où la transformation en SAT est impossible car trop grande et où l’utilisation d’un solveur CSP « classique » est généralement la meilleure solution. Ces situations arrivent généralement lorsque la modélisation du problème considéré fait intervenir des contraintes en intentions ou globales faisant intervenir de nombreuses variables.
Pour éviter les problèmes intrinsèquement liés à la taille des formules générées lors du passage d’une formule CSP à une formule SAT, de nombreux travaux essaient de transformer de manière paresseuse les formules. Plus précisément, ces approches font travailler en symbiose un solveur CSP et un solveur SAT. Dans ces approches, le solveur SAT va générer des solutions qui seront ensuite proposées au solveur CSP. Si une interprétation donnée par le solveur SAT est un modèle pour la formule CSP alors le problème est prouvé satisfiable, sinon une clause expliquant pourquoi l’interprétation n’est pas un modèle est ajoutée à la formule et le processus est répété tant qu’une solution correcte n’est pas exhibée ou que le solveur SAT prouve l’insatisfaisabilité de la formule construite par l’ajout successif de clauses étant des conséquences logiques de l’instance CSP considérée [9,12].
Cette idée d’utiliser un solveur SAT en combinaison d’un formalisme plus expressif n’est pas uniquement limité au cadre de l’implémentation de solveurs CSP. Il existe même un domaine de recherche complet dédié à la résolution de problème combinant une formule SAT et une théorie : Satisfiability Modulo Theories (SMT) [3]. De manière plus générale, lorsqu’il est impossible de modéliser exactement un problème dans un certain formalisme, il est souvent indispensable de considérer une approximation du problème. Ce type d’approche, nommée CEGAR [5], est très répandue pour la résolution de problèmes difficiles. Dans ce contexte, il est possible de considérer deux types d’approximation : sous-approximation et sur-approximation.
Dans le cadre CSP, les méthodes de transformations paresseuses peuvent être vues comme des approches CEGAR considérant des sous-approximations. De manière générale, ce type d’approximation est plus efficace lorsque le problème à résoudre ne possède pas de solutions. En effet, il est souvent indispensable de transformer entièrement la formule en SAT afin de trouver un modèle qui est cohérent avec le réseau de contraintes considéré. Afin de pallier ce problème deux solutions peuvent être considérés : (i) raffiner la notion de sur-approximation et/ou (ii) considérer des sous-approximations. Ainsi, l’un des premier objectif sera de proposer et d’implémenter de nouvelles sur-approximation pour CSP. L’une des premières voies qui devra être explorée par le candidat sera la possibilité d’étudier de nouvelles sur-approximations du problème via des mécanismes impactant les domaines de certaines variables (suppression de valeurs) ou en remplaçant certaines contraintes par d’autres plus fortes mais étant plus « simple » à transformer en SAT. Une autre des voix à exploiter est la possibilité d’utiliser une approche CEGAR s’appuyant sur de nouvelles sous-approximations. Pour cela, les premières pistes que le candidat aura à explorer sont la possibilité de sous-approximer le problème en supprimant des contraintes, en modifiant le domaine de certaines variables, ou en affaiblissant certaines contraintes.
Ces premiers travaux permettront par la suite de considérer un schéma plus général que CEGAR, nommée RECAR [8], et qui permet de jongler entre sur-approximation et sous-approximation dans le but de tirer avantage du meilleur des deux versions de CEGAR. Étant donné que le candidat retenu aura à conduire de nombreuses expérimentations afin de valider les algorithmes proposées, il est primordial que ce dernier ait des bases solides en algorithmique et en programmation en C/C++ ou Java.