Optimisation exacte et approchée

Encodage CSP-SAT

Résoudre un CSP consiste à trouver une affectation des
variables qui satisfasse les contraintes. L’une des principales
forces des CSP est la declarativité: les variables peuvent être de
plusieurs types (domaines finis, floating point numbers, intervalles,
ensembles, …) et les contraintes également (contraintes linéaires
arithmétiques, contraintes ensemblistes, contraintes non linéaires,
contraintes booléennes, contraintes symboliques, …). De plus, des
contraintes globales améliorent non seulement la résolution, mais
aussi la déclarativité et l’expressivité : elles proposent de
nouveaux constructeurs et de nouvelles relations telles que la
contrainte alldifferent bien connue (qui force toutes les variables
d’une liste à avoir des valeurs différentes), cumulative (pour
ordonnancer des tâches partageant des ressources), … D’un autre
côté, le problème de satisfiabilité en logique propositionnelle (SAT)
est réduit (en terme de déclarativité) à des variables booléennes et
des formules propositionnelles. Cependant, les solveurs SAT sont
maintenant capables de manipuler des instances de très grande taille
(des millions de variables). Il est donc tentant 1) de coder les CSP
en SAT afin de bénéficier de l’expressivité et de la déclarativité
des CSP et de la puissance des solveurs SAT, et 2) d’introduire plus
de déclarativité dans SAT, par exemple avec la notion de contraintes
globales au niveau CSP. Coder directement des contraintes
ensemblistes en SAT est une tâche fastidieuse. De plus, si l’on
désire optimiser le modèle en termes de nombre de clauses et de
variables, on arrive très rapidement à des modèles très compliqués et
totalement illisibles. Cela est souvent source d’erreurs. L’approche
choisie est donc basée sur un encodage automatique des contraintes en
SAT à l’aide de règles où chaque règle encode une contrainte
particulière (e.g., intersection, union, appartenance, cardinalité,
…). Deux types de perspectives sont envisagées : 1) proposer de
nouvelles règles d’encodage et 2) analyser la conservation de
certaines propriétés lors des transformations (Arc Consistance, Borne
Consistance, GAC, …).