Approche Décompositionnelle pour la compilation de Systèmes de Contraintes

Various classical problems in computer science can be formulated as ConstraintSolving Problems (CSP), consisting in a query on a conjunction of constraints. Typical instancesof such queries are satisfiability (with or without witness), optimization under constraints, modelenumeration, model counting and canonicalization. Constraint systems can be Conjunctive NormalForm (CNF) formulas, as well as (Integer) Linear Programs ((I)LP) and, in its most generic form,Constraint Programs (CP).In both industrial and academic contexts, instances are generally structured and, in most cases,sparse: each constraint involves only a small set of variables, and variables are only involved ina small set of constraints. Moreover, large practical instances tend to have a tree-like structure,which can efficiently be captured by the notion of treewidth, as commonly considered in the fixed-parameter tractability community.Using dynamic programming to solve problems for which a "good" tree decomposition is available israther old, and has been rediscovered many times in the history of computer science, under variousnames: message passing in factor graphs, belief propagation in belief networks, arc consistency inconstraint networks, etc.This work introduces the CoSTreD (Constraint System Tree Decomposition) method, based onsymbolic representations and operators on them to improve the scalability of CSP solving.CoSTreD is based upon two operators: a projection operator which allows to deal with satisfiabilityand canonicalization locally on the tree decomposition, and a coprojection operator, extending themethod to optimization queries. We establish sufficient conditions under which these operatorspreserve the semantics of the CSP. Finally, CoSTreD is extended to deal with parameter (or mode)variables, mostly by (i) adapting the notion of tree decomposition to deal with parameter variables,(ii) using symbolic representations to avoid the combinatorial explosion of mode enumeration, and(iii) mitigating the contamination of constraints by parameter variables during message passing.Plusieurs problèmes classiques en informatique peuvent être formulés comme desproblèmes de résolution de contraintes (CSP), consistant en une requête sur une conjonctionde contraintes. Les exemples typiques de telles requêtes sont la satisfiabilité (avec ou sanstémoin), l’optimisation sous contraintes, l’énumération de modèles, le comptage de modèles et lacanonisation. Les systèmes de contraintes peuvent être des formules CNF (Conjunctive NormalForm), ainsi que des programmes linéaires (entiers) ((I)LP) et, dans sa forme la plus générique,des systèmes de contraintes (CP).Dans les contextes industriels et académiques, les instances sont généralement structuréeset, dans la plupart des cas, creuses : chaque contrainte n’implique qu’un petit ensemble devariables, et les variables ne sont impliquées que dans un petit ensemble de contraintes. De plus,en pratique, les grandes instances ont tendance à avoir une structure arborescente, qui peut êtrefacilement appréhendée par la notion de largeur arborescente, telle que communément admisedans la communauté de tractabilité à paramètre fixé (FPT).L’utilisation de la programmation dynamique pour résoudre les problèmes pour lesquels une"bonne" décomposition arborescente est disponible est assez ancienne, et a été redécouverte denombreuses fois dans l’histoire de l’informatique, sous différents noms : message passing dansles factor graphs, belief propagation dans les belief networks, arc consistency dans les constraintnetworks, etc.Ce travail introduit la méthode CoSTreD (Constraint System Tree Decomposition), basée surdes représentations symboliques et des opérateurs sur celles-ci pour améliorer la scalabilité de larésolution de CSP.CoSTreD est basée sur deux opérateurs : un opérateur de projection qui permet de traiter lasatisfiabilité et la canonisation localement sur la décomposition de l’arbre, et un opérateur de co-projection, étendant cette méthode aux requêtes d’optimisation. Nous établissons des conditionssuffisantes sous lesquelles ces opérateurs préservent la sémantique du CSP. Enfin, CoSTreD estétendu pour traiter les variables paramètres (ou mode), principalement en (i) adaptant la notionde décomposition d’arbre pour traiter les variables paramètres, (ii) utilisant des représentationssymboliques pour éviter l’explosion combinatoire de l’énumération des modes, et (iii) atténuantla contamination des contraintes par les variables paramètres pendant le passage des messages