Constraint System Decomposition
Approche Décompositionnelle pour la compilation de Systèmes de Contraintes
Résumé
Various classical problems in computer science can be formulated as Constraint
Solving Problems (CSP), consisting in a query on a conjunction of constraints. Typical instances
of such queries are satisfiability (with or without witness), optimization under constraints, model
enumeration, model counting and canonicalization. Constraint systems can be Conjunctive Normal
Form (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 in
a 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 is
rather old, and has been rediscovered many times in the history of computer science, under various
names: message passing in factor graphs, belief propagation in belief networks, arc consistency in
constraint networks, etc.
This work introduces the CoSTreD (Constraint System Tree Decomposition) method, based on
symbolic 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 satisfiability
and canonicalization locally on the tree decomposition, and a coprojection operator, extending the
method to optimization queries. We establish sufficient conditions under which these operators
preserve 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 des
problèmes de résolution de contraintes (CSP), consistant en une requête sur une conjonction
de contraintes. Les exemples typiques de telles requêtes sont la satisfiabilité (avec ou sans
témoin), l’optimisation sous contraintes, l’énumération de modèles, le comptage de modèles et la
canonisation. Les systèmes de contraintes peuvent être des formules CNF (Conjunctive Normal
Form), 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ées
et, dans la plupart des cas, creuses : chaque contrainte n’implique qu’un petit ensemble de
variables, 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 être
facilement appréhendée par la notion de largeur arborescente, telle que communément admise
dans 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 de
nombreuses fois dans l’histoire de l’informatique, sous différents noms : message passing dans
les factor graphs, belief propagation dans les belief networks, arc consistency dans les constraint
networks, etc.
Ce travail introduit la méthode CoSTreD (Constraint System Tree Decomposition), basée sur
des représentations symboliques et des opérateurs sur celles-ci pour améliorer la scalabilité de la
résolution de CSP.
CoSTreD est basée sur deux opérateurs : un opérateur de projection qui permet de traiter la
satisfiabilité 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 conditions
suffisantes 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 notion
de décomposition d’arbre pour traiter les variables paramètres, (ii) utilisant des représentations
symboliques pour éviter l’explosion combinatoire de l’énumération des modes, et (iii) atténuant
la contamination des contraintes par les variables paramètres pendant le passage des messages.
Origine : Fichiers produits par l'(les) auteur(s)